Step |
Hyp |
Ref |
Expression |
0 |
|
ctng |
|- toNrmGrp |
1 |
|
vg |
|- g |
2 |
|
cvv |
|- _V |
3 |
|
vf |
|- f |
4 |
1
|
cv |
|- g |
5 |
|
csts |
|- sSet |
6 |
|
cds |
|- dist |
7 |
|
cnx |
|- ndx |
8 |
7 6
|
cfv |
|- ( dist ` ndx ) |
9 |
3
|
cv |
|- f |
10 |
|
csg |
|- -g |
11 |
4 10
|
cfv |
|- ( -g ` g ) |
12 |
9 11
|
ccom |
|- ( f o. ( -g ` g ) ) |
13 |
8 12
|
cop |
|- <. ( dist ` ndx ) , ( f o. ( -g ` g ) ) >. |
14 |
4 13 5
|
co |
|- ( g sSet <. ( dist ` ndx ) , ( f o. ( -g ` g ) ) >. ) |
15 |
|
cts |
|- TopSet |
16 |
7 15
|
cfv |
|- ( TopSet ` ndx ) |
17 |
|
cmopn |
|- MetOpen |
18 |
12 17
|
cfv |
|- ( MetOpen ` ( f o. ( -g ` g ) ) ) |
19 |
16 18
|
cop |
|- <. ( TopSet ` ndx ) , ( MetOpen ` ( f o. ( -g ` g ) ) ) >. |
20 |
14 19 5
|
co |
|- ( ( g sSet <. ( dist ` ndx ) , ( f o. ( -g ` g ) ) >. ) sSet <. ( TopSet ` ndx ) , ( MetOpen ` ( f o. ( -g ` g ) ) ) >. ) |
21 |
1 3 2 2 20
|
cmpo |
|- ( g e. _V , f e. _V |-> ( ( g sSet <. ( dist ` ndx ) , ( f o. ( -g ` g ) ) >. ) sSet <. ( TopSet ` ndx ) , ( MetOpen ` ( f o. ( -g ` g ) ) ) >. ) ) |
22 |
0 21
|
wceq |
|- toNrmGrp = ( g e. _V , f e. _V |-> ( ( g sSet <. ( dist ` ndx ) , ( f o. ( -g ` g ) ) >. ) sSet <. ( TopSet ` ndx ) , ( MetOpen ` ( f o. ( -g ` g ) ) ) >. ) ) |