Step | Hyp | Ref
| Expression |
1 | | tngval.t |
. 2
β’ π = (πΊ toNrmGrp π) |
2 | | elex 3465 |
. . 3
β’ (πΊ β π β πΊ β V) |
3 | | elex 3465 |
. . 3
β’ (π β π β π β V) |
4 | | simpl 484 |
. . . . . 6
β’ ((π = πΊ β§ π = π) β π = πΊ) |
5 | | simpr 486 |
. . . . . . . . 9
β’ ((π = πΊ β§ π = π) β π = π) |
6 | 4 | fveq2d 6850 |
. . . . . . . . . 10
β’ ((π = πΊ β§ π = π) β (-gβπ) = (-gβπΊ)) |
7 | | tngval.m |
. . . . . . . . . 10
β’ β =
(-gβπΊ) |
8 | 6, 7 | eqtr4di 2791 |
. . . . . . . . 9
β’ ((π = πΊ β§ π = π) β (-gβπ) = β ) |
9 | 5, 8 | coeq12d 5824 |
. . . . . . . 8
β’ ((π = πΊ β§ π = π) β (π β (-gβπ)) = (π β β )) |
10 | | tngval.d |
. . . . . . . 8
β’ π· = (π β β ) |
11 | 9, 10 | eqtr4di 2791 |
. . . . . . 7
β’ ((π = πΊ β§ π = π) β (π β (-gβπ)) = π·) |
12 | 11 | opeq2d 4841 |
. . . . . 6
β’ ((π = πΊ β§ π = π) β β¨(distβndx), (π β
(-gβπ))β© = β¨(distβndx), π·β©) |
13 | 4, 12 | oveq12d 7379 |
. . . . 5
β’ ((π = πΊ β§ π = π) β (π sSet β¨(distβndx), (π β
(-gβπ))β©) = (πΊ sSet β¨(distβndx), π·β©)) |
14 | 11 | fveq2d 6850 |
. . . . . . 7
β’ ((π = πΊ β§ π = π) β (MetOpenβ(π β (-gβπ))) = (MetOpenβπ·)) |
15 | | tngval.j |
. . . . . . 7
β’ π½ = (MetOpenβπ·) |
16 | 14, 15 | eqtr4di 2791 |
. . . . . 6
β’ ((π = πΊ β§ π = π) β (MetOpenβ(π β (-gβπ))) = π½) |
17 | 16 | opeq2d 4841 |
. . . . 5
β’ ((π = πΊ β§ π = π) β β¨(TopSetβndx),
(MetOpenβ(π β
(-gβπ)))β© = β¨(TopSetβndx), π½β©) |
18 | 13, 17 | oveq12d 7379 |
. . . 4
β’ ((π = πΊ β§ π = π) β ((π sSet β¨(distβndx), (π β
(-gβπ))β©) sSet β¨(TopSetβndx),
(MetOpenβ(π β
(-gβπ)))β©) = ((πΊ sSet β¨(distβndx), π·β©) sSet
β¨(TopSetβndx), π½β©)) |
19 | | df-tng 23963 |
. . . 4
β’ toNrmGrp
= (π β V, π β V β¦ ((π sSet β¨(distβndx),
(π β
(-gβπ))β©) sSet β¨(TopSetβndx),
(MetOpenβ(π β
(-gβπ)))β©)) |
20 | | ovex 7394 |
. . . 4
β’ ((πΊ sSet β¨(distβndx),
π·β©) sSet
β¨(TopSetβndx), π½β©) β V |
21 | 18, 19, 20 | ovmpoa 7514 |
. . 3
β’ ((πΊ β V β§ π β V) β (πΊ toNrmGrp π) = ((πΊ sSet β¨(distβndx), π·β©) sSet
β¨(TopSetβndx), π½β©)) |
22 | 2, 3, 21 | syl2an 597 |
. 2
β’ ((πΊ β π β§ π β π) β (πΊ toNrmGrp π) = ((πΊ sSet β¨(distβndx), π·β©) sSet
β¨(TopSetβndx), π½β©)) |
23 | 1, 22 | eqtrid 2785 |
1
β’ ((πΊ β π β§ π β π) β π = ((πΊ sSet β¨(distβndx), π·β©) sSet
β¨(TopSetβndx), π½β©)) |