List of theorems referencing the symbol IDENT

(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))))
(150) Theorem 111: [Composition with an identity map is restriction] (Is_map(F)) •imp (F @ ident(S) = F •ON S)
(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))))
(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)))