Step | Hyp | Ref
| Expression |
1 | | sralmod.a |
. . . 4
⊢ 𝐴 = ((subringAlg ‘𝑊)‘𝑆) |
2 | 1 | a1i 11 |
. . 3
⊢ (𝑆 ∈ (SubRing‘𝑊) → 𝐴 = ((subringAlg ‘𝑊)‘𝑆)) |
3 | | eqid 2778 |
. . . 4
⊢
(Base‘𝑊) =
(Base‘𝑊) |
4 | 3 | subrgss 19173 |
. . 3
⊢ (𝑆 ∈ (SubRing‘𝑊) → 𝑆 ⊆ (Base‘𝑊)) |
5 | 2, 4 | srabase 19575 |
. 2
⊢ (𝑆 ∈ (SubRing‘𝑊) → (Base‘𝑊) = (Base‘𝐴)) |
6 | 2, 4 | sraaddg 19576 |
. 2
⊢ (𝑆 ∈ (SubRing‘𝑊) →
(+g‘𝑊) =
(+g‘𝐴)) |
7 | 2, 4 | srasca 19578 |
. 2
⊢ (𝑆 ∈ (SubRing‘𝑊) → (𝑊 ↾s 𝑆) = (Scalar‘𝐴)) |
8 | 2, 4 | sravsca 19579 |
. 2
⊢ (𝑆 ∈ (SubRing‘𝑊) →
(.r‘𝑊) = (
·𝑠 ‘𝐴)) |
9 | | eqid 2778 |
. . 3
⊢ (𝑊 ↾s 𝑆) = (𝑊 ↾s 𝑆) |
10 | 9, 3 | ressbas 16326 |
. 2
⊢ (𝑆 ∈ (SubRing‘𝑊) → (𝑆 ∩ (Base‘𝑊)) = (Base‘(𝑊 ↾s 𝑆))) |
11 | | eqid 2778 |
. . 3
⊢
(+g‘𝑊) = (+g‘𝑊) |
12 | 9, 11 | ressplusg 16385 |
. 2
⊢ (𝑆 ∈ (SubRing‘𝑊) →
(+g‘𝑊) =
(+g‘(𝑊
↾s 𝑆))) |
13 | | eqid 2778 |
. . 3
⊢
(.r‘𝑊) = (.r‘𝑊) |
14 | 9, 13 | ressmulr 16398 |
. 2
⊢ (𝑆 ∈ (SubRing‘𝑊) →
(.r‘𝑊) =
(.r‘(𝑊
↾s 𝑆))) |
15 | | eqid 2778 |
. . 3
⊢
(1r‘𝑊) = (1r‘𝑊) |
16 | 9, 15 | subrg1 19182 |
. 2
⊢ (𝑆 ∈ (SubRing‘𝑊) →
(1r‘𝑊) =
(1r‘(𝑊
↾s 𝑆))) |
17 | 9 | subrgring 19175 |
. 2
⊢ (𝑆 ∈ (SubRing‘𝑊) → (𝑊 ↾s 𝑆) ∈ Ring) |
18 | | subrgrcl 19177 |
. . . 4
⊢ (𝑆 ∈ (SubRing‘𝑊) → 𝑊 ∈ Ring) |
19 | | ringgrp 18939 |
. . . 4
⊢ (𝑊 ∈ Ring → 𝑊 ∈ Grp) |
20 | 18, 19 | syl 17 |
. . 3
⊢ (𝑆 ∈ (SubRing‘𝑊) → 𝑊 ∈ Grp) |
21 | | eqidd 2779 |
. . . 4
⊢ (𝑆 ∈ (SubRing‘𝑊) → (Base‘𝑊) = (Base‘𝑊)) |
22 | 6 | oveqdr 6950 |
. . . 4
⊢ ((𝑆 ∈ (SubRing‘𝑊) ∧ (𝑥 ∈ (Base‘𝑊) ∧ 𝑦 ∈ (Base‘𝑊))) → (𝑥(+g‘𝑊)𝑦) = (𝑥(+g‘𝐴)𝑦)) |
23 | 21, 5, 22 | grppropd 17824 |
. . 3
⊢ (𝑆 ∈ (SubRing‘𝑊) → (𝑊 ∈ Grp ↔ 𝐴 ∈ Grp)) |
24 | 20, 23 | mpbid 224 |
. 2
⊢ (𝑆 ∈ (SubRing‘𝑊) → 𝐴 ∈ Grp) |
25 | 18 | 3ad2ant1 1124 |
. . 3
⊢ ((𝑆 ∈ (SubRing‘𝑊) ∧ 𝑥 ∈ (𝑆 ∩ (Base‘𝑊)) ∧ 𝑦 ∈ (Base‘𝑊)) → 𝑊 ∈ Ring) |
26 | | inss2 4054 |
. . . . 5
⊢ (𝑆 ∩ (Base‘𝑊)) ⊆ (Base‘𝑊) |
27 | 26 | sseli 3817 |
. . . 4
⊢ (𝑥 ∈ (𝑆 ∩ (Base‘𝑊)) → 𝑥 ∈ (Base‘𝑊)) |
28 | 27 | 3ad2ant2 1125 |
. . 3
⊢ ((𝑆 ∈ (SubRing‘𝑊) ∧ 𝑥 ∈ (𝑆 ∩ (Base‘𝑊)) ∧ 𝑦 ∈ (Base‘𝑊)) → 𝑥 ∈ (Base‘𝑊)) |
29 | | simp3 1129 |
. . 3
⊢ ((𝑆 ∈ (SubRing‘𝑊) ∧ 𝑥 ∈ (𝑆 ∩ (Base‘𝑊)) ∧ 𝑦 ∈ (Base‘𝑊)) → 𝑦 ∈ (Base‘𝑊)) |
30 | 3, 13 | ringcl 18948 |
. . 3
⊢ ((𝑊 ∈ Ring ∧ 𝑥 ∈ (Base‘𝑊) ∧ 𝑦 ∈ (Base‘𝑊)) → (𝑥(.r‘𝑊)𝑦) ∈ (Base‘𝑊)) |
31 | 25, 28, 29, 30 | syl3anc 1439 |
. 2
⊢ ((𝑆 ∈ (SubRing‘𝑊) ∧ 𝑥 ∈ (𝑆 ∩ (Base‘𝑊)) ∧ 𝑦 ∈ (Base‘𝑊)) → (𝑥(.r‘𝑊)𝑦) ∈ (Base‘𝑊)) |
32 | 18 | adantr 474 |
. . 3
⊢ ((𝑆 ∈ (SubRing‘𝑊) ∧ (𝑥 ∈ (𝑆 ∩ (Base‘𝑊)) ∧ 𝑦 ∈ (Base‘𝑊) ∧ 𝑧 ∈ (Base‘𝑊))) → 𝑊 ∈ Ring) |
33 | | simpr1 1205 |
. . . 4
⊢ ((𝑆 ∈ (SubRing‘𝑊) ∧ (𝑥 ∈ (𝑆 ∩ (Base‘𝑊)) ∧ 𝑦 ∈ (Base‘𝑊) ∧ 𝑧 ∈ (Base‘𝑊))) → 𝑥 ∈ (𝑆 ∩ (Base‘𝑊))) |
34 | 26, 33 | sseldi 3819 |
. . 3
⊢ ((𝑆 ∈ (SubRing‘𝑊) ∧ (𝑥 ∈ (𝑆 ∩ (Base‘𝑊)) ∧ 𝑦 ∈ (Base‘𝑊) ∧ 𝑧 ∈ (Base‘𝑊))) → 𝑥 ∈ (Base‘𝑊)) |
35 | | simpr2 1207 |
. . 3
⊢ ((𝑆 ∈ (SubRing‘𝑊) ∧ (𝑥 ∈ (𝑆 ∩ (Base‘𝑊)) ∧ 𝑦 ∈ (Base‘𝑊) ∧ 𝑧 ∈ (Base‘𝑊))) → 𝑦 ∈ (Base‘𝑊)) |
36 | | simpr3 1209 |
. . 3
⊢ ((𝑆 ∈ (SubRing‘𝑊) ∧ (𝑥 ∈ (𝑆 ∩ (Base‘𝑊)) ∧ 𝑦 ∈ (Base‘𝑊) ∧ 𝑧 ∈ (Base‘𝑊))) → 𝑧 ∈ (Base‘𝑊)) |
37 | 3, 11, 13 | ringdi 18953 |
. . 3
⊢ ((𝑊 ∈ Ring ∧ (𝑥 ∈ (Base‘𝑊) ∧ 𝑦 ∈ (Base‘𝑊) ∧ 𝑧 ∈ (Base‘𝑊))) → (𝑥(.r‘𝑊)(𝑦(+g‘𝑊)𝑧)) = ((𝑥(.r‘𝑊)𝑦)(+g‘𝑊)(𝑥(.r‘𝑊)𝑧))) |
38 | 32, 34, 35, 36, 37 | syl13anc 1440 |
. 2
⊢ ((𝑆 ∈ (SubRing‘𝑊) ∧ (𝑥 ∈ (𝑆 ∩ (Base‘𝑊)) ∧ 𝑦 ∈ (Base‘𝑊) ∧ 𝑧 ∈ (Base‘𝑊))) → (𝑥(.r‘𝑊)(𝑦(+g‘𝑊)𝑧)) = ((𝑥(.r‘𝑊)𝑦)(+g‘𝑊)(𝑥(.r‘𝑊)𝑧))) |
39 | 18 | adantr 474 |
. . 3
⊢ ((𝑆 ∈ (SubRing‘𝑊) ∧ (𝑥 ∈ (𝑆 ∩ (Base‘𝑊)) ∧ 𝑦 ∈ (𝑆 ∩ (Base‘𝑊)) ∧ 𝑧 ∈ (Base‘𝑊))) → 𝑊 ∈ Ring) |
40 | | simpr1 1205 |
. . . 4
⊢ ((𝑆 ∈ (SubRing‘𝑊) ∧ (𝑥 ∈ (𝑆 ∩ (Base‘𝑊)) ∧ 𝑦 ∈ (𝑆 ∩ (Base‘𝑊)) ∧ 𝑧 ∈ (Base‘𝑊))) → 𝑥 ∈ (𝑆 ∩ (Base‘𝑊))) |
41 | 26, 40 | sseldi 3819 |
. . 3
⊢ ((𝑆 ∈ (SubRing‘𝑊) ∧ (𝑥 ∈ (𝑆 ∩ (Base‘𝑊)) ∧ 𝑦 ∈ (𝑆 ∩ (Base‘𝑊)) ∧ 𝑧 ∈ (Base‘𝑊))) → 𝑥 ∈ (Base‘𝑊)) |
42 | | simpr2 1207 |
. . . 4
⊢ ((𝑆 ∈ (SubRing‘𝑊) ∧ (𝑥 ∈ (𝑆 ∩ (Base‘𝑊)) ∧ 𝑦 ∈ (𝑆 ∩ (Base‘𝑊)) ∧ 𝑧 ∈ (Base‘𝑊))) → 𝑦 ∈ (𝑆 ∩ (Base‘𝑊))) |
43 | 26, 42 | sseldi 3819 |
. . 3
⊢ ((𝑆 ∈ (SubRing‘𝑊) ∧ (𝑥 ∈ (𝑆 ∩ (Base‘𝑊)) ∧ 𝑦 ∈ (𝑆 ∩ (Base‘𝑊)) ∧ 𝑧 ∈ (Base‘𝑊))) → 𝑦 ∈ (Base‘𝑊)) |
44 | | simpr3 1209 |
. . 3
⊢ ((𝑆 ∈ (SubRing‘𝑊) ∧ (𝑥 ∈ (𝑆 ∩ (Base‘𝑊)) ∧ 𝑦 ∈ (𝑆 ∩ (Base‘𝑊)) ∧ 𝑧 ∈ (Base‘𝑊))) → 𝑧 ∈ (Base‘𝑊)) |
45 | 3, 11, 13 | ringdir 18954 |
. . 3
⊢ ((𝑊 ∈ Ring ∧ (𝑥 ∈ (Base‘𝑊) ∧ 𝑦 ∈ (Base‘𝑊) ∧ 𝑧 ∈ (Base‘𝑊))) → ((𝑥(+g‘𝑊)𝑦)(.r‘𝑊)𝑧) = ((𝑥(.r‘𝑊)𝑧)(+g‘𝑊)(𝑦(.r‘𝑊)𝑧))) |
46 | 39, 41, 43, 44, 45 | syl13anc 1440 |
. 2
⊢ ((𝑆 ∈ (SubRing‘𝑊) ∧ (𝑥 ∈ (𝑆 ∩ (Base‘𝑊)) ∧ 𝑦 ∈ (𝑆 ∩ (Base‘𝑊)) ∧ 𝑧 ∈ (Base‘𝑊))) → ((𝑥(+g‘𝑊)𝑦)(.r‘𝑊)𝑧) = ((𝑥(.r‘𝑊)𝑧)(+g‘𝑊)(𝑦(.r‘𝑊)𝑧))) |
47 | 3, 13 | ringass 18951 |
. . 3
⊢ ((𝑊 ∈ Ring ∧ (𝑥 ∈ (Base‘𝑊) ∧ 𝑦 ∈ (Base‘𝑊) ∧ 𝑧 ∈ (Base‘𝑊))) → ((𝑥(.r‘𝑊)𝑦)(.r‘𝑊)𝑧) = (𝑥(.r‘𝑊)(𝑦(.r‘𝑊)𝑧))) |
48 | 39, 41, 43, 44, 47 | syl13anc 1440 |
. 2
⊢ ((𝑆 ∈ (SubRing‘𝑊) ∧ (𝑥 ∈ (𝑆 ∩ (Base‘𝑊)) ∧ 𝑦 ∈ (𝑆 ∩ (Base‘𝑊)) ∧ 𝑧 ∈ (Base‘𝑊))) → ((𝑥(.r‘𝑊)𝑦)(.r‘𝑊)𝑧) = (𝑥(.r‘𝑊)(𝑦(.r‘𝑊)𝑧))) |
49 | 3, 13, 15 | ringlidm 18958 |
. . 3
⊢ ((𝑊 ∈ Ring ∧ 𝑥 ∈ (Base‘𝑊)) →
((1r‘𝑊)(.r‘𝑊)𝑥) = 𝑥) |
50 | 18, 49 | sylan 575 |
. 2
⊢ ((𝑆 ∈ (SubRing‘𝑊) ∧ 𝑥 ∈ (Base‘𝑊)) → ((1r‘𝑊)(.r‘𝑊)𝑥) = 𝑥) |
51 | 5, 6, 7, 8, 10, 12, 14, 16, 17, 24, 31, 38, 46, 48, 50 | islmodd 19261 |
1
⊢ (𝑆 ∈ (SubRing‘𝑊) → 𝐴 ∈ LMod) |