Step |
Hyp |
Ref |
Expression |
1 |
|
efmndbas.g |
|- G = ( EndoFMnd ` A ) |
2 |
|
efmndbas.b |
|- B = ( Base ` G ) |
3 |
|
ovex |
|- ( A ^m A ) e. _V |
4 |
|
eqid |
|- { <. ( Base ` ndx ) , ( A ^m A ) >. , <. ( +g ` ndx ) , ( f e. ( A ^m A ) , g e. ( A ^m A ) |-> ( f o. g ) ) >. , <. ( TopSet ` ndx ) , ( Xt_ ` ( A X. { ~P A } ) ) >. } = { <. ( Base ` ndx ) , ( A ^m A ) >. , <. ( +g ` ndx ) , ( f e. ( A ^m A ) , g e. ( A ^m A ) |-> ( f o. g ) ) >. , <. ( TopSet ` ndx ) , ( Xt_ ` ( A X. { ~P A } ) ) >. } |
5 |
4
|
topgrpbas |
|- ( ( A ^m A ) e. _V -> ( A ^m A ) = ( Base ` { <. ( Base ` ndx ) , ( A ^m A ) >. , <. ( +g ` ndx ) , ( f e. ( A ^m A ) , g e. ( A ^m A ) |-> ( f o. g ) ) >. , <. ( TopSet ` ndx ) , ( Xt_ ` ( A X. { ~P A } ) ) >. } ) ) |
6 |
3 5
|
mp1i |
|- ( A e. _V -> ( A ^m A ) = ( Base ` { <. ( Base ` ndx ) , ( A ^m A ) >. , <. ( +g ` ndx ) , ( f e. ( A ^m A ) , g e. ( A ^m A ) |-> ( f o. g ) ) >. , <. ( TopSet ` ndx ) , ( Xt_ ` ( A X. { ~P A } ) ) >. } ) ) |
7 |
|
eqid |
|- ( A ^m A ) = ( A ^m A ) |
8 |
|
eqid |
|- ( f e. ( A ^m A ) , g e. ( A ^m A ) |-> ( f o. g ) ) = ( f e. ( A ^m A ) , g e. ( A ^m A ) |-> ( f o. g ) ) |
9 |
|
eqid |
|- ( Xt_ ` ( A X. { ~P A } ) ) = ( Xt_ ` ( A X. { ~P A } ) ) |
10 |
1 7 8 9
|
efmnd |
|- ( A e. _V -> G = { <. ( Base ` ndx ) , ( A ^m A ) >. , <. ( +g ` ndx ) , ( f e. ( A ^m A ) , g e. ( A ^m A ) |-> ( f o. g ) ) >. , <. ( TopSet ` ndx ) , ( Xt_ ` ( A X. { ~P A } ) ) >. } ) |
11 |
10
|
fveq2d |
|- ( A e. _V -> ( Base ` G ) = ( Base ` { <. ( Base ` ndx ) , ( A ^m A ) >. , <. ( +g ` ndx ) , ( f e. ( A ^m A ) , g e. ( A ^m A ) |-> ( f o. g ) ) >. , <. ( TopSet ` ndx ) , ( Xt_ ` ( A X. { ~P A } ) ) >. } ) ) |
12 |
6 11
|
eqtr4d |
|- ( A e. _V -> ( A ^m A ) = ( Base ` G ) ) |
13 |
|
base0 |
|- (/) = ( Base ` (/) ) |
14 |
|
reldmmap |
|- Rel dom ^m |
15 |
14
|
ovprc1 |
|- ( -. A e. _V -> ( A ^m A ) = (/) ) |
16 |
|
fvprc |
|- ( -. A e. _V -> ( EndoFMnd ` A ) = (/) ) |
17 |
1 16
|
eqtrid |
|- ( -. A e. _V -> G = (/) ) |
18 |
17
|
fveq2d |
|- ( -. A e. _V -> ( Base ` G ) = ( Base ` (/) ) ) |
19 |
13 15 18
|
3eqtr4a |
|- ( -. A e. _V -> ( A ^m A ) = ( Base ` G ) ) |
20 |
12 19
|
pm2.61i |
|- ( A ^m A ) = ( Base ` G ) |
21 |
2 20
|
eqtr4i |
|- B = ( A ^m A ) |