:: GRCAT_1 semantic presentation begin theorem Th1: :: GRCAT_1:1 for UN being Universe for u1, u2, u3, u4 being Element of UN holds ( [u1,u2,u3] in UN & [u1,u2,u3,u4] in UN ) proof let UN be Universe; ::_thesis: for u1, u2, u3, u4 being Element of UN holds ( [u1,u2,u3] in UN & [u1,u2,u3,u4] in UN ) let u1, u2, u3, u4 be Element of UN; ::_thesis: ( [u1,u2,u3] in UN & [u1,u2,u3,u4] in UN ) ( [u1,u2,u3] = [[u1,u2],u3] & [u1,u2,u3,u4] = [[u1,u2,u3],u4] ) ; hence ( [u1,u2,u3] in UN & [u1,u2,u3,u4] in UN ) by CLASSES2:58; ::_thesis: verum end; theorem Th2: :: GRCAT_1:2 ( op2 . ({},{}) = {} & op1 . {} = {} & op0 = {} ) proof [{},{}] in [:{{}},{{}}:] by ZFMISC_1:28; hence op2 . ({},{}) = {} by CARD_1:49, FUNCT_2:50; ::_thesis: ( op1 . {} = {} & op0 = {} ) {} in {{}} by TARSKI:def_1; hence op1 . {} = {} by CARD_1:49, FUNCT_2:50; ::_thesis: op0 = {} thus op0 = {} ; ::_thesis: verum end; theorem Th3: :: GRCAT_1:3 for UN being Universe holds ( {{}} in UN & [{{}},{{}}] in UN & [:{{}},{{}}:] in UN & op2 in UN & op1 in UN ) proof let UN be Universe; ::_thesis: ( {{}} in UN & [{{}},{{}}] in UN & [:{{}},{{}}:] in UN & op2 in UN & op1 in UN ) set D = {{}}; thus A1: {{}} in UN by CLASSES2:56, CLASSES2:57; ::_thesis: ( [{{}},{{}}] in UN & [:{{}},{{}}:] in UN & op2 in UN & op1 in UN ) hence [{{}},{{}}] in UN by CLASSES2:58; ::_thesis: ( [:{{}},{{}}:] in UN & op2 in UN & op1 in UN ) A2: op2 in Funcs ([:{{}},{{}}:],{{}}) by CARD_1:49, FUNCT_2:8; thus [:{{}},{{}}:] in UN by A1, CLASSES2:61; ::_thesis: ( op2 in UN & op1 in UN ) then Funcs ([:{{}},{{}}:],{{}}) in UN by A1, CLASSES2:61; hence op2 in UN by A2, ORDINAL1:10; ::_thesis: op1 in UN A3: op1 in Funcs ({{}},{{}}) by CARD_1:49, FUNCT_2:8; Funcs ({{}},{{}}) in UN by A1, CLASSES2:61; hence op1 in UN by A3, ORDINAL1:10; ::_thesis: verum end; registration cluster Trivial-addLoopStr -> midpoint_operator ; coherence Trivial-addLoopStr is midpoint_operator proof set G = Trivial-addLoopStr ; A1: for a being Element of Trivial-addLoopStr ex x being Element of Trivial-addLoopStr st Double x = a proof set x = the Element of Trivial-addLoopStr; let a be Element of Trivial-addLoopStr; ::_thesis: ex x being Element of Trivial-addLoopStr st Double x = a take the Element of Trivial-addLoopStr ; ::_thesis: Double the Element of Trivial-addLoopStr = a thus Double the Element of Trivial-addLoopStr = {} by CARD_1:49, TARSKI:def_1 .= a by CARD_1:49, TARSKI:def_1 ; ::_thesis: verum end; for a being Element of Trivial-addLoopStr st Double a = 0. Trivial-addLoopStr holds a = 0. Trivial-addLoopStr by CARD_1:49, TARSKI:def_1; hence Trivial-addLoopStr is midpoint_operator by A1, MIDSP_2:def_5; ::_thesis: verum end; end; theorem :: GRCAT_1:4 ( ( for x being Element of Trivial-addLoopStr holds x = {} ) & ( for x, y being Element of Trivial-addLoopStr holds x + y = {} ) & ( for x being Element of Trivial-addLoopStr holds - x = {} ) & 0. Trivial-addLoopStr = {} ) by CARD_1:49, TARSKI:def_1; definition let C be Category; let O be non empty Subset of the carrier of C; func Morphs O -> Subset of the carrier' of C equals :: GRCAT_1:def 1 union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } ; coherence union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } is Subset of the carrier' of C by CAT_2:19; end; :: deftheorem defines Morphs GRCAT_1:def_1_:_ for C being Category for O being non empty Subset of the carrier of C holds Morphs O = union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } ; registration let C be Category; let O be non empty Subset of the carrier of C; cluster Morphs O -> non empty ; coherence not Morphs O is empty by CAT_2:19; end; definition let C be Category; let O be non empty Subset of the carrier of C; func dom O -> Function of (Morphs O),O equals :: GRCAT_1:def 2 the Source of C | (Morphs O); coherence the Source of C | (Morphs O) is Function of (Morphs O),O by CAT_2:20; func cod O -> Function of (Morphs O),O equals :: GRCAT_1:def 3 the Target of C | (Morphs O); coherence the Target of C | (Morphs O) is Function of (Morphs O),O by CAT_2:20; func comp O -> PartFunc of [:(Morphs O),(Morphs O):],(Morphs O) equals :: GRCAT_1:def 4 the Comp of C || (Morphs O); coherence the Comp of C || (Morphs O) is PartFunc of [:(Morphs O),(Morphs O):],(Morphs O) by CAT_2:20; canceled; end; :: deftheorem defines dom GRCAT_1:def_2_:_ for C being Category for O being non empty Subset of the carrier of C holds dom O = the Source of C | (Morphs O); :: deftheorem defines cod GRCAT_1:def_3_:_ for C being Category for O being non empty Subset of the carrier of C holds cod O = the Target of C | (Morphs O); :: deftheorem defines comp GRCAT_1:def_4_:_ for C being Category for O being non empty Subset of the carrier of C holds comp O = the Comp of C || (Morphs O); :: deftheorem GRCAT_1:def_5_:_ canceled; definition let C be Category; let O be non empty Subset of the carrier of C; func cat O -> Subcategory of C equals :: GRCAT_1:def 6 CatStr(# O,(Morphs O),(dom O),(cod O),(comp O) #); coherence CatStr(# O,(Morphs O),(dom O),(cod O),(comp O) #) is Subcategory of C proof CatStr(# O,(Morphs O),(dom O),(cod O),(comp O) #) is full Subcategory of C by CAT_2:21; hence CatStr(# O,(Morphs O),(dom O),(cod O),(comp O) #) is Subcategory of C ; ::_thesis: verum end; end; :: deftheorem defines cat GRCAT_1:def_6_:_ for C being Category for O being non empty Subset of the carrier of C holds cat O = CatStr(# O,(Morphs O),(dom O),(cod O),(comp O) #); registration let C be Category; let O be non empty Subset of the carrier of C; cluster cat O -> strict ; coherence cat O is strict ; end; theorem :: GRCAT_1:5 for C being Category for O being non empty Subset of the carrier of C holds the carrier of (cat O) = O ; definition let G be non empty 1-sorted ; let H be non empty ZeroStr ; func ZeroMap (G,H) -> Function of G,H equals :: GRCAT_1:def 7 the carrier of G --> (0. H); coherence the carrier of G --> (0. H) is Function of G,H ; end; :: deftheorem defines ZeroMap GRCAT_1:def_7_:_ for G being non empty 1-sorted for H being non empty ZeroStr holds ZeroMap (G,H) = the carrier of G --> (0. H); theorem Th6: :: GRCAT_1:6 comp Trivial-addLoopStr = op1 proof reconsider f = comp Trivial-addLoopStr as Function of {{}},{{}} by CARD_1:49; for x being set st x in {{}} holds op1 . x = f . x proof let x be set ; ::_thesis: ( x in {{}} implies op1 . x = f . x ) assume x in {{}} ; ::_thesis: op1 . x = f . x then reconsider x = x as Element of Trivial-addLoopStr by CARD_1:49; x = {} by CARD_1:49, TARSKI:def_1; then op1 . x = - x by Th2, CARD_1:49, TARSKI:def_1 .= f . x by VECTSP_1:def_13 ; hence op1 . x = f . x ; ::_thesis: verum end; hence comp Trivial-addLoopStr = op1 by CARD_1:49, FUNCT_2:12; ::_thesis: verum end; registration let G be non empty addMagma ; let H be non empty right_zeroed addLoopStr ; cluster ZeroMap (G,H) -> additive ; coherence ZeroMap (G,H) is additive proof set f = ZeroMap (G,H); let x, y be Element of G; :: according to VECTSP_1:def_20 ::_thesis: (ZeroMap (G,H)) . (x + y) = ((ZeroMap (G,H)) . x) + ((ZeroMap (G,H)) . y) A1: (ZeroMap (G,H)) . y = 0. H by FUNCOP_1:7; ( (ZeroMap (G,H)) . (x + y) = 0. H & (ZeroMap (G,H)) . x = 0. H ) by FUNCOP_1:7; hence (ZeroMap (G,H)) . (x + y) = ((ZeroMap (G,H)) . x) + ((ZeroMap (G,H)) . y) by A1, RLVECT_1:def_4; ::_thesis: verum end; end; registration let G be non empty addMagma ; let H be non empty right_zeroed addLoopStr ; cluster Relation-like the carrier of G -defined the carrier of H -valued Function-like non empty total quasi_total additive for Element of bool [: the carrier of G, the carrier of H:]; existence ex b1 being Function of G,H st b1 is additive proof take ZeroMap (G,H) ; ::_thesis: ZeroMap (G,H) is additive thus ZeroMap (G,H) is additive ; ::_thesis: verum end; end; theorem Th7: :: GRCAT_1:7 for G1, G2, G3 being non empty addMagma for f being Function of G1,G2 for g being Function of G2,G3 st f is additive & g is additive holds g * f is additive proof let G1, G2, G3 be non empty addMagma ; ::_thesis: for f being Function of G1,G2 for g being Function of G2,G3 st f is additive & g is additive holds g * f is additive let f be Function of G1,G2; ::_thesis: for g being Function of G2,G3 st f is additive & g is additive holds g * f is additive let g be Function of G2,G3; ::_thesis: ( f is additive & g is additive implies g * f is additive ) assume that A1: f is additive and A2: g is additive ; ::_thesis: g * f is additive set h = g * f; now__::_thesis:_for_x,_y_being_Element_of_G1_holds_(g_*_f)_._(x_+_y)_=_((g_*_f)_._x)_+_((g_*_f)_._y) let x, y be Element of G1; ::_thesis: (g * f) . (x + y) = ((g * f) . x) + ((g * f) . y) A3: ( g . (f . x) = (g * f) . x & g . (f . y) = (g * f) . y ) by FUNCT_2:15; thus (g * f) . (x + y) = g . (f . (x + y)) by FUNCT_2:15 .= g . ((f . x) + (f . y)) by A1, VECTSP_1:def_20 .= ((g * f) . x) + ((g * f) . y) by A2, A3, VECTSP_1:def_20 ; ::_thesis: verum end; hence g * f is additive by VECTSP_1:def_20; ::_thesis: verum end; registration let G1 be non empty addMagma ; let G2, G3 be non empty right_zeroed addLoopStr ; let f be additive Function of G1,G2; let g be additive Function of G2,G3; clusterf * g -> additive for Function of G1,G3; coherence for b1 being Function of G1,G3 st b1 = g * f holds b1 is additive by Th7; end; definition attrc1 is strict ; struct GroupMorphismStr -> ; aggrGroupMorphismStr(# Source, Target, Fun #) -> GroupMorphismStr ; sel Source c1 -> AddGroup; sel Target c1 -> AddGroup; sel Fun c1 -> Function of the Source of c1, the Target of c1; end; definition canceled; let f be GroupMorphismStr ; func dom f -> AddGroup equals :: GRCAT_1:def 9 the Source of f; coherence the Source of f is AddGroup ; func cod f -> AddGroup equals :: GRCAT_1:def 10 the Target of f; coherence the Target of f is AddGroup ; end; :: deftheorem GRCAT_1:def_8_:_ canceled; :: deftheorem defines dom GRCAT_1:def_9_:_ for f being GroupMorphismStr holds dom f = the Source of f; :: deftheorem defines cod GRCAT_1:def_10_:_ for f being GroupMorphismStr holds cod f = the Target of f; definition let f be GroupMorphismStr ; func fun f -> Function of (dom f),(cod f) equals :: GRCAT_1:def 11 the Fun of f; coherence the Fun of f is Function of (dom f),(cod f) ; end; :: deftheorem defines fun GRCAT_1:def_11_:_ for f being GroupMorphismStr holds fun f = the Fun of f; theorem :: GRCAT_1:8 for f being GroupMorphismStr for G1, G2 being AddGroup for f0 being Function of G1,G2 st f = GroupMorphismStr(# G1,G2,f0 #) holds ( dom f = G1 & cod f = G2 & fun f = f0 ) ; definition let G, H be AddGroup; func ZERO (G,H) -> GroupMorphismStr equals :: GRCAT_1:def 12 GroupMorphismStr(# G,H,(ZeroMap (G,H)) #); coherence GroupMorphismStr(# G,H,(ZeroMap (G,H)) #) is GroupMorphismStr ; end; :: deftheorem defines ZERO GRCAT_1:def_12_:_ for G, H being AddGroup holds ZERO (G,H) = GroupMorphismStr(# G,H,(ZeroMap (G,H)) #); registration let G, H be AddGroup; cluster ZERO (G,H) -> strict ; coherence ZERO (G,H) is strict ; end; definition let IT be GroupMorphismStr ; attrIT is GroupMorphism-like means :Def13: :: GRCAT_1:def 13 fun IT is additive ; end; :: deftheorem Def13 defines GroupMorphism-like GRCAT_1:def_13_:_ for IT being GroupMorphismStr holds ( IT is GroupMorphism-like iff fun IT is additive ); registration cluster strict GroupMorphism-like for GroupMorphismStr ; existence ex b1 being GroupMorphismStr st ( b1 is strict & b1 is GroupMorphism-like ) proof set G = the AddGroup; set z = ZERO ( the AddGroup, the AddGroup); fun (ZERO ( the AddGroup, the AddGroup)) is additive ; then ZERO ( the AddGroup, the AddGroup) is GroupMorphism-like by Def13; hence ex b1 being GroupMorphismStr st ( b1 is strict & b1 is GroupMorphism-like ) ; ::_thesis: verum end; end; definition mode GroupMorphism is GroupMorphism-like GroupMorphismStr ; end; theorem Th9: :: GRCAT_1:9 for F being GroupMorphism holds the Fun of F is additive proof let F be GroupMorphism; ::_thesis: the Fun of F is additive the Fun of F = fun F ; hence the Fun of F is additive by Def13; ::_thesis: verum end; registration let G, H be AddGroup; cluster ZERO (G,H) -> GroupMorphism-like ; coherence ZERO (G,H) is GroupMorphism-like proof set z = ZERO (G,H); fun (ZERO (G,H)) is additive ; hence ZERO (G,H) is GroupMorphism-like by Def13; ::_thesis: verum end; end; definition let G, H be AddGroup; mode Morphism of G,H -> GroupMorphism means :Def14: :: GRCAT_1:def 14 ( dom it = G & cod it = H ); existence ex b1 being GroupMorphism st ( dom b1 = G & cod b1 = H ) proof take ZERO (G,H) ; ::_thesis: ( dom (ZERO (G,H)) = G & cod (ZERO (G,H)) = H ) thus ( dom (ZERO (G,H)) = G & cod (ZERO (G,H)) = H ) ; ::_thesis: verum end; end; :: deftheorem Def14 defines Morphism GRCAT_1:def_14_:_ for G, H being AddGroup for b3 being GroupMorphism holds ( b3 is Morphism of G,H iff ( dom b3 = G & cod b3 = H ) ); registration let G, H be AddGroup; cluster strict GroupMorphism-like for Morphism of G,H; existence ex b1 being Morphism of G,H st b1 is strict proof ( dom (ZERO (G,H)) = G & cod (ZERO (G,H)) = H ) ; then ZERO (G,H) is Morphism of G,H by Def14; hence ex b1 being Morphism of G,H st b1 is strict ; ::_thesis: verum end; end; theorem Th10: :: GRCAT_1:10 for G, H being AddGroup for f being strict GroupMorphismStr st dom f = G & cod f = H & fun f is additive holds f is strict Morphism of G,H proof let G, H be AddGroup; ::_thesis: for f being strict GroupMorphismStr st dom f = G & cod f = H & fun f is additive holds f is strict Morphism of G,H let f be strict GroupMorphismStr ; ::_thesis: ( dom f = G & cod f = H & fun f is additive implies f is strict Morphism of G,H ) assume that A1: ( dom f = G & cod f = H ) and A2: fun f is additive ; ::_thesis: f is strict Morphism of G,H reconsider f9 = f as strict GroupMorphism by A2, Def13; f9 is strict Morphism of G,H by A1, Def14; hence f is strict Morphism of G,H ; ::_thesis: verum end; theorem Th11: :: GRCAT_1:11 for G, H being AddGroup for f being Function of G,H st f is additive holds GroupMorphismStr(# G,H,f #) is strict Morphism of G,H proof let G, H be AddGroup; ::_thesis: for f being Function of G,H st f is additive holds GroupMorphismStr(# G,H,f #) is strict Morphism of G,H let f be Function of G,H; ::_thesis: ( f is additive implies GroupMorphismStr(# G,H,f #) is strict Morphism of G,H ) assume A1: f is additive ; ::_thesis: GroupMorphismStr(# G,H,f #) is strict Morphism of G,H set F = GroupMorphismStr(# G,H,f #); fun GroupMorphismStr(# G,H,f #) = f ; hence GroupMorphismStr(# G,H,f #) is strict Morphism of G,H by A1, Th10; ::_thesis: verum end; registration let G be non empty addMagma ; cluster id G -> additive ; coherence id G is additive proof set f = id G; let x, y be Element of G; :: according to VECTSP_1:def_20 ::_thesis: (id G) . (x + y) = ((id G) . x) + ((id G) . y) ( (id G) . (x + y) = x + y & (id G) . x = x ) by FUNCT_1:18; hence (id G) . (x + y) = ((id G) . x) + ((id G) . y) by FUNCT_1:18; ::_thesis: verum end; end; definition let G be AddGroup; func ID G -> Morphism of G,G equals :: GRCAT_1:def 15 GroupMorphismStr(# G,G,(id G) #); coherence GroupMorphismStr(# G,G,(id G) #) is Morphism of G,G proof set i = GroupMorphismStr(# G,G,(id G) #); fun GroupMorphismStr(# G,G,(id G) #) = id G ; hence GroupMorphismStr(# G,G,(id G) #) is Morphism of G,G by Th10; ::_thesis: verum end; end; :: deftheorem defines ID GRCAT_1:def_15_:_ for G being AddGroup holds ID G = GroupMorphismStr(# G,G,(id G) #); registration let G be AddGroup; cluster ID G -> strict ; coherence ID G is strict ; end; definition let G, H be AddGroup; :: original: ZERO redefine func ZERO (G,H) -> strict Morphism of G,H; coherence ZERO (G,H) is strict Morphism of G,H proof set i = ZERO (G,H); fun (ZERO (G,H)) = ZeroMap (G,H) ; hence ZERO (G,H) is strict Morphism of G,H by Th10; ::_thesis: verum end; end; theorem Th12: :: GRCAT_1:12 for G, H being AddGroup for F being Morphism of G,H ex f being Function of G,H st ( GroupMorphismStr(# the Source of F, the Target of F, the Fun of F #) = GroupMorphismStr(# G,H,f #) & f is additive ) proof let G, H be AddGroup; ::_thesis: for F being Morphism of G,H ex f being Function of G,H st ( GroupMorphismStr(# the Source of F, the Target of F, the Fun of F #) = GroupMorphismStr(# G,H,f #) & f is additive ) let F be Morphism of G,H; ::_thesis: ex f being Function of G,H st ( GroupMorphismStr(# the Source of F, the Target of F, the Fun of F #) = GroupMorphismStr(# G,H,f #) & f is additive ) A1: the Target of F = cod F .= H by Def14 ; A2: the Source of F = dom F .= G by Def14 ; then reconsider f = the Fun of F as Function of G,H by A1; take f ; ::_thesis: ( GroupMorphismStr(# the Source of F, the Target of F, the Fun of F #) = GroupMorphismStr(# G,H,f #) & f is additive ) thus ( GroupMorphismStr(# the Source of F, the Target of F, the Fun of F #) = GroupMorphismStr(# G,H,f #) & f is additive ) by A2, A1, Th9; ::_thesis: verum end; theorem Th13: :: GRCAT_1:13 for G, H being AddGroup for F being strict Morphism of G,H ex f being Function of G,H st F = GroupMorphismStr(# G,H,f #) proof let G, H be AddGroup; ::_thesis: for F being strict Morphism of G,H ex f being Function of G,H st F = GroupMorphismStr(# G,H,f #) let F be strict Morphism of G,H; ::_thesis: ex f being Function of G,H st F = GroupMorphismStr(# G,H,f #) consider f being Function of G,H such that A1: F = GroupMorphismStr(# G,H,f #) and f is additive by Th12; take f ; ::_thesis: F = GroupMorphismStr(# G,H,f #) thus F = GroupMorphismStr(# G,H,f #) by A1; ::_thesis: verum end; theorem Th14: :: GRCAT_1:14 for F being GroupMorphism ex G, H being AddGroup st F is Morphism of G,H proof let F be GroupMorphism; ::_thesis: ex G, H being AddGroup st F is Morphism of G,H take G = the Source of F; ::_thesis: ex H being AddGroup st F is Morphism of G,H take H = the Target of F; ::_thesis: F is Morphism of G,H ( dom F = G & cod F = H ) ; hence F is Morphism of G,H by Def14; ::_thesis: verum end; theorem :: GRCAT_1:15 for F being strict GroupMorphism ex G, H being AddGroup ex f being Function of G,H st ( F is Morphism of G,H & F = GroupMorphismStr(# G,H,f #) & f is additive ) proof let F be strict GroupMorphism; ::_thesis: ex G, H being AddGroup ex f being Function of G,H st ( F is Morphism of G,H & F = GroupMorphismStr(# G,H,f #) & f is additive ) consider G, H being AddGroup such that A1: F is Morphism of G,H by Th14; reconsider F9 = F as Morphism of G,H by A1; consider f being Function of G,H such that A2: ( F9 = GroupMorphismStr(# G,H,f #) & f is additive ) by Th12; take G ; ::_thesis: ex H being AddGroup ex f being Function of G,H st ( F is Morphism of G,H & F = GroupMorphismStr(# G,H,f #) & f is additive ) take H ; ::_thesis: ex f being Function of G,H st ( F is Morphism of G,H & F = GroupMorphismStr(# G,H,f #) & f is additive ) take f ; ::_thesis: ( F is Morphism of G,H & F = GroupMorphismStr(# G,H,f #) & f is additive ) thus ( F is Morphism of G,H & F = GroupMorphismStr(# G,H,f #) & f is additive ) by A2; ::_thesis: verum end; theorem Th16: :: GRCAT_1:16 for g, f being GroupMorphism st dom g = cod f holds ex G1, G2, G3 being AddGroup st ( g is Morphism of G2,G3 & f is Morphism of G1,G2 ) proof defpred S1[ GroupMorphism, GroupMorphism] means dom \$1 = cod \$2; let g, f be GroupMorphism; ::_thesis: ( dom g = cod f implies ex G1, G2, G3 being AddGroup st ( g is Morphism of G2,G3 & f is Morphism of G1,G2 ) ) assume A1: S1[g,f] ; ::_thesis: ex G1, G2, G3 being AddGroup st ( g is Morphism of G2,G3 & f is Morphism of G1,G2 ) consider G2, G3 being AddGroup such that A2: g is Morphism of G2,G3 by Th14; consider G1, G29 being AddGroup such that A3: f is Morphism of G1,G29 by Th14; A4: G29 = cod f by A3, Def14; G2 = dom g by A2, Def14; hence ex G1, G2, G3 being AddGroup st ( g is Morphism of G2,G3 & f is Morphism of G1,G2 ) by A1, A2, A3, A4; ::_thesis: verum end; definition let G, F be GroupMorphism; assume A1: dom G = cod F ; funcG * F -> strict GroupMorphism means :Def16: :: GRCAT_1:def 16 for G1, G2, G3 being AddGroup for g being Function of G2,G3 for f being Function of G1,G2 st GroupMorphismStr(# the Source of G, the Target of G, the Fun of G #) = GroupMorphismStr(# G2,G3,g #) & GroupMorphismStr(# the Source of F, the Target of F, the Fun of F #) = GroupMorphismStr(# G1,G2,f #) holds it = GroupMorphismStr(# G1,G3,(g * f) #); existence ex b1 being strict GroupMorphism st for G1, G2, G3 being AddGroup for g being Function of G2,G3 for f being Function of G1,G2 st GroupMorphismStr(# the Source of G, the Target of G, the Fun of G #) = GroupMorphismStr(# G2,G3,g #) & GroupMorphismStr(# the Source of F, the Target of F, the Fun of F #) = GroupMorphismStr(# G1,G2,f #) holds b1 = GroupMorphismStr(# G1,G3,(g * f) #) proof consider G19, G29, G39 being AddGroup such that A2: G is Morphism of G29,G39 and A3: F is Morphism of G19,G29 by A1, Th16; consider f9 being Function of G19,G29 such that A4: GroupMorphismStr(# the Source of F, the Target of F, the Fun of F #) = GroupMorphismStr(# G19,G29,f9 #) and A5: f9 is additive by A3, Th12; consider g9 being Function of G29,G39 such that A6: GroupMorphismStr(# the Source of G, the Target of G, the Fun of G #) = GroupMorphismStr(# G29,G39,g9 #) and A7: g9 is additive by A2, Th12; g9 * f9 is additive by A7, A5; then reconsider T9 = GroupMorphismStr(# G19,G39,(g9 * f9) #) as strict GroupMorphism by Th11; take T9 ; ::_thesis: for G1, G2, G3 being AddGroup for g being Function of G2,G3 for f being Function of G1,G2 st GroupMorphismStr(# the Source of G, the Target of G, the Fun of G #) = GroupMorphismStr(# G2,G3,g #) & GroupMorphismStr(# the Source of F, the Target of F, the Fun of F #) = GroupMorphismStr(# G1,G2,f #) holds T9 = GroupMorphismStr(# G1,G3,(g * f) #) thus for G1, G2, G3 being AddGroup for g being Function of G2,G3 for f being Function of G1,G2 st GroupMorphismStr(# the Source of G, the Target of G, the Fun of G #) = GroupMorphismStr(# G2,G3,g #) & GroupMorphismStr(# the Source of F, the Target of F, the Fun of F #) = GroupMorphismStr(# G1,G2,f #) holds T9 = GroupMorphismStr(# G1,G3,(g * f) #) by A6, A4; ::_thesis: verum end; uniqueness for b1, b2 being strict GroupMorphism st ( for G1, G2, G3 being AddGroup for g being Function of G2,G3 for f being Function of G1,G2 st GroupMorphismStr(# the Source of G, the Target of G, the Fun of G #) = GroupMorphismStr(# G2,G3,g #) & GroupMorphismStr(# the Source of F, the Target of F, the Fun of F #) = GroupMorphismStr(# G1,G2,f #) holds b1 = GroupMorphismStr(# G1,G3,(g * f) #) ) & ( for G1, G2, G3 being AddGroup for g being Function of G2,G3 for f being Function of G1,G2 st GroupMorphismStr(# the Source of G, the Target of G, the Fun of G #) = GroupMorphismStr(# G2,G3,g #) & GroupMorphismStr(# the Source of F, the Target of F, the Fun of F #) = GroupMorphismStr(# G1,G2,f #) holds b2 = GroupMorphismStr(# G1,G3,(g * f) #) ) holds b1 = b2 proof consider G19, G299 being AddGroup such that A8: F is Morphism of G19,G299 by Th14; reconsider F9 = F as Morphism of G19,G299 by A8; consider G29, G39 being AddGroup such that A9: G is Morphism of G29,G39 by Th14; G29 = dom G by A9, Def14; then reconsider F9 = F9 as Morphism of G19,G29 by A1, Def14; consider f9 being Function of G19,G29 such that A10: GroupMorphismStr(# the Source of F9, the Target of F9, the Fun of F9 #) = GroupMorphismStr(# G19,G29,f9 #) and f9 is additive by Th12; reconsider G9 = G as Morphism of G29,G39 by A9; let S1, S2 be strict GroupMorphism; ::_thesis: ( ( for G1, G2, G3 being AddGroup for g being Function of G2,G3 for f being Function of G1,G2 st GroupMorphismStr(# the Source of G, the Target of G, the Fun of G #) = GroupMorphismStr(# G2,G3,g #) & GroupMorphismStr(# the Source of F, the Target of F, the Fun of F #) = GroupMorphismStr(# G1,G2,f #) holds S1 = GroupMorphismStr(# G1,G3,(g * f) #) ) & ( for G1, G2, G3 being AddGroup for g being Function of G2,G3 for f being Function of G1,G2 st GroupMorphismStr(# the Source of G, the Target of G, the Fun of G #) = GroupMorphismStr(# G2,G3,g #) & GroupMorphismStr(# the Source of F, the Target of F, the Fun of F #) = GroupMorphismStr(# G1,G2,f #) holds S2 = GroupMorphismStr(# G1,G3,(g * f) #) ) implies S1 = S2 ) assume that A11: for G1, G2, G3 being AddGroup for g being Function of G2,G3 for f being Function of G1,G2 st GroupMorphismStr(# the Source of G, the Target of G, the Fun of G #) = GroupMorphismStr(# G2,G3,g #) & GroupMorphismStr(# the Source of F, the Target of F, the Fun of F #) = GroupMorphismStr(# G1,G2,f #) holds S1 = GroupMorphismStr(# G1,G3,(g * f) #) and A12: for G1, G2, G3 being AddGroup for g being Function of G2,G3 for f being Function of G1,G2 st GroupMorphismStr(# the Source of G, the Target of G, the Fun of G #) = GroupMorphismStr(# G2,G3,g #) & GroupMorphismStr(# the Source of F, the Target of F, the Fun of F #) = GroupMorphismStr(# G1,G2,f #) holds S2 = GroupMorphismStr(# G1,G3,(g * f) #) ; ::_thesis: S1 = S2 consider g9 being Function of G29,G39 such that A13: GroupMorphismStr(# the Source of G9, the Target of G9, the Fun of G9 #) = GroupMorphismStr(# G29,G39,g9 #) and g9 is additive by Th12; thus S1 = GroupMorphismStr(# G19,G39,(g9 * f9) #) by A11, A13, A10 .= S2 by A12, A13, A10 ; ::_thesis: verum end; end; :: deftheorem Def16 defines * GRCAT_1:def_16_:_ for G, F being GroupMorphism st dom G = cod F holds for b3 being strict GroupMorphism holds ( b3 = G * F iff for G1, G2, G3 being AddGroup for g being Function of G2,G3 for f being Function of G1,G2 st GroupMorphismStr(# the Source of G, the Target of G, the Fun of G #) = GroupMorphismStr(# G2,G3,g #) & GroupMorphismStr(# the Source of F, the Target of F, the Fun of F #) = GroupMorphismStr(# G1,G2,f #) holds b3 = GroupMorphismStr(# G1,G3,(g * f) #) ); theorem Th17: :: GRCAT_1:17 for G1, G2, G3 being AddGroup for G being Morphism of G2,G3 for F being Morphism of G1,G2 holds G * F is Morphism of G1,G3 proof let G1, G2, G3 be AddGroup; ::_thesis: for G being Morphism of G2,G3 for F being Morphism of G1,G2 holds G * F is Morphism of G1,G3 let G be Morphism of G2,G3; ::_thesis: for F being Morphism of G1,G2 holds G * F is Morphism of G1,G3 let F be Morphism of G1,G2; ::_thesis: G * F is Morphism of G1,G3 consider g being Function of G2,G3 such that A1: GroupMorphismStr(# the Source of G, the Target of G, the Fun of G #) = GroupMorphismStr(# G2,G3,g #) and g is additive by Th12; consider f being Function of G1,G2 such that A2: GroupMorphismStr(# the Source of F, the Target of F, the Fun of F #) = GroupMorphismStr(# G1,G2,f #) and f is additive by Th12; dom G = G2 by Def14 .= cod F by Def14 ; then G * F = GroupMorphismStr(# G1,G3,(g * f) #) by A1, A2, Def16; then ( dom (G * F) = G1 & cod (G * F) = G3 ) ; hence G * F is Morphism of G1,G3 by Def14; ::_thesis: verum end; definition let G1, G2, G3 be AddGroup; let G be Morphism of G2,G3; let F be Morphism of G1,G2; :: original: * redefine funcG * F -> strict Morphism of G1,G3; coherence G * F is strict Morphism of G1,G3 by Th17; end; theorem Th18: :: GRCAT_1:18 for G1, G2, G3 being AddGroup for G being Morphism of G2,G3 for F being Morphism of G1,G2 for g being Function of G2,G3 for f being Function of G1,G2 st G = GroupMorphismStr(# G2,G3,g #) & F = GroupMorphismStr(# G1,G2,f #) holds G * F = GroupMorphismStr(# G1,G3,(g * f) #) proof let G1, G2, G3 be AddGroup; ::_thesis: for G being Morphism of G2,G3 for F being Morphism of G1,G2 for g being Function of G2,G3 for f being Function of G1,G2 st G = GroupMorphismStr(# G2,G3,g #) & F = GroupMorphismStr(# G1,G2,f #) holds G * F = GroupMorphismStr(# G1,G3,(g * f) #) let G be Morphism of G2,G3; ::_thesis: for F being Morphism of G1,G2 for g being Function of G2,G3 for f being Function of G1,G2 st G = GroupMorphismStr(# G2,G3,g #) & F = GroupMorphismStr(# G1,G2,f #) holds G * F = GroupMorphismStr(# G1,G3,(g * f) #) let F be Morphism of G1,G2; ::_thesis: for g being Function of G2,G3 for f being Function of G1,G2 st G = GroupMorphismStr(# G2,G3,g #) & F = GroupMorphismStr(# G1,G2,f #) holds G * F = GroupMorphismStr(# G1,G3,(g * f) #) let g be Function of G2,G3; ::_thesis: for f being Function of G1,G2 st G = GroupMorphismStr(# G2,G3,g #) & F = GroupMorphismStr(# G1,G2,f #) holds G * F = GroupMorphismStr(# G1,G3,(g * f) #) let f be Function of G1,G2; ::_thesis: ( G = GroupMorphismStr(# G2,G3,g #) & F = GroupMorphismStr(# G1,G2,f #) implies G * F = GroupMorphismStr(# G1,G3,(g * f) #) ) assume A1: ( G = GroupMorphismStr(# G2,G3,g #) & F = GroupMorphismStr(# G1,G2,f #) ) ; ::_thesis: G * F = GroupMorphismStr(# G1,G3,(g * f) #) dom G = G2 by Def14 .= cod F by Def14 ; hence G * F = GroupMorphismStr(# G1,G3,(g * f) #) by A1, Def16; ::_thesis: verum end; theorem Th19: :: GRCAT_1:19 for f, g being strict GroupMorphism st dom g = cod f holds ex G1, G2, G3 being AddGroup ex f0 being Function of G1,G2 ex g0 being Function of G2,G3 st ( f = GroupMorphismStr(# G1,G2,f0 #) & g = GroupMorphismStr(# G2,G3,g0 #) & g * f = GroupMorphismStr(# G1,G3,(g0 * f0) #) ) proof let f, g be strict GroupMorphism; ::_thesis: ( dom g = cod f implies ex G1, G2, G3 being AddGroup ex f0 being Function of G1,G2 ex g0 being Function of G2,G3 st ( f = GroupMorphismStr(# G1,G2,f0 #) & g = GroupMorphismStr(# G2,G3,g0 #) & g * f = GroupMorphismStr(# G1,G3,(g0 * f0) #) ) ) assume A1: dom g = cod f ; ::_thesis: ex G1, G2, G3 being AddGroup ex f0 being Function of G1,G2 ex g0 being Function of G2,G3 st ( f = GroupMorphismStr(# G1,G2,f0 #) & g = GroupMorphismStr(# G2,G3,g0 #) & g * f = GroupMorphismStr(# G1,G3,(g0 * f0) #) ) set G1 = dom f; set G2 = cod f; set G3 = cod g; reconsider f9 = f as strict Morphism of dom f, cod f by Def14; reconsider g9 = g as strict Morphism of cod f, cod g by A1, Def14; consider f0 being Function of (dom f),(cod f) such that A2: f9 = GroupMorphismStr(# (dom f),(cod f),f0 #) ; consider g0 being Function of (cod f),(cod g) such that A3: g9 = GroupMorphismStr(# (cod f),(cod g),g0 #) by Th13; take dom f ; ::_thesis: ex G2, G3 being AddGroup ex f0 being Function of (dom f),G2 ex g0 being Function of G2,G3 st ( f = GroupMorphismStr(# (dom f),G2,f0 #) & g = GroupMorphismStr(# G2,G3,g0 #) & g * f = GroupMorphismStr(# (dom f),G3,(g0 * f0) #) ) take cod f ; ::_thesis: ex G3 being AddGroup ex f0 being Function of (dom f),(cod f) ex g0 being Function of (cod f),G3 st ( f = GroupMorphismStr(# (dom f),(cod f),f0 #) & g = GroupMorphismStr(# (cod f),G3,g0 #) & g * f = GroupMorphismStr(# (dom f),G3,(g0 * f0) #) ) take cod g ; ::_thesis: ex f0 being Function of (dom f),(cod f) ex g0 being Function of (cod f),(cod g) st ( f = GroupMorphismStr(# (dom f),(cod f),f0 #) & g = GroupMorphismStr(# (cod f),(cod g),g0 #) & g * f = GroupMorphismStr(# (dom f),(cod g),(g0 * f0) #) ) take f0 ; ::_thesis: ex g0 being Function of (cod f),(cod g) st ( f = GroupMorphismStr(# (dom f),(cod f),f0 #) & g = GroupMorphismStr(# (cod f),(cod g),g0 #) & g * f = GroupMorphismStr(# (dom f),(cod g),(g0 * f0) #) ) take g0 ; ::_thesis: ( f = GroupMorphismStr(# (dom f),(cod f),f0 #) & g = GroupMorphismStr(# (cod f),(cod g),g0 #) & g * f = GroupMorphismStr(# (dom f),(cod g),(g0 * f0) #) ) thus ( f = GroupMorphismStr(# (dom f),(cod f),f0 #) & g = GroupMorphismStr(# (cod f),(cod g),g0 #) & g * f = GroupMorphismStr(# (dom f),(cod g),(g0 * f0) #) ) by A2, A3, Th18; ::_thesis: verum end; theorem Th20: :: GRCAT_1:20 for f, g being strict GroupMorphism st dom g = cod f holds ( dom (g * f) = dom f & cod (g * f) = cod g ) proof let f, g be strict GroupMorphism; ::_thesis: ( dom g = cod f implies ( dom (g * f) = dom f & cod (g * f) = cod g ) ) assume dom g = cod f ; ::_thesis: ( dom (g * f) = dom f & cod (g * f) = cod g ) then A1: ex G1, G2, G3 being AddGroup ex f0 being Function of G1,G2 ex g0 being Function of G2,G3 st ( f = GroupMorphismStr(# G1,G2,f0 #) & g = GroupMorphismStr(# G2,G3,g0 #) & g * f = GroupMorphismStr(# G1,G3,(g0 * f0) #) ) by Th19; hence dom (g * f) = dom f ; ::_thesis: cod (g * f) = cod g thus cod (g * f) = cod g by A1; ::_thesis: verum end; theorem Th21: :: GRCAT_1:21 for G1, G2, G3, G4 being AddGroup for f being strict Morphism of G1,G2 for g being strict Morphism of G2,G3 for h being strict Morphism of G3,G4 holds h * (g * f) = (h * g) * f proof let G1, G2, G3, G4 be AddGroup; ::_thesis: for f being strict Morphism of G1,G2 for g being strict Morphism of G2,G3 for h being strict Morphism of G3,G4 holds h * (g * f) = (h * g) * f let f be strict Morphism of G1,G2; ::_thesis: for g being strict Morphism of G2,G3 for h being strict Morphism of G3,G4 holds h * (g * f) = (h * g) * f let g be strict Morphism of G2,G3; ::_thesis: for h being strict Morphism of G3,G4 holds h * (g * f) = (h * g) * f let h be strict Morphism of G3,G4; ::_thesis: h * (g * f) = (h * g) * f consider f0 being Function of G1,G2 such that A1: f = GroupMorphismStr(# G1,G2,f0 #) by Th13; consider g0 being Function of G2,G3 such that A2: g = GroupMorphismStr(# G2,G3,g0 #) by Th13; consider h0 being Function of G3,G4 such that A3: h = GroupMorphismStr(# G3,G4,h0 #) by Th13; A4: h * g = GroupMorphismStr(# G2,G4,(h0 * g0) #) by A2, A3, Th18; g * f = GroupMorphismStr(# G1,G3,(g0 * f0) #) by A1, A2, Th18; then h * (g * f) = GroupMorphismStr(# G1,G4,(h0 * (g0 * f0)) #) by A3, Th18 .= GroupMorphismStr(# G1,G4,((h0 * g0) * f0) #) by RELAT_1:36 .= (h * g) * f by A1, A4, Th18 ; hence h * (g * f) = (h * g) * f ; ::_thesis: verum end; theorem Th22: :: GRCAT_1:22 for f, g, h being strict GroupMorphism st dom h = cod g & dom g = cod f holds h * (g * f) = (h * g) * f proof let f, g, h be strict GroupMorphism; ::_thesis: ( dom h = cod g & dom g = cod f implies h * (g * f) = (h * g) * f ) assume that A1: dom h = cod g and A2: dom g = cod f ; ::_thesis: h * (g * f) = (h * g) * f set G2 = cod f; set G3 = cod g; reconsider h9 = h as Morphism of cod g, cod h by A1, Def14; reconsider g9 = g as Morphism of cod f, cod g by A2, Def14; reconsider f9 = f as Morphism of dom f, cod f by Def14; h9 * (g9 * f9) = (h9 * g9) * f9 by Th21; hence h * (g * f) = (h * g) * f ; ::_thesis: verum end; theorem :: GRCAT_1:23 for G being AddGroup holds ( dom (ID G) = G & cod (ID G) = G & ( for f being strict GroupMorphism st cod f = G holds (ID G) * f = f ) & ( for g being strict GroupMorphism st dom g = G holds g * (ID G) = g ) ) proof let G be AddGroup; ::_thesis: ( dom (ID G) = G & cod (ID G) = G & ( for f being strict GroupMorphism st cod f = G holds (ID G) * f = f ) & ( for g being strict GroupMorphism st dom g = G holds g * (ID G) = g ) ) set i = ID G; thus dom (ID G) = G ; ::_thesis: ( cod (ID G) = G & ( for f being strict GroupMorphism st cod f = G holds (ID G) * f = f ) & ( for g being strict GroupMorphism st dom g = G holds g * (ID G) = g ) ) thus cod (ID G) = G ; ::_thesis: ( ( for f being strict GroupMorphism st cod f = G holds (ID G) * f = f ) & ( for g being strict GroupMorphism st dom g = G holds g * (ID G) = g ) ) thus for f being strict GroupMorphism st cod f = G holds (ID G) * f = f ::_thesis: for g being strict GroupMorphism st dom g = G holds g * (ID G) = g proof let f be strict GroupMorphism; ::_thesis: ( cod f = G implies (ID G) * f = f ) assume A1: cod f = G ; ::_thesis: (ID G) * f = f set H = dom f; reconsider f9 = f as Morphism of dom f,G by A1, Def14; consider m being Function of (dom f),G such that A2: f9 = GroupMorphismStr(# (dom f),G,m #) by Th13; ( dom (ID G) = G & (id G) * m = m ) by FUNCT_2:17; hence (ID G) * f = f by A1, A2, Def16; ::_thesis: verum end; thus for g being strict GroupMorphism st dom g = G holds g * (ID G) = g ::_thesis: verum proof let f be strict GroupMorphism; ::_thesis: ( dom f = G implies f * (ID G) = f ) assume A3: dom f = G ; ::_thesis: f * (ID G) = f set H = cod f; reconsider f9 = f as Morphism of G, cod f by A3, Def14; consider m being Function of G,(cod f) such that A4: f9 = GroupMorphismStr(# G,(cod f),m #) by Th13; ( cod (ID G) = G & m * (id G) = m ) by FUNCT_2:17; hence f * (ID G) = f by A3, A4, Def16; ::_thesis: verum end; end; definition let IT be set ; attrIT is Group_DOMAIN-like means :Def17: :: GRCAT_1:def 17 for x being set st x in IT holds x is strict AddGroup; end; :: deftheorem Def17 defines Group_DOMAIN-like GRCAT_1:def_17_:_ for IT being set holds ( IT is Group_DOMAIN-like iff for x being set st x in IT holds x is strict AddGroup ); registration cluster non empty Group_DOMAIN-like for set ; existence ex b1 being set st ( b1 is Group_DOMAIN-like & not b1 is empty ) proof set D = {Trivial-addLoopStr}; take {Trivial-addLoopStr} ; ::_thesis: ( {Trivial-addLoopStr} is Group_DOMAIN-like & not {Trivial-addLoopStr} is empty ) for x being set st x in {Trivial-addLoopStr} holds x is strict AddGroup by TARSKI:def_1; hence ( {Trivial-addLoopStr} is Group_DOMAIN-like & not {Trivial-addLoopStr} is empty ) by Def17; ::_thesis: verum end; end; definition mode Group_DOMAIN is non empty Group_DOMAIN-like set ; end; definition let V be Group_DOMAIN; :: original: Element redefine mode Element of V -> AddGroup; coherence for b1 being Element of V holds b1 is AddGroup by Def17; end; registration let V be Group_DOMAIN; cluster non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like for Element of V; existence ex b1 being Element of V st b1 is strict proof set v = the Element of V; the Element of V is strict AddGroup by Def17; hence ex b1 being Element of V st b1 is strict ; ::_thesis: verum end; end; definition let IT be set ; attrIT is GroupMorphism_DOMAIN-like means :Def18: :: GRCAT_1:def 18 for x being set st x in IT holds x is strict GroupMorphism; end; :: deftheorem Def18 defines GroupMorphism_DOMAIN-like GRCAT_1:def_18_:_ for IT being set holds ( IT is GroupMorphism_DOMAIN-like iff for x being set st x in IT holds x is strict GroupMorphism ); registration cluster non empty GroupMorphism_DOMAIN-like for set ; existence ex b1 being set st ( b1 is GroupMorphism_DOMAIN-like & not b1 is empty ) proof set G = the AddGroup; take {(ID the AddGroup)} ; ::_thesis: ( {(ID the AddGroup)} is GroupMorphism_DOMAIN-like & not {(ID the AddGroup)} is empty ) for x being set st x in {(ID the AddGroup)} holds x is strict GroupMorphism by TARSKI:def_1; hence ( {(ID the AddGroup)} is GroupMorphism_DOMAIN-like & not {(ID the AddGroup)} is empty ) by Def18; ::_thesis: verum end; end; definition mode GroupMorphism_DOMAIN is non empty GroupMorphism_DOMAIN-like set ; end; definition let M be GroupMorphism_DOMAIN; :: original: Element redefine mode Element of M -> GroupMorphism; coherence for b1 being Element of M holds b1 is GroupMorphism by Def18; end; registration let M be GroupMorphism_DOMAIN; cluster strict GroupMorphism-like for Element of M; existence ex b1 being Element of M st b1 is strict proof set m = the Element of M; the Element of M is strict GroupMorphism by Def18; hence ex b1 being Element of M st b1 is strict ; ::_thesis: verum end; end; theorem Th24: :: GRCAT_1:24 for f being strict GroupMorphism holds {f} is GroupMorphism_DOMAIN proof let f be strict GroupMorphism; ::_thesis: {f} is GroupMorphism_DOMAIN for x being set st x in {f} holds x is strict GroupMorphism by TARSKI:def_1; hence {f} is GroupMorphism_DOMAIN by Def18; ::_thesis: verum end; definition let G, H be AddGroup; mode GroupMorphism_DOMAIN of G,H -> GroupMorphism_DOMAIN means :Def19: :: GRCAT_1:def 19 for x being Element of it holds x is strict Morphism of G,H; existence ex b1 being GroupMorphism_DOMAIN st for x being Element of b1 holds x is strict Morphism of G,H proof reconsider D = {(ZERO (G,H))} as GroupMorphism_DOMAIN by Th24; take D ; ::_thesis: for x being Element of D holds x is strict Morphism of G,H thus for x being Element of D holds x is strict Morphism of G,H by TARSKI:def_1; ::_thesis: verum end; end; :: deftheorem Def19 defines GroupMorphism_DOMAIN GRCAT_1:def_19_:_ for G, H being AddGroup for b3 being GroupMorphism_DOMAIN holds ( b3 is GroupMorphism_DOMAIN of G,H iff for x being Element of b3 holds x is strict Morphism of G,H ); theorem Th25: :: GRCAT_1:25 for D being non empty set for G, H being AddGroup holds ( D is GroupMorphism_DOMAIN of G,H iff for x being Element of D holds x is strict Morphism of G,H ) proof let D be non empty set ; ::_thesis: for G, H being AddGroup holds ( D is GroupMorphism_DOMAIN of G,H iff for x being Element of D holds x is strict Morphism of G,H ) let G, H be AddGroup; ::_thesis: ( D is GroupMorphism_DOMAIN of G,H iff for x being Element of D holds x is strict Morphism of G,H ) thus ( D is GroupMorphism_DOMAIN of G,H implies for x being Element of D holds x is strict Morphism of G,H ) by Def19; ::_thesis: ( ( for x being Element of D holds x is strict Morphism of G,H ) implies D is GroupMorphism_DOMAIN of G,H ) thus ( ( for x being Element of D holds x is strict Morphism of G,H ) implies D is GroupMorphism_DOMAIN of G,H ) ::_thesis: verum proof assume A1: for x being Element of D holds x is strict Morphism of G,H ; ::_thesis: D is GroupMorphism_DOMAIN of G,H then for x being set st x in D holds x is strict GroupMorphism ; then reconsider D9 = D as GroupMorphism_DOMAIN by Def18; for x being Element of D9 holds x is strict Morphism of G,H by A1; hence D is GroupMorphism_DOMAIN of G,H by Def19; ::_thesis: verum end; end; theorem :: GRCAT_1:26 for G, H being AddGroup for f being strict Morphism of G,H holds {f} is GroupMorphism_DOMAIN of G,H proof let G, H be AddGroup; ::_thesis: for f being strict Morphism of G,H holds {f} is GroupMorphism_DOMAIN of G,H let f be strict Morphism of G,H; ::_thesis: {f} is GroupMorphism_DOMAIN of G,H for x being Element of {f} holds x is strict Morphism of G,H by TARSKI:def_1; hence {f} is GroupMorphism_DOMAIN of G,H by Th25; ::_thesis: verum end; definition let G, H be 1-sorted ; mode MapsSet of G,H -> set means :Def20: :: GRCAT_1:def 20 for x being set st x in it holds x is Function of G,H; existence ex b1 being set st for x being set st x in b1 holds x is Function of G,H proof take {} ; ::_thesis: for x being set st x in {} holds x is Function of G,H thus for x being set st x in {} holds x is Function of G,H ; ::_thesis: verum end; end; :: deftheorem Def20 defines MapsSet GRCAT_1:def_20_:_ for G, H being 1-sorted for b3 being set holds ( b3 is MapsSet of G,H iff for x being set st x in b3 holds x is Function of G,H ); definition let G, H be 1-sorted ; func Maps (G,H) -> MapsSet of G,H equals :: GRCAT_1:def 21 Funcs ( the carrier of G, the carrier of H); coherence Funcs ( the carrier of G, the carrier of H) is MapsSet of G,H proof let x be set ; :: according to GRCAT_1:def_20 ::_thesis: ( x in Funcs ( the carrier of G, the carrier of H) implies x is Function of G,H ) assume x in Funcs ( the carrier of G, the carrier of H) ; ::_thesis: x is Function of G,H hence x is Function of G,H by FUNCT_2:66; ::_thesis: verum end; end; :: deftheorem defines Maps GRCAT_1:def_21_:_ for G, H being 1-sorted holds Maps (G,H) = Funcs ( the carrier of G, the carrier of H); registration let G be 1-sorted ; let H be non empty 1-sorted ; cluster Maps (G,H) -> non empty ; coherence not Maps (G,H) is empty ; end; registration let G be 1-sorted ; let H be non empty 1-sorted ; cluster non empty for MapsSet of G,H; existence not for b1 being MapsSet of G,H holds b1 is empty proof not Maps (G,H) is empty ; hence not for b1 being MapsSet of G,H holds b1 is empty ; ::_thesis: verum end; end; definition let G be 1-sorted ; let H be non empty 1-sorted ; let M be non empty MapsSet of G,H; :: original: Element redefine mode Element of M -> Function of G,H; coherence for b1 being Element of M holds b1 is Function of G,H by Def20; end; definition let G, H be AddGroup; func Morphs (G,H) -> GroupMorphism_DOMAIN of G,H means :Def22: :: GRCAT_1:def 22 for x being set holds ( x in it iff x is strict Morphism of G,H ); existence ex b1 being GroupMorphism_DOMAIN of G,H st for x being set holds ( x in b1 iff x is strict Morphism of G,H ) proof reconsider f0 = ZeroMap (G,H) as Element of Maps (G,H) by FUNCT_2:8; set D = { GroupMorphismStr(# G,H,f #) where f is Element of Maps (G,H) : f is additive } ; GroupMorphismStr(# G,H,f0 #) in { GroupMorphismStr(# G,H,f #) where f is Element of Maps (G,H) : f is additive } ; then reconsider D = { GroupMorphismStr(# G,H,f #) where f is Element of Maps (G,H) : f is additive } as non empty set ; A1: for x being set st x in D holds x is strict Morphism of G,H proof let x be set ; ::_thesis: ( x in D implies x is strict Morphism of G,H ) assume x in D ; ::_thesis: x is strict Morphism of G,H then ex f being Element of Maps (G,H) st ( x = GroupMorphismStr(# G,H,f #) & f is additive ) ; hence x is strict Morphism of G,H by Th11; ::_thesis: verum end; then A2: for x being Element of D holds x is strict Morphism of G,H ; A3: for x being set st x is strict Morphism of G,H holds x in D proof let x be set ; ::_thesis: ( x is strict Morphism of G,H implies x in D ) assume x is strict Morphism of G,H ; ::_thesis: x in D then reconsider x = x as strict Morphism of G,H ; A4: ( dom x = G & cod x = H ) by Def14; then reconsider f = the Fun of x as Function of G,H ; reconsider g = f as Element of Maps (G,H) by FUNCT_2:8; A5: x = GroupMorphismStr(# G,H,g #) by A4; the Fun of x is additive by Th9; hence x in D by A5; ::_thesis: verum end; reconsider D = D as GroupMorphism_DOMAIN of G,H by A2, Th25; take D ; ::_thesis: for x being set holds ( x in D iff x is strict Morphism of G,H ) thus for x being set holds ( x in D iff x is strict Morphism of G,H ) by A1, A3; ::_thesis: verum end; uniqueness for b1, b2 being GroupMorphism_DOMAIN of G,H st ( for x being set holds ( x in b1 iff x is strict Morphism of G,H ) ) & ( for x being set holds ( x in b2 iff x is strict Morphism of G,H ) ) holds b1 = b2 proof let D1, D2 be GroupMorphism_DOMAIN of G,H; ::_thesis: ( ( for x being set holds ( x in D1 iff x is strict Morphism of G,H ) ) & ( for x being set holds ( x in D2 iff x is strict Morphism of G,H ) ) implies D1 = D2 ) assume that A6: for x being set holds ( x in D1 iff x is strict Morphism of G,H ) and A7: for x being set holds ( x in D2 iff x is strict Morphism of G,H ) ; ::_thesis: D1 = D2 for x being set holds ( x in D1 iff x in D2 ) proof let x be set ; ::_thesis: ( x in D1 iff x in D2 ) thus ( x in D1 implies x in D2 ) ::_thesis: ( x in D2 implies x in D1 ) proof assume x in D1 ; ::_thesis: x in D2 then x is strict Morphism of G,H by A6; hence x in D2 by A7; ::_thesis: verum end; thus ( x in D2 implies x in D1 ) ::_thesis: verum proof assume x in D2 ; ::_thesis: x in D1 then x is strict Morphism of G,H by A7; hence x in D1 by A6; ::_thesis: verum end; end; hence D1 = D2 by TARSKI:1; ::_thesis: verum end; end; :: deftheorem Def22 defines Morphs GRCAT_1:def_22_:_ for G, H being AddGroup for b3 being GroupMorphism_DOMAIN of G,H holds ( b3 = Morphs (G,H) iff for x being set holds ( x in b3 iff x is strict Morphism of G,H ) ); definition let G, H be AddGroup; let M be GroupMorphism_DOMAIN of G,H; :: original: Element redefine mode Element of M -> Morphism of G,H; coherence for b1 being Element of M holds b1 is Morphism of G,H by Def19; end; registration let G, H be AddGroup; let M be GroupMorphism_DOMAIN of G,H; cluster strict GroupMorphism-like for Element of M; existence ex b1 being Element of M st b1 is strict proof set m = the Element of M; the Element of M is strict Morphism of G,H by Def19; hence ex b1 being Element of M st b1 is strict ; ::_thesis: verum end; end; definition let x, y be set ; pred GO x,y means :Def23: :: GRCAT_1:def 23 ex x1, x2, x3, x4 being set st ( x = [x1,x2,x3,x4] & ex G being strict AddGroup st ( y = G & x1 = the carrier of G & x2 = the addF of G & x3 = comp G & x4 = 0. G ) ); end; :: deftheorem Def23 defines GO GRCAT_1:def_23_:_ for x, y being set holds ( GO x,y iff ex x1, x2, x3, x4 being set st ( x = [x1,x2,x3,x4] & ex G being strict AddGroup st ( y = G & x1 = the carrier of G & x2 = the addF of G & x3 = comp G & x4 = 0. G ) ) ); theorem Th27: :: GRCAT_1:27 for x, y1, y2 being set st GO x,y1 & GO x,y2 holds y1 = y2 proof let x, y1, y2 be set ; ::_thesis: ( GO x,y1 & GO x,y2 implies y1 = y2 ) assume that A1: GO x,y1 and A2: GO x,y2 ; ::_thesis: y1 = y2 consider a1, a2, a3, a4 being set such that A3: x = [a1,a2,a3,a4] and A4: ex G being strict AddGroup st ( y1 = G & a1 = the carrier of G & a2 = the addF of G & a3 = comp G & a4 = 0. G ) by A1, Def23; consider G1 being strict AddGroup such that A5: y1 = G1 and A6: ( a1 = the carrier of G1 & a2 = the addF of G1 ) and a3 = comp G1 and A7: a4 = 0. G1 by A4; consider b1, b2, b3, b4 being set such that A8: x = [b1,b2,b3,b4] and A9: ex G being strict AddGroup st ( y2 = G & b1 = the carrier of G & b2 = the addF of G & b3 = comp G & b4 = 0. G ) by A2, Def23; consider G2 being strict AddGroup such that A10: y2 = G2 and A11: ( b1 = the carrier of G2 & b2 = the addF of G2 ) and b3 = comp G2 and A12: b4 = 0. G2 by A9; ( the carrier of G1 = the carrier of G2 & the addF of G1 = the addF of G2 ) by A3, A8, A6, A11, XTUPLE_0:5; hence y1 = y2 by A3, A8, A5, A7, A10, A12, XTUPLE_0:5; ::_thesis: verum end; theorem Th28: :: GRCAT_1:28 for UN being Universe ex x being set st ( x in UN & GO x, Trivial-addLoopStr ) proof let UN be Universe; ::_thesis: ex x being set st ( x in UN & GO x, Trivial-addLoopStr ) reconsider x2 = op2 as Element of UN by Th3; reconsider x3 = comp Trivial-addLoopStr as Element of UN by Th3, Th6; reconsider u = {} as Element of UN by CLASSES2:56; set x1 = {u}; Extract {} = u ; then reconsider x4 = Extract {} as Element of UN ; take x = [{u},x2,x3,x4]; ::_thesis: ( x in UN & GO x, Trivial-addLoopStr ) thus x in UN by Th1; ::_thesis: GO x, Trivial-addLoopStr take {u} ; :: according to GRCAT_1:def_23 ::_thesis: ex x2, x3, x4 being set st ( x = [{u},x2,x3,x4] & ex G being strict AddGroup st ( Trivial-addLoopStr = G & {u} = the carrier of G & x2 = the addF of G & x3 = comp G & x4 = 0. G ) ) take x2 ; ::_thesis: ex x3, x4 being set st ( x = [{u},x2,x3,x4] & ex G being strict AddGroup st ( Trivial-addLoopStr = G & {u} = the carrier of G & x2 = the addF of G & x3 = comp G & x4 = 0. G ) ) take x3 ; ::_thesis: ex x4 being set st ( x = [{u},x2,x3,x4] & ex G being strict AddGroup st ( Trivial-addLoopStr = G & {u} = the carrier of G & x2 = the addF of G & x3 = comp G & x4 = 0. G ) ) take x4 ; ::_thesis: ( x = [{u},x2,x3,x4] & ex G being strict AddGroup st ( Trivial-addLoopStr = G & {u} = the carrier of G & x2 = the addF of G & x3 = comp G & x4 = 0. G ) ) thus x = [{u},x2,x3,x4] ; ::_thesis: ex G being strict AddGroup st ( Trivial-addLoopStr = G & {u} = the carrier of G & x2 = the addF of G & x3 = comp G & x4 = 0. G ) take Trivial-addLoopStr ; ::_thesis: ( Trivial-addLoopStr = Trivial-addLoopStr & {u} = the carrier of Trivial-addLoopStr & x2 = the addF of Trivial-addLoopStr & x3 = comp Trivial-addLoopStr & x4 = 0. Trivial-addLoopStr ) thus ( Trivial-addLoopStr = Trivial-addLoopStr & {u} = the carrier of Trivial-addLoopStr & x2 = the addF of Trivial-addLoopStr & x3 = comp Trivial-addLoopStr & x4 = 0. Trivial-addLoopStr ) by CARD_1:49; ::_thesis: verum end; definition let UN be Universe; func GroupObjects UN -> set means :Def24: :: GRCAT_1:def 24 for y being set holds ( y in it iff ex x being set st ( x in UN & GO x,y ) ); existence ex b1 being set st for y being set holds ( y in b1 iff ex x being set st ( x in UN & GO x,y ) ) proof defpred S1[ set , set ] means GO \$1,\$2; A1: for x, y1, y2 being set st S1[x,y1] & S1[x,y2] holds y1 = y2 by Th27; consider Y being set such that A2: for y being set holds ( y in Y iff ex x being set st ( x in UN & S1[x,y] ) ) from TARSKI:sch_1(A1); take Y ; ::_thesis: for y being set holds ( y in Y iff ex x being set st ( x in UN & GO x,y ) ) thus for y being set holds ( y in Y iff ex x being set st ( x in UN & GO x,y ) ) by A2; ::_thesis: verum end; uniqueness for b1, b2 being set st ( for y being set holds ( y in b1 iff ex x being set st ( x in UN & GO x,y ) ) ) & ( for y being set holds ( y in b2 iff ex x being set st ( x in UN & GO x,y ) ) ) holds b1 = b2 proof defpred S1[ set ] means ex x being set st ( x in UN & GO x,\$1 ); for X1, X2 being set st ( for x being set holds ( x in X1 iff S1[x] ) ) & ( for x being set holds ( x in X2 iff S1[x] ) ) holds X1 = X2 from XBOOLE_0:sch_3(); hence for b1, b2 being set st ( for y being set holds ( y in b1 iff ex x being set st ( x in UN & GO x,y ) ) ) & ( for y being set holds ( y in b2 iff ex x being set st ( x in UN & GO x,y ) ) ) holds b1 = b2 ; ::_thesis: verum end; end; :: deftheorem Def24 defines GroupObjects GRCAT_1:def_24_:_ for UN being Universe for b2 being set holds ( b2 = GroupObjects UN iff for y being set holds ( y in b2 iff ex x being set st ( x in UN & GO x,y ) ) ); theorem Th29: :: GRCAT_1:29 for UN being Universe holds Trivial-addLoopStr in GroupObjects UN proof let UN be Universe; ::_thesis: Trivial-addLoopStr in GroupObjects UN ex x being set st ( x in UN & GO x, Trivial-addLoopStr ) by Th28; hence Trivial-addLoopStr in GroupObjects UN by Def24; ::_thesis: verum end; registration let UN be Universe; cluster GroupObjects UN -> non empty ; coherence not GroupObjects UN is empty by Th29; end; theorem Th30: :: GRCAT_1:30 for UN being Universe for x being Element of GroupObjects UN holds x is strict AddGroup proof let UN be Universe; ::_thesis: for x being Element of GroupObjects UN holds x is strict AddGroup let x be Element of GroupObjects UN; ::_thesis: x is strict AddGroup consider u being set such that u in UN and A1: GO u,x by Def24; ex x1, x2, x3, x4 being set st ( u = [x1,x2,x3,x4] & ex G being strict AddGroup st ( x = G & x1 = the carrier of G & x2 = the addF of G & x3 = comp G & x4 = 0. G ) ) by A1, Def23; hence x is strict AddGroup ; ::_thesis: verum end; registration let UN be Universe; cluster GroupObjects UN -> Group_DOMAIN-like ; coherence GroupObjects UN is Group_DOMAIN-like proof let x be set ; :: according to GRCAT_1:def_17 ::_thesis: ( x in GroupObjects UN implies x is strict AddGroup ) thus ( x in GroupObjects UN implies x is strict AddGroup ) by Th30; ::_thesis: verum end; end; definition let V be Group_DOMAIN; func Morphs V -> GroupMorphism_DOMAIN means :Def25: :: GRCAT_1:def 25 for x being set holds ( x in it iff ex G, H being strict Element of V st x is strict Morphism of G,H ); existence ex b1 being GroupMorphism_DOMAIN st for x being set holds ( x in b1 iff ex G, H being strict Element of V st x is strict Morphism of G,H ) proof set G0 = the strict Element of V; set M = Morphs ( the strict Element of V, the strict Element of V); set S = { (Morphs (G,H)) where G, H is strict Element of V : verum } ; ( ZERO ( the strict Element of V, the strict Element of V) is Element of Morphs ( the strict Element of V, the strict Element of V) & Morphs ( the strict Element of V, the strict Element of V) in { (Morphs (G,H)) where G, H is strict Element of V : verum } ) by Def22; then reconsider T = union { (Morphs (G,H)) where G, H is strict Element of V : verum } as non empty set by TARSKI:def_4; A1: for x being set holds ( x in T iff ex G, H being strict Element of V st x is strict Morphism of G,H ) proof let x be set ; ::_thesis: ( x in T iff ex G, H being strict Element of V st x is strict Morphism of G,H ) thus ( x in T implies ex G, H being strict Element of V st x is strict Morphism of G,H ) ::_thesis: ( ex G, H being strict Element of V st x is strict Morphism of G,H implies x in T ) proof assume x in T ; ::_thesis: ex G, H being strict Element of V st x is strict Morphism of G,H then consider Y being set such that A2: x in Y and A3: Y in { (Morphs (G,H)) where G, H is strict Element of V : verum } by TARSKI:def_4; consider G, H being strict Element of V such that A4: Y = Morphs (G,H) by A3; take G ; ::_thesis: ex H being strict Element of V st x is strict Morphism of G,H take H ; ::_thesis: x is strict Morphism of G,H thus x is strict Morphism of G,H by A2, A4, Def22; ::_thesis: verum end; thus ( ex G, H being strict Element of V st x is strict Morphism of G,H implies x in T ) ::_thesis: verum proof given G, H being strict Element of V such that A5: x is strict Morphism of G,H ; ::_thesis: x in T set M = Morphs (G,H); A6: Morphs (G,H) in { (Morphs (G,H)) where G, H is strict Element of V : verum } ; x in Morphs (G,H) by A5, Def22; hence x in T by A6, TARSKI:def_4; ::_thesis: verum end; end; now__::_thesis:_for_x_being_set_st_x_in_T_holds_ x_is_strict_GroupMorphism let x be set ; ::_thesis: ( x in T implies x is strict GroupMorphism ) assume x in T ; ::_thesis: x is strict GroupMorphism then ex G, H being strict Element of V st x is strict Morphism of G,H by A1; hence x is strict GroupMorphism ; ::_thesis: verum end; then reconsider T9 = T as GroupMorphism_DOMAIN by Def18; take T9 ; ::_thesis: for x being set holds ( x in T9 iff ex G, H being strict Element of V st x is strict Morphism of G,H ) thus for x being set holds ( x in T9 iff ex G, H being strict Element of V st x is strict Morphism of G,H ) by A1; ::_thesis: verum end; uniqueness for b1, b2 being GroupMorphism_DOMAIN st ( for x being set holds ( x in b1 iff ex G, H being strict Element of V st x is strict Morphism of G,H ) ) & ( for x being set holds ( x in b2 iff ex G, H being strict Element of V st x is strict Morphism of G,H ) ) holds b1 = b2 proof let D1, D2 be GroupMorphism_DOMAIN; ::_thesis: ( ( for x being set holds ( x in D1 iff ex G, H being strict Element of V st x is strict Morphism of G,H ) ) & ( for x being set holds ( x in D2 iff ex G, H being strict Element of V st x is strict Morphism of G,H ) ) implies D1 = D2 ) assume that A7: for x being set holds ( x in D1 iff ex G, H being strict Element of V st x is strict Morphism of G,H ) and A8: for x being set holds ( x in D2 iff ex G, H being strict Element of V st x is strict Morphism of G,H ) ; ::_thesis: D1 = D2 now__::_thesis:_for_x_being_set_holds_ (_x_in_D1_iff_x_in_D2_) let x be set ; ::_thesis: ( x in D1 iff x in D2 ) ( x in D1 iff ex G, H being strict Element of V st x is strict Morphism of G,H ) by A7; hence ( x in D1 iff x in D2 ) by A8; ::_thesis: verum end; hence D1 = D2 by TARSKI:1; ::_thesis: verum end; end; :: deftheorem Def25 defines Morphs GRCAT_1:def_25_:_ for V being Group_DOMAIN for b2 being GroupMorphism_DOMAIN holds ( b2 = Morphs V iff for x being set holds ( x in b2 iff ex G, H being strict Element of V st x is strict Morphism of G,H ) ); definition let V be Group_DOMAIN; let F be Element of Morphs V; :: original: dom redefine func dom F -> strict Element of V; coherence dom F is strict Element of V proof consider G, H being strict Element of V such that A1: F is strict Morphism of G,H by Def25; reconsider F9 = F as Morphism of G,H by A1; dom F9 = G by Def14; hence dom F is strict Element of V ; ::_thesis: verum end; :: original: cod redefine func cod F -> strict Element of V; coherence cod F is strict Element of V proof consider G, H being strict Element of V such that A2: F is strict Morphism of G,H by Def25; reconsider F9 = F as Morphism of G,H by A2; cod F9 = H by Def14; hence cod F is strict Element of V ; ::_thesis: verum end; end; definition let V be Group_DOMAIN; let G be Element of V; func ID G -> strict Element of Morphs V equals :: GRCAT_1:def 26 ID G; coherence ID G is strict Element of Morphs V proof reconsider G9 = G as strict Element of V by Def17; ID G9 is strict Element of Morphs V by Def25; hence ID G is strict Element of Morphs V ; ::_thesis: verum end; end; :: deftheorem defines ID GRCAT_1:def_26_:_ for V being Group_DOMAIN for G being Element of V holds ID G = ID G; definition let V be Group_DOMAIN; func dom V -> Function of (Morphs V),V means :Def27: :: GRCAT_1:def 27 for f being Element of Morphs V holds it . f = dom f; existence ex b1 being Function of (Morphs V),V st for f being Element of Morphs V holds b1 . f = dom f proof deffunc H1( Element of Morphs V) -> strict Element of V = dom \$1; consider F being Function of (Morphs V),V such that A1: for f being Element of Morphs V holds F . f = H1(f) from FUNCT_2:sch_4(); take F ; ::_thesis: for f being Element of Morphs V holds F . f = dom f thus for f being Element of Morphs V holds F . f = dom f by A1; ::_thesis: verum end; uniqueness for b1, b2 being Function of (Morphs V),V st ( for f being Element of Morphs V holds b1 . f = dom f ) & ( for f being Element of Morphs V holds b2 . f = dom f ) holds b1 = b2 proof let F1, F2 be Function of (Morphs V),V; ::_thesis: ( ( for f being Element of Morphs V holds F1 . f = dom f ) & ( for f being Element of Morphs V holds F2 . f = dom f ) implies F1 = F2 ) assume that A2: for f being Element of Morphs V holds F1 . f = dom f and A3: for f being Element of Morphs V holds F2 . f = dom f ; ::_thesis: F1 = F2 now__::_thesis:_for_f_being_Element_of_Morphs_V_holds_F1_._f_=_F2_._f let f be Element of Morphs V; ::_thesis: F1 . f = F2 . f F1 . f = dom f by A2; hence F1 . f = F2 . f by A3; ::_thesis: verum end; hence F1 = F2 by FUNCT_2:63; ::_thesis: verum end; func cod V -> Function of (Morphs V),V means :Def28: :: GRCAT_1:def 28 for f being Element of Morphs V holds it . f = cod f; existence ex b1 being Function of (Morphs V),V st for f being Element of Morphs V holds b1 . f = cod f proof deffunc H1( Element of Morphs V) -> strict Element of V = cod \$1; consider F being Function of (Morphs V),V such that A4: for f being Element of Morphs V holds F . f = H1(f) from FUNCT_2:sch_4(); take F ; ::_thesis: for f being Element of Morphs V holds F . f = cod f thus for f being Element of Morphs V holds F . f = cod f by A4; ::_thesis: verum end; uniqueness for b1, b2 being Function of (Morphs V),V st ( for f being Element of Morphs V holds b1 . f = cod f ) & ( for f being Element of Morphs V holds b2 . f = cod f ) holds b1 = b2 proof let F1, F2 be Function of (Morphs V),V; ::_thesis: ( ( for f being Element of Morphs V holds F1 . f = cod f ) & ( for f being Element of Morphs V holds F2 . f = cod f ) implies F1 = F2 ) assume that A5: for f being Element of Morphs V holds F1 . f = cod f and A6: for f being Element of Morphs V holds F2 . f = cod f ; ::_thesis: F1 = F2 now__::_thesis:_for_f_being_Element_of_Morphs_V_holds_F1_._f_=_F2_._f let f be Element of Morphs V; ::_thesis: F1 . f = F2 . f F1 . f = cod f by A5; hence F1 . f = F2 . f by A6; ::_thesis: verum end; hence F1 = F2 by FUNCT_2:63; ::_thesis: verum end; end; :: deftheorem Def27 defines dom GRCAT_1:def_27_:_ for V being Group_DOMAIN for b2 being Function of (Morphs V),V holds ( b2 = dom V iff for f being Element of Morphs V holds b2 . f = dom f ); :: deftheorem Def28 defines cod GRCAT_1:def_28_:_ for V being Group_DOMAIN for b2 being Function of (Morphs V),V holds ( b2 = cod V iff for f being Element of Morphs V holds b2 . f = cod f ); theorem Th31: :: GRCAT_1:31 for V being Group_DOMAIN for g, f being Element of Morphs V st dom g = cod f holds ex G1, G2, G3 being strict Element of V st ( g is Morphism of G2,G3 & f is Morphism of G1,G2 ) proof let V be Group_DOMAIN; ::_thesis: for g, f being Element of Morphs V st dom g = cod f holds ex G1, G2, G3 being strict Element of V st ( g is Morphism of G2,G3 & f is Morphism of G1,G2 ) set X = Morphs V; defpred S1[ Element of Morphs V, Element of Morphs V] means dom \$1 = cod \$2; let g, f be Element of Morphs V; ::_thesis: ( dom g = cod f implies ex G1, G2, G3 being strict Element of V st ( g is Morphism of G2,G3 & f is Morphism of G1,G2 ) ) assume A1: S1[g,f] ; ::_thesis: ex G1, G2, G3 being strict Element of V st ( g is Morphism of G2,G3 & f is Morphism of G1,G2 ) consider G2, G3 being strict Element of V such that A2: g is strict Morphism of G2,G3 by Def25; consider G1, G29 being strict Element of V such that A3: f is strict Morphism of G1,G29 by Def25; A4: G29 = cod f by A3, Def14; G2 = dom g by A2, Def14; hence ex G1, G2, G3 being strict Element of V st ( g is Morphism of G2,G3 & f is Morphism of G1,G2 ) by A1, A2, A3, A4; ::_thesis: verum end; theorem Th32: :: GRCAT_1:32 for V being Group_DOMAIN for g, f being Element of Morphs V st dom g = cod f holds g * f in Morphs V proof let V be Group_DOMAIN; ::_thesis: for g, f being Element of Morphs V st dom g = cod f holds g * f in Morphs V set X = Morphs V; defpred S1[ Element of Morphs V, Element of Morphs V] means dom \$1 = cod \$2; let g, f be Element of Morphs V; ::_thesis: ( dom g = cod f implies g * f in Morphs V ) assume S1[g,f] ; ::_thesis: g * f in Morphs V then consider G1, G2, G3 being strict Element of V such that A1: g is Morphism of G2,G3 and A2: f is Morphism of G1,G2 by Th31; reconsider f9 = f as Morphism of G1,G2 by A2; reconsider g9 = g as Morphism of G2,G3 by A1; g9 * f9 is Morphism of G1,G3 ; hence g * f in Morphs V by Def25; ::_thesis: verum end; definition let V be Group_DOMAIN; func comp V -> PartFunc of [:(Morphs V),(Morphs V):],(Morphs V) means :Def30: :: GRCAT_1:def 29 ( ( for g, f being Element of Morphs V holds ( [g,f] in dom it iff dom g = cod f ) ) & ( for g, f being Element of Morphs V st [g,f] in dom it holds it . (g,f) = g * f ) ); existence ex b1 being PartFunc of [:(Morphs V),(Morphs V):],(Morphs V) st ( ( for g, f being Element of Morphs V holds ( [g,f] in dom b1 iff dom g = cod f ) ) & ( for g, f being Element of Morphs V st [g,f] in dom b1 holds b1 . (g,f) = g * f ) ) proof set X = Morphs V; defpred S1[ Element of Morphs V, Element of Morphs V] means dom \$1 = cod \$2; deffunc H1( Element of Morphs V, Element of Morphs V) -> strict GroupMorphism = \$1 * \$2; A1: for g, f being Element of Morphs V st S1[g,f] holds H1(g,f) in Morphs V by Th32; consider c being PartFunc of [:(Morphs V),(Morphs V):],(Morphs V) such that A2: ( ( for g, f being Element of Morphs V holds ( [g,f] in dom c iff S1[g,f] ) ) & ( for g, f being Element of Morphs V st [g,f] in dom c holds c . (g,f) = H1(g,f) ) ) from BINOP_1:sch_8(A1); take c ; ::_thesis: ( ( for g, f being Element of Morphs V holds ( [g,f] in dom c iff dom g = cod f ) ) & ( for g, f being Element of Morphs V st [g,f] in dom c holds c . (g,f) = g * f ) ) thus ( ( for g, f being Element of Morphs V holds ( [g,f] in dom c iff dom g = cod f ) ) & ( for g, f being Element of Morphs V st [g,f] in dom c holds c . (g,f) = g * f ) ) by A2; ::_thesis: verum end; uniqueness for b1, b2 being PartFunc of [:(Morphs V),(Morphs V):],(Morphs V) st ( for g, f being Element of Morphs V holds ( [g,f] in dom b1 iff dom g = cod f ) ) & ( for g, f being Element of Morphs V st [g,f] in dom b1 holds b1 . (g,f) = g * f ) & ( for g, f being Element of Morphs V holds ( [g,f] in dom b2 iff dom g = cod f ) ) & ( for g, f being Element of Morphs V st [g,f] in dom b2 holds b2 . (g,f) = g * f ) holds b1 = b2 proof set X = Morphs V; defpred S1[ Element of Morphs V, Element of Morphs V] means dom \$1 = cod \$2; let c1, c2 be PartFunc of [:(Morphs V),(Morphs V):],(Morphs V); ::_thesis: ( ( for g, f being Element of Morphs V holds ( [g,f] in dom c1 iff dom g = cod f ) ) & ( for g, f being Element of Morphs V st [g,f] in dom c1 holds c1 . (g,f) = g * f ) & ( for g, f being Element of Morphs V holds ( [g,f] in dom c2 iff dom g = cod f ) ) & ( for g, f being Element of Morphs V st [g,f] in dom c2 holds c2 . (g,f) = g * f ) implies c1 = c2 ) assume that A3: for g, f being Element of Morphs V holds ( [g,f] in dom c1 iff S1[g,f] ) and A4: for g, f being Element of Morphs V st [g,f] in dom c1 holds c1 . (g,f) = g * f and A5: for g, f being Element of Morphs V holds ( [g,f] in dom c2 iff S1[g,f] ) and A6: for g, f being Element of Morphs V st [g,f] in dom c2 holds c2 . (g,f) = g * f ; ::_thesis: c1 = c2 set V9 = dom c1; A7: dom c1 c= [:(Morphs V),(Morphs V):] by RELAT_1:def_18; now__::_thesis:_for_x_being_set_st_x_in_dom_c1_holds_ x_in_dom_c2 let x be set ; ::_thesis: ( x in dom c1 implies x in dom c2 ) assume A8: x in dom c1 ; ::_thesis: x in dom c2 then consider g, f being Element of Morphs V such that A9: x = [g,f] by A7, SUBSET_1:43; S1[g,f] by A3, A8, A9; hence x in dom c2 by A5, A9; ::_thesis: verum end; then A10: dom c1 c= dom c2 by TARSKI:def_3; A11: for x, y being set st [x,y] in dom c1 holds c1 . (x,y) = c2 . (x,y) proof let x, y be set ; ::_thesis: ( [x,y] in dom c1 implies c1 . (x,y) = c2 . (x,y) ) assume A12: [x,y] in dom c1 ; ::_thesis: c1 . (x,y) = c2 . (x,y) then reconsider x = x, y = y as Element of Morphs V by A7, ZFMISC_1:87; c1 . (x,y) = x * y by A4, A12; hence c1 . (x,y) = c2 . (x,y) by A6, A10, A12; ::_thesis: verum end; now__::_thesis:_for_x_being_set_st_x_in_dom_c2_holds_ x_in_dom_c1 let x be set ; ::_thesis: ( x in dom c2 implies x in dom c1 ) assume A13: x in dom c2 ; ::_thesis: x in dom c1 dom c2 c= [:(Morphs V),(Morphs V):] by RELAT_1:def_18; then consider g, f being Element of Morphs V such that A14: x = [g,f] by A13, SUBSET_1:43; S1[g,f] by A5, A13, A14; hence x in dom c1 by A3, A14; ::_thesis: verum end; then dom c2 c= dom c1 by TARSKI:def_3; then dom c1 = dom c2 by A10, XBOOLE_0:def_10; hence c1 = c2 by A11, BINOP_1:20; ::_thesis: verum end; end; :: deftheorem Def30 defines comp GRCAT_1:def_29_:_ for V being Group_DOMAIN for b2 being PartFunc of [:(Morphs V),(Morphs V):],(Morphs V) holds ( b2 = comp V iff ( ( for g, f being Element of Morphs V holds ( [g,f] in dom b2 iff dom g = cod f ) ) & ( for g, f being Element of Morphs V st [g,f] in dom b2 holds b2 . (g,f) = g * f ) ) ); definition let UN be Universe; func GroupCat UN -> non empty non void strict CatStr equals :: GRCAT_1:def 30 CatStr(# (GroupObjects UN),(Morphs (GroupObjects UN)),(dom (GroupObjects UN)),(cod (GroupObjects UN)),(comp (GroupObjects UN)) #); coherence CatStr(# (GroupObjects UN),(Morphs (GroupObjects UN)),(dom (GroupObjects UN)),(cod (GroupObjects UN)),(comp (GroupObjects UN)) #) is non empty non void strict CatStr ; end; :: deftheorem defines GroupCat GRCAT_1:def_30_:_ for UN being Universe holds GroupCat UN = CatStr(# (GroupObjects UN),(Morphs (GroupObjects UN)),(dom (GroupObjects UN)),(cod (GroupObjects UN)),(comp (GroupObjects UN)) #); registration let UN be Universe; cluster GroupCat UN -> non empty non void strict ; coherence ( GroupCat UN is strict & not GroupCat UN is void & not GroupCat UN is empty ) ; end; theorem Th33: :: GRCAT_1:33 for UN being Universe for f, g being Morphism of (GroupCat UN) holds ( [g,f] in dom the Comp of (GroupCat UN) iff dom g = cod f ) proof let UN be Universe; ::_thesis: for f, g being Morphism of (GroupCat UN) holds ( [g,f] in dom the Comp of (GroupCat UN) iff dom g = cod f ) set C = GroupCat UN; set V = GroupObjects UN; let f, g be Morphism of (GroupCat UN); ::_thesis: ( [g,f] in dom the Comp of (GroupCat UN) iff dom g = cod f ) reconsider f9 = f as Element of Morphs (GroupObjects UN) ; reconsider g9 = g as Element of Morphs (GroupObjects UN) ; ( dom g = dom g9 & cod f = cod f9 ) by Def27, Def28; hence ( [g,f] in dom the Comp of (GroupCat UN) iff dom g = cod f ) by Def30; ::_thesis: verum end; theorem Th34: :: GRCAT_1:34 for UN being Universe for f being Morphism of (GroupCat UN) for f9 being Element of Morphs (GroupObjects UN) for b being Object of (GroupCat UN) for b9 being Element of GroupObjects UN holds ( f is strict Element of Morphs (GroupObjects UN) & f9 is Morphism of (GroupCat UN) & b is strict Element of GroupObjects UN & b9 is Object of (GroupCat UN) ) proof let UN be Universe; ::_thesis: for f being Morphism of (GroupCat UN) for f9 being Element of Morphs (GroupObjects UN) for b being Object of (GroupCat UN) for b9 being Element of GroupObjects UN holds ( f is strict Element of Morphs (GroupObjects UN) & f9 is Morphism of (GroupCat UN) & b is strict Element of GroupObjects UN & b9 is Object of (GroupCat UN) ) set C = GroupCat UN; set V = GroupObjects UN; set X = Morphs (GroupObjects UN); let f be Morphism of (GroupCat UN); ::_thesis: for f9 being Element of Morphs (GroupObjects UN) for b being Object of (GroupCat UN) for b9 being Element of GroupObjects UN holds ( f is strict Element of Morphs (GroupObjects UN) & f9 is Morphism of (GroupCat UN) & b is strict Element of GroupObjects UN & b9 is Object of (GroupCat UN) ) let f9 be Element of Morphs (GroupObjects UN); ::_thesis: for b being Object of (GroupCat UN) for b9 being Element of GroupObjects UN holds ( f is strict Element of Morphs (GroupObjects UN) & f9 is Morphism of (GroupCat UN) & b is strict Element of GroupObjects UN & b9 is Object of (GroupCat UN) ) let b be Object of (GroupCat UN); ::_thesis: for b9 being Element of GroupObjects UN holds ( f is strict Element of Morphs (GroupObjects UN) & f9 is Morphism of (GroupCat UN) & b is strict Element of GroupObjects UN & b9 is Object of (GroupCat UN) ) let b9 be Element of GroupObjects UN; ::_thesis: ( f is strict Element of Morphs (GroupObjects UN) & f9 is Morphism of (GroupCat UN) & b is strict Element of GroupObjects UN & b9 is Object of (GroupCat UN) ) consider x being set such that x in UN and A1: GO x,b by Def24; ex G, H being strict Element of GroupObjects UN st f is strict Morphism of G,H by Def25; hence f is strict Element of Morphs (GroupObjects UN) ; ::_thesis: ( f9 is Morphism of (GroupCat UN) & b is strict Element of GroupObjects UN & b9 is Object of (GroupCat UN) ) thus f9 is Morphism of (GroupCat UN) ; ::_thesis: ( b is strict Element of GroupObjects UN & b9 is Object of (GroupCat UN) ) ex x1, x2, x3, x4 being set st ( x = [x1,x2,x3,x4] & ex G being strict AddGroup st ( b = G & x1 = the carrier of G & x2 = the addF of G & x3 = comp G & x4 = 0. G ) ) by A1, Def23; hence b is strict Element of GroupObjects UN ; ::_thesis: b9 is Object of (GroupCat UN) thus b9 is Object of (GroupCat UN) ; ::_thesis: verum end; theorem :: GRCAT_1:35 canceled; theorem Th36: :: GRCAT_1:36 for UN being Universe for f, g being Morphism of (GroupCat UN) for f9, g9 being Element of Morphs (GroupObjects UN) st f = f9 & g = g9 holds ( ( dom g = cod f implies dom g9 = cod f9 ) & ( dom g9 = cod f9 implies dom g = cod f ) & ( dom g = cod f implies [g9,f9] in dom (comp (GroupObjects UN)) ) & ( [g9,f9] in dom (comp (GroupObjects UN)) implies dom g = cod f ) & ( dom g = cod f implies g (*) f = g9 * f9 ) & ( dom f = dom g implies dom f9 = dom g9 ) & ( dom f9 = dom g9 implies dom f = dom g ) & ( cod f = cod g implies cod f9 = cod g9 ) & ( cod f9 = cod g9 implies cod f = cod g ) ) proof let UN be Universe; ::_thesis: for f, g being Morphism of (GroupCat UN) for f9, g9 being Element of Morphs (GroupObjects UN) st f = f9 & g = g9 holds ( ( dom g = cod f implies dom g9 = cod f9 ) & ( dom g9 = cod f9 implies dom g = cod f ) & ( dom g = cod f implies [g9,f9] in dom (comp (GroupObjects UN)) ) & ( [g9,f9] in dom (comp (GroupObjects UN)) implies dom g = cod f ) & ( dom g = cod f implies g (*) f = g9 * f9 ) & ( dom f = dom g implies dom f9 = dom g9 ) & ( dom f9 = dom g9 implies dom f = dom g ) & ( cod f = cod g implies cod f9 = cod g9 ) & ( cod f9 = cod g9 implies cod f = cod g ) ) set C = GroupCat UN; set V = GroupObjects UN; set X = Morphs (GroupObjects UN); let f, g be Morphism of (GroupCat UN); ::_thesis: for f9, g9 being Element of Morphs (GroupObjects UN) st f = f9 & g = g9 holds ( ( dom g = cod f implies dom g9 = cod f9 ) & ( dom g9 = cod f9 implies dom g = cod f ) & ( dom g = cod f implies [g9,f9] in dom (comp (GroupObjects UN)) ) & ( [g9,f9] in dom (comp (GroupObjects UN)) implies dom g = cod f ) & ( dom g = cod f implies g (*) f = g9 * f9 ) & ( dom f = dom g implies dom f9 = dom g9 ) & ( dom f9 = dom g9 implies dom f = dom g ) & ( cod f = cod g implies cod f9 = cod g9 ) & ( cod f9 = cod g9 implies cod f = cod g ) ) let f9, g9 be Element of Morphs (GroupObjects UN); ::_thesis: ( f = f9 & g = g9 implies ( ( dom g = cod f implies dom g9 = cod f9 ) & ( dom g9 = cod f9 implies dom g = cod f ) & ( dom g = cod f implies [g9,f9] in dom (comp (GroupObjects UN)) ) & ( [g9,f9] in dom (comp (GroupObjects UN)) implies dom g = cod f ) & ( dom g = cod f implies g (*) f = g9 * f9 ) & ( dom f = dom g implies dom f9 = dom g9 ) & ( dom f9 = dom g9 implies dom f = dom g ) & ( cod f = cod g implies cod f9 = cod g9 ) & ( cod f9 = cod g9 implies cod f = cod g ) ) ) assume that A1: f = f9 and A2: g = g9 ; ::_thesis: ( ( dom g = cod f implies dom g9 = cod f9 ) & ( dom g9 = cod f9 implies dom g = cod f ) & ( dom g = cod f implies [g9,f9] in dom (comp (GroupObjects UN)) ) & ( [g9,f9] in dom (comp (GroupObjects UN)) implies dom g = cod f ) & ( dom g = cod f implies g (*) f = g9 * f9 ) & ( dom f = dom g implies dom f9 = dom g9 ) & ( dom f9 = dom g9 implies dom f = dom g ) & ( cod f = cod g implies cod f9 = cod g9 ) & ( cod f9 = cod g9 implies cod f = cod g ) ) A3: cod f = cod f9 by A1, Def28; hence ( dom g = cod f iff dom g9 = cod f9 ) by A2, Def27; ::_thesis: ( ( dom g = cod f implies [g9,f9] in dom (comp (GroupObjects UN)) ) & ( [g9,f9] in dom (comp (GroupObjects UN)) implies dom g = cod f ) & ( dom g = cod f implies g (*) f = g9 * f9 ) & ( dom f = dom g implies dom f9 = dom g9 ) & ( dom f9 = dom g9 implies dom f = dom g ) & ( cod f = cod g implies cod f9 = cod g9 ) & ( cod f9 = cod g9 implies cod f = cod g ) ) dom g = dom g9 by A2, Def27; hence A4: ( dom g = cod f iff [g9,f9] in dom (comp (GroupObjects UN)) ) by A3, Def30; ::_thesis: ( ( dom g = cod f implies g (*) f = g9 * f9 ) & ( dom f = dom g implies dom f9 = dom g9 ) & ( dom f9 = dom g9 implies dom f = dom g ) & ( cod f = cod g implies cod f9 = cod g9 ) & ( cod f9 = cod g9 implies cod f = cod g ) ) thus ( dom g = cod f implies g (*) f = g9 * f9 ) ::_thesis: ( ( dom f = dom g implies dom f9 = dom g9 ) & ( dom f9 = dom g9 implies dom f = dom g ) & ( cod f = cod g implies cod f9 = cod g9 ) & ( cod f9 = cod g9 implies cod f = cod g ) ) proof assume A5: dom g = cod f ; ::_thesis: g (*) f = g9 * f9 then [g,f] in dom the Comp of (GroupCat UN) by Th33; hence g (*) f = (comp (GroupObjects UN)) . (g9,f9) by A1, A2, CAT_1:def_1 .= g9 * f9 by A4, A5, Def30 ; ::_thesis: verum end; dom f = dom f9 by A1, Def27; hence ( dom f = dom g iff dom f9 = dom g9 ) by A2, Def27; ::_thesis: ( cod f = cod g iff cod f9 = cod g9 ) cod g = cod g9 by A2, Def28; hence ( cod f = cod g iff cod f9 = cod g9 ) by A1, Def28; ::_thesis: verum end; Lm1: for UN being Universe for f, g being Morphism of (GroupCat UN) st dom g = cod f holds ( dom (g (*) f) = dom f & cod (g (*) f) = cod g ) proof let UN be Universe; ::_thesis: for f, g being Morphism of (GroupCat UN) st dom g = cod f holds ( dom (g (*) f) = dom f & cod (g (*) f) = cod g ) set X = Morphs (GroupObjects UN); let f, g be Morphism of (GroupCat UN); ::_thesis: ( dom g = cod f implies ( dom (g (*) f) = dom f & cod (g (*) f) = cod g ) ) assume A1: dom g = cod f ; ::_thesis: ( dom (g (*) f) = dom f & cod (g (*) f) = cod g ) reconsider g9 = g as strict Element of Morphs (GroupObjects UN) by Th34; reconsider f9 = f as strict Element of Morphs (GroupObjects UN) by Th34; A2: dom g9 = cod f9 by A1, Th36; then reconsider gf = g9 * f9 as Element of Morphs (GroupObjects UN) by Th32; A3: gf = g (*) f by A1, Th36; ( dom (g9 * f9) = dom f9 & cod (g9 * f9) = cod g9 ) by A2, Th20; hence ( dom (g (*) f) = dom f & cod (g (*) f) = cod g ) by A3, Th36; ::_thesis: verum end; registration let UN be Universe; cluster GroupCat UN -> non empty non void strict Category-like reflexive ; coherence ( GroupCat UN is reflexive & GroupCat UN is Category-like ) proof set C = GroupCat UN; thus GroupCat UN is reflexive ::_thesis: GroupCat UN is Category-like proof let a be Element of (GroupCat UN); :: according to CAT_1:def_9 ::_thesis: not Hom (a,a) = {} reconsider G = a as Element of GroupObjects UN ; consider x being set such that x in UN and W2: GO x,G by Def24; set ii = ID G; consider x1, x2, x3, x4 being set such that x = [x1,x2,x3,x4] and W3: ex H being strict AddGroup st ( G = H & x1 = the carrier of H & x2 = the addF of H & x3 = comp H & x4 = 0. H ) by W2, Def23; reconsider G = G as strict Element of GroupObjects UN by W3; reconsider ii = ID G as Morphism of (GroupCat UN) ; reconsider ia = ii as GroupMorphismStr ; A: dom ii = dom ia by Def27 .= a ; cod ii = cod ia by Def28 .= a ; then ii in Hom (a,a) by A; hence Hom (a,a) <> {} ; ::_thesis: verum end; let f, g be Morphism of (GroupCat UN); :: according to CAT_1:def_6 ::_thesis: ( ( not [g,f] in proj1 the Comp of (GroupCat UN) or dom g = cod f ) & ( not dom g = cod f or [g,f] in proj1 the Comp of (GroupCat UN) ) ) reconsider ff = f, gg = g as Element of Morphs (GroupObjects UN) ; thus ( [g,f] in dom the Comp of (GroupCat UN) iff dom g = cod f ) by Th36; ::_thesis: verum end; end; Lm3: for UN being Universe for a being Element of (GroupCat UN) for aa being Element of GroupObjects UN st a = aa holds for i being Morphism of a,a st i = ID aa holds for b being Element of (GroupCat UN) holds ( ( Hom (a,b) <> {} implies for g being Morphism of a,b holds g (*) i = g ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds i (*) f = f ) ) proof let UN be Universe; ::_thesis: for a being Element of (GroupCat UN) for aa being Element of GroupObjects UN st a = aa holds for i being Morphism of a,a st i = ID aa holds for b being Element of (GroupCat UN) holds ( ( Hom (a,b) <> {} implies for g being Morphism of a,b holds g (*) i = g ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds i (*) f = f ) ) let a be Element of (GroupCat UN); ::_thesis: for aa being Element of GroupObjects UN st a = aa holds for i being Morphism of a,a st i = ID aa holds for b being Element of (GroupCat UN) holds ( ( Hom (a,b) <> {} implies for g being Morphism of a,b holds g (*) i = g ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds i (*) f = f ) ) let aa be Element of GroupObjects UN; ::_thesis: ( a = aa implies for i being Morphism of a,a st i = ID aa holds for b being Element of (GroupCat UN) holds ( ( Hom (a,b) <> {} implies for g being Morphism of a,b holds g (*) i = g ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds i (*) f = f ) ) ) assume a = aa ; ::_thesis: for i being Morphism of a,a st i = ID aa holds for b being Element of (GroupCat UN) holds ( ( Hom (a,b) <> {} implies for g being Morphism of a,b holds g (*) i = g ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds i (*) f = f ) ) let i be Morphism of a,a; ::_thesis: ( i = ID aa implies for b being Element of (GroupCat UN) holds ( ( Hom (a,b) <> {} implies for g being Morphism of a,b holds g (*) i = g ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds i (*) f = f ) ) ) assume Z2: i = ID aa ; ::_thesis: for b being Element of (GroupCat UN) holds ( ( Hom (a,b) <> {} implies for g being Morphism of a,b holds g (*) i = g ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds i (*) f = f ) ) let b be Element of (GroupCat UN); ::_thesis: ( ( Hom (a,b) <> {} implies for g being Morphism of a,b holds g (*) i = g ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds i (*) f = f ) ) thus ( Hom (a,b) <> {} implies for g being Morphism of a,b holds g (*) i = g ) ::_thesis: ( Hom (b,a) <> {} implies for f being Morphism of b,a holds i (*) f = f ) proof assume Z3: Hom (a,b) <> {} ; ::_thesis: for g being Morphism of a,b holds g (*) i = g let g be Morphism of a,b; ::_thesis: g (*) i = g reconsider gg = g, ii = i as Element of Morphs (GroupObjects UN) ; consider G1, H1 being strict Element of GroupObjects UN such that W1: gg is strict Morphism of G1,H1 by Def25; consider f being Function of G1,H1 such that W2: gg = GroupMorphismStr(# G1,H1,f #) by W1, Th13; D: ii = GroupMorphismStr(# aa,aa,(id aa) #) by Z2; C: cod ii = aa by Z2; C2: dom gg = G1 by W2; E: Hom (a,a) <> {} ; dom g = a by Z3, CAT_1:5 .= cod i by E, CAT_1:5 ; then C1: dom gg = cod ii by Th36; then aa = dom gg by C; then B: aa = G1 by C2; then reconsider f = f as Function of aa,H1 ; G1: GroupMorphismStr(# the Source of gg, the Target of gg, the Fun of gg #) = GroupMorphismStr(# aa,H1,f #) by W2, B; A: [gg,ii] in dom (comp (GroupObjects UN)) by Def30, C1; then [g,i] in dom the Comp of (GroupCat UN) ; hence g (*) i = the Comp of (GroupCat UN) . (g,i) by CAT_1:def_1 .= (comp (GroupObjects UN)) . (g,i) .= gg * ii by A, Def30 .= GroupMorphismStr(# aa,H1,(f * (id aa)) #) by D, Def16, G1, C1 .= GroupMorphismStr(# aa,H1,f #) by FUNCT_2:17 .= g by B, W2 ; ::_thesis: verum end; thus ( Hom (b,a) <> {} implies for f being Morphism of b,a holds i (*) f = f ) ::_thesis: verum proof assume Z3: Hom (b,a) <> {} ; ::_thesis: for f being Morphism of b,a holds i (*) f = f let g be Morphism of b,a; ::_thesis: i (*) g = g reconsider gg = g, ii = i as Element of Morphs (GroupObjects UN) ; consider G1, H1 being strict Element of GroupObjects UN such that W1: gg is strict Morphism of G1,H1 by Def25; consider f being Function of G1,H1 such that W2: gg = GroupMorphismStr(# G1,H1,f #) by W1, Th13; D: ii = GroupMorphismStr(# aa,aa,(id aa) #) by Z2; C: dom ii = aa by Z2; C2: cod gg = H1 by W2; E: Hom (a,a) <> {} ; cod g = a by Z3, CAT_1:5 .= dom i by E, CAT_1:5 ; then C1: cod gg = dom ii by Th36; then aa = cod gg by C; then B: aa = H1 by C2; then reconsider f = f as Function of G1,aa ; G1: GroupMorphismStr(# the Source of gg, the Target of gg, the Fun of gg #) = GroupMorphismStr(# G1,aa,f #) by W2, B; A: [ii,gg] in dom (comp (GroupObjects UN)) by Def30, C1; then [i,g] in dom the Comp of (GroupCat UN) ; hence i (*) g = the Comp of (GroupCat UN) . (i,g) by CAT_1:def_1 .= (comp (GroupObjects UN)) . (i,g) .= ii * gg by A, Def30 .= GroupMorphismStr(# G1,aa,((id aa) * f) #) by D, Def16, G1, C1 .= GroupMorphismStr(# G1,aa,f #) by FUNCT_2:17 .= g by B, W2 ; ::_thesis: verum end; end; registration let UN be Universe; cluster GroupCat UN -> non empty non void strict transitive associative with_identities ; coherence ( GroupCat UN is transitive & GroupCat UN is associative & GroupCat UN is with_identities ) proof set C = GroupCat UN; set X = Morphs (GroupObjects UN); thus GroupCat UN is transitive ::_thesis: ( GroupCat UN is associative & GroupCat UN is with_identities ) proof let f, g be Morphism of (GroupCat UN); :: according to CAT_1:def_7 ::_thesis: ( not dom g = cod f or ( dom (g (*) f) = dom f & cod (g (*) f) = cod g ) ) assume A1: dom g = cod f ; ::_thesis: ( dom (g (*) f) = dom f & cod (g (*) f) = cod g ) reconsider g9 = g as strict Element of Morphs (GroupObjects UN) by Th34; reconsider f9 = f as strict Element of Morphs (GroupObjects UN) by Th34; A2: dom g9 = cod f9 by A1, Th36; then reconsider gf = g9 * f9 as Element of Morphs (GroupObjects UN) by Th32; A3: gf = g (*) f by A1, Th36; ( dom (g9 * f9) = dom f9 & cod (g9 * f9) = cod g9 ) by A2, Th20; hence ( dom (g (*) f) = dom f & cod (g (*) f) = cod g ) by A3, Th36; ::_thesis: verum end; thus GroupCat UN is associative ::_thesis: GroupCat UN is with_identities proof let f, g, h be Morphism of (GroupCat UN); :: according to CAT_1:def_8 ::_thesis: ( not dom h = cod g or not dom g = cod f or h (*) (g (*) f) = (h (*) g) (*) f ) assume A1: ( dom h = cod g & dom g = cod f ) ; ::_thesis: h (*) (g (*) f) = (h (*) g) (*) f reconsider f9 = f, g9 = g, h9 = h as strict Element of Morphs (GroupObjects UN) by Th34; A2: ( h9 * g9 = h (*) g & dom (h (*) g) = cod f ) by A1, Lm1, Th36; A3: ( dom h9 = cod g9 & dom g9 = cod f9 ) by A1, Th36; then reconsider gf = g9 * f9, hg = h9 * g9 as Element of Morphs (GroupObjects UN) by Th32; ( g9 * f9 = g (*) f & dom h = cod (g (*) f) ) by A1, Lm1, Th36; then h (*) (g (*) f) = h9 * gf by Th36 .= hg * f9 by A3, Th22 .= (h (*) g) (*) f by A2, Th36 ; hence h (*) (g (*) f) = (h (*) g) (*) f ; ::_thesis: verum end; thus GroupCat UN is with_identities ::_thesis: verum proof let a be Element of (GroupCat UN); :: according to CAT_1:def_10 ::_thesis: ex b1 being Morphism of a,a st for b2 being Element of the carrier of (GroupCat UN) holds ( ( Hom (a,b2) = {} or for b3 being Morphism of a,b2 holds b3 (*) b1 = b3 ) & ( Hom (b2,a) = {} or for b3 being Morphism of b2,a holds b1 (*) b3 = b3 ) ) reconsider aa = a as Element of GroupObjects UN ; reconsider ii = ID aa as Morphism of (GroupCat UN) ; reconsider ia = ii as GroupMorphismStr ; A: dom ii = dom ia by Def27 .= a ; cod ii = cod ia by Def28 .= a ; then reconsider ii = ii as Morphism of a,a by A, CAT_1:4; take ii ; ::_thesis: for b1 being Element of the carrier of (GroupCat UN) holds ( ( Hom (a,b1) = {} or for b2 being Morphism of a,b1 holds b2 (*) ii = b2 ) & ( Hom (b1,a) = {} or for b2 being Morphism of b1,a holds ii (*) b2 = b2 ) ) thus for b1 being Element of the carrier of (GroupCat UN) holds ( ( Hom (a,b1) = {} or for b2 being Morphism of a,b1 holds b2 (*) ii = b2 ) & ( Hom (b1,a) = {} or for b2 being Morphism of b1,a holds ii (*) b2 = b2 ) ) by Lm3; ::_thesis: verum end; end; end; definition let UN be Universe; func AbGroupObjects UN -> Subset of the carrier of (GroupCat UN) equals :: GRCAT_1:def 31 { G where G is Element of (GroupCat UN) : ex H being AbGroup st G = H } ; coherence { G where G is Element of (GroupCat UN) : ex H being AbGroup st G = H } is Subset of the carrier of (GroupCat UN) proof set D2 = the carrier of (GroupCat UN); now__::_thesis:_for_x_being_set_st_x_in__{__G_where_G_is_Element_of_the_carrier_of_(GroupCat_UN)_:_ex_H_being_AbGroup_st_G_=_H__}__holds_ x_in_the_carrier_of_(GroupCat_UN) let x be set ; ::_thesis: ( x in { G where G is Element of the carrier of (GroupCat UN) : ex H being AbGroup st G = H } implies x in the carrier of (GroupCat UN) ) assume x in { G where G is Element of the carrier of (GroupCat UN) : ex H being AbGroup st G = H } ; ::_thesis: x in the carrier of (GroupCat UN) then ex G being Element of the carrier of (GroupCat UN) st ( x = G & ex H being AbGroup st G = H ) ; hence x in the carrier of (GroupCat UN) ; ::_thesis: verum end; hence { G where G is Element of (GroupCat UN) : ex H being AbGroup st G = H } is Subset of the carrier of (GroupCat UN) by TARSKI:def_3; ::_thesis: verum end; end; :: deftheorem defines AbGroupObjects GRCAT_1:def_31_:_ for UN being Universe holds AbGroupObjects UN = { G where G is Element of (GroupCat UN) : ex H being AbGroup st G = H } ; theorem Th37: :: GRCAT_1:37 for UN being Universe holds Trivial-addLoopStr in AbGroupObjects UN proof let UN be Universe; ::_thesis: Trivial-addLoopStr in AbGroupObjects UN Trivial-addLoopStr in the carrier of (GroupCat UN) by Th29; hence Trivial-addLoopStr in AbGroupObjects UN ; ::_thesis: verum end; registration let UN be Universe; cluster AbGroupObjects UN -> non empty ; coherence not AbGroupObjects UN is empty by Th37; end; definition let UN be Universe; func AbGroupCat UN -> Subcategory of GroupCat UN equals :: GRCAT_1:def 32 cat (AbGroupObjects UN); coherence cat (AbGroupObjects UN) is Subcategory of GroupCat UN ; end; :: deftheorem defines AbGroupCat GRCAT_1:def_32_:_ for UN being Universe holds AbGroupCat UN = cat (AbGroupObjects UN); registration let UN be Universe; cluster AbGroupCat UN -> strict ; coherence AbGroupCat UN is strict ; end; theorem :: GRCAT_1:38 for UN being Universe holds the carrier of (AbGroupCat UN) = AbGroupObjects UN ; definition let UN be Universe; func MidOpGroupObjects UN -> Subset of the carrier of (AbGroupCat UN) equals :: GRCAT_1:def 33 { G where G is Element of (AbGroupCat UN) : ex H being midpoint_operator AbGroup st G = H } ; coherence { G where G is Element of (AbGroupCat UN) : ex H being midpoint_operator AbGroup st G = H } is Subset of the carrier of (AbGroupCat UN) proof set D2 = the carrier of (AbGroupCat UN); now__::_thesis:_for_x_being_set_st_x_in__{__G_where_G_is_Element_of_the_carrier_of_(AbGroupCat_UN)_:_ex_H_being_midpoint_operator_AbGroup_st_G_=_H__}__holds_ x_in_the_carrier_of_(AbGroupCat_UN) let x be set ; ::_thesis: ( x in { G where G is Element of the carrier of (AbGroupCat UN) : ex H being midpoint_operator AbGroup st G = H } implies x in the carrier of (AbGroupCat UN) ) assume x in { G where G is Element of the carrier of (AbGroupCat UN) : ex H being midpoint_operator AbGroup st G = H } ; ::_thesis: x in the carrier of (AbGroupCat UN) then ex G being Element of the carrier of (AbGroupCat UN) st ( x = G & ex H being midpoint_operator AbGroup st G = H ) ; hence x in the carrier of (AbGroupCat UN) ; ::_thesis: verum end; hence { G where G is Element of (AbGroupCat UN) : ex H being midpoint_operator AbGroup st G = H } is Subset of the carrier of (AbGroupCat UN) by TARSKI:def_3; ::_thesis: verum end; end; :: deftheorem defines MidOpGroupObjects GRCAT_1:def_33_:_ for UN being Universe holds MidOpGroupObjects UN = { G where G is Element of (AbGroupCat UN) : ex H being midpoint_operator AbGroup st G = H } ; registration let UN be Universe; cluster MidOpGroupObjects UN -> non empty ; coherence not MidOpGroupObjects UN is empty proof set T = Trivial-addLoopStr ; set D2 = the carrier of (AbGroupCat UN); set D1 = { G where G is Element of the carrier of (AbGroupCat UN) : ex H being midpoint_operator AbGroup st G = H } ; Trivial-addLoopStr in the carrier of (AbGroupCat UN) by Th37; then Trivial-addLoopStr in { G where G is Element of the carrier of (AbGroupCat UN) : ex H being midpoint_operator AbGroup st G = H } ; then reconsider D1 = { G where G is Element of the carrier of (AbGroupCat UN) : ex H being midpoint_operator AbGroup st G = H } as non empty set ; now__::_thesis:_for_x_being_set_st_x_in_D1_holds_ x_in_the_carrier_of_(AbGroupCat_UN) let x be set ; ::_thesis: ( x in D1 implies x in the carrier of (AbGroupCat UN) ) assume x in D1 ; ::_thesis: x in the carrier of (AbGroupCat UN) then ex G being Element of the carrier of (AbGroupCat UN) st ( x = G & ex H being midpoint_operator AbGroup st G = H ) ; hence x in the carrier of (AbGroupCat UN) ; ::_thesis: verum end; hence not MidOpGroupObjects UN is empty ; ::_thesis: verum end; end; definition let UN be Universe; func MidOpGroupCat UN -> Subcategory of AbGroupCat UN equals :: GRCAT_1:def 34 cat (MidOpGroupObjects UN); coherence cat (MidOpGroupObjects UN) is Subcategory of AbGroupCat UN ; end; :: deftheorem defines MidOpGroupCat GRCAT_1:def_34_:_ for UN being Universe holds MidOpGroupCat UN = cat (MidOpGroupObjects UN); registration let UN be Universe; cluster MidOpGroupCat UN -> strict ; coherence MidOpGroupCat UN is strict ; end; theorem :: GRCAT_1:39 for UN being Universe holds the carrier of (MidOpGroupCat UN) = MidOpGroupObjects UN ; theorem :: GRCAT_1:40 for UN being Universe holds Trivial-addLoopStr in MidOpGroupObjects UN proof let UN be Universe; ::_thesis: Trivial-addLoopStr in MidOpGroupObjects UN Trivial-addLoopStr in the carrier of (AbGroupCat UN) by Th37; hence Trivial-addLoopStr in MidOpGroupObjects UN ; ::_thesis: verum end; theorem :: GRCAT_1:41 for S, T being non empty 1-sorted for f being Function of S,T st f is one-to-one & f is onto holds ( f * (f ") = id T & (f ") * f = id S & f " is one-to-one & f " is onto ) proof let S, T be non empty 1-sorted ; ::_thesis: for f being Function of S,T st f is one-to-one & f is onto holds ( f * (f ") = id T & (f ") * f = id S & f " is one-to-one & f " is onto ) let f be Function of S,T; ::_thesis: ( f is one-to-one & f is onto implies ( f * (f ") = id T & (f ") * f = id S & f " is one-to-one & f " is onto ) ) A1: [#] T = the carrier of T ; assume A2: ( f is one-to-one & f is onto ) ; ::_thesis: ( f * (f ") = id T & (f ") * f = id S & f " is one-to-one & f " is onto ) then A3: rng f = the carrier of T by FUNCT_2:def_3; then ( dom f = the carrier of S & rng (f ") = [#] S ) by A2, A1, FUNCT_2:def_1, TOPS_2:49; hence ( f * (f ") = id T & (f ") * f = id S & f " is one-to-one & f " is onto ) by A2, A3, A1, FUNCT_2:def_3, TOPS_2:50, TOPS_2:52; ::_thesis: verum end; theorem :: GRCAT_1:42 for UN being Universe for a being Object of (GroupCat UN) for aa being Element of GroupObjects UN st a = aa holds id a = ID aa proof let UN be Universe; ::_thesis: for a being Object of (GroupCat UN) for aa being Element of GroupObjects UN st a = aa holds id a = ID aa let a be Object of (GroupCat UN); ::_thesis: for aa being Element of GroupObjects UN st a = aa holds id a = ID aa let aa be Element of GroupObjects UN; ::_thesis: ( a = aa implies id a = ID aa ) set C = GroupCat UN; assume Z: a = aa ; ::_thesis: id a = ID aa reconsider ii = ID aa as Morphism of (GroupCat UN) ; reconsider ia = ii as GroupMorphismStr ; A: dom ii = dom ia by Def27 .= a by Z ; cod ii = cod ia by Def28 .= a by Z ; then reconsider ii = ii as Morphism of a,a by A, CAT_1:4; for b being Object of (GroupCat UN) holds ( ( Hom (a,b) <> {} implies for f being Morphism of a,b holds f (*) ii = f ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds ii (*) f = f ) ) by Z, Lm3; hence id a = ID aa by CAT_1:def_12; ::_thesis: verum end;