List of theorems referencing the symbol INV
(122) Theorem 90: [Members of the inverse map] Is_map(F) •imp (([X,Y] in F) •eq ([Y,X] in inv(F)))
(130) Theorem 98: [Inverse map basic properties] Is_map(inv(F)) & range(inv(F)) = domain(F) & domain(inv(F)) = range(F)
(131) Theorem 99: [Double inverse map] Is_map(F) •imp (F = inv(inv(F)))
(132) Theorem 100: [Inverse of a one-one map] one_1_map(F) •imp (one_1_map(inv(F)) & (F = inv(inv(F))) & (range(inv(F)) = domain(F)) & (domain(inv(F)) = range(F)))
(133) Theorem 101: [Inverse image of an element] (one_1_map(F) & (X in domain(F))) •imp (inv(F)~[F~[X]] = X)
(134) Theorem 102: [Inverse image of an element's map image] one_1_map(F) •imp (((X in domain(F)) •imp (inv(F)~[F~[X]] = X)) & ((X in range(F)) •imp (F~[inv(F)~[X]] = X)))
(145) Theorem 106: [Map inversion and unionset formation commute] inv(Un(S)) = Un({inv(f): f in S})
(149) Theorem 110: [Elementary properties of identity maps] one_1_map(ident(S)) & (domain(ident(S)) = S) & (range(ident(S)) = S) & (inv(ident(S)) = ident(S)) & ((X in S) •imp (ident(S)~[X] = X)) & (Is_map(F) •imp (((domain(F) •incin S) •imp (F @ ident(S) = F)) & ((range(F) •incin S) •imp (ident(S) @ F = F))))
(151) Theorem 112: [Composition with the inverse map] Svm(F) •imp (F @ inv(F) = ident(range(F)))
(152) Theorem 113: [Inverses of one-one maps] one_1_map(F) •imp (((F @ inv(F)) = ident(range(F))) & ((inv(F) @ F) = ident(domain(F))))
(154) Theorem 115: [Product of Inverses] (Is_map(F) & Is_map(G)) •imp (inv(F @ G) = inv(G) @ inv(F))
(155) Theorem 116: [One-one-ness and singlevaluedness] one_1_map(F) •eq (Svm(F) & Svm(inv(F)))
(156) Theorem 117: [An inverse pair of maps must be 1-1 and must be each other's inverses] (Is_map(F) & Is_map(G) & (domain(F) = range(G)) & (range(F) = domain(G)) & (F @ G = ident(range(F))) & (G @ F = ident(domain(F)))) •imp (one_1_map(F) & (G = inv(F)))
(166) Theorem 127: [Single-valued and one-one maps] Is_map(F) •imp (one_1_map(F) •eq one_1_map(inv(F)))
(215) Theorem 175: [Range of a restricted inverse map] G •INV_IM R = range(inv(G) •ON R)
(216) Theorem 176: [Single-valued inverse image as a setformer] Svm(inv(G)) •imp (G •INV_IM R = {inv(G)~[w]: w in (R * range(G))})
(217) Theorem 177: [Inverse image of a range element] (one_1_map(G) & (Y in range(G))) •imp (G •INV_IM {Y} = {inv(G)~[Y]})
(520+) Theorem sigma_theory7: [Sum permutation theorem] (Finite(F) & Svm(F) & one_1_map(G) & (domain(F) = domain(G)) & (range(F) •incin s)) •imp (sigma_thryvar(F) = sigma_thryvar({[y,F~[inv(G)~[y]]]: y in range(G)}))
(900) Theorem 745: (R_SIGMA(0) = R_0) & (FORALL x in OM | (cdr(x) in Re) •imp (R_SIGMA({x}) = cdr(x))) & (FORALL f in OM | (Finite(f) & (range(f) •incin Re)) •imp (R_SIGMA(f) in Re)) & (FORALL f in OM, c in f | (Finite(f) & (range(f) •incin Re)) •imp (R_SIGMA(f) = R_SIGMA(f - {c}) •R_PLUS cdr(c))) & (FORALL f in OM | (Finite(f) & Is_map(f) & (range(f) •incin Re)) •imp (FORALL t | R_SIGMA(f) = R_SIGMA(f •ON (domain(f) * t)) •R_PLUS R_SIGMA(f •ON (domain(f) - t)))) & (FORALL f in OM, g | (Finite(f) & Svm(f) & Svm(g) & (domain(f) = domain(g)) & (range(f) •incin Re)) •imp (R_SIGMA(f) = R_SIGMA({[y,R_SIGMA(f •ON (g •INV_IM {y}))]: y in range(g)}))) & (FORALL f in OM, g | (Finite(f) & Svm(f) & one_1_map(g) & (domain(f) = domain(g)) & (range(f) •incin Re)) •imp (R_SIGMA(f) = R_SIGMA({[y,f~[inv(g)~[y]]]: y in range(g)})))
(901) Theorem 746: (R_SIGMA(0) = R_0) & ((cdr(X) in Re) •imp (R_SIGMA({X}) = cdr(X))) & ((Finite(F) & (range(F) •incin Re)) •imp (R_SIGMA(F) in Re)) & ((Finite(F) & (range(F) •incin Re)) •imp (R_SIGMA(F) = R_SIGMA(F - {c}) •R_PLUS cdr(c))) & ((Finite(F) & Is_map(F) & (range(F) •incin Re)) •imp R_SIGMA(F) = R_SIGMA(F •ON (domain(F) * T)) •R_PLUS R_SIGMA(F •ON (domain(F) - T))) & ((Finite(F) & Svm(F) & Svm(G) & (domain(F) = domain(G)) & (range(F) •incin Re)) •imp (R_SIGMA(F) = R_SIGMA({[y,R_SIGMA(F •ON (G •INV_IM {y}))]: y in range(G)}))) & ((Finite(F) & Svm(F) & one_1_map(G) & (domain(F) = domain(G)) & (range(F) •incin Re)) •imp (R_SIGMA(F) = R_SIGMA({[y,F~[inv(G)~[y]]]: y in range(G)})))