Step | Hyp | Ref
| Expression |
1 | | sralmod.a |
. . . 4
β’ π΄ = ((subringAlg βπ)βπ) |
2 | 1 | a1i 11 |
. . 3
β’ (π β (SubRingβπ) β π΄ = ((subringAlg βπ)βπ)) |
3 | | eqid 2726 |
. . . 4
β’
(Baseβπ) =
(Baseβπ) |
4 | 3 | subrgss 20471 |
. . 3
β’ (π β (SubRingβπ) β π β (Baseβπ)) |
5 | 2, 4 | srabase 21023 |
. 2
β’ (π β (SubRingβπ) β (Baseβπ) = (Baseβπ΄)) |
6 | 2, 4 | sraaddg 21025 |
. 2
β’ (π β (SubRingβπ) β
(+gβπ) =
(+gβπ΄)) |
7 | 2, 4 | srasca 21029 |
. 2
β’ (π β (SubRingβπ) β (π βΎs π) = (Scalarβπ΄)) |
8 | 2, 4 | sravsca 21031 |
. 2
β’ (π β (SubRingβπ) β
(.rβπ) = (
Β·π βπ΄)) |
9 | | eqid 2726 |
. . 3
β’ (π βΎs π) = (π βΎs π) |
10 | 9, 3 | ressbas 17185 |
. 2
β’ (π β (SubRingβπ) β (π β© (Baseβπ)) = (Baseβ(π βΎs π))) |
11 | | eqid 2726 |
. . 3
β’
(+gβπ) = (+gβπ) |
12 | 9, 11 | ressplusg 17241 |
. 2
β’ (π β (SubRingβπ) β
(+gβπ) =
(+gβ(π
βΎs π))) |
13 | | eqid 2726 |
. . 3
β’
(.rβπ) = (.rβπ) |
14 | 9, 13 | ressmulr 17258 |
. 2
β’ (π β (SubRingβπ) β
(.rβπ) =
(.rβ(π
βΎs π))) |
15 | | eqid 2726 |
. . 3
β’
(1rβπ) = (1rβπ) |
16 | 9, 15 | subrg1 20481 |
. 2
β’ (π β (SubRingβπ) β
(1rβπ) =
(1rβ(π
βΎs π))) |
17 | 9 | subrgring 20473 |
. 2
β’ (π β (SubRingβπ) β (π βΎs π) β Ring) |
18 | | subrgrcl 20475 |
. . . 4
β’ (π β (SubRingβπ) β π β Ring) |
19 | | ringgrp 20140 |
. . . 4
β’ (π β Ring β π β Grp) |
20 | 18, 19 | syl 17 |
. . 3
β’ (π β (SubRingβπ) β π β Grp) |
21 | | eqidd 2727 |
. . . 4
β’ (π β (SubRingβπ) β (Baseβπ) = (Baseβπ)) |
22 | 6 | oveqdr 7432 |
. . . 4
β’ ((π β (SubRingβπ) β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ))) β (π₯(+gβπ)π¦) = (π₯(+gβπ΄)π¦)) |
23 | 21, 5, 22 | grppropd 18878 |
. . 3
β’ (π β (SubRingβπ) β (π β Grp β π΄ β Grp)) |
24 | 20, 23 | mpbid 231 |
. 2
β’ (π β (SubRingβπ) β π΄ β Grp) |
25 | 18 | 3ad2ant1 1130 |
. . 3
β’ ((π β (SubRingβπ) β§ π₯ β (π β© (Baseβπ)) β§ π¦ β (Baseβπ)) β π β Ring) |
26 | | elinel2 4191 |
. . . 4
β’ (π₯ β (π β© (Baseβπ)) β π₯ β (Baseβπ)) |
27 | 26 | 3ad2ant2 1131 |
. . 3
β’ ((π β (SubRingβπ) β§ π₯ β (π β© (Baseβπ)) β§ π¦ β (Baseβπ)) β π₯ β (Baseβπ)) |
28 | | simp3 1135 |
. . 3
β’ ((π β (SubRingβπ) β§ π₯ β (π β© (Baseβπ)) β§ π¦ β (Baseβπ)) β π¦ β (Baseβπ)) |
29 | 3, 13 | ringcl 20152 |
. . 3
β’ ((π β Ring β§ π₯ β (Baseβπ) β§ π¦ β (Baseβπ)) β (π₯(.rβπ)π¦) β (Baseβπ)) |
30 | 25, 27, 28, 29 | syl3anc 1368 |
. 2
β’ ((π β (SubRingβπ) β§ π₯ β (π β© (Baseβπ)) β§ π¦ β (Baseβπ)) β (π₯(.rβπ)π¦) β (Baseβπ)) |
31 | 18 | adantr 480 |
. . 3
β’ ((π β (SubRingβπ) β§ (π₯ β (π β© (Baseβπ)) β§ π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β π β Ring) |
32 | | simpr1 1191 |
. . . 4
β’ ((π β (SubRingβπ) β§ (π₯ β (π β© (Baseβπ)) β§ π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β π₯ β (π β© (Baseβπ))) |
33 | 32 | elin2d 4194 |
. . 3
β’ ((π β (SubRingβπ) β§ (π₯ β (π β© (Baseβπ)) β§ π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β π₯ β (Baseβπ)) |
34 | | simpr2 1192 |
. . 3
β’ ((π β (SubRingβπ) β§ (π₯ β (π β© (Baseβπ)) β§ π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β π¦ β (Baseβπ)) |
35 | | simpr3 1193 |
. . 3
β’ ((π β (SubRingβπ) β§ (π₯ β (π β© (Baseβπ)) β§ π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β π§ β (Baseβπ)) |
36 | 3, 11, 13 | ringdi 20160 |
. . 3
β’ ((π β Ring β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β (π₯(.rβπ)(π¦(+gβπ)π§)) = ((π₯(.rβπ)π¦)(+gβπ)(π₯(.rβπ)π§))) |
37 | 31, 33, 34, 35, 36 | syl13anc 1369 |
. 2
β’ ((π β (SubRingβπ) β§ (π₯ β (π β© (Baseβπ)) β§ π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β (π₯(.rβπ)(π¦(+gβπ)π§)) = ((π₯(.rβπ)π¦)(+gβπ)(π₯(.rβπ)π§))) |
38 | 18 | adantr 480 |
. . 3
β’ ((π β (SubRingβπ) β§ (π₯ β (π β© (Baseβπ)) β§ π¦ β (π β© (Baseβπ)) β§ π§ β (Baseβπ))) β π β Ring) |
39 | | simpr1 1191 |
. . . 4
β’ ((π β (SubRingβπ) β§ (π₯ β (π β© (Baseβπ)) β§ π¦ β (π β© (Baseβπ)) β§ π§ β (Baseβπ))) β π₯ β (π β© (Baseβπ))) |
40 | 39 | elin2d 4194 |
. . 3
β’ ((π β (SubRingβπ) β§ (π₯ β (π β© (Baseβπ)) β§ π¦ β (π β© (Baseβπ)) β§ π§ β (Baseβπ))) β π₯ β (Baseβπ)) |
41 | | simpr2 1192 |
. . . 4
β’ ((π β (SubRingβπ) β§ (π₯ β (π β© (Baseβπ)) β§ π¦ β (π β© (Baseβπ)) β§ π§ β (Baseβπ))) β π¦ β (π β© (Baseβπ))) |
42 | 41 | elin2d 4194 |
. . 3
β’ ((π β (SubRingβπ) β§ (π₯ β (π β© (Baseβπ)) β§ π¦ β (π β© (Baseβπ)) β§ π§ β (Baseβπ))) β π¦ β (Baseβπ)) |
43 | | simpr3 1193 |
. . 3
β’ ((π β (SubRingβπ) β§ (π₯ β (π β© (Baseβπ)) β§ π¦ β (π β© (Baseβπ)) β§ π§ β (Baseβπ))) β π§ β (Baseβπ)) |
44 | 3, 11, 13 | ringdir 20161 |
. . 3
β’ ((π β Ring β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β ((π₯(+gβπ)π¦)(.rβπ)π§) = ((π₯(.rβπ)π§)(+gβπ)(π¦(.rβπ)π§))) |
45 | 38, 40, 42, 43, 44 | syl13anc 1369 |
. 2
β’ ((π β (SubRingβπ) β§ (π₯ β (π β© (Baseβπ)) β§ π¦ β (π β© (Baseβπ)) β§ π§ β (Baseβπ))) β ((π₯(+gβπ)π¦)(.rβπ)π§) = ((π₯(.rβπ)π§)(+gβπ)(π¦(.rβπ)π§))) |
46 | 3, 13 | ringass 20155 |
. . 3
β’ ((π β Ring β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β ((π₯(.rβπ)π¦)(.rβπ)π§) = (π₯(.rβπ)(π¦(.rβπ)π§))) |
47 | 38, 40, 42, 43, 46 | syl13anc 1369 |
. 2
β’ ((π β (SubRingβπ) β§ (π₯ β (π β© (Baseβπ)) β§ π¦ β (π β© (Baseβπ)) β§ π§ β (Baseβπ))) β ((π₯(.rβπ)π¦)(.rβπ)π§) = (π₯(.rβπ)(π¦(.rβπ)π§))) |
48 | 3, 13, 15 | ringlidm 20165 |
. . 3
β’ ((π β Ring β§ π₯ β (Baseβπ)) β
((1rβπ)(.rβπ)π₯) = π₯) |
49 | 18, 48 | sylan 579 |
. 2
β’ ((π β (SubRingβπ) β§ π₯ β (Baseβπ)) β ((1rβπ)(.rβπ)π₯) = π₯) |
50 | 5, 6, 7, 8, 10, 12, 14, 16, 17, 24, 30, 37, 45, 47, 49 | islmodd 20709 |
1
β’ (π β (SubRingβπ) β π΄ β LMod) |