Step | Hyp | Ref
| Expression |
1 | | eqcom 2739 |
. 2
β’ ((πΏβπ΄) = (πΏβπ΅) β (πΏβπ΅) = (πΏβπ΄)) |
2 | | eqid 2732 |
. . . . . 6
β’
(RSpanββ€ring) =
(RSpanββ€ring) |
3 | | eqid 2732 |
. . . . . 6
β’
(β€ring ~QG
((RSpanββ€ring)β{π})) = (β€ring
~QG ((RSpanββ€ring)β{π})) |
4 | | zncyg.y |
. . . . . 6
β’ π =
(β€/nβ€βπ) |
5 | | zndvds.2 |
. . . . . 6
β’ πΏ = (β€RHomβπ) |
6 | 2, 3, 4, 5 | znzrhval 21093 |
. . . . 5
β’ ((π β β0
β§ π΅ β β€)
β (πΏβπ΅) = [π΅](β€ring
~QG ((RSpanββ€ring)β{π}))) |
7 | 6 | 3adant2 1131 |
. . . 4
β’ ((π β β0
β§ π΄ β β€
β§ π΅ β β€)
β (πΏβπ΅) = [π΅](β€ring
~QG ((RSpanββ€ring)β{π}))) |
8 | 2, 3, 4, 5 | znzrhval 21093 |
. . . . 5
β’ ((π β β0
β§ π΄ β β€)
β (πΏβπ΄) = [π΄](β€ring
~QG ((RSpanββ€ring)β{π}))) |
9 | 8 | 3adant3 1132 |
. . . 4
β’ ((π β β0
β§ π΄ β β€
β§ π΅ β β€)
β (πΏβπ΄) = [π΄](β€ring
~QG ((RSpanββ€ring)β{π}))) |
10 | 7, 9 | eqeq12d 2748 |
. . 3
β’ ((π β β0
β§ π΄ β β€
β§ π΅ β β€)
β ((πΏβπ΅) = (πΏβπ΄) β [π΅](β€ring
~QG ((RSpanββ€ring)β{π})) = [π΄](β€ring
~QG ((RSpanββ€ring)β{π})))) |
11 | | zringring 21012 |
. . . . . 6
β’
β€ring β Ring |
12 | | nn0z 12579 |
. . . . . . . . 9
β’ (π β β0
β π β
β€) |
13 | 12 | 3ad2ant1 1133 |
. . . . . . . 8
β’ ((π β β0
β§ π΄ β β€
β§ π΅ β β€)
β π β
β€) |
14 | 13 | snssd 4811 |
. . . . . . 7
β’ ((π β β0
β§ π΄ β β€
β§ π΅ β β€)
β {π} β
β€) |
15 | | zringbas 21015 |
. . . . . . . 8
β’ β€ =
(Baseββ€ring) |
16 | | eqid 2732 |
. . . . . . . 8
β’
(LIdealββ€ring) =
(LIdealββ€ring) |
17 | 2, 15, 16 | rspcl 20839 |
. . . . . . 7
β’
((β€ring β Ring β§ {π} β β€) β
((RSpanββ€ring)β{π}) β
(LIdealββ€ring)) |
18 | 11, 14, 17 | sylancr 587 |
. . . . . 6
β’ ((π β β0
β§ π΄ β β€
β§ π΅ β β€)
β ((RSpanββ€ring)β{π}) β
(LIdealββ€ring)) |
19 | 16 | lidlsubg 20830 |
. . . . . 6
β’
((β€ring β Ring β§
((RSpanββ€ring)β{π}) β
(LIdealββ€ring)) β
((RSpanββ€ring)β{π}) β
(SubGrpββ€ring)) |
20 | 11, 18, 19 | sylancr 587 |
. . . . 5
β’ ((π β β0
β§ π΄ β β€
β§ π΅ β β€)
β ((RSpanββ€ring)β{π}) β
(SubGrpββ€ring)) |
21 | 15, 3 | eqger 19052 |
. . . . 5
β’
(((RSpanββ€ring)β{π}) β
(SubGrpββ€ring) β (β€ring
~QG ((RSpanββ€ring)β{π})) Er β€) |
22 | 20, 21 | syl 17 |
. . . 4
β’ ((π β β0
β§ π΄ β β€
β§ π΅ β β€)
β (β€ring ~QG
((RSpanββ€ring)β{π})) Er β€) |
23 | | simp3 1138 |
. . . 4
β’ ((π β β0
β§ π΄ β β€
β§ π΅ β β€)
β π΅ β
β€) |
24 | 22, 23 | erth 8748 |
. . 3
β’ ((π β β0
β§ π΄ β β€
β§ π΅ β β€)
β (π΅(β€ring
~QG ((RSpanββ€ring)β{π}))π΄ β [π΅](β€ring
~QG ((RSpanββ€ring)β{π})) = [π΄](β€ring
~QG ((RSpanββ€ring)β{π})))) |
25 | | zringabl 21013 |
. . . . 5
β’
β€ring β Abel |
26 | 15, 16 | lidlss 20825 |
. . . . . 6
β’
(((RSpanββ€ring)β{π}) β
(LIdealββ€ring) β
((RSpanββ€ring)β{π}) β β€) |
27 | 18, 26 | syl 17 |
. . . . 5
β’ ((π β β0
β§ π΄ β β€
β§ π΅ β β€)
β ((RSpanββ€ring)β{π}) β β€) |
28 | | eqid 2732 |
. . . . . 6
β’
(-gββ€ring) =
(-gββ€ring) |
29 | 15, 28, 3 | eqgabl 19696 |
. . . . 5
β’
((β€ring β Abel β§
((RSpanββ€ring)β{π}) β β€) β (π΅(β€ring
~QG ((RSpanββ€ring)β{π}))π΄ β (π΅ β β€ β§ π΄ β β€ β§ (π΄(-gββ€ring)π΅) β
((RSpanββ€ring)β{π})))) |
30 | 25, 27, 29 | sylancr 587 |
. . . 4
β’ ((π β β0
β§ π΄ β β€
β§ π΅ β β€)
β (π΅(β€ring
~QG ((RSpanββ€ring)β{π}))π΄ β (π΅ β β€ β§ π΄ β β€ β§ (π΄(-gββ€ring)π΅) β
((RSpanββ€ring)β{π})))) |
31 | | simp2 1137 |
. . . . . . 7
β’ ((π β β0
β§ π΄ β β€
β§ π΅ β β€)
β π΄ β
β€) |
32 | 23, 31 | jca 512 |
. . . . . 6
β’ ((π β β0
β§ π΄ β β€
β§ π΅ β β€)
β (π΅ β β€
β§ π΄ β
β€)) |
33 | 32 | biantrurd 533 |
. . . . 5
β’ ((π β β0
β§ π΄ β β€
β§ π΅ β β€)
β ((π΄(-gββ€ring)π΅) β
((RSpanββ€ring)β{π}) β ((π΅ β β€ β§ π΄ β β€) β§ (π΄(-gββ€ring)π΅) β
((RSpanββ€ring)β{π})))) |
34 | | df-3an 1089 |
. . . . 5
β’ ((π΅ β β€ β§ π΄ β β€ β§ (π΄(-gββ€ring)π΅) β
((RSpanββ€ring)β{π})) β ((π΅ β β€ β§ π΄ β β€) β§ (π΄(-gββ€ring)π΅) β
((RSpanββ€ring)β{π}))) |
35 | 33, 34 | bitr4di 288 |
. . . 4
β’ ((π β β0
β§ π΄ β β€
β§ π΅ β β€)
β ((π΄(-gββ€ring)π΅) β
((RSpanββ€ring)β{π}) β (π΅ β β€ β§ π΄ β β€ β§ (π΄(-gββ€ring)π΅) β
((RSpanββ€ring)β{π})))) |
36 | | zsubrg 20990 |
. . . . . . . . 9
β’ β€
β (SubRingββfld) |
37 | | subrgsubg 20361 |
. . . . . . . . 9
β’ (β€
β (SubRingββfld) β β€ β
(SubGrpββfld)) |
38 | 36, 37 | mp1i 13 |
. . . . . . . 8
β’ ((π β β0
β§ π΄ β β€
β§ π΅ β β€)
β β€ β (SubGrpββfld)) |
39 | | cnfldsub 20965 |
. . . . . . . . 9
β’ β
= (-gββfld) |
40 | | df-zring 21010 |
. . . . . . . . 9
β’
β€ring = (βfld βΎs
β€) |
41 | 39, 40, 28 | subgsub 19012 |
. . . . . . . 8
β’ ((β€
β (SubGrpββfld) β§ π΄ β β€ β§ π΅ β β€) β (π΄ β π΅) = (π΄(-gββ€ring)π΅)) |
42 | 38, 41 | syld3an1 1410 |
. . . . . . 7
β’ ((π β β0
β§ π΄ β β€
β§ π΅ β β€)
β (π΄ β π΅) = (π΄(-gββ€ring)π΅)) |
43 | 42 | eqcomd 2738 |
. . . . . 6
β’ ((π β β0
β§ π΄ β β€
β§ π΅ β β€)
β (π΄(-gββ€ring)π΅) = (π΄ β π΅)) |
44 | | dvdsrzring 21022 |
. . . . . . . 8
β’ β₯
= (β₯rββ€ring) |
45 | 15, 2, 44 | rspsn 20884 |
. . . . . . 7
β’
((β€ring β Ring β§ π β β€) β
((RSpanββ€ring)β{π}) = {π₯ β£ π β₯ π₯}) |
46 | 11, 13, 45 | sylancr 587 |
. . . . . 6
β’ ((π β β0
β§ π΄ β β€
β§ π΅ β β€)
β ((RSpanββ€ring)β{π}) = {π₯ β£ π β₯ π₯}) |
47 | 43, 46 | eleq12d 2827 |
. . . . 5
β’ ((π β β0
β§ π΄ β β€
β§ π΅ β β€)
β ((π΄(-gββ€ring)π΅) β
((RSpanββ€ring)β{π}) β (π΄ β π΅) β {π₯ β£ π β₯ π₯})) |
48 | | ovex 7438 |
. . . . . 6
β’ (π΄ β π΅) β V |
49 | | breq2 5151 |
. . . . . 6
β’ (π₯ = (π΄ β π΅) β (π β₯ π₯ β π β₯ (π΄ β π΅))) |
50 | 48, 49 | elab 3667 |
. . . . 5
β’ ((π΄ β π΅) β {π₯ β£ π β₯ π₯} β π β₯ (π΄ β π΅)) |
51 | 47, 50 | bitrdi 286 |
. . . 4
β’ ((π β β0
β§ π΄ β β€
β§ π΅ β β€)
β ((π΄(-gββ€ring)π΅) β
((RSpanββ€ring)β{π}) β π β₯ (π΄ β π΅))) |
52 | 30, 35, 51 | 3bitr2d 306 |
. . 3
β’ ((π β β0
β§ π΄ β β€
β§ π΅ β β€)
β (π΅(β€ring
~QG ((RSpanββ€ring)β{π}))π΄ β π β₯ (π΄ β π΅))) |
53 | 10, 24, 52 | 3bitr2d 306 |
. 2
β’ ((π β β0
β§ π΄ β β€
β§ π΅ β β€)
β ((πΏβπ΅) = (πΏβπ΄) β π β₯ (π΄ β π΅))) |
54 | 1, 53 | bitrid 282 |
1
β’ ((π β β0
β§ π΄ β β€
β§ π΅ β β€)
β ((πΏβπ΄) = (πΏβπ΅) β π β₯ (π΄ β π΅))) |