Metamath Proof Explorer

Theorem funcestrcsetclem9

Description: Lemma 9 for funcestrcsetc . (Contributed by AV, 23-Mar-2020)

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

Proof

Step Hyp Ref Expression
1 funcestrcsetc.e 
 |-  E = ( ExtStrCat ` U )
2 funcestrcsetc.s 
 |-  S = ( SetCat ` U )
3 funcestrcsetc.b 
 |-  B = ( Base ` E )
4 funcestrcsetc.c 
 |-  C = ( Base ` S )
5 funcestrcsetc.u 
 |-  ( ph -> U e. WUni )
6 funcestrcsetc.f 
 |-  ( ph -> F = ( x e. B |-> ( Base ` x ) ) )
7 funcestrcsetc.g 
 |-  ( ph -> G = ( x e. B , y e. B |-> ( _I |` ( ( Base ` y ) ^m ( Base ` x ) ) ) ) )
8 5 adantr 
 |-  ( ( ph /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> U e. WUni )
9 eqid 
 |-  ( Hom ` E ) = ( Hom ` E )
10 1 5 estrcbas 
 |-  ( ph -> U = ( Base ` E ) )
11 3 10 eqtr4id 
 |-  ( ph -> B = U )
12 11 eleq2d 
 |-  ( ph -> ( X e. B <-> X e. U ) )
13 12 biimpcd 
 |-  ( X e. B -> ( ph -> X e. U ) )
14 13 3ad2ant1 
 |-  ( ( X e. B /\ Y e. B /\ Z e. B ) -> ( ph -> X e. U ) )
15 14 impcom 
 |-  ( ( ph /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> X e. U )
16 11 eleq2d 
 |-  ( ph -> ( Y e. B <-> Y e. U ) )
17 16 biimpcd 
 |-  ( Y e. B -> ( ph -> Y e. U ) )
18 17 3ad2ant2 
 |-  ( ( X e. B /\ Y e. B /\ Z e. B ) -> ( ph -> Y e. U ) )
19 18 impcom 
 |-  ( ( ph /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> Y e. U )
20 eqid 
 |-  ( Base ` X ) = ( Base ` X )
21 eqid 
 |-  ( Base ` Y ) = ( Base ` Y )
22 1 8 9 15 19 20 21 estrchom 
 |-  ( ( ph /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X ( Hom ` E ) Y ) = ( ( Base ` Y ) ^m ( Base ` X ) ) )
23 22 eleq2d 
 |-  ( ( ph /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( H e. ( X ( Hom ` E ) Y ) <-> H e. ( ( Base ` Y ) ^m ( Base ` X ) ) ) )
24 11 eleq2d 
 |-  ( ph -> ( Z e. B <-> Z e. U ) )
25 24 biimpcd 
 |-  ( Z e. B -> ( ph -> Z e. U ) )
26 25 3ad2ant3 
 |-  ( ( X e. B /\ Y e. B /\ Z e. B ) -> ( ph -> Z e. U ) )
27 26 impcom 
 |-  ( ( ph /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> Z e. U )
28 eqid 
 |-  ( Base ` Z ) = ( Base ` Z )
29 1 8 9 19 27 21 28 estrchom 
 |-  ( ( ph /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( Y ( Hom ` E ) Z ) = ( ( Base ` Z ) ^m ( Base ` Y ) ) )
30 29 eleq2d 
 |-  ( ( ph /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( K e. ( Y ( Hom ` E ) Z ) <-> K e. ( ( Base ` Z ) ^m ( Base ` Y ) ) ) )
31 23 30 anbi12d 
 |-  ( ( ph /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( H e. ( X ( Hom ` E ) Y ) /\ K e. ( Y ( Hom ` E ) Z ) ) <-> ( H e. ( ( Base ` Y ) ^m ( Base ` X ) ) /\ K e. ( ( Base ` Z ) ^m ( Base ` Y ) ) ) ) )
32 elmapi 
 |-  ( K e. ( ( Base ` Z ) ^m ( Base ` Y ) ) -> K : ( Base ` Y ) --> ( Base ` Z ) )
33 elmapi 
 |-  ( H e. ( ( Base ` Y ) ^m ( Base ` X ) ) -> H : ( Base ` X ) --> ( Base ` Y ) )
34 fco 
 |-  ( ( K : ( Base ` Y ) --> ( Base ` Z ) /\ H : ( Base ` X ) --> ( Base ` Y ) ) -> ( K o. H ) : ( Base ` X ) --> ( Base ` Z ) )
35 32 33 34 syl2an 
 |-  ( ( K e. ( ( Base ` Z ) ^m ( Base ` Y ) ) /\ H e. ( ( Base ` Y ) ^m ( Base ` X ) ) ) -> ( K o. H ) : ( Base ` X ) --> ( Base ` Z ) )
36 fvex 
 |-  ( Base ` Z ) e. _V
37 fvex 
 |-  ( Base ` X ) e. _V
38 36 37 elmap 
 |-  ( ( K o. H ) e. ( ( Base ` Z ) ^m ( Base ` X ) ) <-> ( K o. H ) : ( Base ` X ) --> ( Base ` Z ) )
39 35 38 sylibr 
 |-  ( ( K e. ( ( Base ` Z ) ^m ( Base ` Y ) ) /\ H e. ( ( Base ` Y ) ^m ( Base ` X ) ) ) -> ( K o. H ) e. ( ( Base ` Z ) ^m ( Base ` X ) ) )
40 39 ancoms 
 |-  ( ( H e. ( ( Base ` Y ) ^m ( Base ` X ) ) /\ K e. ( ( Base ` Z ) ^m ( Base ` Y ) ) ) -> ( K o. H ) e. ( ( Base ` Z ) ^m ( Base ` X ) ) )
41 40 adantl 
 |-  ( ( ( ph /\ ( X e. B /\ Y e. B /\ Z e. B ) ) /\ ( H e. ( ( Base ` Y ) ^m ( Base ` X ) ) /\ K e. ( ( Base ` Z ) ^m ( Base ` Y ) ) ) ) -> ( K o. H ) e. ( ( Base ` Z ) ^m ( Base ` X ) ) )
42 fvresi 
 |-  ( ( K o. H ) e. ( ( Base ` Z ) ^m ( Base ` X ) ) -> ( ( _I |` ( ( Base ` Z ) ^m ( Base ` X ) ) ) ` ( K o. H ) ) = ( K o. H ) )
43 41 42 syl 
 |-  ( ( ( ph /\ ( X e. B /\ Y e. B /\ Z e. B ) ) /\ ( H e. ( ( Base ` Y ) ^m ( Base ` X ) ) /\ K e. ( ( Base ` Z ) ^m ( Base ` Y ) ) ) ) -> ( ( _I |` ( ( Base ` Z ) ^m ( Base ` X ) ) ) ` ( K o. H ) ) = ( K o. H ) )
44 1 2 3 4 5 6 7 20 28 funcestrcsetclem5 
 |-  ( ( ph /\ ( X e. B /\ Z e. B ) ) -> ( X G Z ) = ( _I |` ( ( Base ` Z ) ^m ( Base ` X ) ) ) )
45 44 3adantr2 
 |-  ( ( ph /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X G Z ) = ( _I |` ( ( Base ` Z ) ^m ( Base ` X ) ) ) )
46 45 adantr 
 |-  ( ( ( ph /\ ( X e. B /\ Y e. B /\ Z e. B ) ) /\ ( H e. ( ( Base ` Y ) ^m ( Base ` X ) ) /\ K e. ( ( Base ` Z ) ^m ( Base ` Y ) ) ) ) -> ( X G Z ) = ( _I |` ( ( Base ` Z ) ^m ( Base ` X ) ) ) )
47 8 adantr 
 |-  ( ( ( ph /\ ( X e. B /\ Y e. B /\ Z e. B ) ) /\ ( H e. ( ( Base ` Y ) ^m ( Base ` X ) ) /\ K e. ( ( Base ` Z ) ^m ( Base ` Y ) ) ) ) -> U e. WUni )
48 eqid 
 |-  ( comp ` E ) = ( comp ` E )
49 15 adantr 
 |-  ( ( ( ph /\ ( X e. B /\ Y e. B /\ Z e. B ) ) /\ ( H e. ( ( Base ` Y ) ^m ( Base ` X ) ) /\ K e. ( ( Base ` Z ) ^m ( Base ` Y ) ) ) ) -> X e. U )
50 19 adantr 
 |-  ( ( ( ph /\ ( X e. B /\ Y e. B /\ Z e. B ) ) /\ ( H e. ( ( Base ` Y ) ^m ( Base ` X ) ) /\ K e. ( ( Base ` Z ) ^m ( Base ` Y ) ) ) ) -> Y e. U )
51 27 adantr 
 |-  ( ( ( ph /\ ( X e. B /\ Y e. B /\ Z e. B ) ) /\ ( H e. ( ( Base ` Y ) ^m ( Base ` X ) ) /\ K e. ( ( Base ` Z ) ^m ( Base ` Y ) ) ) ) -> Z e. U )
52 33 ad2antrl 
 |-  ( ( ( ph /\ ( X e. B /\ Y e. B /\ Z e. B ) ) /\ ( H e. ( ( Base ` Y ) ^m ( Base ` X ) ) /\ K e. ( ( Base ` Z ) ^m ( Base ` Y ) ) ) ) -> H : ( Base ` X ) --> ( Base ` Y ) )
53 32 ad2antll 
 |-  ( ( ( ph /\ ( X e. B /\ Y e. B /\ Z e. B ) ) /\ ( H e. ( ( Base ` Y ) ^m ( Base ` X ) ) /\ K e. ( ( Base ` Z ) ^m ( Base ` Y ) ) ) ) -> K : ( Base ` Y ) --> ( Base ` Z ) )
54 1 47 48 49 50 51 20 21 28 52 53 estrcco 
 |-  ( ( ( ph /\ ( X e. B /\ Y e. B /\ Z e. B ) ) /\ ( H e. ( ( Base ` Y ) ^m ( Base ` X ) ) /\ K e. ( ( Base ` Z ) ^m ( Base ` Y ) ) ) ) -> ( K ( <. X , Y >. ( comp ` E ) Z ) H ) = ( K o. H ) )
55 46 54 fveq12d 
 |-  ( ( ( ph /\ ( X e. B /\ Y e. B /\ Z e. B ) ) /\ ( H e. ( ( Base ` Y ) ^m ( Base ` X ) ) /\ K e. ( ( Base ` Z ) ^m ( Base ` Y ) ) ) ) -> ( ( X G Z ) ` ( K ( <. X , Y >. ( comp ` E ) Z ) H ) ) = ( ( _I |` ( ( Base ` Z ) ^m ( Base ` X ) ) ) ` ( K o. H ) ) )
56 eqid 
 |-  ( comp ` S ) = ( comp ` S )
57 1 2 3 4 5 6 funcestrcsetclem2 
 |-  ( ( ph /\ X e. B ) -> ( F ` X ) e. U )
58 57 3ad2antr1 
 |-  ( ( ph /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( F ` X ) e. U )
59 58 adantr 
 |-  ( ( ( ph /\ ( X e. B /\ Y e. B /\ Z e. B ) ) /\ ( H e. ( ( Base ` Y ) ^m ( Base ` X ) ) /\ K e. ( ( Base ` Z ) ^m ( Base ` Y ) ) ) ) -> ( F ` X ) e. U )
60 1 2 3 4 5 6 funcestrcsetclem2 
 |-  ( ( ph /\ Y e. B ) -> ( F ` Y ) e. U )
61 60 3ad2antr2 
 |-  ( ( ph /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( F ` Y ) e. U )
62 61 adantr 
 |-  ( ( ( ph /\ ( X e. B /\ Y e. B /\ Z e. B ) ) /\ ( H e. ( ( Base ` Y ) ^m ( Base ` X ) ) /\ K e. ( ( Base ` Z ) ^m ( Base ` Y ) ) ) ) -> ( F ` Y ) e. U )
63 1 2 3 4 5 6 funcestrcsetclem2 
 |-  ( ( ph /\ Z e. B ) -> ( F ` Z ) e. U )
64 63 3ad2antr3 
 |-  ( ( ph /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( F ` Z ) e. U )
65 64 adantr 
 |-  ( ( ( ph /\ ( X e. B /\ Y e. B /\ Z e. B ) ) /\ ( H e. ( ( Base ` Y ) ^m ( Base ` X ) ) /\ K e. ( ( Base ` Z ) ^m ( Base ` Y ) ) ) ) -> ( F ` Z ) e. U )
66 1 2 3 4 5 6 funcestrcsetclem1 
 |-  ( ( ph /\ X e. B ) -> ( F ` X ) = ( Base ` X ) )
67 66 3ad2antr1 
 |-  ( ( ph /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( F ` X ) = ( Base ` X ) )
68 1 2 3 4 5 6 funcestrcsetclem1 
 |-  ( ( ph /\ Y e. B ) -> ( F ` Y ) = ( Base ` Y ) )
69 68 3ad2antr2 
 |-  ( ( ph /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( F ` Y ) = ( Base ` Y ) )
70 67 69 feq23d 
 |-  ( ( ph /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( H : ( F ` X ) --> ( F ` Y ) <-> H : ( Base ` X ) --> ( Base ` Y ) ) )
71 70 adantr 
 |-  ( ( ( ph /\ ( X e. B /\ Y e. B /\ Z e. B ) ) /\ ( H e. ( ( Base ` Y ) ^m ( Base ` X ) ) /\ K e. ( ( Base ` Z ) ^m ( Base ` Y ) ) ) ) -> ( H : ( F ` X ) --> ( F ` Y ) <-> H : ( Base ` X ) --> ( Base ` Y ) ) )
72 52 71 mpbird 
 |-  ( ( ( ph /\ ( X e. B /\ Y e. B /\ Z e. B ) ) /\ ( H e. ( ( Base ` Y ) ^m ( Base ` X ) ) /\ K e. ( ( Base ` Z ) ^m ( Base ` Y ) ) ) ) -> H : ( F ` X ) --> ( F ` Y ) )
73 simpll 
 |-  ( ( ( ph /\ ( X e. B /\ Y e. B /\ Z e. B ) ) /\ ( H e. ( ( Base ` Y ) ^m ( Base ` X ) ) /\ K e. ( ( Base ` Z ) ^m ( Base ` Y ) ) ) ) -> ph )
74 3simpa 
 |-  ( ( X e. B /\ Y e. B /\ Z e. B ) -> ( X e. B /\ Y e. B ) )
75 74 ad2antlr 
 |-  ( ( ( ph /\ ( X e. B /\ Y e. B /\ Z e. B ) ) /\ ( H e. ( ( Base ` Y ) ^m ( Base ` X ) ) /\ K e. ( ( Base ` Z ) ^m ( Base ` Y ) ) ) ) -> ( X e. B /\ Y e. B ) )
76 simprl 
 |-  ( ( ( ph /\ ( X e. B /\ Y e. B /\ Z e. B ) ) /\ ( H e. ( ( Base ` Y ) ^m ( Base ` X ) ) /\ K e. ( ( Base ` Z ) ^m ( Base ` Y ) ) ) ) -> H e. ( ( Base ` Y ) ^m ( Base ` X ) ) )
77 1 2 3 4 5 6 7 20 21 funcestrcsetclem6 
 |-  ( ( ph /\ ( X e. B /\ Y e. B ) /\ H e. ( ( Base ` Y ) ^m ( Base ` X ) ) ) -> ( ( X G Y ) ` H ) = H )
78 73 75 76 77 syl3anc 
 |-  ( ( ( ph /\ ( X e. B /\ Y e. B /\ Z e. B ) ) /\ ( H e. ( ( Base ` Y ) ^m ( Base ` X ) ) /\ K e. ( ( Base ` Z ) ^m ( Base ` Y ) ) ) ) -> ( ( X G Y ) ` H ) = H )
79 78 feq1d 
 |-  ( ( ( ph /\ ( X e. B /\ Y e. B /\ Z e. B ) ) /\ ( H e. ( ( Base ` Y ) ^m ( Base ` X ) ) /\ K e. ( ( Base ` Z ) ^m ( Base ` Y ) ) ) ) -> ( ( ( X G Y ) ` H ) : ( F ` X ) --> ( F ` Y ) <-> H : ( F ` X ) --> ( F ` Y ) ) )
80 72 79 mpbird 
 |-  ( ( ( ph /\ ( X e. B /\ Y e. B /\ Z e. B ) ) /\ ( H e. ( ( Base ` Y ) ^m ( Base ` X ) ) /\ K e. ( ( Base ` Z ) ^m ( Base ` Y ) ) ) ) -> ( ( X G Y ) ` H ) : ( F ` X ) --> ( F ` Y ) )
81 1 2 3 4 5 6 funcestrcsetclem1 
 |-  ( ( ph /\ Z e. B ) -> ( F ` Z ) = ( Base ` Z ) )
82 81 3ad2antr3 
 |-  ( ( ph /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( F ` Z ) = ( Base ` Z ) )
83 69 82 feq23d 
 |-  ( ( ph /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( K : ( F ` Y ) --> ( F ` Z ) <-> K : ( Base ` Y ) --> ( Base ` Z ) ) )
84 83 adantr 
 |-  ( ( ( ph /\ ( X e. B /\ Y e. B /\ Z e. B ) ) /\ ( H e. ( ( Base ` Y ) ^m ( Base ` X ) ) /\ K e. ( ( Base ` Z ) ^m ( Base ` Y ) ) ) ) -> ( K : ( F ` Y ) --> ( F ` Z ) <-> K : ( Base ` Y ) --> ( Base ` Z ) ) )
85 53 84 mpbird 
 |-  ( ( ( ph /\ ( X e. B /\ Y e. B /\ Z e. B ) ) /\ ( H e. ( ( Base ` Y ) ^m ( Base ` X ) ) /\ K e. ( ( Base ` Z ) ^m ( Base ` Y ) ) ) ) -> K : ( F ` Y ) --> ( F ` Z ) )
86 3simpc 
 |-  ( ( X e. B /\ Y e. B /\ Z e. B ) -> ( Y e. B /\ Z e. B ) )
87 86 ad2antlr 
 |-  ( ( ( ph /\ ( X e. B /\ Y e. B /\ Z e. B ) ) /\ ( H e. ( ( Base ` Y ) ^m ( Base ` X ) ) /\ K e. ( ( Base ` Z ) ^m ( Base ` Y ) ) ) ) -> ( Y e. B /\ Z e. B ) )
88 simprr 
 |-  ( ( ( ph /\ ( X e. B /\ Y e. B /\ Z e. B ) ) /\ ( H e. ( ( Base ` Y ) ^m ( Base ` X ) ) /\ K e. ( ( Base ` Z ) ^m ( Base ` Y ) ) ) ) -> K e. ( ( Base ` Z ) ^m ( Base ` Y ) ) )
89 1 2 3 4 5 6 7 21 28 funcestrcsetclem6 
 |-  ( ( ph /\ ( Y e. B /\ Z e. B ) /\ K e. ( ( Base ` Z ) ^m ( Base ` Y ) ) ) -> ( ( Y G Z ) ` K ) = K )
90 73 87 88 89 syl3anc 
 |-  ( ( ( ph /\ ( X e. B /\ Y e. B /\ Z e. B ) ) /\ ( H e. ( ( Base ` Y ) ^m ( Base ` X ) ) /\ K e. ( ( Base ` Z ) ^m ( Base ` Y ) ) ) ) -> ( ( Y G Z ) ` K ) = K )
91 90 feq1d 
 |-  ( ( ( ph /\ ( X e. B /\ Y e. B /\ Z e. B ) ) /\ ( H e. ( ( Base ` Y ) ^m ( Base ` X ) ) /\ K e. ( ( Base ` Z ) ^m ( Base ` Y ) ) ) ) -> ( ( ( Y G Z ) ` K ) : ( F ` Y ) --> ( F ` Z ) <-> K : ( F ` Y ) --> ( F ` Z ) ) )
92 85 91 mpbird 
 |-  ( ( ( ph /\ ( X e. B /\ Y e. B /\ Z e. B ) ) /\ ( H e. ( ( Base ` Y ) ^m ( Base ` X ) ) /\ K e. ( ( Base ` Z ) ^m ( Base ` Y ) ) ) ) -> ( ( Y G Z ) ` K ) : ( F ` Y ) --> ( F ` Z ) )
93 2 47 56 59 62 65 80 92 setcco 
 |-  ( ( ( ph /\ ( X e. B /\ Y e. B /\ Z e. B ) ) /\ ( H e. ( ( Base ` Y ) ^m ( Base ` X ) ) /\ K e. ( ( Base ` Z ) ^m ( Base ` Y ) ) ) ) -> ( ( ( Y G Z ) ` K ) ( <. ( F ` X ) , ( F ` Y ) >. ( comp ` S ) ( F ` Z ) ) ( ( X G Y ) ` H ) ) = ( ( ( Y G Z ) ` K ) o. ( ( X G Y ) ` H ) ) )
94 90 78 coeq12d 
 |-  ( ( ( ph /\ ( X e. B /\ Y e. B /\ Z e. B ) ) /\ ( H e. ( ( Base ` Y ) ^m ( Base ` X ) ) /\ K e. ( ( Base ` Z ) ^m ( Base ` Y ) ) ) ) -> ( ( ( Y G Z ) ` K ) o. ( ( X G Y ) ` H ) ) = ( K o. H ) )
95 93 94 eqtrd 
 |-  ( ( ( ph /\ ( X e. B /\ Y e. B /\ Z e. B ) ) /\ ( H e. ( ( Base ` Y ) ^m ( Base ` X ) ) /\ K e. ( ( Base ` Z ) ^m ( Base ` Y ) ) ) ) -> ( ( ( Y G Z ) ` K ) ( <. ( F ` X ) , ( F ` Y ) >. ( comp ` S ) ( F ` Z ) ) ( ( X G Y ) ` H ) ) = ( K o. H ) )
96 43 55 95 3eqtr4d 
 |-  ( ( ( ph /\ ( X e. B /\ Y e. B /\ Z e. B ) ) /\ ( H e. ( ( Base ` Y ) ^m ( Base ` X ) ) /\ K e. ( ( Base ` Z ) ^m ( Base ` Y ) ) ) ) -> ( ( X G Z ) ` ( K ( <. X , Y >. ( comp ` E ) Z ) H ) ) = ( ( ( Y G Z ) ` K ) ( <. ( F ` X ) , ( F ` Y ) >. ( comp ` S ) ( F ` Z ) ) ( ( X G Y ) ` H ) ) )
97 96 ex 
 |-  ( ( ph /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( H e. ( ( Base ` Y ) ^m ( Base ` X ) ) /\ K e. ( ( Base ` Z ) ^m ( Base ` Y ) ) ) -> ( ( X G Z ) ` ( K ( <. X , Y >. ( comp ` E ) Z ) H ) ) = ( ( ( Y G Z ) ` K ) ( <. ( F ` X ) , ( F ` Y ) >. ( comp ` S ) ( F ` Z ) ) ( ( X G Y ) ` H ) ) ) )
98 31 97 sylbid 
 |-  ( ( ph /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( H e. ( X ( Hom ` E ) Y ) /\ K e. ( Y ( Hom ` E ) Z ) ) -> ( ( X G Z ) ` ( K ( <. X , Y >. ( comp ` E ) Z ) H ) ) = ( ( ( Y G Z ) ` K ) ( <. ( F ` X ) , ( F ` Y ) >. ( comp ` S ) ( F ` Z ) ) ( ( X G Y ) ` H ) ) ) )
99 98 3impia 
 |-  ( ( ph /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( H e. ( X ( Hom ` E ) Y ) /\ K e. ( Y ( Hom ` E ) Z ) ) ) -> ( ( X G Z ) ` ( K ( <. X , Y >. ( comp ` E ) Z ) H ) ) = ( ( ( Y G Z ) ` K ) ( <. ( F ` X ) , ( F ` Y ) >. ( comp ` S ) ( F ` Z ) ) ( ( X G Y ) ` H ) ) )