Step | Hyp | Ref
| Expression |
1 | | nrgring 24043 |
. . . 4
β’ (π
β NrmRing β π
β Ring) |
2 | | nrginvrcn.u |
. . . . 5
β’ π = (Unitβπ
) |
3 | | eqid 2733 |
. . . . 5
β’
((mulGrpβπ
)
βΎs π) =
((mulGrpβπ
)
βΎs π) |
4 | 2, 3 | unitgrp 20101 |
. . . 4
β’ (π
β Ring β
((mulGrpβπ
)
βΎs π)
β Grp) |
5 | 2, 3 | unitgrpbas 20100 |
. . . . 5
β’ π =
(Baseβ((mulGrpβπ
) βΎs π)) |
6 | | nrginvrcn.i |
. . . . . 6
β’ πΌ = (invrβπ
) |
7 | 2, 3, 6 | invrfval 20107 |
. . . . 5
β’ πΌ =
(invgβ((mulGrpβπ
) βΎs π)) |
8 | 5, 7 | grpinvf 18802 |
. . . 4
β’
(((mulGrpβπ
)
βΎs π)
β Grp β πΌ:πβΆπ) |
9 | 1, 4, 8 | 3syl 18 |
. . 3
β’ (π
β NrmRing β πΌ:πβΆπ) |
10 | | 1rp 12924 |
. . . . . . . 8
β’ 1 β
β+ |
11 | 10 | ne0ii 4298 |
. . . . . . 7
β’
β+ β β
|
12 | 1 | ad2antrr 725 |
. . . . . . . . . . . . . 14
β’ (((π
β NrmRing β§ (π₯ β π β§ π β β+)) β§ π¦ β π) β π
β Ring) |
13 | | nrginvrcn.x |
. . . . . . . . . . . . . . . 16
β’ π = (Baseβπ
) |
14 | 13, 2 | unitss 20094 |
. . . . . . . . . . . . . . 15
β’ π β π |
15 | | simplrl 776 |
. . . . . . . . . . . . . . 15
β’ (((π
β NrmRing β§ (π₯ β π β§ π β β+)) β§ π¦ β π) β π₯ β π) |
16 | 14, 15 | sselid 3943 |
. . . . . . . . . . . . . 14
β’ (((π
β NrmRing β§ (π₯ β π β§ π β β+)) β§ π¦ β π) β π₯ β π) |
17 | | simpr 486 |
. . . . . . . . . . . . . . 15
β’ (((π
β NrmRing β§ (π₯ β π β§ π β β+)) β§ π¦ β π) β π¦ β π) |
18 | 14, 17 | sselid 3943 |
. . . . . . . . . . . . . 14
β’ (((π
β NrmRing β§ (π₯ β π β§ π β β+)) β§ π¦ β π) β π¦ β π) |
19 | | eqid 2733 |
. . . . . . . . . . . . . . 15
β’
(1rβπ
) = (1rβπ
) |
20 | | eqid 2733 |
. . . . . . . . . . . . . . 15
β’
(0gβπ
) = (0gβπ
) |
21 | 13, 19, 20 | ring1eq0 20019 |
. . . . . . . . . . . . . 14
β’ ((π
β Ring β§ π₯ β π β§ π¦ β π) β ((1rβπ
) = (0gβπ
) β π₯ = π¦)) |
22 | 12, 16, 18, 21 | syl3anc 1372 |
. . . . . . . . . . . . 13
β’ (((π
β NrmRing β§ (π₯ β π β§ π β β+)) β§ π¦ β π) β ((1rβπ
) = (0gβπ
) β π₯ = π¦)) |
23 | | eqid 2733 |
. . . . . . . . . . . . . . . 16
β’ (πΌβπ¦) = (πΌβπ¦) |
24 | | nrgngp 24042 |
. . . . . . . . . . . . . . . . . . 19
β’ (π
β NrmRing β π
β NrmGrp) |
25 | | ngpms 23972 |
. . . . . . . . . . . . . . . . . . 19
β’ (π
β NrmGrp β π
β MetSp) |
26 | | msxms 23823 |
. . . . . . . . . . . . . . . . . . 19
β’ (π
β MetSp β π
β
βMetSp) |
27 | 24, 25, 26 | 3syl 18 |
. . . . . . . . . . . . . . . . . 18
β’ (π
β NrmRing β π
β
βMetSp) |
28 | 27 | ad2antrr 725 |
. . . . . . . . . . . . . . . . 17
β’ (((π
β NrmRing β§ (π₯ β π β§ π β β+)) β§ π¦ β π) β π
β βMetSp) |
29 | 9 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π
β NrmRing β§ (π₯ β π β§ π β β+)) β πΌ:πβΆπ) |
30 | 29 | ffvelcdmda 7036 |
. . . . . . . . . . . . . . . . . 18
β’ (((π
β NrmRing β§ (π₯ β π β§ π β β+)) β§ π¦ β π) β (πΌβπ¦) β π) |
31 | 14, 30 | sselid 3943 |
. . . . . . . . . . . . . . . . 17
β’ (((π
β NrmRing β§ (π₯ β π β§ π β β+)) β§ π¦ β π) β (πΌβπ¦) β π) |
32 | | eqid 2733 |
. . . . . . . . . . . . . . . . . 18
β’
(distβπ
) =
(distβπ
) |
33 | 13, 32 | xmseq0 23833 |
. . . . . . . . . . . . . . . . 17
β’ ((π
β βMetSp β§
(πΌβπ¦) β π β§ (πΌβπ¦) β π) β (((πΌβπ¦)(distβπ
)(πΌβπ¦)) = 0 β (πΌβπ¦) = (πΌβπ¦))) |
34 | 28, 31, 31, 33 | syl3anc 1372 |
. . . . . . . . . . . . . . . 16
β’ (((π
β NrmRing β§ (π₯ β π β§ π β β+)) β§ π¦ β π) β (((πΌβπ¦)(distβπ
)(πΌβπ¦)) = 0 β (πΌβπ¦) = (πΌβπ¦))) |
35 | 23, 34 | mpbiri 258 |
. . . . . . . . . . . . . . 15
β’ (((π
β NrmRing β§ (π₯ β π β§ π β β+)) β§ π¦ β π) β ((πΌβπ¦)(distβπ
)(πΌβπ¦)) = 0) |
36 | | simplrr 777 |
. . . . . . . . . . . . . . . 16
β’ (((π
β NrmRing β§ (π₯ β π β§ π β β+)) β§ π¦ β π) β π β β+) |
37 | 36 | rpgt0d 12965 |
. . . . . . . . . . . . . . 15
β’ (((π
β NrmRing β§ (π₯ β π β§ π β β+)) β§ π¦ β π) β 0 < π) |
38 | 35, 37 | eqbrtrd 5128 |
. . . . . . . . . . . . . 14
β’ (((π
β NrmRing β§ (π₯ β π β§ π β β+)) β§ π¦ β π) β ((πΌβπ¦)(distβπ
)(πΌβπ¦)) < π) |
39 | | fveq2 6843 |
. . . . . . . . . . . . . . . 16
β’ (π₯ = π¦ β (πΌβπ₯) = (πΌβπ¦)) |
40 | 39 | oveq1d 7373 |
. . . . . . . . . . . . . . 15
β’ (π₯ = π¦ β ((πΌβπ₯)(distβπ
)(πΌβπ¦)) = ((πΌβπ¦)(distβπ
)(πΌβπ¦))) |
41 | 40 | breq1d 5116 |
. . . . . . . . . . . . . 14
β’ (π₯ = π¦ β (((πΌβπ₯)(distβπ
)(πΌβπ¦)) < π β ((πΌβπ¦)(distβπ
)(πΌβπ¦)) < π)) |
42 | 38, 41 | syl5ibrcom 247 |
. . . . . . . . . . . . 13
β’ (((π
β NrmRing β§ (π₯ β π β§ π β β+)) β§ π¦ β π) β (π₯ = π¦ β ((πΌβπ₯)(distβπ
)(πΌβπ¦)) < π)) |
43 | 22, 42 | syld 47 |
. . . . . . . . . . . 12
β’ (((π
β NrmRing β§ (π₯ β π β§ π β β+)) β§ π¦ β π) β ((1rβπ
) = (0gβπ
) β ((πΌβπ₯)(distβπ
)(πΌβπ¦)) < π)) |
44 | 43 | imp 408 |
. . . . . . . . . . 11
β’ ((((π
β NrmRing β§ (π₯ β π β§ π β β+)) β§ π¦ β π) β§ (1rβπ
) = (0gβπ
)) β ((πΌβπ₯)(distβπ
)(πΌβπ¦)) < π) |
45 | 44 | an32s 651 |
. . . . . . . . . 10
β’ ((((π
β NrmRing β§ (π₯ β π β§ π β β+)) β§
(1rβπ
) =
(0gβπ
))
β§ π¦ β π) β ((πΌβπ₯)(distβπ
)(πΌβπ¦)) < π) |
46 | 45 | a1d 25 |
. . . . . . . . 9
β’ ((((π
β NrmRing β§ (π₯ β π β§ π β β+)) β§
(1rβπ
) =
(0gβπ
))
β§ π¦ β π) β ((π₯(distβπ
)π¦) < π β ((πΌβπ₯)(distβπ
)(πΌβπ¦)) < π)) |
47 | 46 | ralrimiva 3140 |
. . . . . . . 8
β’ (((π
β NrmRing β§ (π₯ β π β§ π β β+)) β§
(1rβπ
) =
(0gβπ
))
β βπ¦ β
π ((π₯(distβπ
)π¦) < π β ((πΌβπ₯)(distβπ
)(πΌβπ¦)) < π)) |
48 | 47 | ralrimivw 3144 |
. . . . . . 7
β’ (((π
β NrmRing β§ (π₯ β π β§ π β β+)) β§
(1rβπ
) =
(0gβπ
))
β βπ β
β+ βπ¦ β π ((π₯(distβπ
)π¦) < π β ((πΌβπ₯)(distβπ
)(πΌβπ¦)) < π)) |
49 | | r19.2z 4453 |
. . . . . . 7
β’
((β+ β β
β§ βπ β β+ βπ¦ β π ((π₯(distβπ
)π¦) < π β ((πΌβπ₯)(distβπ
)(πΌβπ¦)) < π)) β βπ β β+ βπ¦ β π ((π₯(distβπ
)π¦) < π β ((πΌβπ₯)(distβπ
)(πΌβπ¦)) < π)) |
50 | 11, 48, 49 | sylancr 588 |
. . . . . 6
β’ (((π
β NrmRing β§ (π₯ β π β§ π β β+)) β§
(1rβπ
) =
(0gβπ
))
β βπ β
β+ βπ¦ β π ((π₯(distβπ
)π¦) < π β ((πΌβπ₯)(distβπ
)(πΌβπ¦)) < π)) |
51 | | eqid 2733 |
. . . . . . 7
β’
(normβπ
) =
(normβπ
) |
52 | | simpll 766 |
. . . . . . 7
β’ (((π
β NrmRing β§ (π₯ β π β§ π β β+)) β§
(1rβπ
)
β (0gβπ
)) β π
β NrmRing) |
53 | 1 | ad2antrr 725 |
. . . . . . . 8
β’ (((π
β NrmRing β§ (π₯ β π β§ π β β+)) β§
(1rβπ
)
β (0gβπ
)) β π
β Ring) |
54 | | simpr 486 |
. . . . . . . 8
β’ (((π
β NrmRing β§ (π₯ β π β§ π β β+)) β§
(1rβπ
)
β (0gβπ
)) β (1rβπ
) β
(0gβπ
)) |
55 | 19, 20 | isnzr 20745 |
. . . . . . . 8
β’ (π
β NzRing β (π
β Ring β§
(1rβπ
)
β (0gβπ
))) |
56 | 53, 54, 55 | sylanbrc 584 |
. . . . . . 7
β’ (((π
β NrmRing β§ (π₯ β π β§ π β β+)) β§
(1rβπ
)
β (0gβπ
)) β π
β NzRing) |
57 | | simplrl 776 |
. . . . . . 7
β’ (((π
β NrmRing β§ (π₯ β π β§ π β β+)) β§
(1rβπ
)
β (0gβπ
)) β π₯ β π) |
58 | | simplrr 777 |
. . . . . . 7
β’ (((π
β NrmRing β§ (π₯ β π β§ π β β+)) β§
(1rβπ
)
β (0gβπ
)) β π β β+) |
59 | | eqid 2733 |
. . . . . . 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 24071 |
. . . . . 6
β’ (((π
β NrmRing β§ (π₯ β π β§ π β β+)) β§
(1rβπ
)
β (0gβπ
)) β βπ β β+ βπ¦ β π ((π₯(distβπ
)π¦) < π β ((πΌβπ₯)(distβπ
)(πΌβπ¦)) < π)) |
61 | 50, 60 | pm2.61dane 3029 |
. . . . 5
β’ ((π
β NrmRing β§ (π₯ β π β§ π β β+)) β
βπ β
β+ βπ¦ β π ((π₯(distβπ
)π¦) < π β ((πΌβπ₯)(distβπ
)(πΌβπ¦)) < π)) |
62 | 15, 17 | ovresd 7522 |
. . . . . . . . 9
β’ (((π
β NrmRing β§ (π₯ β π β§ π β β+)) β§ π¦ β π) β (π₯((distβπ
) βΎ (π Γ π))π¦) = (π₯(distβπ
)π¦)) |
63 | 62 | breq1d 5116 |
. . . . . . . 8
β’ (((π
β NrmRing β§ (π₯ β π β§ π β β+)) β§ π¦ β π) β ((π₯((distβπ
) βΎ (π Γ π))π¦) < π β (π₯(distβπ
)π¦) < π )) |
64 | | simpl 484 |
. . . . . . . . . . . 12
β’ ((π₯ β π β§ π β β+) β π₯ β π) |
65 | | ffvelcdm 7033 |
. . . . . . . . . . . 12
β’ ((πΌ:πβΆπ β§ π₯ β π) β (πΌβπ₯) β π) |
66 | 9, 64, 65 | syl2an 597 |
. . . . . . . . . . 11
β’ ((π
β NrmRing β§ (π₯ β π β§ π β β+)) β (πΌβπ₯) β π) |
67 | 66 | adantr 482 |
. . . . . . . . . 10
β’ (((π
β NrmRing β§ (π₯ β π β§ π β β+)) β§ π¦ β π) β (πΌβπ₯) β π) |
68 | 67, 30 | ovresd 7522 |
. . . . . . . . 9
β’ (((π
β NrmRing β§ (π₯ β π β§ π β β+)) β§ π¦ β π) β ((πΌβπ₯)((distβπ
) βΎ (π Γ π))(πΌβπ¦)) = ((πΌβπ₯)(distβπ
)(πΌβπ¦))) |
69 | 68 | breq1d 5116 |
. . . . . . . 8
β’ (((π
β NrmRing β§ (π₯ β π β§ π β β+)) β§ π¦ β π) β (((πΌβπ₯)((distβπ
) βΎ (π Γ π))(πΌβπ¦)) < π β ((πΌβπ₯)(distβπ
)(πΌβπ¦)) < π)) |
70 | 63, 69 | imbi12d 345 |
. . . . . . 7
β’ (((π
β NrmRing β§ (π₯ β π β§ π β β+)) β§ π¦ β π) β (((π₯((distβπ
) βΎ (π Γ π))π¦) < π β ((πΌβπ₯)((distβπ
) βΎ (π Γ π))(πΌβπ¦)) < π) β ((π₯(distβπ
)π¦) < π β ((πΌβπ₯)(distβπ
)(πΌβπ¦)) < π))) |
71 | 70 | ralbidva 3169 |
. . . . . 6
β’ ((π
β NrmRing β§ (π₯ β π β§ π β β+)) β
(βπ¦ β π ((π₯((distβπ
) βΎ (π Γ π))π¦) < π β ((πΌβπ₯)((distβπ
) βΎ (π Γ π))(πΌβπ¦)) < π) β βπ¦ β π ((π₯(distβπ
)π¦) < π β ((πΌβπ₯)(distβπ
)(πΌβπ¦)) < π))) |
72 | 71 | rexbidv 3172 |
. . . . 5
β’ ((π
β NrmRing β§ (π₯ β π β§ π β β+)) β
(βπ β
β+ βπ¦ β π ((π₯((distβπ
) βΎ (π Γ π))π¦) < π β ((πΌβπ₯)((distβπ
) βΎ (π Γ π))(πΌβπ¦)) < π) β βπ β β+ βπ¦ β π ((π₯(distβπ
)π¦) < π β ((πΌβπ₯)(distβπ
)(πΌβπ¦)) < π))) |
73 | 61, 72 | mpbird 257 |
. . . 4
β’ ((π
β NrmRing β§ (π₯ β π β§ π β β+)) β
βπ β
β+ βπ¦ β π ((π₯((distβπ
) βΎ (π Γ π))π¦) < π β ((πΌβπ₯)((distβπ
) βΎ (π Γ π))(πΌβπ¦)) < π)) |
74 | 73 | ralrimivva 3194 |
. . 3
β’ (π
β NrmRing β
βπ₯ β π βπ β β+ βπ β β+
βπ¦ β π ((π₯((distβπ
) βΎ (π Γ π))π¦) < π β ((πΌβπ₯)((distβπ
) βΎ (π Γ π))(πΌβπ¦)) < π)) |
75 | | xpss12 5649 |
. . . . . . 7
β’ ((π β π β§ π β π) β (π Γ π) β (π Γ π)) |
76 | 14, 14, 75 | mp2an 691 |
. . . . . 6
β’ (π Γ π) β (π Γ π) |
77 | | resabs1 5968 |
. . . . . 6
β’ ((π Γ π) β (π Γ π) β (((distβπ
) βΎ (π Γ π)) βΎ (π Γ π)) = ((distβπ
) βΎ (π Γ π))) |
78 | 76, 77 | ax-mp 5 |
. . . . 5
β’
(((distβπ
)
βΎ (π Γ π)) βΎ (π Γ π)) = ((distβπ
) βΎ (π Γ π)) |
79 | | eqid 2733 |
. . . . . . . 8
β’
((distβπ
)
βΎ (π Γ π)) = ((distβπ
) βΎ (π Γ π)) |
80 | 13, 79 | xmsxmet 23825 |
. . . . . . 7
β’ (π
β βMetSp β
((distβπ
) βΎ
(π Γ π)) β
(βMetβπ)) |
81 | 24, 25, 26, 80 | 4syl 19 |
. . . . . 6
β’ (π
β NrmRing β
((distβπ
) βΎ
(π Γ π)) β
(βMetβπ)) |
82 | | xmetres2 23730 |
. . . . . 6
β’
((((distβπ
)
βΎ (π Γ π)) β
(βMetβπ) β§
π β π) β (((distβπ
) βΎ (π Γ π)) βΎ (π Γ π)) β (βMetβπ)) |
83 | 81, 14, 82 | sylancl 587 |
. . . . 5
β’ (π
β NrmRing β
(((distβπ
) βΎ
(π Γ π)) βΎ (π Γ π)) β (βMetβπ)) |
84 | 78, 83 | eqeltrrid 2839 |
. . . 4
β’ (π
β NrmRing β
((distβπ
) βΎ
(π Γ π)) β
(βMetβπ)) |
85 | | eqid 2733 |
. . . . 5
β’
(MetOpenβ((distβπ
) βΎ (π Γ π))) = (MetOpenβ((distβπ
) βΎ (π Γ π))) |
86 | 85, 85 | metcn 23915 |
. . . 4
β’
((((distβπ
)
βΎ (π Γ π)) β
(βMetβπ) β§
((distβπ
) βΎ
(π Γ π)) β
(βMetβπ))
β (πΌ β
((MetOpenβ((distβπ
) βΎ (π Γ π))) Cn (MetOpenβ((distβπ
) βΎ (π Γ π)))) β (πΌ:πβΆπ β§ βπ₯ β π βπ β β+ βπ β β+
βπ¦ β π ((π₯((distβπ
) βΎ (π Γ π))π¦) < π β ((πΌβπ₯)((distβπ
) βΎ (π Γ π))(πΌβπ¦)) < π)))) |
87 | 84, 84, 86 | syl2anc 585 |
. . 3
β’ (π
β NrmRing β (πΌ β
((MetOpenβ((distβπ
) βΎ (π Γ π))) Cn (MetOpenβ((distβπ
) βΎ (π Γ π)))) β (πΌ:πβΆπ β§ βπ₯ β π βπ β β+ βπ β β+
βπ¦ β π ((π₯((distβπ
) βΎ (π Γ π))π¦) < π β ((πΌβπ₯)((distβπ
) βΎ (π Γ π))(πΌβπ¦)) < π)))) |
88 | 9, 74, 87 | mpbir2and 712 |
. 2
β’ (π
β NrmRing β πΌ β
((MetOpenβ((distβπ
) βΎ (π Γ π))) Cn (MetOpenβ((distβπ
) βΎ (π Γ π))))) |
89 | | nrginvrcn.j |
. . . . . . 7
β’ π½ = (TopOpenβπ
) |
90 | 89, 13, 79 | mstopn 23821 |
. . . . . 6
β’ (π
β MetSp β π½ =
(MetOpenβ((distβπ
) βΎ (π Γ π)))) |
91 | 24, 25, 90 | 3syl 18 |
. . . . 5
β’ (π
β NrmRing β π½ =
(MetOpenβ((distβπ
) βΎ (π Γ π)))) |
92 | 91 | oveq1d 7373 |
. . . 4
β’ (π
β NrmRing β (π½ βΎt π) =
((MetOpenβ((distβπ
) βΎ (π Γ π))) βΎt π)) |
93 | 78 | eqcomi 2742 |
. . . . . 6
β’
((distβπ
)
βΎ (π Γ π)) = (((distβπ
) βΎ (π Γ π)) βΎ (π Γ π)) |
94 | | eqid 2733 |
. . . . . 6
β’
(MetOpenβ((distβπ
) βΎ (π Γ π))) = (MetOpenβ((distβπ
) βΎ (π Γ π))) |
95 | 93, 94, 85 | metrest 23896 |
. . . . 5
β’
((((distβπ
)
βΎ (π Γ π)) β
(βMetβπ) β§
π β π) β ((MetOpenβ((distβπ
) βΎ (π Γ π))) βΎt π) = (MetOpenβ((distβπ
) βΎ (π Γ π)))) |
96 | 81, 14, 95 | sylancl 587 |
. . . 4
β’ (π
β NrmRing β
((MetOpenβ((distβπ
) βΎ (π Γ π))) βΎt π) = (MetOpenβ((distβπ
) βΎ (π Γ π)))) |
97 | 92, 96 | eqtrd 2773 |
. . 3
β’ (π
β NrmRing β (π½ βΎt π) =
(MetOpenβ((distβπ
) βΎ (π Γ π)))) |
98 | 97, 97 | oveq12d 7376 |
. 2
β’ (π
β NrmRing β ((π½ βΎt π) Cn (π½ βΎt π)) = ((MetOpenβ((distβπ
) βΎ (π Γ π))) Cn (MetOpenβ((distβπ
) βΎ (π Γ π))))) |
99 | 88, 98 | eleqtrrd 2837 |
1
β’ (π
β NrmRing β πΌ β ((π½ βΎt π) Cn (π½ βΎt π))) |