Step |
Hyp |
Ref |
Expression |
1 |
|
tcphval.n |
β’ πΊ = ( toβPreHil β π ) |
2 |
|
tcphnmval.n |
β’ π = ( norm β πΊ ) |
3 |
|
tcphnmval.v |
β’ π = ( Base β π ) |
4 |
|
tcphnmval.h |
β’ , = ( Β·π β π ) |
5 |
|
eqid |
β’ ( π₯ β π β¦ ( β β ( π₯ , π₯ ) ) ) = ( π₯ β π β¦ ( β β ( π₯ , π₯ ) ) ) |
6 |
|
fvrn0 |
β’ ( β β ( π₯ , π₯ ) ) β ( ran β βͺ { β
} ) |
7 |
6
|
a1i |
β’ ( π₯ β π β ( β β ( π₯ , π₯ ) ) β ( ran β βͺ { β
} ) ) |
8 |
5 7
|
fmpti |
β’ ( π₯ β π β¦ ( β β ( π₯ , π₯ ) ) ) : π βΆ ( ran β βͺ { β
} ) |
9 |
1 3 4
|
tcphval |
β’ πΊ = ( π toNrmGrp ( π₯ β π β¦ ( β β ( π₯ , π₯ ) ) ) ) |
10 |
|
cnex |
β’ β β V |
11 |
|
sqrtf |
β’ β : β βΆ β |
12 |
|
frn |
β’ ( β : β βΆ β β ran β β β ) |
13 |
11 12
|
ax-mp |
β’ ran β β β |
14 |
10 13
|
ssexi |
β’ ran β β V |
15 |
|
p0ex |
β’ { β
} β V |
16 |
14 15
|
unex |
β’ ( ran β βͺ { β
} ) β V |
17 |
9 3 16
|
tngnm |
β’ ( ( π β Grp β§ ( π₯ β π β¦ ( β β ( π₯ , π₯ ) ) ) : π βΆ ( ran β βͺ { β
} ) ) β ( π₯ β π β¦ ( β β ( π₯ , π₯ ) ) ) = ( norm β πΊ ) ) |
18 |
8 17
|
mpan2 |
β’ ( π β Grp β ( π₯ β π β¦ ( β β ( π₯ , π₯ ) ) ) = ( norm β πΊ ) ) |
19 |
2 18
|
eqtr4id |
β’ ( π β Grp β π = ( π₯ β π β¦ ( β β ( π₯ , π₯ ) ) ) ) |