Step | Hyp | Ref
| Expression |
1 | | nrgring 24171 |
. . . 4
β’ (π
β NrmRing β π
β Ring) |
2 | | nrginvrcn.u |
. . . . 5
β’ π = (Unitβπ
) |
3 | | eqid 2732 |
. . . . 5
β’
((mulGrpβπ
)
βΎs π) =
((mulGrpβπ
)
βΎs π) |
4 | 2, 3 | unitgrp 20189 |
. . . 4
β’ (π
β Ring β
((mulGrpβπ
)
βΎs π)
β Grp) |
5 | 2, 3 | unitgrpbas 20188 |
. . . . 5
β’ π =
(Baseβ((mulGrpβπ
) βΎs π)) |
6 | | nrginvrcn.i |
. . . . . 6
β’ πΌ = (invrβπ
) |
7 | 2, 3, 6 | invrfval 20195 |
. . . . 5
β’ πΌ =
(invgβ((mulGrpβπ
) βΎs π)) |
8 | 5, 7 | grpinvf 18867 |
. . . 4
β’
(((mulGrpβπ
)
βΎs π)
β Grp β πΌ:πβΆπ) |
9 | 1, 4, 8 | 3syl 18 |
. . 3
β’ (π
β NrmRing β πΌ:πβΆπ) |
10 | | 1rp 12974 |
. . . . . . . 8
β’ 1 β
β+ |
11 | 10 | ne0ii 4336 |
. . . . . . 7
β’
β+ β β
|
12 | 1 | ad2antrr 724 |
. . . . . . . . . . . . . 14
β’ (((π
β NrmRing β§ (π₯ β π β§ π β β+)) β§ π¦ β π) β π
β Ring) |
13 | | nrginvrcn.x |
. . . . . . . . . . . . . . . 16
β’ π = (Baseβπ
) |
14 | 13, 2 | unitss 20182 |
. . . . . . . . . . . . . . 15
β’ π β π |
15 | | simplrl 775 |
. . . . . . . . . . . . . . 15
β’ (((π
β NrmRing β§ (π₯ β π β§ π β β+)) β§ π¦ β π) β π₯ β π) |
16 | 14, 15 | sselid 3979 |
. . . . . . . . . . . . . 14
β’ (((π
β NrmRing β§ (π₯ β π β§ π β β+)) β§ π¦ β π) β π₯ β π) |
17 | | simpr 485 |
. . . . . . . . . . . . . . 15
β’ (((π
β NrmRing β§ (π₯ β π β§ π β β+)) β§ π¦ β π) β π¦ β π) |
18 | 14, 17 | sselid 3979 |
. . . . . . . . . . . . . 14
β’ (((π
β NrmRing β§ (π₯ β π β§ π β β+)) β§ π¦ β π) β π¦ β π) |
19 | | eqid 2732 |
. . . . . . . . . . . . . . 15
β’
(1rβπ
) = (1rβπ
) |
20 | | eqid 2732 |
. . . . . . . . . . . . . . 15
β’
(0gβπ
) = (0gβπ
) |
21 | 13, 19, 20 | ring1eq0 20103 |
. . . . . . . . . . . . . 14
β’ ((π
β Ring β§ π₯ β π β§ π¦ β π) β ((1rβπ
) = (0gβπ
) β π₯ = π¦)) |
22 | 12, 16, 18, 21 | syl3anc 1371 |
. . . . . . . . . . . . 13
β’ (((π
β NrmRing β§ (π₯ β π β§ π β β+)) β§ π¦ β π) β ((1rβπ
) = (0gβπ
) β π₯ = π¦)) |
23 | | eqid 2732 |
. . . . . . . . . . . . . . . 16
β’ (πΌβπ¦) = (πΌβπ¦) |
24 | | nrgngp 24170 |
. . . . . . . . . . . . . . . . . . 19
β’ (π
β NrmRing β π
β NrmGrp) |
25 | | ngpms 24100 |
. . . . . . . . . . . . . . . . . . 19
β’ (π
β NrmGrp β π
β MetSp) |
26 | | msxms 23951 |
. . . . . . . . . . . . . . . . . . 19
β’ (π
β MetSp β π
β
βMetSp) |
27 | 24, 25, 26 | 3syl 18 |
. . . . . . . . . . . . . . . . . 18
β’ (π
β NrmRing β π
β
βMetSp) |
28 | 27 | ad2antrr 724 |
. . . . . . . . . . . . . . . . 17
β’ (((π
β NrmRing β§ (π₯ β π β§ π β β+)) β§ π¦ β π) β π
β βMetSp) |
29 | 9 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π
β NrmRing β§ (π₯ β π β§ π β β+)) β πΌ:πβΆπ) |
30 | 29 | ffvelcdmda 7083 |
. . . . . . . . . . . . . . . . . 18
β’ (((π
β NrmRing β§ (π₯ β π β§ π β β+)) β§ π¦ β π) β (πΌβπ¦) β π) |
31 | 14, 30 | sselid 3979 |
. . . . . . . . . . . . . . . . 17
β’ (((π
β NrmRing β§ (π₯ β π β§ π β β+)) β§ π¦ β π) β (πΌβπ¦) β π) |
32 | | eqid 2732 |
. . . . . . . . . . . . . . . . . 18
β’
(distβπ
) =
(distβπ
) |
33 | 13, 32 | xmseq0 23961 |
. . . . . . . . . . . . . . . . 17
β’ ((π
β βMetSp β§
(πΌβπ¦) β π β§ (πΌβπ¦) β π) β (((πΌβπ¦)(distβπ
)(πΌβπ¦)) = 0 β (πΌβπ¦) = (πΌβπ¦))) |
34 | 28, 31, 31, 33 | syl3anc 1371 |
. . . . . . . . . . . . . . . 16
β’ (((π
β NrmRing β§ (π₯ β π β§ π β β+)) β§ π¦ β π) β (((πΌβπ¦)(distβπ
)(πΌβπ¦)) = 0 β (πΌβπ¦) = (πΌβπ¦))) |
35 | 23, 34 | mpbiri 257 |
. . . . . . . . . . . . . . 15
β’ (((π
β NrmRing β§ (π₯ β π β§ π β β+)) β§ π¦ β π) β ((πΌβπ¦)(distβπ
)(πΌβπ¦)) = 0) |
36 | | simplrr 776 |
. . . . . . . . . . . . . . . 16
β’ (((π
β NrmRing β§ (π₯ β π β§ π β β+)) β§ π¦ β π) β π β β+) |
37 | 36 | rpgt0d 13015 |
. . . . . . . . . . . . . . 15
β’ (((π
β NrmRing β§ (π₯ β π β§ π β β+)) β§ π¦ β π) β 0 < π) |
38 | 35, 37 | eqbrtrd 5169 |
. . . . . . . . . . . . . 14
β’ (((π
β NrmRing β§ (π₯ β π β§ π β β+)) β§ π¦ β π) β ((πΌβπ¦)(distβπ
)(πΌβπ¦)) < π) |
39 | | fveq2 6888 |
. . . . . . . . . . . . . . . 16
β’ (π₯ = π¦ β (πΌβπ₯) = (πΌβπ¦)) |
40 | 39 | oveq1d 7420 |
. . . . . . . . . . . . . . 15
β’ (π₯ = π¦ β ((πΌβπ₯)(distβπ
)(πΌβπ¦)) = ((πΌβπ¦)(distβπ
)(πΌβπ¦))) |
41 | 40 | breq1d 5157 |
. . . . . . . . . . . . . 14
β’ (π₯ = π¦ β (((πΌβπ₯)(distβπ
)(πΌβπ¦)) < π β ((πΌβπ¦)(distβπ
)(πΌβπ¦)) < π)) |
42 | 38, 41 | syl5ibrcom 246 |
. . . . . . . . . . . . 13
β’ (((π
β NrmRing β§ (π₯ β π β§ π β β+)) β§ π¦ β π) β (π₯ = π¦ β ((πΌβπ₯)(distβπ
)(πΌβπ¦)) < π)) |
43 | 22, 42 | syld 47 |
. . . . . . . . . . . 12
β’ (((π
β NrmRing β§ (π₯ β π β§ π β β+)) β§ π¦ β π) β ((1rβπ
) = (0gβπ
) β ((πΌβπ₯)(distβπ
)(πΌβπ¦)) < π)) |
44 | 43 | imp 407 |
. . . . . . . . . . 11
β’ ((((π
β NrmRing β§ (π₯ β π β§ π β β+)) β§ π¦ β π) β§ (1rβπ
) = (0gβπ
)) β ((πΌβπ₯)(distβπ
)(πΌβπ¦)) < π) |
45 | 44 | an32s 650 |
. . . . . . . . . 10
β’ ((((π
β NrmRing β§ (π₯ β π β§ π β β+)) β§
(1rβπ
) =
(0gβπ
))
β§ π¦ β π) β ((πΌβπ₯)(distβπ
)(πΌβπ¦)) < π) |
46 | 45 | a1d 25 |
. . . . . . . . 9
β’ ((((π
β NrmRing β§ (π₯ β π β§ π β β+)) β§
(1rβπ
) =
(0gβπ
))
β§ π¦ β π) β ((π₯(distβπ
)π¦) < π β ((πΌβπ₯)(distβπ
)(πΌβπ¦)) < π)) |
47 | 46 | ralrimiva 3146 |
. . . . . . . 8
β’ (((π
β NrmRing β§ (π₯ β π β§ π β β+)) β§
(1rβπ
) =
(0gβπ
))
β βπ¦ β
π ((π₯(distβπ
)π¦) < π β ((πΌβπ₯)(distβπ
)(πΌβπ¦)) < π)) |
48 | 47 | ralrimivw 3150 |
. . . . . . 7
β’ (((π
β NrmRing β§ (π₯ β π β§ π β β+)) β§
(1rβπ
) =
(0gβπ
))
β βπ β
β+ βπ¦ β π ((π₯(distβπ
)π¦) < π β ((πΌβπ₯)(distβπ
)(πΌβπ¦)) < π)) |
49 | | r19.2z 4493 |
. . . . . . 7
β’
((β+ β β
β§ βπ β β+ βπ¦ β π ((π₯(distβπ
)π¦) < π β ((πΌβπ₯)(distβπ
)(πΌβπ¦)) < π)) β βπ β β+ βπ¦ β π ((π₯(distβπ
)π¦) < π β ((πΌβπ₯)(distβπ
)(πΌβπ¦)) < π)) |
50 | 11, 48, 49 | sylancr 587 |
. . . . . 6
β’ (((π
β NrmRing β§ (π₯ β π β§ π β β+)) β§
(1rβπ
) =
(0gβπ
))
β βπ β
β+ βπ¦ β π ((π₯(distβπ
)π¦) < π β ((πΌβπ₯)(distβπ
)(πΌβπ¦)) < π)) |
51 | | eqid 2732 |
. . . . . . 7
β’
(normβπ
) =
(normβπ
) |
52 | | simpll 765 |
. . . . . . 7
β’ (((π
β NrmRing β§ (π₯ β π β§ π β β+)) β§
(1rβπ
)
β (0gβπ
)) β π
β NrmRing) |
53 | 1 | ad2antrr 724 |
. . . . . . . 8
β’ (((π
β NrmRing β§ (π₯ β π β§ π β β+)) β§
(1rβπ
)
β (0gβπ
)) β π
β Ring) |
54 | | simpr 485 |
. . . . . . . 8
β’ (((π
β NrmRing β§ (π₯ β π β§ π β β+)) β§
(1rβπ
)
β (0gβπ
)) β (1rβπ
) β
(0gβπ
)) |
55 | 19, 20 | isnzr 20285 |
. . . . . . . 8
β’ (π
β NzRing β (π
β Ring β§
(1rβπ
)
β (0gβπ
))) |
56 | 53, 54, 55 | sylanbrc 583 |
. . . . . . 7
β’ (((π
β NrmRing β§ (π₯ β π β§ π β β+)) β§
(1rβπ
)
β (0gβπ
)) β π
β NzRing) |
57 | | simplrl 775 |
. . . . . . 7
β’ (((π
β NrmRing β§ (π₯ β π β§ π β β+)) β§
(1rβπ
)
β (0gβπ
)) β π₯ β π) |
58 | | simplrr 776 |
. . . . . . 7
β’ (((π
β NrmRing β§ (π₯ β π β§ π β β+)) β§
(1rβπ
)
β (0gβπ
)) β π β β+) |
59 | | eqid 2732 |
. . . . . . 7
β’ (if(1
β€ (((normβπ
)βπ₯) Β· π), 1, (((normβπ
)βπ₯) Β· π)) Β· (((normβπ
)βπ₯) / 2)) = (if(1 β€ (((normβπ
)βπ₯) Β· π), 1, (((normβπ
)βπ₯) Β· π)) Β· (((normβπ
)βπ₯) / 2)) |
60 | 13, 2, 6, 51, 32, 52, 56, 57, 58, 59 | nrginvrcnlem 24199 |
. . . . . 6
β’ (((π
β NrmRing β§ (π₯ β π β§ π β β+)) β§
(1rβπ
)
β (0gβπ
)) β βπ β β+ βπ¦ β π ((π₯(distβπ
)π¦) < π β ((πΌβπ₯)(distβπ
)(πΌβπ¦)) < π)) |
61 | 50, 60 | pm2.61dane 3029 |
. . . . 5
β’ ((π
β NrmRing β§ (π₯ β π β§ π β β+)) β
βπ β
β+ βπ¦ β π ((π₯(distβπ
)π¦) < π β ((πΌβπ₯)(distβπ
)(πΌβπ¦)) < π)) |
62 | 15, 17 | ovresd 7570 |
. . . . . . . . 9
β’ (((π
β NrmRing β§ (π₯ β π β§ π β β+)) β§ π¦ β π) β (π₯((distβπ
) βΎ (π Γ π))π¦) = (π₯(distβπ
)π¦)) |
63 | 62 | breq1d 5157 |
. . . . . . . 8
β’ (((π
β NrmRing β§ (π₯ β π β§ π β β+)) β§ π¦ β π) β ((π₯((distβπ
) βΎ (π Γ π))π¦) < π β (π₯(distβπ
)π¦) < π )) |
64 | | simpl 483 |
. . . . . . . . . . . 12
β’ ((π₯ β π β§ π β β+) β π₯ β π) |
65 | | ffvelcdm 7080 |
. . . . . . . . . . . 12
β’ ((πΌ:πβΆπ β§ π₯ β π) β (πΌβπ₯) β π) |
66 | 9, 64, 65 | syl2an 596 |
. . . . . . . . . . 11
β’ ((π
β NrmRing β§ (π₯ β π β§ π β β+)) β (πΌβπ₯) β π) |
67 | 66 | adantr 481 |
. . . . . . . . . 10
β’ (((π
β NrmRing β§ (π₯ β π β§ π β β+)) β§ π¦ β π) β (πΌβπ₯) β π) |
68 | 67, 30 | ovresd 7570 |
. . . . . . . . 9
β’ (((π
β NrmRing β§ (π₯ β π β§ π β β+)) β§ π¦ β π) β ((πΌβπ₯)((distβπ
) βΎ (π Γ π))(πΌβπ¦)) = ((πΌβπ₯)(distβπ
)(πΌβπ¦))) |
69 | 68 | breq1d 5157 |
. . . . . . . 8
β’ (((π
β NrmRing β§ (π₯ β π β§ π β β+)) β§ π¦ β π) β (((πΌβπ₯)((distβπ
) βΎ (π Γ π))(πΌβπ¦)) < π β ((πΌβπ₯)(distβπ
)(πΌβπ¦)) < π)) |
70 | 63, 69 | imbi12d 344 |
. . . . . . 7
β’ (((π
β NrmRing β§ (π₯ β π β§ π β β+)) β§ π¦ β π) β (((π₯((distβπ
) βΎ (π Γ π))π¦) < π β ((πΌβπ₯)((distβπ
) βΎ (π Γ π))(πΌβπ¦)) < π) β ((π₯(distβπ
)π¦) < π β ((πΌβπ₯)(distβπ
)(πΌβπ¦)) < π))) |
71 | 70 | ralbidva 3175 |
. . . . . 6
β’ ((π
β NrmRing β§ (π₯ β π β§ π β β+)) β
(βπ¦ β π ((π₯((distβπ
) βΎ (π Γ π))π¦) < π β ((πΌβπ₯)((distβπ
) βΎ (π Γ π))(πΌβπ¦)) < π) β βπ¦ β π ((π₯(distβπ
)π¦) < π β ((πΌβπ₯)(distβπ
)(πΌβπ¦)) < π))) |
72 | 71 | rexbidv 3178 |
. . . . 5
β’ ((π
β NrmRing β§ (π₯ β π β§ π β β+)) β
(βπ β
β+ βπ¦ β π ((π₯((distβπ
) βΎ (π Γ π))π¦) < π β ((πΌβπ₯)((distβπ
) βΎ (π Γ π))(πΌβπ¦)) < π) β βπ β β+ βπ¦ β π ((π₯(distβπ
)π¦) < π β ((πΌβπ₯)(distβπ
)(πΌβπ¦)) < π))) |
73 | 61, 72 | mpbird 256 |
. . . 4
β’ ((π
β NrmRing β§ (π₯ β π β§ π β β+)) β
βπ β
β+ βπ¦ β π ((π₯((distβπ
) βΎ (π Γ π))π¦) < π β ((πΌβπ₯)((distβπ
) βΎ (π Γ π))(πΌβπ¦)) < π)) |
74 | 73 | ralrimivva 3200 |
. . 3
β’ (π
β NrmRing β
βπ₯ β π βπ β β+ βπ β β+
βπ¦ β π ((π₯((distβπ
) βΎ (π Γ π))π¦) < π β ((πΌβπ₯)((distβπ
) βΎ (π Γ π))(πΌβπ¦)) < π)) |
75 | | xpss12 5690 |
. . . . . . 7
β’ ((π β π β§ π β π) β (π Γ π) β (π Γ π)) |
76 | 14, 14, 75 | mp2an 690 |
. . . . . 6
β’ (π Γ π) β (π Γ π) |
77 | | resabs1 6009 |
. . . . . 6
β’ ((π Γ π) β (π Γ π) β (((distβπ
) βΎ (π Γ π)) βΎ (π Γ π)) = ((distβπ
) βΎ (π Γ π))) |
78 | 76, 77 | ax-mp 5 |
. . . . 5
β’
(((distβπ
)
βΎ (π Γ π)) βΎ (π Γ π)) = ((distβπ
) βΎ (π Γ π)) |
79 | | eqid 2732 |
. . . . . . . 8
β’
((distβπ
)
βΎ (π Γ π)) = ((distβπ
) βΎ (π Γ π)) |
80 | 13, 79 | xmsxmet 23953 |
. . . . . . 7
β’ (π
β βMetSp β
((distβπ
) βΎ
(π Γ π)) β
(βMetβπ)) |
81 | 24, 25, 26, 80 | 4syl 19 |
. . . . . 6
β’ (π
β NrmRing β
((distβπ
) βΎ
(π Γ π)) β
(βMetβπ)) |
82 | | xmetres2 23858 |
. . . . . 6
β’
((((distβπ
)
βΎ (π Γ π)) β
(βMetβπ) β§
π β π) β (((distβπ
) βΎ (π Γ π)) βΎ (π Γ π)) β (βMetβπ)) |
83 | 81, 14, 82 | sylancl 586 |
. . . . 5
β’ (π
β NrmRing β
(((distβπ
) βΎ
(π Γ π)) βΎ (π Γ π)) β (βMetβπ)) |
84 | 78, 83 | eqeltrrid 2838 |
. . . 4
β’ (π
β NrmRing β
((distβπ
) βΎ
(π Γ π)) β
(βMetβπ)) |
85 | | eqid 2732 |
. . . . 5
β’
(MetOpenβ((distβπ
) βΎ (π Γ π))) = (MetOpenβ((distβπ
) βΎ (π Γ π))) |
86 | 85, 85 | metcn 24043 |
. . . 4
β’
((((distβπ
)
βΎ (π Γ π)) β
(βMetβπ) β§
((distβπ
) βΎ
(π Γ π)) β
(βMetβπ))
β (πΌ β
((MetOpenβ((distβπ
) βΎ (π Γ π))) Cn (MetOpenβ((distβπ
) βΎ (π Γ π)))) β (πΌ:πβΆπ β§ βπ₯ β π βπ β β+ βπ β β+
βπ¦ β π ((π₯((distβπ
) βΎ (π Γ π))π¦) < π β ((πΌβπ₯)((distβπ
) βΎ (π Γ π))(πΌβπ¦)) < π)))) |
87 | 84, 84, 86 | syl2anc 584 |
. . 3
β’ (π
β NrmRing β (πΌ β
((MetOpenβ((distβπ
) βΎ (π Γ π))) Cn (MetOpenβ((distβπ
) βΎ (π Γ π)))) β (πΌ:πβΆπ β§ βπ₯ β π βπ β β+ βπ β β+
βπ¦ β π ((π₯((distβπ
) βΎ (π Γ π))π¦) < π β ((πΌβπ₯)((distβπ
) βΎ (π Γ π))(πΌβπ¦)) < π)))) |
88 | 9, 74, 87 | mpbir2and 711 |
. 2
β’ (π
β NrmRing β πΌ β
((MetOpenβ((distβπ
) βΎ (π Γ π))) Cn (MetOpenβ((distβπ
) βΎ (π Γ π))))) |
89 | | nrginvrcn.j |
. . . . . . 7
β’ π½ = (TopOpenβπ
) |
90 | 89, 13, 79 | mstopn 23949 |
. . . . . 6
β’ (π
β MetSp β π½ =
(MetOpenβ((distβπ
) βΎ (π Γ π)))) |
91 | 24, 25, 90 | 3syl 18 |
. . . . 5
β’ (π
β NrmRing β π½ =
(MetOpenβ((distβπ
) βΎ (π Γ π)))) |
92 | 91 | oveq1d 7420 |
. . . 4
β’ (π
β NrmRing β (π½ βΎt π) =
((MetOpenβ((distβπ
) βΎ (π Γ π))) βΎt π)) |
93 | 78 | eqcomi 2741 |
. . . . . 6
β’
((distβπ
)
βΎ (π Γ π)) = (((distβπ
) βΎ (π Γ π)) βΎ (π Γ π)) |
94 | | eqid 2732 |
. . . . . 6
β’
(MetOpenβ((distβπ
) βΎ (π Γ π))) = (MetOpenβ((distβπ
) βΎ (π Γ π))) |
95 | 93, 94, 85 | metrest 24024 |
. . . . 5
β’
((((distβπ
)
βΎ (π Γ π)) β
(βMetβπ) β§
π β π) β ((MetOpenβ((distβπ
) βΎ (π Γ π))) βΎt π) = (MetOpenβ((distβπ
) βΎ (π Γ π)))) |
96 | 81, 14, 95 | sylancl 586 |
. . . 4
β’ (π
β NrmRing β
((MetOpenβ((distβπ
) βΎ (π Γ π))) βΎt π) = (MetOpenβ((distβπ
) βΎ (π Γ π)))) |
97 | 92, 96 | eqtrd 2772 |
. . 3
β’ (π
β NrmRing β (π½ βΎt π) =
(MetOpenβ((distβπ
) βΎ (π Γ π)))) |
98 | 97, 97 | oveq12d 7423 |
. 2
β’ (π
β NrmRing β ((π½ βΎt π) Cn (π½ βΎt π)) = ((MetOpenβ((distβπ
) βΎ (π Γ π))) Cn (MetOpenβ((distβπ
) βΎ (π Γ π))))) |
99 | 88, 98 | eleqtrrd 2836 |
1
β’ (π
β NrmRing β πΌ β ((π½ βΎt π) Cn (π½ βΎt π))) |