Step | Hyp | Ref
| Expression |
1 | | simpl 484 |
. 2
β’ ((π
β DivRing β§ π β π΅) β π
β DivRing) |
2 | | drngring 20226 |
. . 3
β’ (π
β DivRing β π
β Ring) |
3 | | cntzsdrg.b |
. . . 4
β’ π΅ = (Baseβπ
) |
4 | | cntzsdrg.m |
. . . 4
β’ π = (mulGrpβπ
) |
5 | | cntzsdrg.z |
. . . 4
β’ π = (Cntzβπ) |
6 | 3, 4, 5 | cntzsubr 20298 |
. . 3
β’ ((π
β Ring β§ π β π΅) β (πβπ) β (SubRingβπ
)) |
7 | 2, 6 | sylan 581 |
. 2
β’ ((π
β DivRing β§ π β π΅) β (πβπ) β (SubRingβπ
)) |
8 | | oveq2 7369 |
. . . . . . 7
β’ (π¦ = (0gβπ
) β
(((invrβπ
)βπ₯)(.rβπ
)π¦) = (((invrβπ
)βπ₯)(.rβπ
)(0gβπ
))) |
9 | | oveq1 7368 |
. . . . . . 7
β’ (π¦ = (0gβπ
) β (π¦(.rβπ
)((invrβπ
)βπ₯)) = ((0gβπ
)(.rβπ
)((invrβπ
)βπ₯))) |
10 | 8, 9 | eqeq12d 2749 |
. . . . . 6
β’ (π¦ = (0gβπ
) β
((((invrβπ
)βπ₯)(.rβπ
)π¦) = (π¦(.rβπ
)((invrβπ
)βπ₯)) β (((invrβπ
)βπ₯)(.rβπ
)(0gβπ
)) = ((0gβπ
)(.rβπ
)((invrβπ
)βπ₯)))) |
11 | | eldifsn 4751 |
. . . . . . . 8
β’ (π¦ β (π β {(0gβπ
)}) β (π¦ β π β§ π¦ β (0gβπ
))) |
12 | | eqid 2733 |
. . . . . . . . . . . . . 14
β’
(Unitβπ
) =
(Unitβπ
) |
13 | 4 | oveq1i 7371 |
. . . . . . . . . . . . . 14
β’ (π βΎs
(Unitβπ
)) =
((mulGrpβπ
)
βΎs (Unitβπ
)) |
14 | | eqid 2733 |
. . . . . . . . . . . . . 14
β’
(invrβπ
) = (invrβπ
) |
15 | 12, 13, 14 | invrfval 20110 |
. . . . . . . . . . . . 13
β’
(invrβπ
) = (invgβ(π βΎs
(Unitβπ
))) |
16 | | eqid 2733 |
. . . . . . . . . . . . . . . . 17
β’
(0gβπ
) = (0gβπ
) |
17 | 3, 12, 16 | isdrng 20223 |
. . . . . . . . . . . . . . . 16
β’ (π
β DivRing β (π
β Ring β§
(Unitβπ
) = (π΅ β
{(0gβπ
)}))) |
18 | 17 | simprbi 498 |
. . . . . . . . . . . . . . 15
β’ (π
β DivRing β
(Unitβπ
) = (π΅ β
{(0gβπ
)})) |
19 | 18 | oveq2d 7377 |
. . . . . . . . . . . . . 14
β’ (π
β DivRing β (π βΎs
(Unitβπ
)) = (π βΎs (π΅ β
{(0gβπ
)}))) |
20 | 19 | fveq2d 6850 |
. . . . . . . . . . . . 13
β’ (π
β DivRing β
(invgβ(π
βΎs (Unitβπ
))) = (invgβ(π βΎs (π΅ β
{(0gβπ
)})))) |
21 | 15, 20 | eqtrid 2785 |
. . . . . . . . . . . 12
β’ (π
β DivRing β
(invrβπ
) =
(invgβ(π
βΎs (π΅
β {(0gβπ
)})))) |
22 | 21 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π
β DivRing β§ π β π΅) β§ π₯ β ((πβπ) β {(0gβπ
)})) β
(invrβπ
) =
(invgβ(π
βΎs (π΅
β {(0gβπ
)})))) |
23 | 22 | fveq1d 6848 |
. . . . . . . . . 10
β’ (((π
β DivRing β§ π β π΅) β§ π₯ β ((πβπ) β {(0gβπ
)})) β
((invrβπ
)βπ₯) = ((invgβ(π βΎs (π΅ β
{(0gβπ
)})))βπ₯)) |
24 | 4 | oveq1i 7371 |
. . . . . . . . . . . . . 14
β’ (π βΎs (π΅ β
{(0gβπ
)}))
= ((mulGrpβπ
)
βΎs (π΅
β {(0gβπ
)})) |
25 | 3, 16, 24 | drngmgp 20234 |
. . . . . . . . . . . . 13
β’ (π
β DivRing β (π βΎs (π΅ β
{(0gβπ
)}))
β Grp) |
26 | 25 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ (((π
β DivRing β§ π β π΅) β§ π₯ β ((πβπ) β {(0gβπ
)})) β (π βΎs (π΅ β {(0gβπ
)})) β
Grp) |
27 | | ssdif 4103 |
. . . . . . . . . . . . 13
β’ (π β π΅ β (π β {(0gβπ
)}) β (π΅ β {(0gβπ
)})) |
28 | 27 | ad2antlr 726 |
. . . . . . . . . . . 12
β’ (((π
β DivRing β§ π β π΅) β§ π₯ β ((πβπ) β {(0gβπ
)})) β (π β {(0gβπ
)}) β (π΅ β {(0gβπ
)})) |
29 | | difss 4095 |
. . . . . . . . . . . . . 14
β’ (π΅ β
{(0gβπ
)})
β π΅ |
30 | | eqid 2733 |
. . . . . . . . . . . . . . 15
β’ (π βΎs (π΅ β
{(0gβπ
)}))
= (π βΎs
(π΅ β
{(0gβπ
)})) |
31 | 4, 3 | mgpbas 19910 |
. . . . . . . . . . . . . . 15
β’ π΅ = (Baseβπ) |
32 | 30, 31 | ressbas2 17128 |
. . . . . . . . . . . . . 14
β’ ((π΅ β
{(0gβπ
)})
β π΅ β (π΅ β
{(0gβπ
)})
= (Baseβ(π
βΎs (π΅
β {(0gβπ
)})))) |
33 | 29, 32 | ax-mp 5 |
. . . . . . . . . . . . 13
β’ (π΅ β
{(0gβπ
)})
= (Baseβ(π
βΎs (π΅
β {(0gβπ
)}))) |
34 | | eqid 2733 |
. . . . . . . . . . . . 13
β’
(Cntzβ(π
βΎs (π΅
β {(0gβπ
)}))) = (Cntzβ(π βΎs (π΅ β {(0gβπ
)}))) |
35 | 33, 34 | cntzsubg 19125 |
. . . . . . . . . . . 12
β’ (((π βΎs (π΅ β
{(0gβπ
)}))
β Grp β§ (π β
{(0gβπ
)})
β (π΅ β
{(0gβπ
)}))
β ((Cntzβ(π
βΎs (π΅
β {(0gβπ
)})))β(π β {(0gβπ
)})) β (SubGrpβ(π βΎs (π΅ β
{(0gβπ
)})))) |
36 | 26, 28, 35 | syl2anc 585 |
. . . . . . . . . . 11
β’ (((π
β DivRing β§ π β π΅) β§ π₯ β ((πβπ) β {(0gβπ
)})) β ((Cntzβ(π βΎs (π΅ β
{(0gβπ
)})))β(π β {(0gβπ
)})) β (SubGrpβ(π βΎs (π΅ β
{(0gβπ
)})))) |
37 | | simpr 486 |
. . . . . . . . . . . . . . . 16
β’ ((π
β DivRing β§ π β π΅) β π β π΅) |
38 | | difss 4095 |
. . . . . . . . . . . . . . . 16
β’ (π β
{(0gβπ
)})
β π |
39 | 31, 5 | cntz2ss 19121 |
. . . . . . . . . . . . . . . 16
β’ ((π β π΅ β§ (π β {(0gβπ
)}) β π) β (πβπ) β (πβ(π β {(0gβπ
)}))) |
40 | 37, 38, 39 | sylancl 587 |
. . . . . . . . . . . . . . 15
β’ ((π
β DivRing β§ π β π΅) β (πβπ) β (πβ(π β {(0gβπ
)}))) |
41 | 40 | ssdifssd 4106 |
. . . . . . . . . . . . . 14
β’ ((π
β DivRing β§ π β π΅) β ((πβπ) β {(0gβπ
)}) β (πβ(π β {(0gβπ
)}))) |
42 | 41 | sselda 3948 |
. . . . . . . . . . . . 13
β’ (((π
β DivRing β§ π β π΅) β§ π₯ β ((πβπ) β {(0gβπ
)})) β π₯ β (πβ(π β {(0gβπ
)}))) |
43 | 31, 5 | cntzssv 19116 |
. . . . . . . . . . . . . . 15
β’ (πβπ) β π΅ |
44 | | ssdif 4103 |
. . . . . . . . . . . . . . 15
β’ ((πβπ) β π΅ β ((πβπ) β {(0gβπ
)}) β (π΅ β {(0gβπ
)})) |
45 | 43, 44 | mp1i 13 |
. . . . . . . . . . . . . 14
β’ ((π
β DivRing β§ π β π΅) β ((πβπ) β {(0gβπ
)}) β (π΅ β {(0gβπ
)})) |
46 | 45 | sselda 3948 |
. . . . . . . . . . . . 13
β’ (((π
β DivRing β§ π β π΅) β§ π₯ β ((πβπ) β {(0gβπ
)})) β π₯ β (π΅ β {(0gβπ
)})) |
47 | 42, 46 | elind 4158 |
. . . . . . . . . . . 12
β’ (((π
β DivRing β§ π β π΅) β§ π₯ β ((πβπ) β {(0gβπ
)})) β π₯ β ((πβ(π β {(0gβπ
)})) β© (π΅ β {(0gβπ
)}))) |
48 | 3 | fvexi 6860 |
. . . . . . . . . . . . . 14
β’ π΅ β V |
49 | 48 | difexi 5289 |
. . . . . . . . . . . . 13
β’ (π΅ β
{(0gβπ
)})
β V |
50 | 30, 5, 34 | resscntz 19120 |
. . . . . . . . . . . . 13
β’ (((π΅ β
{(0gβπ
)})
β V β§ (π β
{(0gβπ
)})
β (π΅ β
{(0gβπ
)}))
β ((Cntzβ(π
βΎs (π΅
β {(0gβπ
)})))β(π β {(0gβπ
)})) = ((πβ(π β {(0gβπ
)})) β© (π΅ β {(0gβπ
)}))) |
51 | 49, 28, 50 | sylancr 588 |
. . . . . . . . . . . 12
β’ (((π
β DivRing β§ π β π΅) β§ π₯ β ((πβπ) β {(0gβπ
)})) β ((Cntzβ(π βΎs (π΅ β
{(0gβπ
)})))β(π β {(0gβπ
)})) = ((πβ(π β {(0gβπ
)})) β© (π΅ β {(0gβπ
)}))) |
52 | 47, 51 | eleqtrrd 2837 |
. . . . . . . . . . 11
β’ (((π
β DivRing β§ π β π΅) β§ π₯ β ((πβπ) β {(0gβπ
)})) β π₯ β ((Cntzβ(π βΎs (π΅ β {(0gβπ
)})))β(π β {(0gβπ
)}))) |
53 | | eqid 2733 |
. . . . . . . . . . . 12
β’
(invgβ(π βΎs (π΅ β {(0gβπ
)}))) =
(invgβ(π
βΎs (π΅
β {(0gβπ
)}))) |
54 | 53 | subginvcl 18945 |
. . . . . . . . . . 11
β’
((((Cntzβ(π
βΎs (π΅
β {(0gβπ
)})))β(π β {(0gβπ
)})) β (SubGrpβ(π βΎs (π΅ β
{(0gβπ
)}))) β§ π₯ β ((Cntzβ(π βΎs (π΅ β {(0gβπ
)})))β(π β {(0gβπ
)}))) β
((invgβ(π
βΎs (π΅
β {(0gβπ
)})))βπ₯) β ((Cntzβ(π βΎs (π΅ β {(0gβπ
)})))β(π β {(0gβπ
)}))) |
55 | 36, 52, 54 | syl2anc 585 |
. . . . . . . . . 10
β’ (((π
β DivRing β§ π β π΅) β§ π₯ β ((πβπ) β {(0gβπ
)})) β
((invgβ(π
βΎs (π΅
β {(0gβπ
)})))βπ₯) β ((Cntzβ(π βΎs (π΅ β {(0gβπ
)})))β(π β {(0gβπ
)}))) |
56 | 23, 55 | eqeltrd 2834 |
. . . . . . . . 9
β’ (((π
β DivRing β§ π β π΅) β§ π₯ β ((πβπ) β {(0gβπ
)})) β
((invrβπ
)βπ₯) β ((Cntzβ(π βΎs (π΅ β {(0gβπ
)})))β(π β {(0gβπ
)}))) |
57 | | eqid 2733 |
. . . . . . . . . . . . 13
β’
(.rβπ
) = (.rβπ
) |
58 | 4, 57 | mgpplusg 19908 |
. . . . . . . . . . . 12
β’
(.rβπ
) = (+gβπ) |
59 | 30, 58 | ressplusg 17179 |
. . . . . . . . . . 11
β’ ((π΅ β
{(0gβπ
)})
β V β (.rβπ
) = (+gβ(π βΎs (π΅ β {(0gβπ
)})))) |
60 | 49, 59 | ax-mp 5 |
. . . . . . . . . 10
β’
(.rβπ
) = (+gβ(π βΎs (π΅ β {(0gβπ
)}))) |
61 | 60, 34 | cntzi 19117 |
. . . . . . . . 9
β’
((((invrβπ
)βπ₯) β ((Cntzβ(π βΎs (π΅ β {(0gβπ
)})))β(π β {(0gβπ
)})) β§ π¦ β (π β {(0gβπ
)})) β
(((invrβπ
)βπ₯)(.rβπ
)π¦) = (π¦(.rβπ
)((invrβπ
)βπ₯))) |
62 | 56, 61 | sylan 581 |
. . . . . . . 8
β’ ((((π
β DivRing β§ π β π΅) β§ π₯ β ((πβπ) β {(0gβπ
)})) β§ π¦ β (π β {(0gβπ
)})) β
(((invrβπ
)βπ₯)(.rβπ
)π¦) = (π¦(.rβπ
)((invrβπ
)βπ₯))) |
63 | 11, 62 | sylan2br 596 |
. . . . . . 7
β’ ((((π
β DivRing β§ π β π΅) β§ π₯ β ((πβπ) β {(0gβπ
)})) β§ (π¦ β π β§ π¦ β (0gβπ
))) β (((invrβπ
)βπ₯)(.rβπ
)π¦) = (π¦(.rβπ
)((invrβπ
)βπ₯))) |
64 | 63 | anassrs 469 |
. . . . . 6
β’
(((((π
β
DivRing β§ π β
π΅) β§ π₯ β ((πβπ) β {(0gβπ
)})) β§ π¦ β π) β§ π¦ β (0gβπ
)) β (((invrβπ
)βπ₯)(.rβπ
)π¦) = (π¦(.rβπ
)((invrβπ
)βπ₯))) |
65 | 2 | ad3antrrr 729 |
. . . . . . . 8
β’ ((((π
β DivRing β§ π β π΅) β§ π₯ β ((πβπ) β {(0gβπ
)})) β§ π¦ β π) β π
β Ring) |
66 | 1 | adantr 482 |
. . . . . . . . . 10
β’ (((π
β DivRing β§ π β π΅) β§ π₯ β ((πβπ) β {(0gβπ
)})) β π
β DivRing) |
67 | | eldifi 4090 |
. . . . . . . . . . . 12
β’ (π₯ β ((πβπ) β {(0gβπ
)}) β π₯ β (πβπ)) |
68 | 67 | adantl 483 |
. . . . . . . . . . 11
β’ (((π
β DivRing β§ π β π΅) β§ π₯ β ((πβπ) β {(0gβπ
)})) β π₯ β (πβπ)) |
69 | 43, 68 | sselid 3946 |
. . . . . . . . . 10
β’ (((π
β DivRing β§ π β π΅) β§ π₯ β ((πβπ) β {(0gβπ
)})) β π₯ β π΅) |
70 | | eldifsni 4754 |
. . . . . . . . . . 11
β’ (π₯ β ((πβπ) β {(0gβπ
)}) β π₯ β (0gβπ
)) |
71 | 70 | adantl 483 |
. . . . . . . . . 10
β’ (((π
β DivRing β§ π β π΅) β§ π₯ β ((πβπ) β {(0gβπ
)})) β π₯ β (0gβπ
)) |
72 | 3, 16, 14 | drnginvrcl 20240 |
. . . . . . . . . 10
β’ ((π
β DivRing β§ π₯ β π΅ β§ π₯ β (0gβπ
)) β ((invrβπ
)βπ₯) β π΅) |
73 | 66, 69, 71, 72 | syl3anc 1372 |
. . . . . . . . 9
β’ (((π
β DivRing β§ π β π΅) β§ π₯ β ((πβπ) β {(0gβπ
)})) β
((invrβπ
)βπ₯) β π΅) |
74 | 73 | adantr 482 |
. . . . . . . 8
β’ ((((π
β DivRing β§ π β π΅) β§ π₯ β ((πβπ) β {(0gβπ
)})) β§ π¦ β π) β ((invrβπ
)βπ₯) β π΅) |
75 | 3, 57, 16 | ringrz 20020 |
. . . . . . . 8
β’ ((π
β Ring β§
((invrβπ
)βπ₯) β π΅) β (((invrβπ
)βπ₯)(.rβπ
)(0gβπ
)) = (0gβπ
)) |
76 | 65, 74, 75 | syl2anc 585 |
. . . . . . 7
β’ ((((π
β DivRing β§ π β π΅) β§ π₯ β ((πβπ) β {(0gβπ
)})) β§ π¦ β π) β (((invrβπ
)βπ₯)(.rβπ
)(0gβπ
)) = (0gβπ
)) |
77 | 3, 57, 16 | ringlz 20019 |
. . . . . . . 8
β’ ((π
β Ring β§
((invrβπ
)βπ₯) β π΅) β ((0gβπ
)(.rβπ
)((invrβπ
)βπ₯)) = (0gβπ
)) |
78 | 65, 74, 77 | syl2anc 585 |
. . . . . . 7
β’ ((((π
β DivRing β§ π β π΅) β§ π₯ β ((πβπ) β {(0gβπ
)})) β§ π¦ β π) β ((0gβπ
)(.rβπ
)((invrβπ
)βπ₯)) = (0gβπ
)) |
79 | 76, 78 | eqtr4d 2776 |
. . . . . 6
β’ ((((π
β DivRing β§ π β π΅) β§ π₯ β ((πβπ) β {(0gβπ
)})) β§ π¦ β π) β (((invrβπ
)βπ₯)(.rβπ
)(0gβπ
)) = ((0gβπ
)(.rβπ
)((invrβπ
)βπ₯))) |
80 | 10, 64, 79 | pm2.61ne 3027 |
. . . . 5
β’ ((((π
β DivRing β§ π β π΅) β§ π₯ β ((πβπ) β {(0gβπ
)})) β§ π¦ β π) β (((invrβπ
)βπ₯)(.rβπ
)π¦) = (π¦(.rβπ
)((invrβπ
)βπ₯))) |
81 | 80 | ralrimiva 3140 |
. . . 4
β’ (((π
β DivRing β§ π β π΅) β§ π₯ β ((πβπ) β {(0gβπ
)})) β βπ¦ β π (((invrβπ
)βπ₯)(.rβπ
)π¦) = (π¦(.rβπ
)((invrβπ
)βπ₯))) |
82 | | simplr 768 |
. . . . 5
β’ (((π
β DivRing β§ π β π΅) β§ π₯ β ((πβπ) β {(0gβπ
)})) β π β π΅) |
83 | 31, 58, 5 | cntzel 19111 |
. . . . 5
β’ ((π β π΅ β§ ((invrβπ
)βπ₯) β π΅) β (((invrβπ
)βπ₯) β (πβπ) β βπ¦ β π (((invrβπ
)βπ₯)(.rβπ
)π¦) = (π¦(.rβπ
)((invrβπ
)βπ₯)))) |
84 | 82, 73, 83 | syl2anc 585 |
. . . 4
β’ (((π
β DivRing β§ π β π΅) β§ π₯ β ((πβπ) β {(0gβπ
)})) β
(((invrβπ
)βπ₯) β (πβπ) β βπ¦ β π (((invrβπ
)βπ₯)(.rβπ
)π¦) = (π¦(.rβπ
)((invrβπ
)βπ₯)))) |
85 | 81, 84 | mpbird 257 |
. . 3
β’ (((π
β DivRing β§ π β π΅) β§ π₯ β ((πβπ) β {(0gβπ
)})) β
((invrβπ
)βπ₯) β (πβπ)) |
86 | 85 | ralrimiva 3140 |
. 2
β’ ((π
β DivRing β§ π β π΅) β βπ₯ β ((πβπ) β {(0gβπ
)})((invrβπ
)βπ₯) β (πβπ)) |
87 | 14, 16 | issdrg2 20307 |
. 2
β’ ((πβπ) β (SubDRingβπ
) β (π
β DivRing β§ (πβπ) β (SubRingβπ
) β§ βπ₯ β ((πβπ) β {(0gβπ
)})((invrβπ
)βπ₯) β (πβπ))) |
88 | 1, 7, 86, 87 | syl3anbrc 1344 |
1
β’ ((π
β DivRing β§ π β π΅) β (πβπ) β (SubDRingβπ
)) |