Step | Hyp | Ref
| Expression |
1 | | tnglemOLD.2 |
. . . . . 6
β’ πΈ = Slot πΎ |
2 | | tnglemOLD.3 |
. . . . . 6
β’ πΎ β β |
3 | 1, 2 | ndxid 17074 |
. . . . 5
β’ πΈ = Slot (πΈβndx) |
4 | 1, 2 | ndxarg 17073 |
. . . . . . . 8
β’ (πΈβndx) = πΎ |
5 | 2 | nnrei 12167 |
. . . . . . . 8
β’ πΎ β β |
6 | 4, 5 | eqeltri 2830 |
. . . . . . 7
β’ (πΈβndx) β
β |
7 | | tnglemOLD.4 |
. . . . . . . . 9
β’ πΎ < 9 |
8 | 4, 7 | eqbrtri 5127 |
. . . . . . . 8
β’ (πΈβndx) <
9 |
9 | | 1nn 12169 |
. . . . . . . . 9
β’ 1 β
β |
10 | | 2nn0 12435 |
. . . . . . . . 9
β’ 2 β
β0 |
11 | | 9nn0 12442 |
. . . . . . . . 9
β’ 9 β
β0 |
12 | | 9lt10 12754 |
. . . . . . . . 9
β’ 9 <
;10 |
13 | 9, 10, 11, 12 | declti 12661 |
. . . . . . . 8
β’ 9 <
;12 |
14 | | 9re 12257 |
. . . . . . . . 9
β’ 9 β
β |
15 | | 1nn0 12434 |
. . . . . . . . . . 11
β’ 1 β
β0 |
16 | 15, 10 | deccl 12638 |
. . . . . . . . . 10
β’ ;12 β
β0 |
17 | 16 | nn0rei 12429 |
. . . . . . . . 9
β’ ;12 β β |
18 | 6, 14, 17 | lttri 11286 |
. . . . . . . 8
β’ (((πΈβndx) < 9 β§ 9 <
;12) β (πΈβndx) < ;12) |
19 | 8, 13, 18 | mp2an 691 |
. . . . . . 7
β’ (πΈβndx) < ;12 |
20 | 6, 19 | ltneii 11273 |
. . . . . 6
β’ (πΈβndx) β ;12 |
21 | | dsndx 17271 |
. . . . . 6
β’
(distβndx) = ;12 |
22 | 20, 21 | neeqtrri 3014 |
. . . . 5
β’ (πΈβndx) β
(distβndx) |
23 | 3, 22 | setsnid 17086 |
. . . 4
β’ (πΈβπΊ) = (πΈβ(πΊ sSet β¨(distβndx), (π β
(-gβπΊ))β©)) |
24 | 6, 8 | ltneii 11273 |
. . . . . 6
β’ (πΈβndx) β
9 |
25 | | tsetndx 17238 |
. . . . . 6
β’
(TopSetβndx) = 9 |
26 | 24, 25 | neeqtrri 3014 |
. . . . 5
β’ (πΈβndx) β
(TopSetβndx) |
27 | 3, 26 | setsnid 17086 |
. . . 4
β’ (πΈβ(πΊ sSet β¨(distβndx), (π β
(-gβπΊ))β©)) = (πΈβ((πΊ sSet β¨(distβndx), (π β
(-gβπΊ))β©) sSet β¨(TopSetβndx),
(MetOpenβ(π β
(-gβπΊ)))β©)) |
28 | 23, 27 | eqtri 2761 |
. . 3
β’ (πΈβπΊ) = (πΈβ((πΊ sSet β¨(distβndx), (π β
(-gβπΊ))β©) sSet β¨(TopSetβndx),
(MetOpenβ(π β
(-gβπΊ)))β©)) |
29 | | tngbas.t |
. . . . 5
β’ π = (πΊ toNrmGrp π) |
30 | | eqid 2733 |
. . . . 5
β’
(-gβπΊ) = (-gβπΊ) |
31 | | eqid 2733 |
. . . . 5
β’ (π β
(-gβπΊ)) =
(π β
(-gβπΊ)) |
32 | | eqid 2733 |
. . . . 5
β’
(MetOpenβ(π
β (-gβπΊ))) = (MetOpenβ(π β (-gβπΊ))) |
33 | 29, 30, 31, 32 | tngval 24011 |
. . . 4
β’ ((πΊ β V β§ π β π) β π = ((πΊ sSet β¨(distβndx), (π β
(-gβπΊ))β©) sSet β¨(TopSetβndx),
(MetOpenβ(π β
(-gβπΊ)))β©)) |
34 | 33 | fveq2d 6847 |
. . 3
β’ ((πΊ β V β§ π β π) β (πΈβπ) = (πΈβ((πΊ sSet β¨(distβndx), (π β
(-gβπΊ))β©) sSet β¨(TopSetβndx),
(MetOpenβ(π β
(-gβπΊ)))β©))) |
35 | 28, 34 | eqtr4id 2792 |
. 2
β’ ((πΊ β V β§ π β π) β (πΈβπΊ) = (πΈβπ)) |
36 | 1 | str0 17066 |
. . 3
β’ β
=
(πΈββ
) |
37 | | fvprc 6835 |
. . . 4
β’ (Β¬
πΊ β V β (πΈβπΊ) = β
) |
38 | 37 | adantr 482 |
. . 3
β’ ((Β¬
πΊ β V β§ π β π) β (πΈβπΊ) = β
) |
39 | | reldmtng 24010 |
. . . . . . 7
β’ Rel dom
toNrmGrp |
40 | 39 | ovprc1 7397 |
. . . . . 6
β’ (Β¬
πΊ β V β (πΊ toNrmGrp π) = β
) |
41 | 40 | adantr 482 |
. . . . 5
β’ ((Β¬
πΊ β V β§ π β π) β (πΊ toNrmGrp π) = β
) |
42 | 29, 41 | eqtrid 2785 |
. . . 4
β’ ((Β¬
πΊ β V β§ π β π) β π = β
) |
43 | 42 | fveq2d 6847 |
. . 3
β’ ((Β¬
πΊ β V β§ π β π) β (πΈβπ) = (πΈββ
)) |
44 | 36, 38, 43 | 3eqtr4a 2799 |
. 2
β’ ((Β¬
πΊ β V β§ π β π) β (πΈβπΊ) = (πΈβπ)) |
45 | 35, 44 | pm2.61ian 811 |
1
β’ (π β π β (πΈβπΊ) = (πΈβπ)) |