Metamath Proof Explorer

Theorem estrcco

Description: Composition in the category of extensible structures. (Contributed by AV, 7-Mar-2020)

Ref Expression
Hypotheses estrcbas.c 
|- C = ( ExtStrCat ` U )
estrcbas.u 
|- ( ph -> U e. V )
estrcco.o 
|- .x. = ( comp ` C )
estrcco.x 
|- ( ph -> X e. U )
estrcco.y 
|- ( ph -> Y e. U )
estrcco.z 
|- ( ph -> Z e. U )
estrcco.a 
|- A = ( Base ` X )
estrcco.b 
|- B = ( Base ` Y )
estrcco.d 
|- D = ( Base ` Z )
estrcco.f 
|- ( ph -> F : A --> B )
estrcco.g 
|- ( ph -> G : B --> D )
Assertion estrcco 
|- ( ph -> ( G ( <. X , Y >. .x. Z ) F ) = ( G o. F ) )

Proof

Step Hyp Ref Expression
1 estrcbas.c 
 |-  C = ( ExtStrCat ` U )
2 estrcbas.u 
 |-  ( ph -> U e. V )
3 estrcco.o 
 |-  .x. = ( comp ` C )
4 estrcco.x 
 |-  ( ph -> X e. U )
5 estrcco.y 
 |-  ( ph -> Y e. U )
6 estrcco.z 
 |-  ( ph -> Z e. U )
7 estrcco.a 
 |-  A = ( Base ` X )
8 estrcco.b 
 |-  B = ( Base ` Y )
9 estrcco.d 
 |-  D = ( Base ` Z )
10 estrcco.f 
 |-  ( ph -> F : A --> B )
11 estrcco.g 
 |-  ( ph -> G : B --> D )
12 1 2 3 estrccofval 
 |-  ( ph -> .x. = ( v e. ( U X. U ) , z e. U |-> ( g e. ( ( Base ` z ) ^m ( Base ` ( 2nd ` v ) ) ) , f e. ( ( Base ` ( 2nd ` v ) ) ^m ( Base ` ( 1st ` v ) ) ) |-> ( g o. f ) ) ) )
13 fveq2 
 |-  ( z = Z -> ( Base ` z ) = ( Base ` Z ) )
14 13 adantl 
 |-  ( ( v = <. X , Y >. /\ z = Z ) -> ( Base ` z ) = ( Base ` Z ) )
15 14 adantl 
 |-  ( ( ph /\ ( v = <. X , Y >. /\ z = Z ) ) -> ( Base ` z ) = ( Base ` Z ) )
16 simprl 
 |-  ( ( ph /\ ( v = <. X , Y >. /\ z = Z ) ) -> v = <. X , Y >. )
17 16 fveq2d 
 |-  ( ( ph /\ ( v = <. X , Y >. /\ z = Z ) ) -> ( 2nd ` v ) = ( 2nd ` <. X , Y >. ) )
18 op2ndg 
 |-  ( ( X e. U /\ Y e. U ) -> ( 2nd ` <. X , Y >. ) = Y )
19 4 5 18 syl2anc 
 |-  ( ph -> ( 2nd ` <. X , Y >. ) = Y )
20 19 adantr 
 |-  ( ( ph /\ ( v = <. X , Y >. /\ z = Z ) ) -> ( 2nd ` <. X , Y >. ) = Y )
21 17 20 eqtrd 
 |-  ( ( ph /\ ( v = <. X , Y >. /\ z = Z ) ) -> ( 2nd ` v ) = Y )
22 21 fveq2d 
 |-  ( ( ph /\ ( v = <. X , Y >. /\ z = Z ) ) -> ( Base ` ( 2nd ` v ) ) = ( Base ` Y ) )
23 15 22 oveq12d 
 |-  ( ( ph /\ ( v = <. X , Y >. /\ z = Z ) ) -> ( ( Base ` z ) ^m ( Base ` ( 2nd ` v ) ) ) = ( ( Base ` Z ) ^m ( Base ` Y ) ) )
24 16 fveq2d 
 |-  ( ( ph /\ ( v = <. X , Y >. /\ z = Z ) ) -> ( 1st ` v ) = ( 1st ` <. X , Y >. ) )
25 24 fveq2d 
 |-  ( ( ph /\ ( v = <. X , Y >. /\ z = Z ) ) -> ( Base ` ( 1st ` v ) ) = ( Base ` ( 1st ` <. X , Y >. ) ) )
26 op1stg 
 |-  ( ( X e. U /\ Y e. U ) -> ( 1st ` <. X , Y >. ) = X )
27 4 5 26 syl2anc 
 |-  ( ph -> ( 1st ` <. X , Y >. ) = X )
28 27 fveq2d 
 |-  ( ph -> ( Base ` ( 1st ` <. X , Y >. ) ) = ( Base ` X ) )
29 28 adantr 
 |-  ( ( ph /\ ( v = <. X , Y >. /\ z = Z ) ) -> ( Base ` ( 1st ` <. X , Y >. ) ) = ( Base ` X ) )
30 25 29 eqtrd 
 |-  ( ( ph /\ ( v = <. X , Y >. /\ z = Z ) ) -> ( Base ` ( 1st ` v ) ) = ( Base ` X ) )
31 22 30 oveq12d 
 |-  ( ( ph /\ ( v = <. X , Y >. /\ z = Z ) ) -> ( ( Base ` ( 2nd ` v ) ) ^m ( Base ` ( 1st ` v ) ) ) = ( ( Base ` Y ) ^m ( Base ` X ) ) )
32 eqidd 
 |-  ( ( ph /\ ( v = <. X , Y >. /\ z = Z ) ) -> ( g o. f ) = ( g o. f ) )
33 23 31 32 mpoeq123dv 
 |-  ( ( ph /\ ( v = <. X , Y >. /\ z = Z ) ) -> ( g e. ( ( Base ` z ) ^m ( Base ` ( 2nd ` v ) ) ) , f e. ( ( Base ` ( 2nd ` v ) ) ^m ( Base ` ( 1st ` v ) ) ) |-> ( g o. f ) ) = ( g e. ( ( Base ` Z ) ^m ( Base ` Y ) ) , f e. ( ( Base ` Y ) ^m ( Base ` X ) ) |-> ( g o. f ) ) )
34 4 5 opelxpd 
 |-  ( ph -> <. X , Y >. e. ( U X. U ) )
35 ovex 
 |-  ( ( Base ` Z ) ^m ( Base ` Y ) ) e. _V
36 ovex 
 |-  ( ( Base ` Y ) ^m ( Base ` X ) ) e. _V
37 35 36 mpoex 
 |-  ( g e. ( ( Base ` Z ) ^m ( Base ` Y ) ) , f e. ( ( Base ` Y ) ^m ( Base ` X ) ) |-> ( g o. f ) ) e. _V
38 37 a1i 
 |-  ( ph -> ( g e. ( ( Base ` Z ) ^m ( Base ` Y ) ) , f e. ( ( Base ` Y ) ^m ( Base ` X ) ) |-> ( g o. f ) ) e. _V )
39 12 33 34 6 38 ovmpod 
 |-  ( ph -> ( <. X , Y >. .x. Z ) = ( g e. ( ( Base ` Z ) ^m ( Base ` Y ) ) , f e. ( ( Base ` Y ) ^m ( Base ` X ) ) |-> ( g o. f ) ) )
40 simpl 
 |-  ( ( g = G /\ f = F ) -> g = G )
41 simpr 
 |-  ( ( g = G /\ f = F ) -> f = F )
42 40 41 coeq12d 
 |-  ( ( g = G /\ f = F ) -> ( g o. f ) = ( G o. F ) )
43 42 adantl 
 |-  ( ( ph /\ ( g = G /\ f = F ) ) -> ( g o. f ) = ( G o. F ) )
44 8 a1i 
 |-  ( ph -> B = ( Base ` Y ) )
45 44 eqcomd 
 |-  ( ph -> ( Base ` Y ) = B )
46 9 a1i 
 |-  ( ph -> D = ( Base ` Z ) )
47 46 eqcomd 
 |-  ( ph -> ( Base ` Z ) = D )
48 45 47 feq23d 
 |-  ( ph -> ( G : ( Base ` Y ) --> ( Base ` Z ) <-> G : B --> D ) )
49 11 48 mpbird 
 |-  ( ph -> G : ( Base ` Y ) --> ( Base ` Z ) )
50 fvexd 
 |-  ( ph -> ( Base ` Z ) e. _V )
51 fvexd 
 |-  ( ph -> ( Base ` Y ) e. _V )
52 50 51 elmapd 
 |-  ( ph -> ( G e. ( ( Base ` Z ) ^m ( Base ` Y ) ) <-> G : ( Base ` Y ) --> ( Base ` Z ) ) )
53 49 52 mpbird 
 |-  ( ph -> G e. ( ( Base ` Z ) ^m ( Base ` Y ) ) )
54 7 a1i 
 |-  ( ph -> A = ( Base ` X ) )
55 54 eqcomd 
 |-  ( ph -> ( Base ` X ) = A )
56 55 45 feq23d 
 |-  ( ph -> ( F : ( Base ` X ) --> ( Base ` Y ) <-> F : A --> B ) )
57 10 56 mpbird 
 |-  ( ph -> F : ( Base ` X ) --> ( Base ` Y ) )
58 fvexd 
 |-  ( ph -> ( Base ` X ) e. _V )
59 51 58 elmapd 
 |-  ( ph -> ( F e. ( ( Base ` Y ) ^m ( Base ` X ) ) <-> F : ( Base ` X ) --> ( Base ` Y ) ) )
60 57 59 mpbird 
 |-  ( ph -> F e. ( ( Base ` Y ) ^m ( Base ` X ) ) )
61 coexg 
 |-  ( ( G e. ( ( Base ` Z ) ^m ( Base ` Y ) ) /\ F e. ( ( Base ` Y ) ^m ( Base ` X ) ) ) -> ( G o. F ) e. _V )
62 53 60 61 syl2anc 
 |-  ( ph -> ( G o. F ) e. _V )
63 39 43 53 60 62 ovmpod 
 |-  ( ph -> ( G ( <. X , Y >. .x. Z ) F ) = ( G o. F ) )