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) |