Step | Hyp | Ref
| Expression |
1 | | simpl 483 |
. 2
β’ ((π
β DivRing β§ π β π΅) β π
β DivRing) |
2 | | drngring 20363 |
. . 3
β’ (π
β DivRing β π
β Ring) |
3 | | cntzsdrg.b |
. . . 4
β’ π΅ = (Baseβπ
) |
4 | | cntzsdrg.m |
. . . 4
β’ π = (mulGrpβπ
) |
5 | | cntzsdrg.z |
. . . 4
β’ π = (Cntzβπ) |
6 | 3, 4, 5 | cntzsubr 20352 |
. . 3
β’ ((π
β Ring β§ π β π΅) β (πβπ) β (SubRingβπ
)) |
7 | 2, 6 | sylan 580 |
. 2
β’ ((π
β DivRing β§ π β π΅) β (πβπ) β (SubRingβπ
)) |
8 | | oveq2 7416 |
. . . . . . 7
β’ (π¦ = (0gβπ
) β
(((invrβπ
)βπ₯)(.rβπ
)π¦) = (((invrβπ
)βπ₯)(.rβπ
)(0gβπ
))) |
9 | | oveq1 7415 |
. . . . . . 7
β’ (π¦ = (0gβπ
) β (π¦(.rβπ
)((invrβπ
)βπ₯)) = ((0gβπ
)(.rβπ
)((invrβπ
)βπ₯))) |
10 | 8, 9 | eqeq12d 2748 |
. . . . . 6
β’ (π¦ = (0gβπ
) β
((((invrβπ
)βπ₯)(.rβπ
)π¦) = (π¦(.rβπ
)((invrβπ
)βπ₯)) β (((invrβπ
)βπ₯)(.rβπ
)(0gβπ
)) = ((0gβπ
)(.rβπ
)((invrβπ
)βπ₯)))) |
11 | | eldifsn 4790 |
. . . . . . . 8
β’ (π¦ β (π β {(0gβπ
)}) β (π¦ β π β§ π¦ β (0gβπ
))) |
12 | | eqid 2732 |
. . . . . . . . . . . . . 14
β’
(Unitβπ
) =
(Unitβπ
) |
13 | 4 | oveq1i 7418 |
. . . . . . . . . . . . . 14
β’ (π βΎs
(Unitβπ
)) =
((mulGrpβπ
)
βΎs (Unitβπ
)) |
14 | | eqid 2732 |
. . . . . . . . . . . . . 14
β’
(invrβπ
) = (invrβπ
) |
15 | 12, 13, 14 | invrfval 20202 |
. . . . . . . . . . . . 13
β’
(invrβπ
) = (invgβ(π βΎs
(Unitβπ
))) |
16 | | eqid 2732 |
. . . . . . . . . . . . . . . . 17
β’
(0gβπ
) = (0gβπ
) |
17 | 3, 12, 16 | isdrng 20360 |
. . . . . . . . . . . . . . . 16
β’ (π
β DivRing β (π
β Ring β§
(Unitβπ
) = (π΅ β
{(0gβπ
)}))) |
18 | 17 | simprbi 497 |
. . . . . . . . . . . . . . 15
β’ (π
β DivRing β
(Unitβπ
) = (π΅ β
{(0gβπ
)})) |
19 | 18 | oveq2d 7424 |
. . . . . . . . . . . . . 14
β’ (π
β DivRing β (π βΎs
(Unitβπ
)) = (π βΎs (π΅ β
{(0gβπ
)}))) |
20 | 19 | fveq2d 6895 |
. . . . . . . . . . . . 13
β’ (π
β DivRing β
(invgβ(π
βΎs (Unitβπ
))) = (invgβ(π βΎs (π΅ β
{(0gβπ
)})))) |
21 | 15, 20 | eqtrid 2784 |
. . . . . . . . . . . 12
β’ (π
β DivRing β
(invrβπ
) =
(invgβ(π
βΎs (π΅
β {(0gβπ
)})))) |
22 | 21 | ad2antrr 724 |
. . . . . . . . . . 11
β’ (((π
β DivRing β§ π β π΅) β§ π₯ β ((πβπ) β {(0gβπ
)})) β
(invrβπ
) =
(invgβ(π
βΎs (π΅
β {(0gβπ
)})))) |
23 | 22 | fveq1d 6893 |
. . . . . . . . . 10
β’ (((π
β DivRing β§ π β π΅) β§ π₯ β ((πβπ) β {(0gβπ
)})) β
((invrβπ
)βπ₯) = ((invgβ(π βΎs (π΅ β
{(0gβπ
)})))βπ₯)) |
24 | 4 | oveq1i 7418 |
. . . . . . . . . . . . . 14
β’ (π βΎs (π΅ β
{(0gβπ
)}))
= ((mulGrpβπ
)
βΎs (π΅
β {(0gβπ
)})) |
25 | 3, 16, 24 | drngmgp 20372 |
. . . . . . . . . . . . 13
β’ (π
β DivRing β (π βΎs (π΅ β
{(0gβπ
)}))
β Grp) |
26 | 25 | ad2antrr 724 |
. . . . . . . . . . . 12
β’ (((π
β DivRing β§ π β π΅) β§ π₯ β ((πβπ) β {(0gβπ
)})) β (π βΎs (π΅ β {(0gβπ
)})) β
Grp) |
27 | | ssdif 4139 |
. . . . . . . . . . . . 13
β’ (π β π΅ β (π β {(0gβπ
)}) β (π΅ β {(0gβπ
)})) |
28 | 27 | ad2antlr 725 |
. . . . . . . . . . . 12
β’ (((π
β DivRing β§ π β π΅) β§ π₯ β ((πβπ) β {(0gβπ
)})) β (π β {(0gβπ
)}) β (π΅ β {(0gβπ
)})) |
29 | | difss 4131 |
. . . . . . . . . . . . . 14
β’ (π΅ β
{(0gβπ
)})
β π΅ |
30 | | eqid 2732 |
. . . . . . . . . . . . . . 15
β’ (π βΎs (π΅ β
{(0gβπ
)}))
= (π βΎs
(π΅ β
{(0gβπ
)})) |
31 | 4, 3 | mgpbas 19992 |
. . . . . . . . . . . . . . 15
β’ π΅ = (Baseβπ) |
32 | 30, 31 | ressbas2 17181 |
. . . . . . . . . . . . . 14
β’ ((π΅ β
{(0gβπ
)})
β π΅ β (π΅ β
{(0gβπ
)})
= (Baseβ(π
βΎs (π΅
β {(0gβπ
)})))) |
33 | 29, 32 | ax-mp 5 |
. . . . . . . . . . . . 13
β’ (π΅ β
{(0gβπ
)})
= (Baseβ(π
βΎs (π΅
β {(0gβπ
)}))) |
34 | | eqid 2732 |
. . . . . . . . . . . . 13
β’
(Cntzβ(π
βΎs (π΅
β {(0gβπ
)}))) = (Cntzβ(π βΎs (π΅ β {(0gβπ
)}))) |
35 | 33, 34 | cntzsubg 19202 |
. . . . . . . . . . . 12
β’ (((π βΎs (π΅ β
{(0gβπ
)}))
β Grp β§ (π β
{(0gβπ
)})
β (π΅ β
{(0gβπ
)}))
β ((Cntzβ(π
βΎs (π΅
β {(0gβπ
)})))β(π β {(0gβπ
)})) β (SubGrpβ(π βΎs (π΅ β
{(0gβπ
)})))) |
36 | 26, 28, 35 | syl2anc 584 |
. . . . . . . . . . 11
β’ (((π
β DivRing β§ π β π΅) β§ π₯ β ((πβπ) β {(0gβπ
)})) β ((Cntzβ(π βΎs (π΅ β
{(0gβπ
)})))β(π β {(0gβπ
)})) β (SubGrpβ(π βΎs (π΅ β
{(0gβπ
)})))) |
37 | | simpr 485 |
. . . . . . . . . . . . . . . 16
β’ ((π
β DivRing β§ π β π΅) β π β π΅) |
38 | | difss 4131 |
. . . . . . . . . . . . . . . 16
β’ (π β
{(0gβπ
)})
β π |
39 | 31, 5 | cntz2ss 19198 |
. . . . . . . . . . . . . . . 16
β’ ((π β π΅ β§ (π β {(0gβπ
)}) β π) β (πβπ) β (πβ(π β {(0gβπ
)}))) |
40 | 37, 38, 39 | sylancl 586 |
. . . . . . . . . . . . . . 15
β’ ((π
β DivRing β§ π β π΅) β (πβπ) β (πβ(π β {(0gβπ
)}))) |
41 | 40 | ssdifssd 4142 |
. . . . . . . . . . . . . 14
β’ ((π
β DivRing β§ π β π΅) β ((πβπ) β {(0gβπ
)}) β (πβ(π β {(0gβπ
)}))) |
42 | 41 | sselda 3982 |
. . . . . . . . . . . . 13
β’ (((π
β DivRing β§ π β π΅) β§ π₯ β ((πβπ) β {(0gβπ
)})) β π₯ β (πβ(π β {(0gβπ
)}))) |
43 | 31, 5 | cntzssv 19191 |
. . . . . . . . . . . . . . 15
β’ (πβπ) β π΅ |
44 | | ssdif 4139 |
. . . . . . . . . . . . . . 15
β’ ((πβπ) β π΅ β ((πβπ) β {(0gβπ
)}) β (π΅ β {(0gβπ
)})) |
45 | 43, 44 | mp1i 13 |
. . . . . . . . . . . . . 14
β’ ((π
β DivRing β§ π β π΅) β ((πβπ) β {(0gβπ
)}) β (π΅ β {(0gβπ
)})) |
46 | 45 | sselda 3982 |
. . . . . . . . . . . . 13
β’ (((π
β DivRing β§ π β π΅) β§ π₯ β ((πβπ) β {(0gβπ
)})) β π₯ β (π΅ β {(0gβπ
)})) |
47 | 42, 46 | elind 4194 |
. . . . . . . . . . . 12
β’ (((π
β DivRing β§ π β π΅) β§ π₯ β ((πβπ) β {(0gβπ
)})) β π₯ β ((πβ(π β {(0gβπ
)})) β© (π΅ β {(0gβπ
)}))) |
48 | 3 | fvexi 6905 |
. . . . . . . . . . . . . 14
β’ π΅ β V |
49 | 48 | difexi 5328 |
. . . . . . . . . . . . 13
β’ (π΅ β
{(0gβπ
)})
β V |
50 | 30, 5, 34 | resscntz 19196 |
. . . . . . . . . . . . 13
β’ (((π΅ β
{(0gβπ
)})
β V β§ (π β
{(0gβπ
)})
β (π΅ β
{(0gβπ
)}))
β ((Cntzβ(π
βΎs (π΅
β {(0gβπ
)})))β(π β {(0gβπ
)})) = ((πβ(π β {(0gβπ
)})) β© (π΅ β {(0gβπ
)}))) |
51 | 49, 28, 50 | sylancr 587 |
. . . . . . . . . . . 12
β’ (((π
β DivRing β§ π β π΅) β§ π₯ β ((πβπ) β {(0gβπ
)})) β ((Cntzβ(π βΎs (π΅ β
{(0gβπ
)})))β(π β {(0gβπ
)})) = ((πβ(π β {(0gβπ
)})) β© (π΅ β {(0gβπ
)}))) |
52 | 47, 51 | eleqtrrd 2836 |
. . . . . . . . . . 11
β’ (((π
β DivRing β§ π β π΅) β§ π₯ β ((πβπ) β {(0gβπ
)})) β π₯ β ((Cntzβ(π βΎs (π΅ β {(0gβπ
)})))β(π β {(0gβπ
)}))) |
53 | | eqid 2732 |
. . . . . . . . . . . 12
β’
(invgβ(π βΎs (π΅ β {(0gβπ
)}))) =
(invgβ(π
βΎs (π΅
β {(0gβπ
)}))) |
54 | 53 | subginvcl 19014 |
. . . . . . . . . . 11
β’
((((Cntzβ(π
βΎs (π΅
β {(0gβπ
)})))β(π β {(0gβπ
)})) β (SubGrpβ(π βΎs (π΅ β
{(0gβπ
)}))) β§ π₯ β ((Cntzβ(π βΎs (π΅ β {(0gβπ
)})))β(π β {(0gβπ
)}))) β
((invgβ(π
βΎs (π΅
β {(0gβπ
)})))βπ₯) β ((Cntzβ(π βΎs (π΅ β {(0gβπ
)})))β(π β {(0gβπ
)}))) |
55 | 36, 52, 54 | syl2anc 584 |
. . . . . . . . . 10
β’ (((π
β DivRing β§ π β π΅) β§ π₯ β ((πβπ) β {(0gβπ
)})) β
((invgβ(π
βΎs (π΅
β {(0gβπ
)})))βπ₯) β ((Cntzβ(π βΎs (π΅ β {(0gβπ
)})))β(π β {(0gβπ
)}))) |
56 | 23, 55 | eqeltrd 2833 |
. . . . . . . . 9
β’ (((π
β DivRing β§ π β π΅) β§ π₯ β ((πβπ) β {(0gβπ
)})) β
((invrβπ
)βπ₯) β ((Cntzβ(π βΎs (π΅ β {(0gβπ
)})))β(π β {(0gβπ
)}))) |
57 | | eqid 2732 |
. . . . . . . . . . . . 13
β’
(.rβπ
) = (.rβπ
) |
58 | 4, 57 | mgpplusg 19990 |
. . . . . . . . . . . 12
β’
(.rβπ
) = (+gβπ) |
59 | 30, 58 | ressplusg 17234 |
. . . . . . . . . . 11
β’ ((π΅ β
{(0gβπ
)})
β V β (.rβπ
) = (+gβ(π βΎs (π΅ β {(0gβπ
)})))) |
60 | 49, 59 | ax-mp 5 |
. . . . . . . . . 10
β’
(.rβπ
) = (+gβ(π βΎs (π΅ β {(0gβπ
)}))) |
61 | 60, 34 | cntzi 19192 |
. . . . . . . . 9
β’
((((invrβπ
)βπ₯) β ((Cntzβ(π βΎs (π΅ β {(0gβπ
)})))β(π β {(0gβπ
)})) β§ π¦ β (π β {(0gβπ
)})) β
(((invrβπ
)βπ₯)(.rβπ
)π¦) = (π¦(.rβπ
)((invrβπ
)βπ₯))) |
62 | 56, 61 | sylan 580 |
. . . . . . . 8
β’ ((((π
β DivRing β§ π β π΅) β§ π₯ β ((πβπ) β {(0gβπ
)})) β§ π¦ β (π β {(0gβπ
)})) β
(((invrβπ
)βπ₯)(.rβπ
)π¦) = (π¦(.rβπ
)((invrβπ
)βπ₯))) |
63 | 11, 62 | sylan2br 595 |
. . . . . . 7
β’ ((((π
β DivRing β§ π β π΅) β§ π₯ β ((πβπ) β {(0gβπ
)})) β§ (π¦ β π β§ π¦ β (0gβπ
))) β (((invrβπ
)βπ₯)(.rβπ
)π¦) = (π¦(.rβπ
)((invrβπ
)βπ₯))) |
64 | 63 | anassrs 468 |
. . . . . 6
β’
(((((π
β
DivRing β§ π β
π΅) β§ π₯ β ((πβπ) β {(0gβπ
)})) β§ π¦ β π) β§ π¦ β (0gβπ
)) β (((invrβπ
)βπ₯)(.rβπ
)π¦) = (π¦(.rβπ
)((invrβπ
)βπ₯))) |
65 | 2 | ad3antrrr 728 |
. . . . . . . 8
β’ ((((π
β DivRing β§ π β π΅) β§ π₯ β ((πβπ) β {(0gβπ
)})) β§ π¦ β π) β π
β Ring) |
66 | 1 | adantr 481 |
. . . . . . . . . 10
β’ (((π
β DivRing β§ π β π΅) β§ π₯ β ((πβπ) β {(0gβπ
)})) β π
β DivRing) |
67 | | eldifi 4126 |
. . . . . . . . . . . 12
β’ (π₯ β ((πβπ) β {(0gβπ
)}) β π₯ β (πβπ)) |
68 | 67 | adantl 482 |
. . . . . . . . . . 11
β’ (((π
β DivRing β§ π β π΅) β§ π₯ β ((πβπ) β {(0gβπ
)})) β π₯ β (πβπ)) |
69 | 43, 68 | sselid 3980 |
. . . . . . . . . 10
β’ (((π
β DivRing β§ π β π΅) β§ π₯ β ((πβπ) β {(0gβπ
)})) β π₯ β π΅) |
70 | | eldifsni 4793 |
. . . . . . . . . . 11
β’ (π₯ β ((πβπ) β {(0gβπ
)}) β π₯ β (0gβπ
)) |
71 | 70 | adantl 482 |
. . . . . . . . . 10
β’ (((π
β DivRing β§ π β π΅) β§ π₯ β ((πβπ) β {(0gβπ
)})) β π₯ β (0gβπ
)) |
72 | 3, 16, 14 | drnginvrcl 20378 |
. . . . . . . . . 10
β’ ((π
β DivRing β§ π₯ β π΅ β§ π₯ β (0gβπ
)) β ((invrβπ
)βπ₯) β π΅) |
73 | 66, 69, 71, 72 | syl3anc 1371 |
. . . . . . . . 9
β’ (((π
β DivRing β§ π β π΅) β§ π₯ β ((πβπ) β {(0gβπ
)})) β
((invrβπ
)βπ₯) β π΅) |
74 | 73 | adantr 481 |
. . . . . . . 8
β’ ((((π
β DivRing β§ π β π΅) β§ π₯ β ((πβπ) β {(0gβπ
)})) β§ π¦ β π) β ((invrβπ
)βπ₯) β π΅) |
75 | 3, 57, 16 | ringrz 20107 |
. . . . . . . 8
β’ ((π
β Ring β§
((invrβπ
)βπ₯) β π΅) β (((invrβπ
)βπ₯)(.rβπ
)(0gβπ
)) = (0gβπ
)) |
76 | 65, 74, 75 | syl2anc 584 |
. . . . . . 7
β’ ((((π
β DivRing β§ π β π΅) β§ π₯ β ((πβπ) β {(0gβπ
)})) β§ π¦ β π) β (((invrβπ
)βπ₯)(.rβπ
)(0gβπ
)) = (0gβπ
)) |
77 | 3, 57, 16 | ringlz 20106 |
. . . . . . . 8
β’ ((π
β Ring β§
((invrβπ
)βπ₯) β π΅) β ((0gβπ
)(.rβπ
)((invrβπ
)βπ₯)) = (0gβπ
)) |
78 | 65, 74, 77 | syl2anc 584 |
. . . . . . 7
β’ ((((π
β DivRing β§ π β π΅) β§ π₯ β ((πβπ) β {(0gβπ
)})) β§ π¦ β π) β ((0gβπ
)(.rβπ
)((invrβπ
)βπ₯)) = (0gβπ
)) |
79 | 76, 78 | eqtr4d 2775 |
. . . . . 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 3146 |
. . . 4
β’ (((π
β DivRing β§ π β π΅) β§ π₯ β ((πβπ) β {(0gβπ
)})) β βπ¦ β π (((invrβπ
)βπ₯)(.rβπ
)π¦) = (π¦(.rβπ
)((invrβπ
)βπ₯))) |
82 | | simplr 767 |
. . . . 5
β’ (((π
β DivRing β§ π β π΅) β§ π₯ β ((πβπ) β {(0gβπ
)})) β π β π΅) |
83 | 31, 58, 5 | cntzel 19186 |
. . . . 5
β’ ((π β π΅ β§ ((invrβπ
)βπ₯) β π΅) β (((invrβπ
)βπ₯) β (πβπ) β βπ¦ β π (((invrβπ
)βπ₯)(.rβπ
)π¦) = (π¦(.rβπ
)((invrβπ
)βπ₯)))) |
84 | 82, 73, 83 | syl2anc 584 |
. . . 4
β’ (((π
β DivRing β§ π β π΅) β§ π₯ β ((πβπ) β {(0gβπ
)})) β
(((invrβπ
)βπ₯) β (πβπ) β βπ¦ β π (((invrβπ
)βπ₯)(.rβπ
)π¦) = (π¦(.rβπ
)((invrβπ
)βπ₯)))) |
85 | 81, 84 | mpbird 256 |
. . 3
β’ (((π
β DivRing β§ π β π΅) β§ π₯ β ((πβπ) β {(0gβπ
)})) β
((invrβπ
)βπ₯) β (πβπ)) |
86 | 85 | ralrimiva 3146 |
. 2
β’ ((π
β DivRing β§ π β π΅) β βπ₯ β ((πβπ) β {(0gβπ
)})((invrβπ
)βπ₯) β (πβπ)) |
87 | 14, 16 | issdrg2 20410 |
. 2
β’ ((πβπ) β (SubDRingβπ
) β (π
β DivRing β§ (πβπ) β (SubRingβπ
) β§ βπ₯ β ((πβπ) β {(0gβπ
)})((invrβπ
)βπ₯) β (πβπ))) |
88 | 1, 7, 86, 87 | syl3anbrc 1343 |
1
β’ ((π
β DivRing β§ π β π΅) β (πβπ) β (SubDRingβπ
)) |