Step |
Hyp |
Ref |
Expression |
1 |
|
estrcval.c |
|- C = ( ExtStrCat ` U ) |
2 |
|
estrcval.u |
|- ( ph -> U e. V ) |
3 |
|
estrcval.h |
|- ( ph -> H = ( x e. U , y e. U |-> ( ( Base ` y ) ^m ( Base ` x ) ) ) ) |
4 |
|
estrcval.o |
|- ( 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 ) ) ) ) |
5 |
|
df-estrc |
|- ExtStrCat = ( u e. _V |-> { <. ( Base ` ndx ) , u >. , <. ( Hom ` ndx ) , ( x e. u , y e. u |-> ( ( Base ` y ) ^m ( Base ` x ) ) ) >. , <. ( comp ` ndx ) , ( 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 ) ) ) >. } ) |
6 |
|
simpr |
|- ( ( ph /\ u = U ) -> u = U ) |
7 |
6
|
opeq2d |
|- ( ( ph /\ u = U ) -> <. ( Base ` ndx ) , u >. = <. ( Base ` ndx ) , U >. ) |
8 |
|
eqidd |
|- ( ( ph /\ u = U ) -> ( ( Base ` y ) ^m ( Base ` x ) ) = ( ( Base ` y ) ^m ( Base ` x ) ) ) |
9 |
6 6 8
|
mpoeq123dv |
|- ( ( ph /\ u = U ) -> ( x e. u , y e. u |-> ( ( Base ` y ) ^m ( Base ` x ) ) ) = ( x e. U , y e. U |-> ( ( Base ` y ) ^m ( Base ` x ) ) ) ) |
10 |
3
|
adantr |
|- ( ( ph /\ u = U ) -> H = ( x e. U , y e. U |-> ( ( Base ` y ) ^m ( Base ` x ) ) ) ) |
11 |
9 10
|
eqtr4d |
|- ( ( ph /\ u = U ) -> ( x e. u , y e. u |-> ( ( Base ` y ) ^m ( Base ` x ) ) ) = H ) |
12 |
11
|
opeq2d |
|- ( ( ph /\ u = U ) -> <. ( Hom ` ndx ) , ( x e. u , y e. u |-> ( ( Base ` y ) ^m ( Base ` x ) ) ) >. = <. ( Hom ` ndx ) , H >. ) |
13 |
6
|
sqxpeqd |
|- ( ( ph /\ u = U ) -> ( u X. u ) = ( U X. U ) ) |
14 |
|
eqidd |
|- ( ( ph /\ u = U ) -> ( 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 ` ( 2nd ` v ) ) ) , f e. ( ( Base ` ( 2nd ` v ) ) ^m ( Base ` ( 1st ` v ) ) ) |-> ( g o. f ) ) ) |
15 |
13 6 14
|
mpoeq123dv |
|- ( ( ph /\ u = U ) -> ( 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 ) ) ) = ( 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 ) ) ) ) |
16 |
4
|
adantr |
|- ( ( ph /\ u = U ) -> .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 ) ) ) ) |
17 |
15 16
|
eqtr4d |
|- ( ( ph /\ u = U ) -> ( 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 ) ) ) = .x. ) |
18 |
17
|
opeq2d |
|- ( ( ph /\ u = U ) -> <. ( comp ` ndx ) , ( 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 ) ) ) >. = <. ( comp ` ndx ) , .x. >. ) |
19 |
7 12 18
|
tpeq123d |
|- ( ( ph /\ u = U ) -> { <. ( Base ` ndx ) , u >. , <. ( Hom ` ndx ) , ( x e. u , y e. u |-> ( ( Base ` y ) ^m ( Base ` x ) ) ) >. , <. ( comp ` ndx ) , ( 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 ) ) ) >. } = { <. ( Base ` ndx ) , U >. , <. ( Hom ` ndx ) , H >. , <. ( comp ` ndx ) , .x. >. } ) |
20 |
2
|
elexd |
|- ( ph -> U e. _V ) |
21 |
|
tpex |
|- { <. ( Base ` ndx ) , U >. , <. ( Hom ` ndx ) , H >. , <. ( comp ` ndx ) , .x. >. } e. _V |
22 |
21
|
a1i |
|- ( ph -> { <. ( Base ` ndx ) , U >. , <. ( Hom ` ndx ) , H >. , <. ( comp ` ndx ) , .x. >. } e. _V ) |
23 |
5 19 20 22
|
fvmptd2 |
|- ( ph -> ( ExtStrCat ` U ) = { <. ( Base ` ndx ) , U >. , <. ( Hom ` ndx ) , H >. , <. ( comp ` ndx ) , .x. >. } ) |
24 |
1 23
|
eqtrid |
|- ( ph -> C = { <. ( Base ` ndx ) , U >. , <. ( Hom ` ndx ) , H >. , <. ( comp ` ndx ) , .x. >. } ) |