Step | Hyp | Ref
| Expression |
1 | | tcphval.n |
. 2
β’ πΊ = (toβPreHilβπ) |
2 | | id 22 |
. . . . 5
β’ (π€ = π β π€ = π) |
3 | | fveq2 6846 |
. . . . . . 7
β’ (π€ = π β (Baseβπ€) = (Baseβπ)) |
4 | | tcphval.v |
. . . . . . 7
β’ π = (Baseβπ) |
5 | 3, 4 | eqtr4di 2791 |
. . . . . 6
β’ (π€ = π β (Baseβπ€) = π) |
6 | | fveq2 6846 |
. . . . . . . . 9
β’ (π€ = π β
(Β·πβπ€) =
(Β·πβπ)) |
7 | | tcphval.h |
. . . . . . . . 9
β’ , =
(Β·πβπ) |
8 | 6, 7 | eqtr4di 2791 |
. . . . . . . 8
β’ (π€ = π β
(Β·πβπ€) = , ) |
9 | 8 | oveqd 7378 |
. . . . . . 7
β’ (π€ = π β (π₯(Β·πβπ€)π₯) = (π₯ , π₯)) |
10 | 9 | fveq2d 6850 |
. . . . . 6
β’ (π€ = π β (ββ(π₯(Β·πβπ€)π₯)) = (ββ(π₯ , π₯))) |
11 | 5, 10 | mpteq12dv 5200 |
. . . . 5
β’ (π€ = π β (π₯ β (Baseβπ€) β¦ (ββ(π₯(Β·πβπ€)π₯))) = (π₯ β π β¦ (ββ(π₯ , π₯)))) |
12 | 2, 11 | oveq12d 7379 |
. . . 4
β’ (π€ = π β (π€ toNrmGrp (π₯ β (Baseβπ€) β¦ (ββ(π₯(Β·πβπ€)π₯)))) = (π toNrmGrp (π₯ β π β¦ (ββ(π₯ , π₯))))) |
13 | | df-tcph 24556 |
. . . 4
β’
toβPreHil = (π€
β V β¦ (π€
toNrmGrp (π₯ β
(Baseβπ€) β¦
(ββ(π₯(Β·πβπ€)π₯))))) |
14 | | ovex 7394 |
. . . 4
β’ (π toNrmGrp (π₯ β π β¦ (ββ(π₯ , π₯)))) β V |
15 | 12, 13, 14 | fvmpt 6952 |
. . 3
β’ (π β V β
(toβPreHilβπ) =
(π toNrmGrp (π₯ β π β¦ (ββ(π₯ , π₯))))) |
16 | | fvprc 6838 |
. . . 4
β’ (Β¬
π β V β
(toβPreHilβπ) =
β
) |
17 | | reldmtng 24017 |
. . . . 5
β’ Rel dom
toNrmGrp |
18 | 17 | ovprc1 7400 |
. . . 4
β’ (Β¬
π β V β (π toNrmGrp (π₯ β π β¦ (ββ(π₯ , π₯)))) = β
) |
19 | 16, 18 | eqtr4d 2776 |
. . 3
β’ (Β¬
π β V β
(toβPreHilβπ) =
(π toNrmGrp (π₯ β π β¦ (ββ(π₯ , π₯))))) |
20 | 15, 19 | pm2.61i 182 |
. 2
β’
(toβPreHilβπ) = (π toNrmGrp (π₯ β π β¦ (ββ(π₯ , π₯)))) |
21 | 1, 20 | eqtri 2761 |
1
β’ πΊ = (π toNrmGrp (π₯ β π β¦ (ββ(π₯ , π₯)))) |