Step | Hyp | Ref
| Expression |
1 | | sralmod.a |
. . . 4
β’ π΄ = ((subringAlg βπ)βπ) |
2 | 1 | a1i 9 |
. . 3
β’ (π β (SubRingβπ) β π΄ = ((subringAlg βπ)βπ)) |
3 | | eqid 2187 |
. . . 4
β’
(Baseβπ) =
(Baseβπ) |
4 | 3 | subrgss 13442 |
. . 3
β’ (π β (SubRingβπ) β π β (Baseβπ)) |
5 | | subrgrcl 13446 |
. . 3
β’ (π β (SubRingβπ) β π β Ring) |
6 | 2, 4, 5 | srabaseg 13628 |
. 2
β’ (π β (SubRingβπ) β (Baseβπ) = (Baseβπ΄)) |
7 | 2, 4, 5 | sraaddgg 13629 |
. 2
β’ (π β (SubRingβπ) β
(+gβπ) =
(+gβπ΄)) |
8 | 2, 4, 5 | srascag 13631 |
. 2
β’ (π β (SubRingβπ) β (π βΎs π) = (Scalarβπ΄)) |
9 | 2, 4, 5 | sravscag 13632 |
. 2
β’ (π β (SubRingβπ) β
(.rβπ) = (
Β·π βπ΄)) |
10 | | eqidd 2188 |
. . 3
β’ (π β (SubRingβπ) β (π βΎs π) = (π βΎs π)) |
11 | | eqidd 2188 |
. . 3
β’ (π β (SubRingβπ) β (Baseβπ) = (Baseβπ)) |
12 | | id 19 |
. . 3
β’ (π β (SubRingβπ) β π β (SubRingβπ)) |
13 | 10, 11, 5, 12 | ressbasd 12541 |
. 2
β’ (π β (SubRingβπ) β (π β© (Baseβπ)) = (Baseβ(π βΎs π))) |
14 | | eqidd 2188 |
. . 3
β’ (π β (SubRingβπ) β
(+gβπ) =
(+gβπ)) |
15 | 10, 14, 12, 5 | ressplusgd 12602 |
. 2
β’ (π β (SubRingβπ) β
(+gβπ) =
(+gβ(π
βΎs π))) |
16 | | eqid 2187 |
. . . 4
β’ (π βΎs π) = (π βΎs π) |
17 | | eqid 2187 |
. . . 4
β’
(.rβπ) = (.rβπ) |
18 | 16, 17 | ressmulrg 12618 |
. . 3
β’ ((π β (SubRingβπ) β§ π β Ring) β
(.rβπ) =
(.rβ(π
βΎs π))) |
19 | 5, 18 | mpdan 421 |
. 2
β’ (π β (SubRingβπ) β
(.rβπ) =
(.rβ(π
βΎs π))) |
20 | | eqid 2187 |
. . 3
β’
(1rβπ) = (1rβπ) |
21 | 16, 20 | subrg1 13451 |
. 2
β’ (π β (SubRingβπ) β
(1rβπ) =
(1rβ(π
βΎs π))) |
22 | 16 | subrgring 13444 |
. 2
β’ (π β (SubRingβπ) β (π βΎs π) β Ring) |
23 | 5 | ringgrpd 13257 |
. . 3
β’ (π β (SubRingβπ) β π β Grp) |
24 | 7 | oveqdr 5916 |
. . . 4
β’ ((π β (SubRingβπ) β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ))) β (π₯(+gβπ)π¦) = (π₯(+gβπ΄)π¦)) |
25 | 11, 6, 24 | grppropd 12915 |
. . 3
β’ (π β (SubRingβπ) β (π β Grp β π΄ β Grp)) |
26 | 23, 25 | mpbid 147 |
. 2
β’ (π β (SubRingβπ) β π΄ β Grp) |
27 | 5 | 3ad2ant1 1019 |
. . 3
β’ ((π β (SubRingβπ) β§ π₯ β (π β© (Baseβπ)) β§ π¦ β (Baseβπ)) β π β Ring) |
28 | | elinel2 3334 |
. . . 4
β’ (π₯ β (π β© (Baseβπ)) β π₯ β (Baseβπ)) |
29 | 28 | 3ad2ant2 1020 |
. . 3
β’ ((π β (SubRingβπ) β§ π₯ β (π β© (Baseβπ)) β§ π¦ β (Baseβπ)) β π₯ β (Baseβπ)) |
30 | | simp3 1000 |
. . 3
β’ ((π β (SubRingβπ) β§ π₯ β (π β© (Baseβπ)) β§ π¦ β (Baseβπ)) β π¦ β (Baseβπ)) |
31 | 3, 17 | ringcl 13265 |
. . 3
β’ ((π β Ring β§ π₯ β (Baseβπ) β§ π¦ β (Baseβπ)) β (π₯(.rβπ)π¦) β (Baseβπ)) |
32 | 27, 29, 30, 31 | syl3anc 1248 |
. 2
β’ ((π β (SubRingβπ) β§ π₯ β (π β© (Baseβπ)) β§ π¦ β (Baseβπ)) β (π₯(.rβπ)π¦) β (Baseβπ)) |
33 | 5 | adantr 276 |
. . 3
β’ ((π β (SubRingβπ) β§ (π₯ β (π β© (Baseβπ)) β§ π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β π β Ring) |
34 | | simpr1 1004 |
. . . 4
β’ ((π β (SubRingβπ) β§ (π₯ β (π β© (Baseβπ)) β§ π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β π₯ β (π β© (Baseβπ))) |
35 | 34 | elin2d 3337 |
. . 3
β’ ((π β (SubRingβπ) β§ (π₯ β (π β© (Baseβπ)) β§ π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β π₯ β (Baseβπ)) |
36 | | simpr2 1005 |
. . 3
β’ ((π β (SubRingβπ) β§ (π₯ β (π β© (Baseβπ)) β§ π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β π¦ β (Baseβπ)) |
37 | | simpr3 1006 |
. . 3
β’ ((π β (SubRingβπ) β§ (π₯ β (π β© (Baseβπ)) β§ π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β π§ β (Baseβπ)) |
38 | | eqid 2187 |
. . . 4
β’
(+gβπ) = (+gβπ) |
39 | 3, 38, 17 | ringdi 13270 |
. . 3
β’ ((π β Ring β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β (π₯(.rβπ)(π¦(+gβπ)π§)) = ((π₯(.rβπ)π¦)(+gβπ)(π₯(.rβπ)π§))) |
40 | 33, 35, 36, 37, 39 | syl13anc 1250 |
. 2
β’ ((π β (SubRingβπ) β§ (π₯ β (π β© (Baseβπ)) β§ π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β (π₯(.rβπ)(π¦(+gβπ)π§)) = ((π₯(.rβπ)π¦)(+gβπ)(π₯(.rβπ)π§))) |
41 | 5 | adantr 276 |
. . 3
β’ ((π β (SubRingβπ) β§ (π₯ β (π β© (Baseβπ)) β§ π¦ β (π β© (Baseβπ)) β§ π§ β (Baseβπ))) β π β Ring) |
42 | | simpr1 1004 |
. . . 4
β’ ((π β (SubRingβπ) β§ (π₯ β (π β© (Baseβπ)) β§ π¦ β (π β© (Baseβπ)) β§ π§ β (Baseβπ))) β π₯ β (π β© (Baseβπ))) |
43 | 42 | elin2d 3337 |
. . 3
β’ ((π β (SubRingβπ) β§ (π₯ β (π β© (Baseβπ)) β§ π¦ β (π β© (Baseβπ)) β§ π§ β (Baseβπ))) β π₯ β (Baseβπ)) |
44 | | simpr2 1005 |
. . . 4
β’ ((π β (SubRingβπ) β§ (π₯ β (π β© (Baseβπ)) β§ π¦ β (π β© (Baseβπ)) β§ π§ β (Baseβπ))) β π¦ β (π β© (Baseβπ))) |
45 | 44 | elin2d 3337 |
. . 3
β’ ((π β (SubRingβπ) β§ (π₯ β (π β© (Baseβπ)) β§ π¦ β (π β© (Baseβπ)) β§ π§ β (Baseβπ))) β π¦ β (Baseβπ)) |
46 | | simpr3 1006 |
. . 3
β’ ((π β (SubRingβπ) β§ (π₯ β (π β© (Baseβπ)) β§ π¦ β (π β© (Baseβπ)) β§ π§ β (Baseβπ))) β π§ β (Baseβπ)) |
47 | 3, 38, 17 | ringdir 13271 |
. . 3
β’ ((π β Ring β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β ((π₯(+gβπ)π¦)(.rβπ)π§) = ((π₯(.rβπ)π§)(+gβπ)(π¦(.rβπ)π§))) |
48 | 41, 43, 45, 46, 47 | syl13anc 1250 |
. 2
β’ ((π β (SubRingβπ) β§ (π₯ β (π β© (Baseβπ)) β§ π¦ β (π β© (Baseβπ)) β§ π§ β (Baseβπ))) β ((π₯(+gβπ)π¦)(.rβπ)π§) = ((π₯(.rβπ)π§)(+gβπ)(π¦(.rβπ)π§))) |
49 | 3, 17 | ringass 13268 |
. . 3
β’ ((π β Ring β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β ((π₯(.rβπ)π¦)(.rβπ)π§) = (π₯(.rβπ)(π¦(.rβπ)π§))) |
50 | 41, 43, 45, 46, 49 | syl13anc 1250 |
. 2
β’ ((π β (SubRingβπ) β§ (π₯ β (π β© (Baseβπ)) β§ π¦ β (π β© (Baseβπ)) β§ π§ β (Baseβπ))) β ((π₯(.rβπ)π¦)(.rβπ)π§) = (π₯(.rβπ)(π¦(.rβπ)π§))) |
51 | 3, 17, 20 | ringlidm 13275 |
. . 3
β’ ((π β Ring β§ π₯ β (Baseβπ)) β
((1rβπ)(.rβπ)π₯) = π₯) |
52 | 5, 51 | sylan 283 |
. 2
β’ ((π β (SubRingβπ) β§ π₯ β (Baseβπ)) β ((1rβπ)(.rβπ)π₯) = π₯) |
53 | 6, 7, 8, 9, 13, 15, 19, 21, 22, 26, 32, 40, 48, 50, 52 | islmodd 13482 |
1
β’ (π β (SubRingβπ) β π΄ β LMod) |