Step | Hyp | Ref
| Expression |
1 | | 2idlcpbl.x |
. . . 4
β’ π = (Baseβπ
) |
2 | | 2idlcpbl.t |
. . . 4
β’ Β· =
(.rβπ
) |
3 | | simpll 766 |
. . . 4
β’ (((π
β Ring β§ π β πΌ) β§ (π΄πΈπΆ β§ π΅πΈπ·)) β π
β Ring) |
4 | | eqid 2733 |
. . . . . . . . . . . 12
β’
(LIdealβπ
) =
(LIdealβπ
) |
5 | | eqid 2733 |
. . . . . . . . . . . 12
β’
(opprβπ
) = (opprβπ
) |
6 | | eqid 2733 |
. . . . . . . . . . . 12
β’
(LIdealβ(opprβπ
)) =
(LIdealβ(opprβπ
)) |
7 | | 2idlcpbl.i |
. . . . . . . . . . . 12
β’ πΌ = (2Idealβπ
) |
8 | 4, 5, 6, 7 | 2idlelb 20865 |
. . . . . . . . . . 11
β’ (π β πΌ β (π β (LIdealβπ
) β§ π β
(LIdealβ(opprβπ
)))) |
9 | 8 | simplbi 499 |
. . . . . . . . . 10
β’ (π β πΌ β π β (LIdealβπ
)) |
10 | 9 | ad2antlr 726 |
. . . . . . . . 9
β’ (((π
β Ring β§ π β πΌ) β§ (π΄πΈπΆ β§ π΅πΈπ·)) β π β (LIdealβπ
)) |
11 | 4 | lidlsubg 20838 |
. . . . . . . . 9
β’ ((π
β Ring β§ π β (LIdealβπ
)) β π β (SubGrpβπ
)) |
12 | 3, 10, 11 | syl2anc 585 |
. . . . . . . 8
β’ (((π
β Ring β§ π β πΌ) β§ (π΄πΈπΆ β§ π΅πΈπ·)) β π β (SubGrpβπ
)) |
13 | | 2idlcpbl.r |
. . . . . . . . 9
β’ πΈ = (π
~QG π) |
14 | 1, 13 | eqger 19058 |
. . . . . . . 8
β’ (π β (SubGrpβπ
) β πΈ Er π) |
15 | 12, 14 | syl 17 |
. . . . . . 7
β’ (((π
β Ring β§ π β πΌ) β§ (π΄πΈπΆ β§ π΅πΈπ·)) β πΈ Er π) |
16 | | simprl 770 |
. . . . . . 7
β’ (((π
β Ring β§ π β πΌ) β§ (π΄πΈπΆ β§ π΅πΈπ·)) β π΄πΈπΆ) |
17 | 15, 16 | ersym 8715 |
. . . . . 6
β’ (((π
β Ring β§ π β πΌ) β§ (π΄πΈπΆ β§ π΅πΈπ·)) β πΆπΈπ΄) |
18 | | ringabl 20098 |
. . . . . . . 8
β’ (π
β Ring β π
β Abel) |
19 | 18 | ad2antrr 725 |
. . . . . . 7
β’ (((π
β Ring β§ π β πΌ) β§ (π΄πΈπΆ β§ π΅πΈπ·)) β π
β Abel) |
20 | 1, 7 | 2idlss 20868 |
. . . . . . . 8
β’ (π β πΌ β π β π) |
21 | 20 | ad2antlr 726 |
. . . . . . 7
β’ (((π
β Ring β§ π β πΌ) β§ (π΄πΈπΆ β§ π΅πΈπ·)) β π β π) |
22 | | eqid 2733 |
. . . . . . . 8
β’
(-gβπ
) = (-gβπ
) |
23 | 1, 22, 13 | eqgabl 19702 |
. . . . . . 7
β’ ((π
β Abel β§ π β π) β (πΆπΈπ΄ β (πΆ β π β§ π΄ β π β§ (π΄(-gβπ
)πΆ) β π))) |
24 | 19, 21, 23 | syl2anc 585 |
. . . . . 6
β’ (((π
β Ring β§ π β πΌ) β§ (π΄πΈπΆ β§ π΅πΈπ·)) β (πΆπΈπ΄ β (πΆ β π β§ π΄ β π β§ (π΄(-gβπ
)πΆ) β π))) |
25 | 17, 24 | mpbid 231 |
. . . . 5
β’ (((π
β Ring β§ π β πΌ) β§ (π΄πΈπΆ β§ π΅πΈπ·)) β (πΆ β π β§ π΄ β π β§ (π΄(-gβπ
)πΆ) β π)) |
26 | 25 | simp2d 1144 |
. . . 4
β’ (((π
β Ring β§ π β πΌ) β§ (π΄πΈπΆ β§ π΅πΈπ·)) β π΄ β π) |
27 | | simprr 772 |
. . . . . 6
β’ (((π
β Ring β§ π β πΌ) β§ (π΄πΈπΆ β§ π΅πΈπ·)) β π΅πΈπ·) |
28 | 1, 22, 13 | eqgabl 19702 |
. . . . . . 7
β’ ((π
β Abel β§ π β π) β (π΅πΈπ· β (π΅ β π β§ π· β π β§ (π·(-gβπ
)π΅) β π))) |
29 | 19, 21, 28 | syl2anc 585 |
. . . . . 6
β’ (((π
β Ring β§ π β πΌ) β§ (π΄πΈπΆ β§ π΅πΈπ·)) β (π΅πΈπ· β (π΅ β π β§ π· β π β§ (π·(-gβπ
)π΅) β π))) |
30 | 27, 29 | mpbid 231 |
. . . . 5
β’ (((π
β Ring β§ π β πΌ) β§ (π΄πΈπΆ β§ π΅πΈπ·)) β (π΅ β π β§ π· β π β§ (π·(-gβπ
)π΅) β π)) |
31 | 30 | simp1d 1143 |
. . . 4
β’ (((π
β Ring β§ π β πΌ) β§ (π΄πΈπΆ β§ π΅πΈπ·)) β π΅ β π) |
32 | 1, 2, 3, 26, 31 | ringcld 20080 |
. . 3
β’ (((π
β Ring β§ π β πΌ) β§ (π΄πΈπΆ β§ π΅πΈπ·)) β (π΄ Β· π΅) β π) |
33 | 25 | simp1d 1143 |
. . . 4
β’ (((π
β Ring β§ π β πΌ) β§ (π΄πΈπΆ β§ π΅πΈπ·)) β πΆ β π) |
34 | 30 | simp2d 1144 |
. . . 4
β’ (((π
β Ring β§ π β πΌ) β§ (π΄πΈπΆ β§ π΅πΈπ·)) β π· β π) |
35 | 1, 2, 3, 33, 34 | ringcld 20080 |
. . 3
β’ (((π
β Ring β§ π β πΌ) β§ (π΄πΈπΆ β§ π΅πΈπ·)) β (πΆ Β· π·) β π) |
36 | | ringgrp 20061 |
. . . . . 6
β’ (π
β Ring β π
β Grp) |
37 | 36 | ad2antrr 725 |
. . . . 5
β’ (((π
β Ring β§ π β πΌ) β§ (π΄πΈπΆ β§ π΅πΈπ·)) β π
β Grp) |
38 | 1, 2, 3, 33, 31 | ringcld 20080 |
. . . . 5
β’ (((π
β Ring β§ π β πΌ) β§ (π΄πΈπΆ β§ π΅πΈπ·)) β (πΆ Β· π΅) β π) |
39 | 1, 22 | grpnnncan2 18920 |
. . . . 5
β’ ((π
β Grp β§ ((πΆ Β· π·) β π β§ (π΄ Β· π΅) β π β§ (πΆ Β· π΅) β π)) β (((πΆ Β· π·)(-gβπ
)(πΆ Β· π΅))(-gβπ
)((π΄ Β· π΅)(-gβπ
)(πΆ Β· π΅))) = ((πΆ Β· π·)(-gβπ
)(π΄ Β· π΅))) |
40 | 37, 35, 32, 38, 39 | syl13anc 1373 |
. . . 4
β’ (((π
β Ring β§ π β πΌ) β§ (π΄πΈπΆ β§ π΅πΈπ·)) β (((πΆ Β· π·)(-gβπ
)(πΆ Β· π΅))(-gβπ
)((π΄ Β· π΅)(-gβπ
)(πΆ Β· π΅))) = ((πΆ Β· π·)(-gβπ
)(π΄ Β· π΅))) |
41 | 1, 2, 22, 3, 33, 34, 31 | ringsubdi 20119 |
. . . . . 6
β’ (((π
β Ring β§ π β πΌ) β§ (π΄πΈπΆ β§ π΅πΈπ·)) β (πΆ Β· (π·(-gβπ
)π΅)) = ((πΆ Β· π·)(-gβπ
)(πΆ Β· π΅))) |
42 | 30 | simp3d 1145 |
. . . . . . 7
β’ (((π
β Ring β§ π β πΌ) β§ (π΄πΈπΆ β§ π΅πΈπ·)) β (π·(-gβπ
)π΅) β π) |
43 | 4, 1, 2 | lidlmcl 20840 |
. . . . . . 7
β’ (((π
β Ring β§ π β (LIdealβπ
)) β§ (πΆ β π β§ (π·(-gβπ
)π΅) β π)) β (πΆ Β· (π·(-gβπ
)π΅)) β π) |
44 | 3, 10, 33, 42, 43 | syl22anc 838 |
. . . . . 6
β’ (((π
β Ring β§ π β πΌ) β§ (π΄πΈπΆ β§ π΅πΈπ·)) β (πΆ Β· (π·(-gβπ
)π΅)) β π) |
45 | 41, 44 | eqeltrrd 2835 |
. . . . 5
β’ (((π
β Ring β§ π β πΌ) β§ (π΄πΈπΆ β§ π΅πΈπ·)) β ((πΆ Β· π·)(-gβπ
)(πΆ Β· π΅)) β π) |
46 | | eqid 2733 |
. . . . . . . 8
β’
(.rβ(opprβπ
)) =
(.rβ(opprβπ
)) |
47 | 1, 2, 5, 46 | opprmul 20153 |
. . . . . . 7
β’ (π΅(.rβ(opprβπ
))(π΄(-gβπ
)πΆ))
= ((π΄(-gβπ
)πΆ) Β· π΅) |
48 | 1, 2, 22, 3, 26, 33, 31 | ringsubdir 20120 |
. . . . . . 7
β’ (((π
β Ring β§ π β πΌ) β§ (π΄πΈπΆ β§ π΅πΈπ·)) β ((π΄(-gβπ
)πΆ) Β· π΅) = ((π΄ Β· π΅)(-gβπ
)(πΆ Β· π΅))) |
49 | 47, 48 | eqtrid 2785 |
. . . . . 6
β’ (((π
β Ring β§ π β πΌ) β§ (π΄πΈπΆ β§ π΅πΈπ·)) β (π΅(.rβ(opprβπ
))(π΄(-gβπ
)πΆ))
= ((π΄ Β· π΅)(-gβπ
)(πΆ
Β· π΅))) |
50 | 5 | opprring 20161 |
. . . . . . . 8
β’ (π
β Ring β
(opprβπ
) β Ring) |
51 | 50 | ad2antrr 725 |
. . . . . . 7
β’ (((π
β Ring β§ π β πΌ) β§ (π΄πΈπΆ β§ π΅πΈπ·)) β
(opprβπ
) β Ring) |
52 | 8 | simprbi 498 |
. . . . . . . 8
β’ (π β πΌ β π β
(LIdealβ(opprβπ
))) |
53 | 52 | ad2antlr 726 |
. . . . . . 7
β’ (((π
β Ring β§ π β πΌ) β§ (π΄πΈπΆ β§ π΅πΈπ·)) β π β
(LIdealβ(opprβπ
))) |
54 | 25 | simp3d 1145 |
. . . . . . 7
β’ (((π
β Ring β§ π β πΌ) β§ (π΄πΈπΆ β§ π΅πΈπ·)) β (π΄(-gβπ
)πΆ) β π) |
55 | 5, 1 | opprbas 20157 |
. . . . . . . 8
β’ π =
(Baseβ(opprβπ
)) |
56 | 6, 55, 46 | lidlmcl 20840 |
. . . . . . 7
β’
((((opprβπ
) β Ring β§ π β
(LIdealβ(opprβπ
))) β§ (π΅ β π β§ (π΄(-gβπ
)πΆ) β π)) β (π΅(.rβ(opprβπ
))(π΄(-gβπ
)πΆ))
β π) |
57 | 51, 53, 31, 54, 56 | syl22anc 838 |
. . . . . 6
β’ (((π
β Ring β§ π β πΌ) β§ (π΄πΈπΆ β§ π΅πΈπ·)) β (π΅(.rβ(opprβπ
))(π΄(-gβπ
)πΆ))
β π) |
58 | 49, 57 | eqeltrrd 2835 |
. . . . 5
β’ (((π
β Ring β§ π β πΌ) β§ (π΄πΈπΆ β§ π΅πΈπ·)) β ((π΄ Β· π΅)(-gβπ
)(πΆ Β· π΅)) β π) |
59 | 4, 22 | lidlsubcl 20839 |
. . . . 5
β’ (((π
β Ring β§ π β (LIdealβπ
)) β§ (((πΆ Β· π·)(-gβπ
)(πΆ Β· π΅)) β π β§ ((π΄ Β· π΅)(-gβπ
)(πΆ Β· π΅)) β π)) β (((πΆ Β· π·)(-gβπ
)(πΆ Β· π΅))(-gβπ
)((π΄ Β· π΅)(-gβπ
)(πΆ Β· π΅))) β π) |
60 | 3, 10, 45, 58, 59 | syl22anc 838 |
. . . 4
β’ (((π
β Ring β§ π β πΌ) β§ (π΄πΈπΆ β§ π΅πΈπ·)) β (((πΆ Β· π·)(-gβπ
)(πΆ Β· π΅))(-gβπ
)((π΄ Β· π΅)(-gβπ
)(πΆ Β· π΅))) β π) |
61 | 40, 60 | eqeltrrd 2835 |
. . 3
β’ (((π
β Ring β§ π β πΌ) β§ (π΄πΈπΆ β§ π΅πΈπ·)) β ((πΆ Β· π·)(-gβπ
)(π΄ Β· π΅)) β π) |
62 | 1, 22, 13 | eqgabl 19702 |
. . . 4
β’ ((π
β Abel β§ π β π) β ((π΄ Β· π΅)πΈ(πΆ Β· π·) β ((π΄ Β· π΅) β π β§ (πΆ Β· π·) β π β§ ((πΆ Β· π·)(-gβπ
)(π΄ Β· π΅)) β π))) |
63 | 19, 21, 62 | syl2anc 585 |
. . 3
β’ (((π
β Ring β§ π β πΌ) β§ (π΄πΈπΆ β§ π΅πΈπ·)) β ((π΄ Β· π΅)πΈ(πΆ Β· π·) β ((π΄ Β· π΅) β π β§ (πΆ Β· π·) β π β§ ((πΆ Β· π·)(-gβπ
)(π΄ Β· π΅)) β π))) |
64 | 32, 35, 61, 63 | mpbir3and 1343 |
. 2
β’ (((π
β Ring β§ π β πΌ) β§ (π΄πΈπΆ β§ π΅πΈπ·)) β (π΄ Β· π΅)πΈ(πΆ Β· π·)) |
65 | 64 | ex 414 |
1
β’ ((π
β Ring β§ π β πΌ) β ((π΄πΈπΆ β§ π΅πΈπ·) β (π΄ Β· π΅)πΈ(πΆ Β· π·))) |