Step | Hyp | Ref
| Expression |
1 | | sraassa.a |
. . . 4
β’ π΄ = ((subringAlg βπ)βπ) |
2 | 1 | a1i 11 |
. . 3
β’ ((π β CRing β§ π β (SubRingβπ)) β π΄ = ((subringAlg βπ)βπ)) |
3 | | eqid 2733 |
. . . . 5
β’
(Baseβπ) =
(Baseβπ) |
4 | 3 | subrgss 20237 |
. . . 4
β’ (π β (SubRingβπ) β π β (Baseβπ)) |
5 | 4 | adantl 483 |
. . 3
β’ ((π β CRing β§ π β (SubRingβπ)) β π β (Baseβπ)) |
6 | 2, 5 | srabase 20656 |
. 2
β’ ((π β CRing β§ π β (SubRingβπ)) β (Baseβπ) = (Baseβπ΄)) |
7 | 2, 5 | srasca 20662 |
. 2
β’ ((π β CRing β§ π β (SubRingβπ)) β (π βΎs π) = (Scalarβπ΄)) |
8 | | eqid 2733 |
. . . 4
β’ (π βΎs π) = (π βΎs π) |
9 | 8 | subrgbas 20245 |
. . 3
β’ (π β (SubRingβπ) β π = (Baseβ(π βΎs π))) |
10 | 9 | adantl 483 |
. 2
β’ ((π β CRing β§ π β (SubRingβπ)) β π = (Baseβ(π βΎs π))) |
11 | 2, 5 | sravsca 20664 |
. 2
β’ ((π β CRing β§ π β (SubRingβπ)) β
(.rβπ) = (
Β·π βπ΄)) |
12 | 2, 5 | sramulr 20660 |
. 2
β’ ((π β CRing β§ π β (SubRingβπ)) β
(.rβπ) =
(.rβπ΄)) |
13 | 1 | sralmod 20672 |
. . 3
β’ (π β (SubRingβπ) β π΄ β LMod) |
14 | 13 | adantl 483 |
. 2
β’ ((π β CRing β§ π β (SubRingβπ)) β π΄ β LMod) |
15 | | crngring 19981 |
. . . 4
β’ (π β CRing β π β Ring) |
16 | 15 | adantr 482 |
. . 3
β’ ((π β CRing β§ π β (SubRingβπ)) β π β Ring) |
17 | | eqidd 2734 |
. . . 4
β’ ((π β CRing β§ π β (SubRingβπ)) β (Baseβπ) = (Baseβπ)) |
18 | 2, 5 | sraaddg 20658 |
. . . . 5
β’ ((π β CRing β§ π β (SubRingβπ)) β
(+gβπ) =
(+gβπ΄)) |
19 | 18 | oveqdr 7386 |
. . . 4
β’ (((π β CRing β§ π β (SubRingβπ)) β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ))) β (π₯(+gβπ)π¦) = (π₯(+gβπ΄)π¦)) |
20 | 12 | oveqdr 7386 |
. . . 4
β’ (((π β CRing β§ π β (SubRingβπ)) β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ))) β (π₯(.rβπ)π¦) = (π₯(.rβπ΄)π¦)) |
21 | 17, 6, 19, 20 | ringpropd 20011 |
. . 3
β’ ((π β CRing β§ π β (SubRingβπ)) β (π β Ring β π΄ β Ring)) |
22 | 16, 21 | mpbid 231 |
. 2
β’ ((π β CRing β§ π β (SubRingβπ)) β π΄ β Ring) |
23 | 8 | subrgcrng 20240 |
. 2
β’ ((π β CRing β§ π β (SubRingβπ)) β (π βΎs π) β CRing) |
24 | 16 | adantr 482 |
. . 3
β’ (((π β CRing β§ π β (SubRingβπ)) β§ (π₯ β π β§ π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β π β Ring) |
25 | 5 | adantr 482 |
. . . 4
β’ (((π β CRing β§ π β (SubRingβπ)) β§ (π₯ β π β§ π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β π β (Baseβπ)) |
26 | | simpr1 1195 |
. . . 4
β’ (((π β CRing β§ π β (SubRingβπ)) β§ (π₯ β π β§ π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β π₯ β π) |
27 | 25, 26 | sseldd 3946 |
. . 3
β’ (((π β CRing β§ π β (SubRingβπ)) β§ (π₯ β π β§ π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β π₯ β (Baseβπ)) |
28 | | simpr2 1196 |
. . 3
β’ (((π β CRing β§ π β (SubRingβπ)) β§ (π₯ β π β§ π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β π¦ β (Baseβπ)) |
29 | | simpr3 1197 |
. . 3
β’ (((π β CRing β§ π β (SubRingβπ)) β§ (π₯ β π β§ π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β π§ β (Baseβπ)) |
30 | | eqid 2733 |
. . . 4
β’
(.rβπ) = (.rβπ) |
31 | 3, 30 | ringass 19989 |
. . 3
β’ ((π β Ring β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β ((π₯(.rβπ)π¦)(.rβπ)π§) = (π₯(.rβπ)(π¦(.rβπ)π§))) |
32 | 24, 27, 28, 29, 31 | syl13anc 1373 |
. 2
β’ (((π β CRing β§ π β (SubRingβπ)) β§ (π₯ β π β§ π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β ((π₯(.rβπ)π¦)(.rβπ)π§) = (π₯(.rβπ)(π¦(.rβπ)π§))) |
33 | | eqid 2733 |
. . . . 5
β’
(mulGrpβπ) =
(mulGrpβπ) |
34 | 33 | crngmgp 19977 |
. . . 4
β’ (π β CRing β
(mulGrpβπ) β
CMnd) |
35 | 34 | ad2antrr 725 |
. . 3
β’ (((π β CRing β§ π β (SubRingβπ)) β§ (π₯ β π β§ π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β (mulGrpβπ) β CMnd) |
36 | 33, 3 | mgpbas 19907 |
. . . 4
β’
(Baseβπ) =
(Baseβ(mulGrpβπ)) |
37 | 33, 30 | mgpplusg 19905 |
. . . 4
β’
(.rβπ) = (+gβ(mulGrpβπ)) |
38 | 36, 37 | cmn12 19589 |
. . 3
β’
(((mulGrpβπ)
β CMnd β§ (π¦ β
(Baseβπ) β§ π₯ β (Baseβπ) β§ π§ β (Baseβπ))) β (π¦(.rβπ)(π₯(.rβπ)π§)) = (π₯(.rβπ)(π¦(.rβπ)π§))) |
39 | 35, 28, 27, 29, 38 | syl13anc 1373 |
. 2
β’ (((π β CRing β§ π β (SubRingβπ)) β§ (π₯ β π β§ π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β (π¦(.rβπ)(π₯(.rβπ)π§)) = (π₯(.rβπ)(π¦(.rβπ)π§))) |
40 | 6, 7, 10, 11, 12, 14, 22, 23, 32, 39 | isassad 21286 |
1
β’ ((π β CRing β§ π β (SubRingβπ)) β π΄ β AssAlg) |