Step | Hyp | Ref
| Expression |
1 | | simpll 766 |
. . . 4
β’ (((π
β Ring β§ π β πΌ) β§ (π΄πΈπΆ β§ π΅πΈπ·)) β π
β Ring) |
2 | | eqid 2733 |
. . . . . . . . . . . . 13
β’
(LIdealβπ
) =
(LIdealβπ
) |
3 | | eqid 2733 |
. . . . . . . . . . . . 13
β’
(opprβπ
) = (opprβπ
) |
4 | | eqid 2733 |
. . . . . . . . . . . . 13
β’
(LIdealβ(opprβπ
)) =
(LIdealβ(opprβπ
)) |
5 | | 2idlcpbl.i |
. . . . . . . . . . . . 13
β’ πΌ = (2Idealβπ
) |
6 | 2, 3, 4, 5 | 2idlval 20719 |
. . . . . . . . . . . 12
β’ πΌ = ((LIdealβπ
) β©
(LIdealβ(opprβπ
))) |
7 | 6 | elin2 4158 |
. . . . . . . . . . 11
β’ (π β πΌ β (π β (LIdealβπ
) β§ π β
(LIdealβ(opprβπ
)))) |
8 | 7 | simplbi 499 |
. . . . . . . . . 10
β’ (π β πΌ β π β (LIdealβπ
)) |
9 | 8 | ad2antlr 726 |
. . . . . . . . 9
β’ (((π
β Ring β§ π β πΌ) β§ (π΄πΈπΆ β§ π΅πΈπ·)) β π β (LIdealβπ
)) |
10 | 2 | lidlsubg 20701 |
. . . . . . . . 9
β’ ((π
β Ring β§ π β (LIdealβπ
)) β π β (SubGrpβπ
)) |
11 | 1, 9, 10 | syl2anc 585 |
. . . . . . . 8
β’ (((π
β Ring β§ π β πΌ) β§ (π΄πΈπΆ β§ π΅πΈπ·)) β π β (SubGrpβπ
)) |
12 | | 2idlcpbl.x |
. . . . . . . . 9
β’ π = (Baseβπ
) |
13 | | 2idlcpbl.r |
. . . . . . . . 9
β’ πΈ = (π
~QG π) |
14 | 12, 13 | eqger 18985 |
. . . . . . . 8
β’ (π β (SubGrpβπ
) β πΈ Er π) |
15 | 11, 14 | syl 17 |
. . . . . . 7
β’ (((π
β Ring β§ π β πΌ) β§ (π΄πΈπΆ β§ π΅πΈπ·)) β πΈ Er π) |
16 | | simprl 770 |
. . . . . . 7
β’ (((π
β Ring β§ π β πΌ) β§ (π΄πΈπΆ β§ π΅πΈπ·)) β π΄πΈπΆ) |
17 | 15, 16 | ersym 8663 |
. . . . . 6
β’ (((π
β Ring β§ π β πΌ) β§ (π΄πΈπΆ β§ π΅πΈπ·)) β πΆπΈπ΄) |
18 | | ringabl 20007 |
. . . . . . . 8
β’ (π
β Ring β π
β Abel) |
19 | 18 | ad2antrr 725 |
. . . . . . 7
β’ (((π
β Ring β§ π β πΌ) β§ (π΄πΈπΆ β§ π΅πΈπ·)) β π
β Abel) |
20 | 12, 2 | lidlss 20696 |
. . . . . . . 8
β’ (π β (LIdealβπ
) β π β π) |
21 | 9, 20 | syl 17 |
. . . . . . 7
β’ (((π
β Ring β§ π β πΌ) β§ (π΄πΈπΆ β§ π΅πΈπ·)) β π β π) |
22 | | eqid 2733 |
. . . . . . . 8
β’
(-gβπ
) = (-gβπ
) |
23 | 12, 22, 13 | eqgabl 19618 |
. . . . . . 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 | 12, 22, 13 | eqgabl 19618 |
. . . . . . 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 | | 2idlcpbl.t |
. . . . 5
β’ Β· =
(.rβπ
) |
33 | 12, 32 | ringcl 19986 |
. . . 4
β’ ((π
β Ring β§ π΄ β π β§ π΅ β π) β (π΄ Β· π΅) β π) |
34 | 1, 26, 31, 33 | syl3anc 1372 |
. . 3
β’ (((π
β Ring β§ π β πΌ) β§ (π΄πΈπΆ β§ π΅πΈπ·)) β (π΄ Β· π΅) β π) |
35 | 25 | simp1d 1143 |
. . . 4
β’ (((π
β Ring β§ π β πΌ) β§ (π΄πΈπΆ β§ π΅πΈπ·)) β πΆ β π) |
36 | 30 | simp2d 1144 |
. . . 4
β’ (((π
β Ring β§ π β πΌ) β§ (π΄πΈπΆ β§ π΅πΈπ·)) β π· β π) |
37 | 12, 32 | ringcl 19986 |
. . . 4
β’ ((π
β Ring β§ πΆ β π β§ π· β π) β (πΆ Β· π·) β π) |
38 | 1, 35, 36, 37 | syl3anc 1372 |
. . 3
β’ (((π
β Ring β§ π β πΌ) β§ (π΄πΈπΆ β§ π΅πΈπ·)) β (πΆ Β· π·) β π) |
39 | | ringgrp 19974 |
. . . . . 6
β’ (π
β Ring β π
β Grp) |
40 | 39 | ad2antrr 725 |
. . . . 5
β’ (((π
β Ring β§ π β πΌ) β§ (π΄πΈπΆ β§ π΅πΈπ·)) β π
β Grp) |
41 | 12, 32 | ringcl 19986 |
. . . . . 6
β’ ((π
β Ring β§ πΆ β π β§ π΅ β π) β (πΆ Β· π΅) β π) |
42 | 1, 35, 31, 41 | syl3anc 1372 |
. . . . 5
β’ (((π
β Ring β§ π β πΌ) β§ (π΄πΈπΆ β§ π΅πΈπ·)) β (πΆ Β· π΅) β π) |
43 | 12, 22 | grpnnncan2 18849 |
. . . . 5
β’ ((π
β Grp β§ ((πΆ Β· π·) β π β§ (π΄ Β· π΅) β π β§ (πΆ Β· π΅) β π)) β (((πΆ Β· π·)(-gβπ
)(πΆ Β· π΅))(-gβπ
)((π΄ Β· π΅)(-gβπ
)(πΆ Β· π΅))) = ((πΆ Β· π·)(-gβπ
)(π΄ Β· π΅))) |
44 | 40, 38, 34, 42, 43 | syl13anc 1373 |
. . . 4
β’ (((π
β Ring β§ π β πΌ) β§ (π΄πΈπΆ β§ π΅πΈπ·)) β (((πΆ Β· π·)(-gβπ
)(πΆ Β· π΅))(-gβπ
)((π΄ Β· π΅)(-gβπ
)(πΆ Β· π΅))) = ((πΆ Β· π·)(-gβπ
)(π΄ Β· π΅))) |
45 | 12, 32, 22, 1, 35, 36, 31 | ringsubdi 20028 |
. . . . . 6
β’ (((π
β Ring β§ π β πΌ) β§ (π΄πΈπΆ β§ π΅πΈπ·)) β (πΆ Β· (π·(-gβπ
)π΅)) = ((πΆ Β· π·)(-gβπ
)(πΆ Β· π΅))) |
46 | 30 | simp3d 1145 |
. . . . . . 7
β’ (((π
β Ring β§ π β πΌ) β§ (π΄πΈπΆ β§ π΅πΈπ·)) β (π·(-gβπ
)π΅) β π) |
47 | 2, 12, 32 | lidlmcl 20703 |
. . . . . . 7
β’ (((π
β Ring β§ π β (LIdealβπ
)) β§ (πΆ β π β§ (π·(-gβπ
)π΅) β π)) β (πΆ Β· (π·(-gβπ
)π΅)) β π) |
48 | 1, 9, 35, 46, 47 | syl22anc 838 |
. . . . . 6
β’ (((π
β Ring β§ π β πΌ) β§ (π΄πΈπΆ β§ π΅πΈπ·)) β (πΆ Β· (π·(-gβπ
)π΅)) β π) |
49 | 45, 48 | eqeltrrd 2835 |
. . . . 5
β’ (((π
β Ring β§ π β πΌ) β§ (π΄πΈπΆ β§ π΅πΈπ·)) β ((πΆ Β· π·)(-gβπ
)(πΆ Β· π΅)) β π) |
50 | | eqid 2733 |
. . . . . . . 8
β’
(.rβ(opprβπ
)) =
(.rβ(opprβπ
)) |
51 | 12, 32, 3, 50 | opprmul 20057 |
. . . . . . 7
β’ (π΅(.rβ(opprβπ
))(π΄(-gβπ
)πΆ))
= ((π΄(-gβπ
)πΆ) Β· π΅) |
52 | 12, 32, 22, 1, 26, 35, 31 | ringsubdir 20029 |
. . . . . . 7
β’ (((π
β Ring β§ π β πΌ) β§ (π΄πΈπΆ β§ π΅πΈπ·)) β ((π΄(-gβπ
)πΆ) Β· π΅) = ((π΄ Β· π΅)(-gβπ
)(πΆ Β· π΅))) |
53 | 51, 52 | eqtrid 2785 |
. . . . . 6
β’ (((π
β Ring β§ π β πΌ) β§ (π΄πΈπΆ β§ π΅πΈπ·)) β (π΅(.rβ(opprβπ
))(π΄(-gβπ
)πΆ))
= ((π΄ Β· π΅)(-gβπ
)(πΆ
Β· π΅))) |
54 | 3 | opprring 20065 |
. . . . . . . 8
β’ (π
β Ring β
(opprβπ
) β Ring) |
55 | 54 | ad2antrr 725 |
. . . . . . 7
β’ (((π
β Ring β§ π β πΌ) β§ (π΄πΈπΆ β§ π΅πΈπ·)) β
(opprβπ
) β Ring) |
56 | 7 | simprbi 498 |
. . . . . . . 8
β’ (π β πΌ β π β
(LIdealβ(opprβπ
))) |
57 | 56 | ad2antlr 726 |
. . . . . . 7
β’ (((π
β Ring β§ π β πΌ) β§ (π΄πΈπΆ β§ π΅πΈπ·)) β π β
(LIdealβ(opprβπ
))) |
58 | 25 | simp3d 1145 |
. . . . . . 7
β’ (((π
β Ring β§ π β πΌ) β§ (π΄πΈπΆ β§ π΅πΈπ·)) β (π΄(-gβπ
)πΆ) β π) |
59 | 3, 12 | opprbas 20061 |
. . . . . . . 8
β’ π =
(Baseβ(opprβπ
)) |
60 | 4, 59, 50 | lidlmcl 20703 |
. . . . . . 7
β’
((((opprβπ
) β Ring β§ π β
(LIdealβ(opprβπ
))) β§ (π΅ β π β§ (π΄(-gβπ
)πΆ) β π)) β (π΅(.rβ(opprβπ
))(π΄(-gβπ
)πΆ))
β π) |
61 | 55, 57, 31, 58, 60 | syl22anc 838 |
. . . . . 6
β’ (((π
β Ring β§ π β πΌ) β§ (π΄πΈπΆ β§ π΅πΈπ·)) β (π΅(.rβ(opprβπ
))(π΄(-gβπ
)πΆ))
β π) |
62 | 53, 61 | eqeltrrd 2835 |
. . . . 5
β’ (((π
β Ring β§ π β πΌ) β§ (π΄πΈπΆ β§ π΅πΈπ·)) β ((π΄ Β· π΅)(-gβπ
)(πΆ Β· π΅)) β π) |
63 | 2, 22 | lidlsubcl 20702 |
. . . . 5
β’ (((π
β Ring β§ π β (LIdealβπ
)) β§ (((πΆ Β· π·)(-gβπ
)(πΆ Β· π΅)) β π β§ ((π΄ Β· π΅)(-gβπ
)(πΆ Β· π΅)) β π)) β (((πΆ Β· π·)(-gβπ
)(πΆ Β· π΅))(-gβπ
)((π΄ Β· π΅)(-gβπ
)(πΆ Β· π΅))) β π) |
64 | 1, 9, 49, 62, 63 | syl22anc 838 |
. . . 4
β’ (((π
β Ring β§ π β πΌ) β§ (π΄πΈπΆ β§ π΅πΈπ·)) β (((πΆ Β· π·)(-gβπ
)(πΆ Β· π΅))(-gβπ
)((π΄ Β· π΅)(-gβπ
)(πΆ Β· π΅))) β π) |
65 | 44, 64 | eqeltrrd 2835 |
. . 3
β’ (((π
β Ring β§ π β πΌ) β§ (π΄πΈπΆ β§ π΅πΈπ·)) β ((πΆ Β· π·)(-gβπ
)(π΄ Β· π΅)) β π) |
66 | 12, 22, 13 | eqgabl 19618 |
. . . 4
β’ ((π
β Abel β§ π β π) β ((π΄ Β· π΅)πΈ(πΆ Β· π·) β ((π΄ Β· π΅) β π β§ (πΆ Β· π·) β π β§ ((πΆ Β· π·)(-gβπ
)(π΄ Β· π΅)) β π))) |
67 | 19, 21, 66 | syl2anc 585 |
. . 3
β’ (((π
β Ring β§ π β πΌ) β§ (π΄πΈπΆ β§ π΅πΈπ·)) β ((π΄ Β· π΅)πΈ(πΆ Β· π·) β ((π΄ Β· π΅) β π β§ (πΆ Β· π·) β π β§ ((πΆ Β· π·)(-gβπ
)(π΄ Β· π΅)) β π))) |
68 | 34, 38, 65, 67 | mpbir3and 1343 |
. 2
β’ (((π
β Ring β§ π β πΌ) β§ (π΄πΈπΆ β§ π΅πΈπ·)) β (π΄ Β· π΅)πΈ(πΆ Β· π·)) |
69 | 68 | ex 414 |
1
β’ ((π
β Ring β§ π β πΌ) β ((π΄πΈπΆ β§ π΅πΈπ·) β (π΄ Β· π΅)πΈ(πΆ Β· π·))) |