Step | Hyp | Ref
| Expression |
1 | | sralmod.a |
. . . 4
⊢ 𝐴 = ((subringAlg ‘𝑊)‘𝑆) |
2 | 1 | a1i 11 |
. . 3
⊢ (𝑆 ∈ (SubRing‘𝑊) → 𝐴 = ((subringAlg ‘𝑊)‘𝑆)) |
3 | | eqid 2622 |
. . . 4
⊢
(Base‘𝑊) =
(Base‘𝑊) |
4 | 3 | subrgss 18781 |
. . 3
⊢ (𝑆 ∈ (SubRing‘𝑊) → 𝑆 ⊆ (Base‘𝑊)) |
5 | 2, 4 | srabase 19178 |
. 2
⊢ (𝑆 ∈ (SubRing‘𝑊) → (Base‘𝑊) = (Base‘𝐴)) |
6 | 2, 4 | sraaddg 19179 |
. 2
⊢ (𝑆 ∈ (SubRing‘𝑊) →
(+g‘𝑊) =
(+g‘𝐴)) |
7 | 2, 4 | srasca 19181 |
. 2
⊢ (𝑆 ∈ (SubRing‘𝑊) → (𝑊 ↾s 𝑆) = (Scalar‘𝐴)) |
8 | 2, 4 | sravsca 19182 |
. 2
⊢ (𝑆 ∈ (SubRing‘𝑊) →
(.r‘𝑊) = (
·𝑠 ‘𝐴)) |
9 | | eqid 2622 |
. . 3
⊢ (𝑊 ↾s 𝑆) = (𝑊 ↾s 𝑆) |
10 | 9, 3 | ressbas 15930 |
. 2
⊢ (𝑆 ∈ (SubRing‘𝑊) → (𝑆 ∩ (Base‘𝑊)) = (Base‘(𝑊 ↾s 𝑆))) |
11 | | eqid 2622 |
. . 3
⊢
(+g‘𝑊) = (+g‘𝑊) |
12 | 9, 11 | ressplusg 15993 |
. 2
⊢ (𝑆 ∈ (SubRing‘𝑊) →
(+g‘𝑊) =
(+g‘(𝑊
↾s 𝑆))) |
13 | | eqid 2622 |
. . 3
⊢
(.r‘𝑊) = (.r‘𝑊) |
14 | 9, 13 | ressmulr 16006 |
. 2
⊢ (𝑆 ∈ (SubRing‘𝑊) →
(.r‘𝑊) =
(.r‘(𝑊
↾s 𝑆))) |
15 | | eqid 2622 |
. . 3
⊢
(1r‘𝑊) = (1r‘𝑊) |
16 | 9, 15 | subrg1 18790 |
. 2
⊢ (𝑆 ∈ (SubRing‘𝑊) →
(1r‘𝑊) =
(1r‘(𝑊
↾s 𝑆))) |
17 | 9 | subrgring 18783 |
. 2
⊢ (𝑆 ∈ (SubRing‘𝑊) → (𝑊 ↾s 𝑆) ∈ Ring) |
18 | | subrgrcl 18785 |
. . . 4
⊢ (𝑆 ∈ (SubRing‘𝑊) → 𝑊 ∈ Ring) |
19 | | ringgrp 18552 |
. . . 4
⊢ (𝑊 ∈ Ring → 𝑊 ∈ Grp) |
20 | 18, 19 | syl 17 |
. . 3
⊢ (𝑆 ∈ (SubRing‘𝑊) → 𝑊 ∈ Grp) |
21 | | eqidd 2623 |
. . . 4
⊢ (𝑆 ∈ (SubRing‘𝑊) → (Base‘𝑊) = (Base‘𝑊)) |
22 | 6 | oveqdr 6674 |
. . . 4
⊢ ((𝑆 ∈ (SubRing‘𝑊) ∧ (𝑥 ∈ (Base‘𝑊) ∧ 𝑦 ∈ (Base‘𝑊))) → (𝑥(+g‘𝑊)𝑦) = (𝑥(+g‘𝐴)𝑦)) |
23 | 21, 5, 22 | grppropd 17437 |
. . 3
⊢ (𝑆 ∈ (SubRing‘𝑊) → (𝑊 ∈ Grp ↔ 𝐴 ∈ Grp)) |
24 | 20, 23 | mpbid 222 |
. 2
⊢ (𝑆 ∈ (SubRing‘𝑊) → 𝐴 ∈ Grp) |
25 | 18 | 3ad2ant1 1082 |
. . 3
⊢ ((𝑆 ∈ (SubRing‘𝑊) ∧ 𝑥 ∈ (𝑆 ∩ (Base‘𝑊)) ∧ 𝑦 ∈ (Base‘𝑊)) → 𝑊 ∈ Ring) |
26 | | inss2 3834 |
. . . . 5
⊢ (𝑆 ∩ (Base‘𝑊)) ⊆ (Base‘𝑊) |
27 | 26 | sseli 3599 |
. . . 4
⊢ (𝑥 ∈ (𝑆 ∩ (Base‘𝑊)) → 𝑥 ∈ (Base‘𝑊)) |
28 | 27 | 3ad2ant2 1083 |
. . 3
⊢ ((𝑆 ∈ (SubRing‘𝑊) ∧ 𝑥 ∈ (𝑆 ∩ (Base‘𝑊)) ∧ 𝑦 ∈ (Base‘𝑊)) → 𝑥 ∈ (Base‘𝑊)) |
29 | | simp3 1063 |
. . 3
⊢ ((𝑆 ∈ (SubRing‘𝑊) ∧ 𝑥 ∈ (𝑆 ∩ (Base‘𝑊)) ∧ 𝑦 ∈ (Base‘𝑊)) → 𝑦 ∈ (Base‘𝑊)) |
30 | 3, 13 | ringcl 18561 |
. . 3
⊢ ((𝑊 ∈ Ring ∧ 𝑥 ∈ (Base‘𝑊) ∧ 𝑦 ∈ (Base‘𝑊)) → (𝑥(.r‘𝑊)𝑦) ∈ (Base‘𝑊)) |
31 | 25, 28, 29, 30 | syl3anc 1326 |
. 2
⊢ ((𝑆 ∈ (SubRing‘𝑊) ∧ 𝑥 ∈ (𝑆 ∩ (Base‘𝑊)) ∧ 𝑦 ∈ (Base‘𝑊)) → (𝑥(.r‘𝑊)𝑦) ∈ (Base‘𝑊)) |
32 | 18 | adantr 481 |
. . 3
⊢ ((𝑆 ∈ (SubRing‘𝑊) ∧ (𝑥 ∈ (𝑆 ∩ (Base‘𝑊)) ∧ 𝑦 ∈ (Base‘𝑊) ∧ 𝑧 ∈ (Base‘𝑊))) → 𝑊 ∈ Ring) |
33 | | simpr1 1067 |
. . . 4
⊢ ((𝑆 ∈ (SubRing‘𝑊) ∧ (𝑥 ∈ (𝑆 ∩ (Base‘𝑊)) ∧ 𝑦 ∈ (Base‘𝑊) ∧ 𝑧 ∈ (Base‘𝑊))) → 𝑥 ∈ (𝑆 ∩ (Base‘𝑊))) |
34 | 26, 33 | sseldi 3601 |
. . 3
⊢ ((𝑆 ∈ (SubRing‘𝑊) ∧ (𝑥 ∈ (𝑆 ∩ (Base‘𝑊)) ∧ 𝑦 ∈ (Base‘𝑊) ∧ 𝑧 ∈ (Base‘𝑊))) → 𝑥 ∈ (Base‘𝑊)) |
35 | | simpr2 1068 |
. . 3
⊢ ((𝑆 ∈ (SubRing‘𝑊) ∧ (𝑥 ∈ (𝑆 ∩ (Base‘𝑊)) ∧ 𝑦 ∈ (Base‘𝑊) ∧ 𝑧 ∈ (Base‘𝑊))) → 𝑦 ∈ (Base‘𝑊)) |
36 | | simpr3 1069 |
. . 3
⊢ ((𝑆 ∈ (SubRing‘𝑊) ∧ (𝑥 ∈ (𝑆 ∩ (Base‘𝑊)) ∧ 𝑦 ∈ (Base‘𝑊) ∧ 𝑧 ∈ (Base‘𝑊))) → 𝑧 ∈ (Base‘𝑊)) |
37 | 3, 11, 13 | ringdi 18566 |
. . 3
⊢ ((𝑊 ∈ Ring ∧ (𝑥 ∈ (Base‘𝑊) ∧ 𝑦 ∈ (Base‘𝑊) ∧ 𝑧 ∈ (Base‘𝑊))) → (𝑥(.r‘𝑊)(𝑦(+g‘𝑊)𝑧)) = ((𝑥(.r‘𝑊)𝑦)(+g‘𝑊)(𝑥(.r‘𝑊)𝑧))) |
38 | 32, 34, 35, 36, 37 | syl13anc 1328 |
. 2
⊢ ((𝑆 ∈ (SubRing‘𝑊) ∧ (𝑥 ∈ (𝑆 ∩ (Base‘𝑊)) ∧ 𝑦 ∈ (Base‘𝑊) ∧ 𝑧 ∈ (Base‘𝑊))) → (𝑥(.r‘𝑊)(𝑦(+g‘𝑊)𝑧)) = ((𝑥(.r‘𝑊)𝑦)(+g‘𝑊)(𝑥(.r‘𝑊)𝑧))) |
39 | 18 | adantr 481 |
. . 3
⊢ ((𝑆 ∈ (SubRing‘𝑊) ∧ (𝑥 ∈ (𝑆 ∩ (Base‘𝑊)) ∧ 𝑦 ∈ (𝑆 ∩ (Base‘𝑊)) ∧ 𝑧 ∈ (Base‘𝑊))) → 𝑊 ∈ Ring) |
40 | | simpr1 1067 |
. . . 4
⊢ ((𝑆 ∈ (SubRing‘𝑊) ∧ (𝑥 ∈ (𝑆 ∩ (Base‘𝑊)) ∧ 𝑦 ∈ (𝑆 ∩ (Base‘𝑊)) ∧ 𝑧 ∈ (Base‘𝑊))) → 𝑥 ∈ (𝑆 ∩ (Base‘𝑊))) |
41 | 26, 40 | sseldi 3601 |
. . 3
⊢ ((𝑆 ∈ (SubRing‘𝑊) ∧ (𝑥 ∈ (𝑆 ∩ (Base‘𝑊)) ∧ 𝑦 ∈ (𝑆 ∩ (Base‘𝑊)) ∧ 𝑧 ∈ (Base‘𝑊))) → 𝑥 ∈ (Base‘𝑊)) |
42 | | simpr2 1068 |
. . . 4
⊢ ((𝑆 ∈ (SubRing‘𝑊) ∧ (𝑥 ∈ (𝑆 ∩ (Base‘𝑊)) ∧ 𝑦 ∈ (𝑆 ∩ (Base‘𝑊)) ∧ 𝑧 ∈ (Base‘𝑊))) → 𝑦 ∈ (𝑆 ∩ (Base‘𝑊))) |
43 | 26, 42 | sseldi 3601 |
. . 3
⊢ ((𝑆 ∈ (SubRing‘𝑊) ∧ (𝑥 ∈ (𝑆 ∩ (Base‘𝑊)) ∧ 𝑦 ∈ (𝑆 ∩ (Base‘𝑊)) ∧ 𝑧 ∈ (Base‘𝑊))) → 𝑦 ∈ (Base‘𝑊)) |
44 | | simpr3 1069 |
. . 3
⊢ ((𝑆 ∈ (SubRing‘𝑊) ∧ (𝑥 ∈ (𝑆 ∩ (Base‘𝑊)) ∧ 𝑦 ∈ (𝑆 ∩ (Base‘𝑊)) ∧ 𝑧 ∈ (Base‘𝑊))) → 𝑧 ∈ (Base‘𝑊)) |
45 | 3, 11, 13 | ringdir 18567 |
. . 3
⊢ ((𝑊 ∈ Ring ∧ (𝑥 ∈ (Base‘𝑊) ∧ 𝑦 ∈ (Base‘𝑊) ∧ 𝑧 ∈ (Base‘𝑊))) → ((𝑥(+g‘𝑊)𝑦)(.r‘𝑊)𝑧) = ((𝑥(.r‘𝑊)𝑧)(+g‘𝑊)(𝑦(.r‘𝑊)𝑧))) |
46 | 39, 41, 43, 44, 45 | syl13anc 1328 |
. 2
⊢ ((𝑆 ∈ (SubRing‘𝑊) ∧ (𝑥 ∈ (𝑆 ∩ (Base‘𝑊)) ∧ 𝑦 ∈ (𝑆 ∩ (Base‘𝑊)) ∧ 𝑧 ∈ (Base‘𝑊))) → ((𝑥(+g‘𝑊)𝑦)(.r‘𝑊)𝑧) = ((𝑥(.r‘𝑊)𝑧)(+g‘𝑊)(𝑦(.r‘𝑊)𝑧))) |
47 | 3, 13 | ringass 18564 |
. . 3
⊢ ((𝑊 ∈ Ring ∧ (𝑥 ∈ (Base‘𝑊) ∧ 𝑦 ∈ (Base‘𝑊) ∧ 𝑧 ∈ (Base‘𝑊))) → ((𝑥(.r‘𝑊)𝑦)(.r‘𝑊)𝑧) = (𝑥(.r‘𝑊)(𝑦(.r‘𝑊)𝑧))) |
48 | 39, 41, 43, 44, 47 | syl13anc 1328 |
. 2
⊢ ((𝑆 ∈ (SubRing‘𝑊) ∧ (𝑥 ∈ (𝑆 ∩ (Base‘𝑊)) ∧ 𝑦 ∈ (𝑆 ∩ (Base‘𝑊)) ∧ 𝑧 ∈ (Base‘𝑊))) → ((𝑥(.r‘𝑊)𝑦)(.r‘𝑊)𝑧) = (𝑥(.r‘𝑊)(𝑦(.r‘𝑊)𝑧))) |
49 | 3, 13, 15 | ringlidm 18571 |
. . 3
⊢ ((𝑊 ∈ Ring ∧ 𝑥 ∈ (Base‘𝑊)) →
((1r‘𝑊)(.r‘𝑊)𝑥) = 𝑥) |
50 | 18, 49 | sylan 488 |
. 2
⊢ ((𝑆 ∈ (SubRing‘𝑊) ∧ 𝑥 ∈ (Base‘𝑊)) → ((1r‘𝑊)(.r‘𝑊)𝑥) = 𝑥) |
51 | 5, 6, 7, 8, 10, 12, 14, 16, 17, 24, 31, 38, 46, 48, 50 | islmodd 18869 |
1
⊢ (𝑆 ∈ (SubRing‘𝑊) → 𝐴 ∈ LMod) |