Step | Hyp | Ref
| Expression |
1 | | simpllr 774 |
. . . . 5
β’ ((((π β§ π β (Baseβπ
)) β§ π β π) β§ (1rβπ
) = ((π(.rβπ
)π)(+gβπ
)π)) β π β (Baseβπ
)) |
2 | | ovex 7426 |
. . . . . 6
β’ (π
~QG π) β V |
3 | 2 | ecelqsi 8750 |
. . . . 5
β’ (π β (Baseβπ
) β [π](π
~QG π) β ((Baseβπ
) / (π
~QG π))) |
4 | 1, 3 | syl 17 |
. . . 4
β’ ((((π β§ π β (Baseβπ
)) β§ π β π) β§ (1rβπ
) = ((π(.rβπ
)π)(+gβπ
)π)) β [π](π
~QG π) β ((Baseβπ
) / (π
~QG π))) |
5 | | qsdrng.q |
. . . . . . 7
β’ π = (π
/s (π
~QG π)) |
6 | 5 | a1i 11 |
. . . . . 6
β’ (π β π = (π
/s (π
~QG π))) |
7 | | eqid 2731 |
. . . . . . 7
β’
(Baseβπ
) =
(Baseβπ
) |
8 | 7 | a1i 11 |
. . . . . 6
β’ (π β (Baseβπ
) = (Baseβπ
)) |
9 | | ovexd 7428 |
. . . . . 6
β’ (π β (π
~QG π) β V) |
10 | | qsdrng.r |
. . . . . 6
β’ (π β π
β NzRing) |
11 | 6, 8, 9, 10 | qusbas 17473 |
. . . . 5
β’ (π β ((Baseβπ
) / (π
~QG π)) = (Baseβπ)) |
12 | 11 | ad3antrrr 728 |
. . . 4
β’ ((((π β§ π β (Baseβπ
)) β§ π β π) β§ (1rβπ
) = ((π(.rβπ
)π)(+gβπ
)π)) β ((Baseβπ
) / (π
~QG π)) = (Baseβπ)) |
13 | 4, 12 | eleqtrd 2834 |
. . 3
β’ ((((π β§ π β (Baseβπ
)) β§ π β π) β§ (1rβπ
) = ((π(.rβπ
)π)(+gβπ
)π)) β [π](π
~QG π) β (Baseβπ)) |
14 | | oveq1 7400 |
. . . . 5
β’ (π£ = [π](π
~QG π) β (π£(.rβπ)[π](π
~QG π)) = ([π](π
~QG π)(.rβπ)[π](π
~QG π))) |
15 | 14 | eqeq1d 2733 |
. . . 4
β’ (π£ = [π](π
~QG π) β ((π£(.rβπ)[π](π
~QG π)) = (1rβπ) β ([π](π
~QG π)(.rβπ)[π](π
~QG π)) = (1rβπ))) |
16 | 15 | adantl 482 |
. . 3
β’
(((((π β§ π β (Baseβπ
)) β§ π β π) β§ (1rβπ
) = ((π(.rβπ
)π)(+gβπ
)π)) β§ π£ = [π](π
~QG π)) β ((π£(.rβπ)[π](π
~QG π)) = (1rβπ) β ([π](π
~QG π)(.rβπ)[π](π
~QG π)) = (1rβπ))) |
17 | | eqid 2731 |
. . . . . 6
β’
(.rβπ
) = (.rβπ
) |
18 | | eqid 2731 |
. . . . . 6
β’
(.rβπ) = (.rβπ) |
19 | | nzrring 20245 |
. . . . . . . 8
β’ (π
β NzRing β π
β Ring) |
20 | 10, 19 | syl 17 |
. . . . . . 7
β’ (π β π
β Ring) |
21 | 20 | ad3antrrr 728 |
. . . . . 6
β’ ((((π β§ π β (Baseβπ
)) β§ π β π) β§ (1rβπ
) = ((π(.rβπ
)π)(+gβπ
)π)) β π
β Ring) |
22 | | qsdrngi.1 |
. . . . . . . . . 10
β’ (π β π β (MaxIdealβπ
)) |
23 | 7 | mxidlidl 32430 |
. . . . . . . . . 10
β’ ((π
β Ring β§ π β (MaxIdealβπ
)) β π β (LIdealβπ
)) |
24 | 20, 22, 23 | syl2anc 584 |
. . . . . . . . 9
β’ (π β π β (LIdealβπ
)) |
25 | | qsdrng.0 |
. . . . . . . . . . . 12
β’ π =
(opprβπ
) |
26 | 25 | opprring 20113 |
. . . . . . . . . . 11
β’ (π
β Ring β π β Ring) |
27 | 20, 26 | syl 17 |
. . . . . . . . . 10
β’ (π β π β Ring) |
28 | | qsdrngi.2 |
. . . . . . . . . 10
β’ (π β π β (MaxIdealβπ)) |
29 | | eqid 2731 |
. . . . . . . . . . 11
β’
(Baseβπ) =
(Baseβπ) |
30 | 29 | mxidlidl 32430 |
. . . . . . . . . 10
β’ ((π β Ring β§ π β (MaxIdealβπ)) β π β (LIdealβπ)) |
31 | 27, 28, 30 | syl2anc 584 |
. . . . . . . . 9
β’ (π β π β (LIdealβπ)) |
32 | 24, 31 | elind 4190 |
. . . . . . . 8
β’ (π β π β ((LIdealβπ
) β© (LIdealβπ))) |
33 | | eqid 2731 |
. . . . . . . . 9
β’
(LIdealβπ
) =
(LIdealβπ
) |
34 | | eqid 2731 |
. . . . . . . . 9
β’
(LIdealβπ) =
(LIdealβπ) |
35 | | eqid 2731 |
. . . . . . . . 9
β’
(2Idealβπ
) =
(2Idealβπ
) |
36 | 33, 25, 34, 35 | 2idlval 20804 |
. . . . . . . 8
β’
(2Idealβπ
) =
((LIdealβπ
) β©
(LIdealβπ)) |
37 | 32, 36 | eleqtrrdi 2843 |
. . . . . . 7
β’ (π β π β (2Idealβπ
)) |
38 | 37 | ad3antrrr 728 |
. . . . . 6
β’ ((((π β§ π β (Baseβπ
)) β§ π β π) β§ (1rβπ
) = ((π(.rβπ
)π)(+gβπ
)π)) β π β (2Idealβπ
)) |
39 | | qsdrngilem.1 |
. . . . . . 7
β’ (π β π β (Baseβπ
)) |
40 | 39 | ad3antrrr 728 |
. . . . . 6
β’ ((((π β§ π β (Baseβπ
)) β§ π β π) β§ (1rβπ
) = ((π(.rβπ
)π)(+gβπ
)π)) β π β (Baseβπ
)) |
41 | 5, 7, 17, 18, 21, 38, 1, 40 | qusmul2 20811 |
. . . . 5
β’ ((((π β§ π β (Baseβπ
)) β§ π β π) β§ (1rβπ
) = ((π(.rβπ
)π)(+gβπ
)π)) β ([π](π
~QG π)(.rβπ)[π](π
~QG π)) = [(π(.rβπ
)π)](π
~QG π)) |
42 | | lidlnsg 32415 |
. . . . . . . . 9
β’ ((π
β Ring β§ π β (LIdealβπ
)) β π β (NrmSGrpβπ
)) |
43 | 20, 24, 42 | syl2anc 584 |
. . . . . . . 8
β’ (π β π β (NrmSGrpβπ
)) |
44 | | nsgsubg 19010 |
. . . . . . . 8
β’ (π β (NrmSGrpβπ
) β π β (SubGrpβπ
)) |
45 | | eqid 2731 |
. . . . . . . . 9
β’ (π
~QG π) = (π
~QG π) |
46 | 7, 45 | eqger 19030 |
. . . . . . . 8
β’ (π β (SubGrpβπ
) β (π
~QG π) Er (Baseβπ
)) |
47 | 43, 44, 46 | 3syl 18 |
. . . . . . 7
β’ (π β (π
~QG π) Er (Baseβπ
)) |
48 | 47 | ad3antrrr 728 |
. . . . . 6
β’ ((((π β§ π β (Baseβπ
)) β§ π β π) β§ (1rβπ
) = ((π(.rβπ
)π)(+gβπ
)π)) β (π
~QG π) Er (Baseβπ
)) |
49 | 7, 33 | lidlss 20781 |
. . . . . . . . 9
β’ (π β (LIdealβπ
) β π β (Baseβπ
)) |
50 | 24, 49 | syl 17 |
. . . . . . . 8
β’ (π β π β (Baseβπ
)) |
51 | 50 | ad3antrrr 728 |
. . . . . . 7
β’ ((((π β§ π β (Baseβπ
)) β§ π β π) β§ (1rβπ
) = ((π(.rβπ
)π)(+gβπ
)π)) β π β (Baseβπ
)) |
52 | 7, 17, 21, 1, 40 | ringcld 20037 |
. . . . . . 7
β’ ((((π β§ π β (Baseβπ
)) β§ π β π) β§ (1rβπ
) = ((π(.rβπ
)π)(+gβπ
)π)) β (π(.rβπ
)π) β (Baseβπ
)) |
53 | | eqid 2731 |
. . . . . . . . . 10
β’
(1rβπ
) = (1rβπ
) |
54 | 7, 53 | ringidcl 20040 |
. . . . . . . . 9
β’ (π
β Ring β
(1rβπ
)
β (Baseβπ
)) |
55 | 20, 54 | syl 17 |
. . . . . . . 8
β’ (π β (1rβπ
) β (Baseβπ
)) |
56 | 55 | ad3antrrr 728 |
. . . . . . 7
β’ ((((π β§ π β (Baseβπ
)) β§ π β π) β§ (1rβπ
) = ((π(.rβπ
)π)(+gβπ
)π)) β (1rβπ
) β (Baseβπ
)) |
57 | | simpr 485 |
. . . . . . . . . 10
β’ ((((π β§ π β (Baseβπ
)) β§ π β π) β§ (1rβπ
) = ((π(.rβπ
)π)(+gβπ
)π)) β (1rβπ
) = ((π(.rβπ
)π)(+gβπ
)π)) |
58 | 57 | oveq2d 7409 |
. . . . . . . . 9
β’ ((((π β§ π β (Baseβπ
)) β§ π β π) β§ (1rβπ
) = ((π(.rβπ
)π)(+gβπ
)π)) β (((invgβπ
)β(π(.rβπ
)π))(+gβπ
)(1rβπ
)) = (((invgβπ
)β(π(.rβπ
)π))(+gβπ
)((π(.rβπ
)π)(+gβπ
)π))) |
59 | | eqid 2731 |
. . . . . . . . . . . 12
β’
(+gβπ
) = (+gβπ
) |
60 | | eqid 2731 |
. . . . . . . . . . . 12
β’
(0gβπ
) = (0gβπ
) |
61 | | eqid 2731 |
. . . . . . . . . . . 12
β’
(invgβπ
) = (invgβπ
) |
62 | 20 | ringgrpd 20023 |
. . . . . . . . . . . . 13
β’ (π β π
β Grp) |
63 | 62 | ad3antrrr 728 |
. . . . . . . . . . . 12
β’ ((((π β§ π β (Baseβπ
)) β§ π β π) β§ (1rβπ
) = ((π(.rβπ
)π)(+gβπ
)π)) β π
β Grp) |
64 | 7, 59, 60, 61, 63, 52 | grplinvd 18854 |
. . . . . . . . . . 11
β’ ((((π β§ π β (Baseβπ
)) β§ π β π) β§ (1rβπ
) = ((π(.rβπ
)π)(+gβπ
)π)) β (((invgβπ
)β(π(.rβπ
)π))(+gβπ
)(π(.rβπ
)π)) = (0gβπ
)) |
65 | 64 | oveq1d 7408 |
. . . . . . . . . 10
β’ ((((π β§ π β (Baseβπ
)) β§ π β π) β§ (1rβπ
) = ((π(.rβπ
)π)(+gβπ
)π)) β ((((invgβπ
)β(π(.rβπ
)π))(+gβπ
)(π(.rβπ
)π))(+gβπ
)π) = ((0gβπ
)(+gβπ
)π)) |
66 | 7, 61, 63, 52 | grpinvcld 18848 |
. . . . . . . . . . 11
β’ ((((π β§ π β (Baseβπ
)) β§ π β π) β§ (1rβπ
) = ((π(.rβπ
)π)(+gβπ
)π)) β ((invgβπ
)β(π(.rβπ
)π)) β (Baseβπ
)) |
67 | | simplr 767 |
. . . . . . . . . . . 12
β’ ((((π β§ π β (Baseβπ
)) β§ π β π) β§ (1rβπ
) = ((π(.rβπ
)π)(+gβπ
)π)) β π β π) |
68 | 51, 67 | sseldd 3979 |
. . . . . . . . . . 11
β’ ((((π β§ π β (Baseβπ
)) β§ π β π) β§ (1rβπ
) = ((π(.rβπ
)π)(+gβπ
)π)) β π β (Baseβπ
)) |
69 | 7, 59, 63, 66, 52, 68 | grpassd 18806 |
. . . . . . . . . 10
β’ ((((π β§ π β (Baseβπ
)) β§ π β π) β§ (1rβπ
) = ((π(.rβπ
)π)(+gβπ
)π)) β ((((invgβπ
)β(π(.rβπ
)π))(+gβπ
)(π(.rβπ
)π))(+gβπ
)π) = (((invgβπ
)β(π(.rβπ
)π))(+gβπ
)((π(.rβπ
)π)(+gβπ
)π))) |
70 | 7, 59, 60, 63, 68 | grplidd 18829 |
. . . . . . . . . 10
β’ ((((π β§ π β (Baseβπ
)) β§ π β π) β§ (1rβπ
) = ((π(.rβπ
)π)(+gβπ
)π)) β ((0gβπ
)(+gβπ
)π) = π) |
71 | 65, 69, 70 | 3eqtr3d 2779 |
. . . . . . . . 9
β’ ((((π β§ π β (Baseβπ
)) β§ π β π) β§ (1rβπ
) = ((π(.rβπ
)π)(+gβπ
)π)) β (((invgβπ
)β(π(.rβπ
)π))(+gβπ
)((π(.rβπ
)π)(+gβπ
)π)) = π) |
72 | 58, 71 | eqtrd 2771 |
. . . . . . . 8
β’ ((((π β§ π β (Baseβπ
)) β§ π β π) β§ (1rβπ
) = ((π(.rβπ
)π)(+gβπ
)π)) β (((invgβπ
)β(π(.rβπ
)π))(+gβπ
)(1rβπ
)) = π) |
73 | 72, 67 | eqeltrd 2832 |
. . . . . . 7
β’ ((((π β§ π β (Baseβπ
)) β§ π β π) β§ (1rβπ
) = ((π(.rβπ
)π)(+gβπ
)π)) β (((invgβπ
)β(π(.rβπ
)π))(+gβπ
)(1rβπ
)) β π) |
74 | 7, 61, 59, 45 | eqgval 19029 |
. . . . . . . 8
β’ ((π
β Ring β§ π β (Baseβπ
)) β ((π(.rβπ
)π)(π
~QG π)(1rβπ
) β ((π(.rβπ
)π) β (Baseβπ
) β§ (1rβπ
) β (Baseβπ
) β§
(((invgβπ
)β(π(.rβπ
)π))(+gβπ
)(1rβπ
)) β π))) |
75 | 74 | biimpar 478 |
. . . . . . 7
β’ (((π
β Ring β§ π β (Baseβπ
)) β§ ((π(.rβπ
)π) β (Baseβπ
) β§ (1rβπ
) β (Baseβπ
) β§
(((invgβπ
)β(π(.rβπ
)π))(+gβπ
)(1rβπ
)) β π)) β (π(.rβπ
)π)(π
~QG π)(1rβπ
)) |
76 | 21, 51, 52, 56, 73, 75 | syl23anc 1377 |
. . . . . 6
β’ ((((π β§ π β (Baseβπ
)) β§ π β π) β§ (1rβπ
) = ((π(.rβπ
)π)(+gβπ
)π)) β (π(.rβπ
)π)(π
~QG π)(1rβπ
)) |
77 | 48, 76 | erthi 8737 |
. . . . 5
β’ ((((π β§ π β (Baseβπ
)) β§ π β π) β§ (1rβπ
) = ((π(.rβπ
)π)(+gβπ
)π)) β [(π(.rβπ
)π)](π
~QG π) = [(1rβπ
)](π
~QG π)) |
78 | 41, 77 | eqtrd 2771 |
. . . 4
β’ ((((π β§ π β (Baseβπ
)) β§ π β π) β§ (1rβπ
) = ((π(.rβπ
)π)(+gβπ
)π)) β ([π](π
~QG π)(.rβπ)[π](π
~QG π)) = [(1rβπ
)](π
~QG π)) |
79 | 5, 35, 53 | qus1 20808 |
. . . . . 6
β’ ((π
β Ring β§ π β (2Idealβπ
)) β (π β Ring β§
[(1rβπ
)](π
~QG π) = (1rβπ))) |
80 | 79 | simprd 496 |
. . . . 5
β’ ((π
β Ring β§ π β (2Idealβπ
)) β
[(1rβπ
)](π
~QG π) = (1rβπ)) |
81 | 21, 38, 80 | syl2anc 584 |
. . . 4
β’ ((((π β§ π β (Baseβπ
)) β§ π β π) β§ (1rβπ
) = ((π(.rβπ
)π)(+gβπ
)π)) β [(1rβπ
)](π
~QG π) = (1rβπ)) |
82 | 78, 81 | eqtrd 2771 |
. . 3
β’ ((((π β§ π β (Baseβπ
)) β§ π β π) β§ (1rβπ
) = ((π(.rβπ
)π)(+gβπ
)π)) β ([π](π
~QG π)(.rβπ)[π](π
~QG π)) = (1rβπ)) |
83 | 13, 16, 82 | rspcedvd 3611 |
. 2
β’ ((((π β§ π β (Baseβπ
)) β§ π β π) β§ (1rβπ
) = ((π(.rβπ
)π)(+gβπ
)π)) β βπ£ β (Baseβπ)(π£(.rβπ)[π](π
~QG π)) = (1rβπ)) |
84 | 39 | snssd 4805 |
. . . . . . 7
β’ (π β {π} β (Baseβπ
)) |
85 | 50, 84 | unssd 4182 |
. . . . . 6
β’ (π β (π βͺ {π}) β (Baseβπ
)) |
86 | | eqid 2731 |
. . . . . . 7
β’
(RSpanβπ
) =
(RSpanβπ
) |
87 | 86, 7, 33 | rspcl 20793 |
. . . . . 6
β’ ((π
β Ring β§ (π βͺ {π}) β (Baseβπ
)) β ((RSpanβπ
)β(π βͺ {π})) β (LIdealβπ
)) |
88 | 20, 85, 87 | syl2anc 584 |
. . . . 5
β’ (π β ((RSpanβπ
)β(π βͺ {π})) β (LIdealβπ
)) |
89 | 86, 7 | rspssid 20794 |
. . . . . . 7
β’ ((π
β Ring β§ (π βͺ {π}) β (Baseβπ
)) β (π βͺ {π}) β ((RSpanβπ
)β(π βͺ {π}))) |
90 | 20, 85, 89 | syl2anc 584 |
. . . . . 6
β’ (π β (π βͺ {π}) β ((RSpanβπ
)β(π βͺ {π}))) |
91 | 90 | unssad 4183 |
. . . . 5
β’ (π β π β ((RSpanβπ
)β(π βͺ {π}))) |
92 | 90 | unssbd 4184 |
. . . . . . 7
β’ (π β {π} β ((RSpanβπ
)β(π βͺ {π}))) |
93 | | snssg 4780 |
. . . . . . . 8
β’ (π β (Baseβπ
) β (π β ((RSpanβπ
)β(π βͺ {π})) β {π} β ((RSpanβπ
)β(π βͺ {π})))) |
94 | 93 | biimpar 478 |
. . . . . . 7
β’ ((π β (Baseβπ
) β§ {π} β ((RSpanβπ
)β(π βͺ {π}))) β π β ((RSpanβπ
)β(π βͺ {π}))) |
95 | 39, 92, 94 | syl2anc 584 |
. . . . . 6
β’ (π β π β ((RSpanβπ
)β(π βͺ {π}))) |
96 | | qsdrngilem.2 |
. . . . . 6
β’ (π β Β¬ π β π) |
97 | 95, 96 | eldifd 3955 |
. . . . 5
β’ (π β π β (((RSpanβπ
)β(π βͺ {π})) β π)) |
98 | 7, 20, 22, 88, 91, 97 | mxidlmaxv 32435 |
. . . 4
β’ (π β ((RSpanβπ
)β(π βͺ {π})) = (Baseβπ
)) |
99 | 55, 98 | eleqtrrd 2835 |
. . 3
β’ (π β (1rβπ
) β ((RSpanβπ
)β(π βͺ {π}))) |
100 | 39, 96 | eldifd 3955 |
. . . 4
β’ (π β π β ((Baseβπ
) β π)) |
101 | 86, 7, 60, 17, 20, 59, 24, 100 | elrspunsn 32398 |
. . 3
β’ (π β
((1rβπ
)
β ((RSpanβπ
)β(π βͺ {π})) β βπ β (Baseβπ
)βπ β π (1rβπ
) = ((π(.rβπ
)π)(+gβπ
)π))) |
102 | 99, 101 | mpbid 231 |
. 2
β’ (π β βπ β (Baseβπ
)βπ β π (1rβπ
) = ((π(.rβπ
)π)(+gβπ
)π)) |
103 | 83, 102 | r19.29vva 3212 |
1
β’ (π β βπ£ β (Baseβπ)(π£(.rβπ)[π](π
~QG π)) = (1rβπ)) |