Step |
Hyp |
Ref |
Expression |
1 |
|
oppgtmd.1 |
|- O = ( oppG ` G ) |
2 |
|
tmdmnd |
|- ( G e. TopMnd -> G e. Mnd ) |
3 |
1
|
oppgmnd |
|- ( G e. Mnd -> O e. Mnd ) |
4 |
2 3
|
syl |
|- ( G e. TopMnd -> O e. Mnd ) |
5 |
|
eqid |
|- ( TopOpen ` G ) = ( TopOpen ` G ) |
6 |
|
eqid |
|- ( Base ` G ) = ( Base ` G ) |
7 |
5 6
|
tmdtopon |
|- ( G e. TopMnd -> ( TopOpen ` G ) e. ( TopOn ` ( Base ` G ) ) ) |
8 |
1 6
|
oppgbas |
|- ( Base ` G ) = ( Base ` O ) |
9 |
1 5
|
oppgtopn |
|- ( TopOpen ` G ) = ( TopOpen ` O ) |
10 |
8 9
|
istps |
|- ( O e. TopSp <-> ( TopOpen ` G ) e. ( TopOn ` ( Base ` G ) ) ) |
11 |
7 10
|
sylibr |
|- ( G e. TopMnd -> O e. TopSp ) |
12 |
|
eqid |
|- ( +g ` G ) = ( +g ` G ) |
13 |
|
id |
|- ( G e. TopMnd -> G e. TopMnd ) |
14 |
7 7
|
cnmpt2nd |
|- ( G e. TopMnd -> ( x e. ( Base ` G ) , y e. ( Base ` G ) |-> y ) e. ( ( ( TopOpen ` G ) tX ( TopOpen ` G ) ) Cn ( TopOpen ` G ) ) ) |
15 |
7 7
|
cnmpt1st |
|- ( G e. TopMnd -> ( x e. ( Base ` G ) , y e. ( Base ` G ) |-> x ) e. ( ( ( TopOpen ` G ) tX ( TopOpen ` G ) ) Cn ( TopOpen ` G ) ) ) |
16 |
5 12 13 7 7 14 15
|
cnmpt2plusg |
|- ( G e. TopMnd -> ( x e. ( Base ` G ) , y e. ( Base ` G ) |-> ( y ( +g ` G ) x ) ) e. ( ( ( TopOpen ` G ) tX ( TopOpen ` G ) ) Cn ( TopOpen ` G ) ) ) |
17 |
|
eqid |
|- ( +g ` O ) = ( +g ` O ) |
18 |
|
eqid |
|- ( +f ` O ) = ( +f ` O ) |
19 |
8 17 18
|
plusffval |
|- ( +f ` O ) = ( x e. ( Base ` G ) , y e. ( Base ` G ) |-> ( x ( +g ` O ) y ) ) |
20 |
12 1 17
|
oppgplus |
|- ( x ( +g ` O ) y ) = ( y ( +g ` G ) x ) |
21 |
6 6 20
|
mpoeq123i |
|- ( x e. ( Base ` G ) , y e. ( Base ` G ) |-> ( x ( +g ` O ) y ) ) = ( x e. ( Base ` G ) , y e. ( Base ` G ) |-> ( y ( +g ` G ) x ) ) |
22 |
19 21
|
eqtr2i |
|- ( x e. ( Base ` G ) , y e. ( Base ` G ) |-> ( y ( +g ` G ) x ) ) = ( +f ` O ) |
23 |
22 9
|
istmd |
|- ( O e. TopMnd <-> ( O e. Mnd /\ O e. TopSp /\ ( x e. ( Base ` G ) , y e. ( Base ` G ) |-> ( y ( +g ` G ) x ) ) e. ( ( ( TopOpen ` G ) tX ( TopOpen ` G ) ) Cn ( TopOpen ` G ) ) ) ) |
24 |
4 11 16 23
|
syl3anbrc |
|- ( G e. TopMnd -> O e. TopMnd ) |