Metamath Proof Explorer

Theorem funcsetcestrclem9

Description: Lemma 9 for funcsetcestrc . (Contributed by AV, 28-Mar-2020)

Ref Expression
Hypotheses funcsetcestrc.s 
|- S = ( SetCat ` U )
funcsetcestrc.c 
|- C = ( Base ` S )
funcsetcestrc.f 
|- ( ph -> F = ( x e. C |-> { <. ( Base ` ndx ) , x >. } ) )
funcsetcestrc.u 
|- ( ph -> U e. WUni )
funcsetcestrc.o 
|- ( ph -> _om e. U )
funcsetcestrc.g 
|- ( ph -> G = ( x e. C , y e. C |-> ( _I |` ( y ^m x ) ) ) )
funcsetcestrc.e 
|- E = ( ExtStrCat ` U )
Assertion funcsetcestrclem9 
|- ( ( ph /\ ( X e. C /\ Y e. C /\ Z e. C ) /\ ( H e. ( X ( Hom ` S ) Y ) /\ K e. ( Y ( Hom ` S ) Z ) ) ) -> ( ( X G Z ) ` ( K ( <. X , Y >. ( comp ` S ) Z ) H ) ) = ( ( ( Y G Z ) ` K ) ( <. ( F ` X ) , ( F ` Y ) >. ( comp ` E ) ( F ` Z ) ) ( ( X G Y ) ` H ) ) )

Proof

Step Hyp Ref Expression
1 funcsetcestrc.s 
 |-  S = ( SetCat ` U )
2 funcsetcestrc.c 
 |-  C = ( Base ` S )
3 funcsetcestrc.f 
 |-  ( ph -> F = ( x e. C |-> { <. ( Base ` ndx ) , x >. } ) )
4 funcsetcestrc.u 
 |-  ( ph -> U e. WUni )
5 funcsetcestrc.o 
 |-  ( ph -> _om e. U )
6 funcsetcestrc.g 
 |-  ( ph -> G = ( x e. C , y e. C |-> ( _I |` ( y ^m x ) ) ) )
7 funcsetcestrc.e 
 |-  E = ( ExtStrCat ` U )
8 4 adantr 
 |-  ( ( ph /\ ( X e. C /\ Y e. C /\ Z e. C ) ) -> U e. WUni )
9 eqid 
 |-  ( Hom ` S ) = ( Hom ` S )
10 1 4 setcbas 
 |-  ( ph -> U = ( Base ` S ) )
11 2 10 eqtr4id 
 |-  ( ph -> C = U )
12 11 eleq2d 
 |-  ( ph -> ( X e. C <-> X e. U ) )
13 12 biimpcd 
 |-  ( X e. C -> ( ph -> X e. U ) )
14 13 3ad2ant1 
 |-  ( ( X e. C /\ Y e. C /\ Z e. C ) -> ( ph -> X e. U ) )
15 14 impcom 
 |-  ( ( ph /\ ( X e. C /\ Y e. C /\ Z e. C ) ) -> X e. U )
16 11 eleq2d 
 |-  ( ph -> ( Y e. C <-> Y e. U ) )
17 16 biimpcd 
 |-  ( Y e. C -> ( ph -> Y e. U ) )
18 17 3ad2ant2 
 |-  ( ( X e. C /\ Y e. C /\ Z e. C ) -> ( ph -> Y e. U ) )
19 18 impcom 
 |-  ( ( ph /\ ( X e. C /\ Y e. C /\ Z e. C ) ) -> Y e. U )
20 1 8 9 15 19 setchom 
 |-  ( ( ph /\ ( X e. C /\ Y e. C /\ Z e. C ) ) -> ( X ( Hom ` S ) Y ) = ( Y ^m X ) )
21 20 eleq2d 
 |-  ( ( ph /\ ( X e. C /\ Y e. C /\ Z e. C ) ) -> ( H e. ( X ( Hom ` S ) Y ) <-> H e. ( Y ^m X ) ) )
22 11 eleq2d 
 |-  ( ph -> ( Z e. C <-> Z e. U ) )
23 22 biimpcd 
 |-  ( Z e. C -> ( ph -> Z e. U ) )
24 23 3ad2ant3 
 |-  ( ( X e. C /\ Y e. C /\ Z e. C ) -> ( ph -> Z e. U ) )
25 24 impcom 
 |-  ( ( ph /\ ( X e. C /\ Y e. C /\ Z e. C ) ) -> Z e. U )
26 1 8 9 19 25 setchom 
 |-  ( ( ph /\ ( X e. C /\ Y e. C /\ Z e. C ) ) -> ( Y ( Hom ` S ) Z ) = ( Z ^m Y ) )
27 26 eleq2d 
 |-  ( ( ph /\ ( X e. C /\ Y e. C /\ Z e. C ) ) -> ( K e. ( Y ( Hom ` S ) Z ) <-> K e. ( Z ^m Y ) ) )
28 21 27 anbi12d 
 |-  ( ( ph /\ ( X e. C /\ Y e. C /\ Z e. C ) ) -> ( ( H e. ( X ( Hom ` S ) Y ) /\ K e. ( Y ( Hom ` S ) Z ) ) <-> ( H e. ( Y ^m X ) /\ K e. ( Z ^m Y ) ) ) )
29 elmapi 
 |-  ( K e. ( Z ^m Y ) -> K : Y --> Z )
30 elmapi 
 |-  ( H e. ( Y ^m X ) -> H : X --> Y )
31 fco 
 |-  ( ( K : Y --> Z /\ H : X --> Y ) -> ( K o. H ) : X --> Z )
32 29 30 31 syl2anr 
 |-  ( ( H e. ( Y ^m X ) /\ K e. ( Z ^m Y ) ) -> ( K o. H ) : X --> Z )
33 32 adantl 
 |-  ( ( ( ph /\ ( X e. C /\ Y e. C /\ Z e. C ) ) /\ ( H e. ( Y ^m X ) /\ K e. ( Z ^m Y ) ) ) -> ( K o. H ) : X --> Z )
34 elmapg 
 |-  ( ( Z e. C /\ X e. C ) -> ( ( K o. H ) e. ( Z ^m X ) <-> ( K o. H ) : X --> Z ) )
35 34 ancoms 
 |-  ( ( X e. C /\ Z e. C ) -> ( ( K o. H ) e. ( Z ^m X ) <-> ( K o. H ) : X --> Z ) )
36 35 3adant2 
 |-  ( ( X e. C /\ Y e. C /\ Z e. C ) -> ( ( K o. H ) e. ( Z ^m X ) <-> ( K o. H ) : X --> Z ) )
37 36 ad2antlr 
 |-  ( ( ( ph /\ ( X e. C /\ Y e. C /\ Z e. C ) ) /\ ( H e. ( Y ^m X ) /\ K e. ( Z ^m Y ) ) ) -> ( ( K o. H ) e. ( Z ^m X ) <-> ( K o. H ) : X --> Z ) )
38 33 37 mpbird 
 |-  ( ( ( ph /\ ( X e. C /\ Y e. C /\ Z e. C ) ) /\ ( H e. ( Y ^m X ) /\ K e. ( Z ^m Y ) ) ) -> ( K o. H ) e. ( Z ^m X ) )
39 fvresi 
 |-  ( ( K o. H ) e. ( Z ^m X ) -> ( ( _I |` ( Z ^m X ) ) ` ( K o. H ) ) = ( K o. H ) )
40 38 39 syl 
 |-  ( ( ( ph /\ ( X e. C /\ Y e. C /\ Z e. C ) ) /\ ( H e. ( Y ^m X ) /\ K e. ( Z ^m Y ) ) ) -> ( ( _I |` ( Z ^m X ) ) ` ( K o. H ) ) = ( K o. H ) )
41 1 2 3 4 5 6 funcsetcestrclem5 
 |-  ( ( ph /\ ( X e. C /\ Z e. C ) ) -> ( X G Z ) = ( _I |` ( Z ^m X ) ) )
42 41 3adantr2 
 |-  ( ( ph /\ ( X e. C /\ Y e. C /\ Z e. C ) ) -> ( X G Z ) = ( _I |` ( Z ^m X ) ) )
43 42 adantr 
 |-  ( ( ( ph /\ ( X e. C /\ Y e. C /\ Z e. C ) ) /\ ( H e. ( Y ^m X ) /\ K e. ( Z ^m Y ) ) ) -> ( X G Z ) = ( _I |` ( Z ^m X ) ) )
44 8 adantr 
 |-  ( ( ( ph /\ ( X e. C /\ Y e. C /\ Z e. C ) ) /\ ( H e. ( Y ^m X ) /\ K e. ( Z ^m Y ) ) ) -> U e. WUni )
45 eqid 
 |-  ( comp ` S ) = ( comp ` S )
46 15 adantr 
 |-  ( ( ( ph /\ ( X e. C /\ Y e. C /\ Z e. C ) ) /\ ( H e. ( Y ^m X ) /\ K e. ( Z ^m Y ) ) ) -> X e. U )
47 19 adantr 
 |-  ( ( ( ph /\ ( X e. C /\ Y e. C /\ Z e. C ) ) /\ ( H e. ( Y ^m X ) /\ K e. ( Z ^m Y ) ) ) -> Y e. U )
48 25 adantr 
 |-  ( ( ( ph /\ ( X e. C /\ Y e. C /\ Z e. C ) ) /\ ( H e. ( Y ^m X ) /\ K e. ( Z ^m Y ) ) ) -> Z e. U )
49 30 ad2antrl 
 |-  ( ( ( ph /\ ( X e. C /\ Y e. C /\ Z e. C ) ) /\ ( H e. ( Y ^m X ) /\ K e. ( Z ^m Y ) ) ) -> H : X --> Y )
50 29 ad2antll 
 |-  ( ( ( ph /\ ( X e. C /\ Y e. C /\ Z e. C ) ) /\ ( H e. ( Y ^m X ) /\ K e. ( Z ^m Y ) ) ) -> K : Y --> Z )
51 1 44 45 46 47 48 49 50 setcco 
 |-  ( ( ( ph /\ ( X e. C /\ Y e. C /\ Z e. C ) ) /\ ( H e. ( Y ^m X ) /\ K e. ( Z ^m Y ) ) ) -> ( K ( <. X , Y >. ( comp ` S ) Z ) H ) = ( K o. H ) )
52 43 51 fveq12d 
 |-  ( ( ( ph /\ ( X e. C /\ Y e. C /\ Z e. C ) ) /\ ( H e. ( Y ^m X ) /\ K e. ( Z ^m Y ) ) ) -> ( ( X G Z ) ` ( K ( <. X , Y >. ( comp ` S ) Z ) H ) ) = ( ( _I |` ( Z ^m X ) ) ` ( K o. H ) ) )
53 eqid 
 |-  ( comp ` E ) = ( comp ` E )
54 1 2 3 4 5 funcsetcestrclem2 
 |-  ( ( ph /\ X e. C ) -> ( F ` X ) e. U )
55 54 3ad2antr1 
 |-  ( ( ph /\ ( X e. C /\ Y e. C /\ Z e. C ) ) -> ( F ` X ) e. U )
56 55 adantr 
 |-  ( ( ( ph /\ ( X e. C /\ Y e. C /\ Z e. C ) ) /\ ( H e. ( Y ^m X ) /\ K e. ( Z ^m Y ) ) ) -> ( F ` X ) e. U )
57 1 2 3 4 5 funcsetcestrclem2 
 |-  ( ( ph /\ Y e. C ) -> ( F ` Y ) e. U )
58 57 3ad2antr2 
 |-  ( ( ph /\ ( X e. C /\ Y e. C /\ Z e. C ) ) -> ( F ` Y ) e. U )
59 58 adantr 
 |-  ( ( ( ph /\ ( X e. C /\ Y e. C /\ Z e. C ) ) /\ ( H e. ( Y ^m X ) /\ K e. ( Z ^m Y ) ) ) -> ( F ` Y ) e. U )
60 1 2 3 4 5 funcsetcestrclem2 
 |-  ( ( ph /\ Z e. C ) -> ( F ` Z ) e. U )
61 60 3ad2antr3 
 |-  ( ( ph /\ ( X e. C /\ Y e. C /\ Z e. C ) ) -> ( F ` Z ) e. U )
62 61 adantr 
 |-  ( ( ( ph /\ ( X e. C /\ Y e. C /\ Z e. C ) ) /\ ( H e. ( Y ^m X ) /\ K e. ( Z ^m Y ) ) ) -> ( F ` Z ) e. U )
63 eqid 
 |-  ( Base ` ( F ` X ) ) = ( Base ` ( F ` X ) )
64 eqid 
 |-  ( Base ` ( F ` Y ) ) = ( Base ` ( F ` Y ) )
65 eqid 
 |-  ( Base ` ( F ` Z ) ) = ( Base ` ( F ` Z ) )
66 simpll 
 |-  ( ( ( ph /\ ( X e. C /\ Y e. C /\ Z e. C ) ) /\ ( H e. ( Y ^m X ) /\ K e. ( Z ^m Y ) ) ) -> ph )
67 3simpa 
 |-  ( ( X e. C /\ Y e. C /\ Z e. C ) -> ( X e. C /\ Y e. C ) )
68 67 ad2antlr 
 |-  ( ( ( ph /\ ( X e. C /\ Y e. C /\ Z e. C ) ) /\ ( H e. ( Y ^m X ) /\ K e. ( Z ^m Y ) ) ) -> ( X e. C /\ Y e. C ) )
69 simprl 
 |-  ( ( ( ph /\ ( X e. C /\ Y e. C /\ Z e. C ) ) /\ ( H e. ( Y ^m X ) /\ K e. ( Z ^m Y ) ) ) -> H e. ( Y ^m X ) )
70 1 2 3 4 5 6 funcsetcestrclem6 
 |-  ( ( ph /\ ( X e. C /\ Y e. C ) /\ H e. ( Y ^m X ) ) -> ( ( X G Y ) ` H ) = H )
71 66 68 69 70 syl3anc 
 |-  ( ( ( ph /\ ( X e. C /\ Y e. C /\ Z e. C ) ) /\ ( H e. ( Y ^m X ) /\ K e. ( Z ^m Y ) ) ) -> ( ( X G Y ) ` H ) = H )
72 1 2 3 funcsetcestrclem1 
 |-  ( ( ph /\ X e. C ) -> ( F ` X ) = { <. ( Base ` ndx ) , X >. } )
73 72 3ad2antr1 
 |-  ( ( ph /\ ( X e. C /\ Y e. C /\ Z e. C ) ) -> ( F ` X ) = { <. ( Base ` ndx ) , X >. } )
74 73 fveq2d 
 |-  ( ( ph /\ ( X e. C /\ Y e. C /\ Z e. C ) ) -> ( Base ` ( F ` X ) ) = ( Base ` { <. ( Base ` ndx ) , X >. } ) )
75 eqid 
 |-  { <. ( Base ` ndx ) , X >. } = { <. ( Base ` ndx ) , X >. }
76 75 1strbas 
 |-  ( X e. C -> X = ( Base ` { <. ( Base ` ndx ) , X >. } ) )
77 76 eqcomd 
 |-  ( X e. C -> ( Base ` { <. ( Base ` ndx ) , X >. } ) = X )
78 77 3ad2ant1 
 |-  ( ( X e. C /\ Y e. C /\ Z e. C ) -> ( Base ` { <. ( Base ` ndx ) , X >. } ) = X )
79 78 adantl 
 |-  ( ( ph /\ ( X e. C /\ Y e. C /\ Z e. C ) ) -> ( Base ` { <. ( Base ` ndx ) , X >. } ) = X )
80 74 79 eqtrd 
 |-  ( ( ph /\ ( X e. C /\ Y e. C /\ Z e. C ) ) -> ( Base ` ( F ` X ) ) = X )
81 80 adantr 
 |-  ( ( ( ph /\ ( X e. C /\ Y e. C /\ Z e. C ) ) /\ ( H e. ( Y ^m X ) /\ K e. ( Z ^m Y ) ) ) -> ( Base ` ( F ` X ) ) = X )
82 1 2 3 funcsetcestrclem1 
 |-  ( ( ph /\ Y e. C ) -> ( F ` Y ) = { <. ( Base ` ndx ) , Y >. } )
83 82 3ad2antr2 
 |-  ( ( ph /\ ( X e. C /\ Y e. C /\ Z e. C ) ) -> ( F ` Y ) = { <. ( Base ` ndx ) , Y >. } )
84 83 fveq2d 
 |-  ( ( ph /\ ( X e. C /\ Y e. C /\ Z e. C ) ) -> ( Base ` ( F ` Y ) ) = ( Base ` { <. ( Base ` ndx ) , Y >. } ) )
85 eqid 
 |-  { <. ( Base ` ndx ) , Y >. } = { <. ( Base ` ndx ) , Y >. }
86 85 1strbas 
 |-  ( Y e. C -> Y = ( Base ` { <. ( Base ` ndx ) , Y >. } ) )
87 86 eqcomd 
 |-  ( Y e. C -> ( Base ` { <. ( Base ` ndx ) , Y >. } ) = Y )
88 87 3ad2ant2 
 |-  ( ( X e. C /\ Y e. C /\ Z e. C ) -> ( Base ` { <. ( Base ` ndx ) , Y >. } ) = Y )
89 88 adantl 
 |-  ( ( ph /\ ( X e. C /\ Y e. C /\ Z e. C ) ) -> ( Base ` { <. ( Base ` ndx ) , Y >. } ) = Y )
90 84 89 eqtrd 
 |-  ( ( ph /\ ( X e. C /\ Y e. C /\ Z e. C ) ) -> ( Base ` ( F ` Y ) ) = Y )
91 90 adantr 
 |-  ( ( ( ph /\ ( X e. C /\ Y e. C /\ Z e. C ) ) /\ ( H e. ( Y ^m X ) /\ K e. ( Z ^m Y ) ) ) -> ( Base ` ( F ` Y ) ) = Y )
92 71 81 91 feq123d 
 |-  ( ( ( ph /\ ( X e. C /\ Y e. C /\ Z e. C ) ) /\ ( H e. ( Y ^m X ) /\ K e. ( Z ^m Y ) ) ) -> ( ( ( X G Y ) ` H ) : ( Base ` ( F ` X ) ) --> ( Base ` ( F ` Y ) ) <-> H : X --> Y ) )
93 49 92 mpbird 
 |-  ( ( ( ph /\ ( X e. C /\ Y e. C /\ Z e. C ) ) /\ ( H e. ( Y ^m X ) /\ K e. ( Z ^m Y ) ) ) -> ( ( X G Y ) ` H ) : ( Base ` ( F ` X ) ) --> ( Base ` ( F ` Y ) ) )
94 3simpc 
 |-  ( ( X e. C /\ Y e. C /\ Z e. C ) -> ( Y e. C /\ Z e. C ) )
95 94 ad2antlr 
 |-  ( ( ( ph /\ ( X e. C /\ Y e. C /\ Z e. C ) ) /\ ( H e. ( Y ^m X ) /\ K e. ( Z ^m Y ) ) ) -> ( Y e. C /\ Z e. C ) )
96 simprr 
 |-  ( ( ( ph /\ ( X e. C /\ Y e. C /\ Z e. C ) ) /\ ( H e. ( Y ^m X ) /\ K e. ( Z ^m Y ) ) ) -> K e. ( Z ^m Y ) )
97 1 2 3 4 5 6 funcsetcestrclem6 
 |-  ( ( ph /\ ( Y e. C /\ Z e. C ) /\ K e. ( Z ^m Y ) ) -> ( ( Y G Z ) ` K ) = K )
98 66 95 96 97 syl3anc 
 |-  ( ( ( ph /\ ( X e. C /\ Y e. C /\ Z e. C ) ) /\ ( H e. ( Y ^m X ) /\ K e. ( Z ^m Y ) ) ) -> ( ( Y G Z ) ` K ) = K )
99 1 2 3 funcsetcestrclem1 
 |-  ( ( ph /\ Z e. C ) -> ( F ` Z ) = { <. ( Base ` ndx ) , Z >. } )
100 99 3ad2antr3 
 |-  ( ( ph /\ ( X e. C /\ Y e. C /\ Z e. C ) ) -> ( F ` Z ) = { <. ( Base ` ndx ) , Z >. } )
101 100 fveq2d 
 |-  ( ( ph /\ ( X e. C /\ Y e. C /\ Z e. C ) ) -> ( Base ` ( F ` Z ) ) = ( Base ` { <. ( Base ` ndx ) , Z >. } ) )
102 eqid 
 |-  { <. ( Base ` ndx ) , Z >. } = { <. ( Base ` ndx ) , Z >. }
103 102 1strbas 
 |-  ( Z e. C -> Z = ( Base ` { <. ( Base ` ndx ) , Z >. } ) )
104 103 eqcomd 
 |-  ( Z e. C -> ( Base ` { <. ( Base ` ndx ) , Z >. } ) = Z )
105 104 3ad2ant3 
 |-  ( ( X e. C /\ Y e. C /\ Z e. C ) -> ( Base ` { <. ( Base ` ndx ) , Z >. } ) = Z )
106 105 adantl 
 |-  ( ( ph /\ ( X e. C /\ Y e. C /\ Z e. C ) ) -> ( Base ` { <. ( Base ` ndx ) , Z >. } ) = Z )
107 101 106 eqtrd 
 |-  ( ( ph /\ ( X e. C /\ Y e. C /\ Z e. C ) ) -> ( Base ` ( F ` Z ) ) = Z )
108 107 adantr 
 |-  ( ( ( ph /\ ( X e. C /\ Y e. C /\ Z e. C ) ) /\ ( H e. ( Y ^m X ) /\ K e. ( Z ^m Y ) ) ) -> ( Base ` ( F ` Z ) ) = Z )
109 98 91 108 feq123d 
 |-  ( ( ( ph /\ ( X e. C /\ Y e. C /\ Z e. C ) ) /\ ( H e. ( Y ^m X ) /\ K e. ( Z ^m Y ) ) ) -> ( ( ( Y G Z ) ` K ) : ( Base ` ( F ` Y ) ) --> ( Base ` ( F ` Z ) ) <-> K : Y --> Z ) )
110 50 109 mpbird 
 |-  ( ( ( ph /\ ( X e. C /\ Y e. C /\ Z e. C ) ) /\ ( H e. ( Y ^m X ) /\ K e. ( Z ^m Y ) ) ) -> ( ( Y G Z ) ` K ) : ( Base ` ( F ` Y ) ) --> ( Base ` ( F ` Z ) ) )
111 7 44 53 56 59 62 63 64 65 93 110 estrcco 
 |-  ( ( ( ph /\ ( X e. C /\ Y e. C /\ Z e. C ) ) /\ ( H e. ( Y ^m X ) /\ K e. ( Z ^m Y ) ) ) -> ( ( ( Y G Z ) ` K ) ( <. ( F ` X ) , ( F ` Y ) >. ( comp ` E ) ( F ` Z ) ) ( ( X G Y ) ` H ) ) = ( ( ( Y G Z ) ` K ) o. ( ( X G Y ) ` H ) ) )
112 98 71 coeq12d 
 |-  ( ( ( ph /\ ( X e. C /\ Y e. C /\ Z e. C ) ) /\ ( H e. ( Y ^m X ) /\ K e. ( Z ^m Y ) ) ) -> ( ( ( Y G Z ) ` K ) o. ( ( X G Y ) ` H ) ) = ( K o. H ) )
113 111 112 eqtrd 
 |-  ( ( ( ph /\ ( X e. C /\ Y e. C /\ Z e. C ) ) /\ ( H e. ( Y ^m X ) /\ K e. ( Z ^m Y ) ) ) -> ( ( ( Y G Z ) ` K ) ( <. ( F ` X ) , ( F ` Y ) >. ( comp ` E ) ( F ` Z ) ) ( ( X G Y ) ` H ) ) = ( K o. H ) )
114 40 52 113 3eqtr4d 
 |-  ( ( ( ph /\ ( X e. C /\ Y e. C /\ Z e. C ) ) /\ ( H e. ( Y ^m X ) /\ K e. ( Z ^m Y ) ) ) -> ( ( X G Z ) ` ( K ( <. X , Y >. ( comp ` S ) Z ) H ) ) = ( ( ( Y G Z ) ` K ) ( <. ( F ` X ) , ( F ` Y ) >. ( comp ` E ) ( F ` Z ) ) ( ( X G Y ) ` H ) ) )
115 114 ex 
 |-  ( ( ph /\ ( X e. C /\ Y e. C /\ Z e. C ) ) -> ( ( H e. ( Y ^m X ) /\ K e. ( Z ^m Y ) ) -> ( ( X G Z ) ` ( K ( <. X , Y >. ( comp ` S ) Z ) H ) ) = ( ( ( Y G Z ) ` K ) ( <. ( F ` X ) , ( F ` Y ) >. ( comp ` E ) ( F ` Z ) ) ( ( X G Y ) ` H ) ) ) )
116 28 115 sylbid 
 |-  ( ( ph /\ ( X e. C /\ Y e. C /\ Z e. C ) ) -> ( ( H e. ( X ( Hom ` S ) Y ) /\ K e. ( Y ( Hom ` S ) Z ) ) -> ( ( X G Z ) ` ( K ( <. X , Y >. ( comp ` S ) Z ) H ) ) = ( ( ( Y G Z ) ` K ) ( <. ( F ` X ) , ( F ` Y ) >. ( comp ` E ) ( F ` Z ) ) ( ( X G Y ) ` H ) ) ) )
117 116 3impia 
 |-  ( ( ph /\ ( X e. C /\ Y e. C /\ Z e. C ) /\ ( H e. ( X ( Hom ` S ) Y ) /\ K e. ( Y ( Hom ` S ) Z ) ) ) -> ( ( X G Z ) ` ( K ( <. X , Y >. ( comp ` S ) Z ) H ) ) = ( ( ( Y G Z ) ` K ) ( <. ( F ` X ) , ( F ` Y ) >. ( comp ` E ) ( F ` Z ) ) ( ( X G Y ) ` H ) ) )