Step | Hyp | Ref
| Expression |
1 | | tcphval.n |
. 2
β’ πΊ = (toβPreHilβπ) |
2 | | id 22 |
. . . . 5
β’ (π€ = π β π€ = π) |
3 | | fveq2 6892 |
. . . . . . 7
β’ (π€ = π β (Baseβπ€) = (Baseβπ)) |
4 | | tcphval.v |
. . . . . . 7
β’ π = (Baseβπ) |
5 | 3, 4 | eqtr4di 2791 |
. . . . . 6
β’ (π€ = π β (Baseβπ€) = π) |
6 | | fveq2 6892 |
. . . . . . . . 9
β’ (π€ = π β
(Β·πβπ€) =
(Β·πβπ)) |
7 | | tcphval.h |
. . . . . . . . 9
β’ , =
(Β·πβπ) |
8 | 6, 7 | eqtr4di 2791 |
. . . . . . . 8
β’ (π€ = π β
(Β·πβπ€) = , ) |
9 | 8 | oveqd 7426 |
. . . . . . 7
β’ (π€ = π β (π₯(Β·πβπ€)π₯) = (π₯ , π₯)) |
10 | 9 | fveq2d 6896 |
. . . . . 6
β’ (π€ = π β (ββ(π₯(Β·πβπ€)π₯)) = (ββ(π₯ , π₯))) |
11 | 5, 10 | mpteq12dv 5240 |
. . . . 5
β’ (π€ = π β (π₯ β (Baseβπ€) β¦ (ββ(π₯(Β·πβπ€)π₯))) = (π₯ β π β¦ (ββ(π₯ , π₯)))) |
12 | 2, 11 | oveq12d 7427 |
. . . 4
β’ (π€ = π β (π€ toNrmGrp (π₯ β (Baseβπ€) β¦ (ββ(π₯(Β·πβπ€)π₯)))) = (π toNrmGrp (π₯ β π β¦ (ββ(π₯ , π₯))))) |
13 | | df-tcph 24686 |
. . . 4
β’
toβPreHil = (π€
β V β¦ (π€
toNrmGrp (π₯ β
(Baseβπ€) β¦
(ββ(π₯(Β·πβπ€)π₯))))) |
14 | | ovex 7442 |
. . . 4
β’ (π toNrmGrp (π₯ β π β¦ (ββ(π₯ , π₯)))) β V |
15 | 12, 13, 14 | fvmpt 6999 |
. . 3
β’ (π β V β
(toβPreHilβπ) =
(π toNrmGrp (π₯ β π β¦ (ββ(π₯ , π₯))))) |
16 | | fvprc 6884 |
. . . 4
β’ (Β¬
π β V β
(toβPreHilβπ) =
β
) |
17 | | reldmtng 24147 |
. . . . 5
β’ Rel dom
toNrmGrp |
18 | 17 | ovprc1 7448 |
. . . 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 (π₯ β π β¦ (ββ(π₯ , π₯)))) |