Step | Hyp | Ref
| Expression |
1 | | sraassab.s |
. . . . . . . 8
⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑊)) |
2 | | eqid 2728 |
. . . . . . . . 9
⊢
(Base‘𝑊) =
(Base‘𝑊) |
3 | 2 | subrgss 20511 |
. . . . . . . 8
⊢ (𝑆 ∈ (SubRing‘𝑊) → 𝑆 ⊆ (Base‘𝑊)) |
4 | 1, 3 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑆 ⊆ (Base‘𝑊)) |
5 | 4 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐴 ∈ AssAlg) → 𝑆 ⊆ (Base‘𝑊)) |
6 | 5 | sselda 3980 |
. . . . 5
⊢ (((𝜑 ∧ 𝐴 ∈ AssAlg) ∧ 𝑦 ∈ 𝑆) → 𝑦 ∈ (Base‘𝑊)) |
7 | | simpllr 775 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝐴 ∈ AssAlg) ∧ 𝑦 ∈ 𝑆) ∧ 𝑥 ∈ (Base‘𝑊)) → 𝐴 ∈ AssAlg) |
8 | | eqid 2728 |
. . . . . . . . . . . . . 14
⊢ (𝑊 ↾s 𝑆) = (𝑊 ↾s 𝑆) |
9 | 8 | subrgbas 20520 |
. . . . . . . . . . . . 13
⊢ (𝑆 ∈ (SubRing‘𝑊) → 𝑆 = (Base‘(𝑊 ↾s 𝑆))) |
10 | 1, 9 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑆 = (Base‘(𝑊 ↾s 𝑆))) |
11 | | sraassab.a |
. . . . . . . . . . . . . . 15
⊢ 𝐴 = ((subringAlg ‘𝑊)‘𝑆) |
12 | 11 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐴 = ((subringAlg ‘𝑊)‘𝑆)) |
13 | 12, 4 | srasca 21069 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑊 ↾s 𝑆) = (Scalar‘𝐴)) |
14 | 13 | fveq2d 6901 |
. . . . . . . . . . . 12
⊢ (𝜑 → (Base‘(𝑊 ↾s 𝑆)) =
(Base‘(Scalar‘𝐴))) |
15 | 10, 14 | eqtrd 2768 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑆 = (Base‘(Scalar‘𝐴))) |
16 | 15 | eqimssd 4036 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑆 ⊆ (Base‘(Scalar‘𝐴))) |
17 | 16 | sselda 3980 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → 𝑦 ∈ (Base‘(Scalar‘𝐴))) |
18 | 17 | ad4ant13 750 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝐴 ∈ AssAlg) ∧ 𝑦 ∈ 𝑆) ∧ 𝑥 ∈ (Base‘𝑊)) → 𝑦 ∈ (Base‘(Scalar‘𝐴))) |
19 | 12, 4 | srabase 21063 |
. . . . . . . . . . 11
⊢ (𝜑 → (Base‘𝑊) = (Base‘𝐴)) |
20 | 19 | eqimssd 4036 |
. . . . . . . . . 10
⊢ (𝜑 → (Base‘𝑊) ⊆ (Base‘𝐴)) |
21 | 20 | ad2antrr 725 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐴 ∈ AssAlg) ∧ 𝑦 ∈ 𝑆) → (Base‘𝑊) ⊆ (Base‘𝐴)) |
22 | 21 | sselda 3980 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝐴 ∈ AssAlg) ∧ 𝑦 ∈ 𝑆) ∧ 𝑥 ∈ (Base‘𝑊)) → 𝑥 ∈ (Base‘𝐴)) |
23 | | sraassab.w |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑊 ∈ Ring) |
24 | | eqid 2728 |
. . . . . . . . . . . 12
⊢
(1r‘𝑊) = (1r‘𝑊) |
25 | 2, 24 | ringidcl 20202 |
. . . . . . . . . . 11
⊢ (𝑊 ∈ Ring →
(1r‘𝑊)
∈ (Base‘𝑊)) |
26 | 23, 25 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (1r‘𝑊) ∈ (Base‘𝑊)) |
27 | 26, 19 | eleqtrd 2831 |
. . . . . . . . 9
⊢ (𝜑 → (1r‘𝑊) ∈ (Base‘𝐴)) |
28 | 27 | ad3antrrr 729 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝐴 ∈ AssAlg) ∧ 𝑦 ∈ 𝑆) ∧ 𝑥 ∈ (Base‘𝑊)) → (1r‘𝑊) ∈ (Base‘𝐴)) |
29 | | eqid 2728 |
. . . . . . . . 9
⊢
(Base‘𝐴) =
(Base‘𝐴) |
30 | | eqid 2728 |
. . . . . . . . 9
⊢
(Scalar‘𝐴) =
(Scalar‘𝐴) |
31 | | eqid 2728 |
. . . . . . . . 9
⊢
(Base‘(Scalar‘𝐴)) = (Base‘(Scalar‘𝐴)) |
32 | | eqid 2728 |
. . . . . . . . 9
⊢ (
·𝑠 ‘𝐴) = ( ·𝑠
‘𝐴) |
33 | | eqid 2728 |
. . . . . . . . 9
⊢
(.r‘𝐴) = (.r‘𝐴) |
34 | 29, 30, 31, 32, 33 | assaassr 21793 |
. . . . . . . 8
⊢ ((𝐴 ∈ AssAlg ∧ (𝑦 ∈
(Base‘(Scalar‘𝐴)) ∧ 𝑥 ∈ (Base‘𝐴) ∧ (1r‘𝑊) ∈ (Base‘𝐴))) → (𝑥(.r‘𝐴)(𝑦( ·𝑠
‘𝐴)(1r‘𝑊))) = (𝑦( ·𝑠
‘𝐴)(𝑥(.r‘𝐴)(1r‘𝑊)))) |
35 | 7, 18, 22, 28, 34 | syl13anc 1370 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝐴 ∈ AssAlg) ∧ 𝑦 ∈ 𝑆) ∧ 𝑥 ∈ (Base‘𝑊)) → (𝑥(.r‘𝐴)(𝑦( ·𝑠
‘𝐴)(1r‘𝑊))) = (𝑦( ·𝑠
‘𝐴)(𝑥(.r‘𝐴)(1r‘𝑊)))) |
36 | 12, 4 | sramulr 21067 |
. . . . . . . . . 10
⊢ (𝜑 → (.r‘𝑊) = (.r‘𝐴)) |
37 | 36 | ad3antrrr 729 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝐴 ∈ AssAlg) ∧ 𝑦 ∈ 𝑆) ∧ 𝑥 ∈ (Base‘𝑊)) → (.r‘𝑊) = (.r‘𝐴)) |
38 | 37 | oveqd 7437 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝐴 ∈ AssAlg) ∧ 𝑦 ∈ 𝑆) ∧ 𝑥 ∈ (Base‘𝑊)) → (𝑥(.r‘𝑊)(𝑦( ·𝑠
‘𝐴)(1r‘𝑊))) = (𝑥(.r‘𝐴)(𝑦( ·𝑠
‘𝐴)(1r‘𝑊)))) |
39 | 12, 4 | sravsca 21071 |
. . . . . . . . . . . 12
⊢ (𝜑 → (.r‘𝑊) = (
·𝑠 ‘𝐴)) |
40 | 39 | ad3antrrr 729 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝐴 ∈ AssAlg) ∧ 𝑦 ∈ 𝑆) ∧ 𝑥 ∈ (Base‘𝑊)) → (.r‘𝑊) = (
·𝑠 ‘𝐴)) |
41 | 40 | oveqd 7437 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝐴 ∈ AssAlg) ∧ 𝑦 ∈ 𝑆) ∧ 𝑥 ∈ (Base‘𝑊)) → (𝑦(.r‘𝑊)(1r‘𝑊)) = (𝑦( ·𝑠
‘𝐴)(1r‘𝑊))) |
42 | | eqid 2728 |
. . . . . . . . . . 11
⊢
(.r‘𝑊) = (.r‘𝑊) |
43 | 23 | ad3antrrr 729 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝐴 ∈ AssAlg) ∧ 𝑦 ∈ 𝑆) ∧ 𝑥 ∈ (Base‘𝑊)) → 𝑊 ∈ Ring) |
44 | 6 | adantr 480 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝐴 ∈ AssAlg) ∧ 𝑦 ∈ 𝑆) ∧ 𝑥 ∈ (Base‘𝑊)) → 𝑦 ∈ (Base‘𝑊)) |
45 | 2, 42, 24, 43, 44 | ringridmd 20209 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝐴 ∈ AssAlg) ∧ 𝑦 ∈ 𝑆) ∧ 𝑥 ∈ (Base‘𝑊)) → (𝑦(.r‘𝑊)(1r‘𝑊)) = 𝑦) |
46 | 41, 45 | eqtr3d 2770 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝐴 ∈ AssAlg) ∧ 𝑦 ∈ 𝑆) ∧ 𝑥 ∈ (Base‘𝑊)) → (𝑦( ·𝑠
‘𝐴)(1r‘𝑊)) = 𝑦) |
47 | 46 | oveq2d 7436 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝐴 ∈ AssAlg) ∧ 𝑦 ∈ 𝑆) ∧ 𝑥 ∈ (Base‘𝑊)) → (𝑥(.r‘𝑊)(𝑦( ·𝑠
‘𝐴)(1r‘𝑊))) = (𝑥(.r‘𝑊)𝑦)) |
48 | 38, 47 | eqtr3d 2770 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝐴 ∈ AssAlg) ∧ 𝑦 ∈ 𝑆) ∧ 𝑥 ∈ (Base‘𝑊)) → (𝑥(.r‘𝐴)(𝑦( ·𝑠
‘𝐴)(1r‘𝑊))) = (𝑥(.r‘𝑊)𝑦)) |
49 | 40 | oveqd 7437 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝐴 ∈ AssAlg) ∧ 𝑦 ∈ 𝑆) ∧ 𝑥 ∈ (Base‘𝑊)) → (𝑦(.r‘𝑊)(𝑥(.r‘𝐴)(1r‘𝑊))) = (𝑦( ·𝑠
‘𝐴)(𝑥(.r‘𝐴)(1r‘𝑊)))) |
50 | 37 | oveqd 7437 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝐴 ∈ AssAlg) ∧ 𝑦 ∈ 𝑆) ∧ 𝑥 ∈ (Base‘𝑊)) → (𝑥(.r‘𝑊)(1r‘𝑊)) = (𝑥(.r‘𝐴)(1r‘𝑊))) |
51 | | simpr 484 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝐴 ∈ AssAlg) ∧ 𝑦 ∈ 𝑆) ∧ 𝑥 ∈ (Base‘𝑊)) → 𝑥 ∈ (Base‘𝑊)) |
52 | 2, 42, 24, 43, 51 | ringridmd 20209 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝐴 ∈ AssAlg) ∧ 𝑦 ∈ 𝑆) ∧ 𝑥 ∈ (Base‘𝑊)) → (𝑥(.r‘𝑊)(1r‘𝑊)) = 𝑥) |
53 | 50, 52 | eqtr3d 2770 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝐴 ∈ AssAlg) ∧ 𝑦 ∈ 𝑆) ∧ 𝑥 ∈ (Base‘𝑊)) → (𝑥(.r‘𝐴)(1r‘𝑊)) = 𝑥) |
54 | 53 | oveq2d 7436 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝐴 ∈ AssAlg) ∧ 𝑦 ∈ 𝑆) ∧ 𝑥 ∈ (Base‘𝑊)) → (𝑦(.r‘𝑊)(𝑥(.r‘𝐴)(1r‘𝑊))) = (𝑦(.r‘𝑊)𝑥)) |
55 | 49, 54 | eqtr3d 2770 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝐴 ∈ AssAlg) ∧ 𝑦 ∈ 𝑆) ∧ 𝑥 ∈ (Base‘𝑊)) → (𝑦( ·𝑠
‘𝐴)(𝑥(.r‘𝐴)(1r‘𝑊))) = (𝑦(.r‘𝑊)𝑥)) |
56 | 35, 48, 55 | 3eqtr3rd 2777 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝐴 ∈ AssAlg) ∧ 𝑦 ∈ 𝑆) ∧ 𝑥 ∈ (Base‘𝑊)) → (𝑦(.r‘𝑊)𝑥) = (𝑥(.r‘𝑊)𝑦)) |
57 | 56 | ralrimiva 3143 |
. . . . 5
⊢ (((𝜑 ∧ 𝐴 ∈ AssAlg) ∧ 𝑦 ∈ 𝑆) → ∀𝑥 ∈ (Base‘𝑊)(𝑦(.r‘𝑊)𝑥) = (𝑥(.r‘𝑊)𝑦)) |
58 | | eqid 2728 |
. . . . . . 7
⊢
(mulGrp‘𝑊) =
(mulGrp‘𝑊) |
59 | 58, 2 | mgpbas 20080 |
. . . . . 6
⊢
(Base‘𝑊) =
(Base‘(mulGrp‘𝑊)) |
60 | 58, 42 | mgpplusg 20078 |
. . . . . 6
⊢
(.r‘𝑊) = (+g‘(mulGrp‘𝑊)) |
61 | | sraassab.z |
. . . . . 6
⊢ 𝑍 =
(Cntr‘(mulGrp‘𝑊)) |
62 | 59, 60, 61 | elcntr 19281 |
. . . . 5
⊢ (𝑦 ∈ 𝑍 ↔ (𝑦 ∈ (Base‘𝑊) ∧ ∀𝑥 ∈ (Base‘𝑊)(𝑦(.r‘𝑊)𝑥) = (𝑥(.r‘𝑊)𝑦))) |
63 | 6, 57, 62 | sylanbrc 582 |
. . . 4
⊢ (((𝜑 ∧ 𝐴 ∈ AssAlg) ∧ 𝑦 ∈ 𝑆) → 𝑦 ∈ 𝑍) |
64 | 63 | ex 412 |
. . 3
⊢ ((𝜑 ∧ 𝐴 ∈ AssAlg) → (𝑦 ∈ 𝑆 → 𝑦 ∈ 𝑍)) |
65 | 64 | ssrdv 3986 |
. 2
⊢ ((𝜑 ∧ 𝐴 ∈ AssAlg) → 𝑆 ⊆ 𝑍) |
66 | 19 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝑆 ⊆ 𝑍) → (Base‘𝑊) = (Base‘𝐴)) |
67 | 13 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝑆 ⊆ 𝑍) → (𝑊 ↾s 𝑆) = (Scalar‘𝐴)) |
68 | 10 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝑆 ⊆ 𝑍) → 𝑆 = (Base‘(𝑊 ↾s 𝑆))) |
69 | 39 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝑆 ⊆ 𝑍) → (.r‘𝑊) = (
·𝑠 ‘𝐴)) |
70 | 36 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝑆 ⊆ 𝑍) → (.r‘𝑊) = (.r‘𝐴)) |
71 | 11 | sralmod 21080 |
. . . . 5
⊢ (𝑆 ∈ (SubRing‘𝑊) → 𝐴 ∈ LMod) |
72 | 1, 71 | syl 17 |
. . . 4
⊢ (𝜑 → 𝐴 ∈ LMod) |
73 | 72 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝑆 ⊆ 𝑍) → 𝐴 ∈ LMod) |
74 | 11, 2 | sraring 21079 |
. . . . 5
⊢ ((𝑊 ∈ Ring ∧ 𝑆 ⊆ (Base‘𝑊)) → 𝐴 ∈ Ring) |
75 | 23, 4, 74 | syl2anc 583 |
. . . 4
⊢ (𝜑 → 𝐴 ∈ Ring) |
76 | 75 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝑆 ⊆ 𝑍) → 𝐴 ∈ Ring) |
77 | 23 | ad2antrr 725 |
. . . 4
⊢ (((𝜑 ∧ 𝑆 ⊆ 𝑍) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ (Base‘𝑊) ∧ 𝑧 ∈ (Base‘𝑊))) → 𝑊 ∈ Ring) |
78 | 4 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑆 ⊆ 𝑍) → 𝑆 ⊆ (Base‘𝑊)) |
79 | 78 | sselda 3980 |
. . . . 5
⊢ (((𝜑 ∧ 𝑆 ⊆ 𝑍) ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ (Base‘𝑊)) |
80 | 79 | 3ad2antr1 1186 |
. . . 4
⊢ (((𝜑 ∧ 𝑆 ⊆ 𝑍) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ (Base‘𝑊) ∧ 𝑧 ∈ (Base‘𝑊))) → 𝑥 ∈ (Base‘𝑊)) |
81 | | simpr2 1193 |
. . . 4
⊢ (((𝜑 ∧ 𝑆 ⊆ 𝑍) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ (Base‘𝑊) ∧ 𝑧 ∈ (Base‘𝑊))) → 𝑦 ∈ (Base‘𝑊)) |
82 | | simpr3 1194 |
. . . 4
⊢ (((𝜑 ∧ 𝑆 ⊆ 𝑍) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ (Base‘𝑊) ∧ 𝑧 ∈ (Base‘𝑊))) → 𝑧 ∈ (Base‘𝑊)) |
83 | 2, 42, 77, 80, 81, 82 | ringassd 20197 |
. . 3
⊢ (((𝜑 ∧ 𝑆 ⊆ 𝑍) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ (Base‘𝑊) ∧ 𝑧 ∈ (Base‘𝑊))) → ((𝑥(.r‘𝑊)𝑦)(.r‘𝑊)𝑧) = (𝑥(.r‘𝑊)(𝑦(.r‘𝑊)𝑧))) |
84 | | ssel2 3975 |
. . . . . . . 8
⊢ ((𝑆 ⊆ 𝑍 ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ 𝑍) |
85 | 84 | ad2ant2lr 747 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑆 ⊆ 𝑍) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ (Base‘𝑊))) → 𝑥 ∈ 𝑍) |
86 | | simprr 772 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑆 ⊆ 𝑍) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ (Base‘𝑊))) → 𝑦 ∈ (Base‘𝑊)) |
87 | 59, 60, 61 | cntri 19283 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝑍 ∧ 𝑦 ∈ (Base‘𝑊)) → (𝑥(.r‘𝑊)𝑦) = (𝑦(.r‘𝑊)𝑥)) |
88 | 85, 86, 87 | syl2anc 583 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑆 ⊆ 𝑍) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ (Base‘𝑊))) → (𝑥(.r‘𝑊)𝑦) = (𝑦(.r‘𝑊)𝑥)) |
89 | 88 | 3adantr3 1169 |
. . . . 5
⊢ (((𝜑 ∧ 𝑆 ⊆ 𝑍) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ (Base‘𝑊) ∧ 𝑧 ∈ (Base‘𝑊))) → (𝑥(.r‘𝑊)𝑦) = (𝑦(.r‘𝑊)𝑥)) |
90 | 89 | oveq1d 7435 |
. . . 4
⊢ (((𝜑 ∧ 𝑆 ⊆ 𝑍) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ (Base‘𝑊) ∧ 𝑧 ∈ (Base‘𝑊))) → ((𝑥(.r‘𝑊)𝑦)(.r‘𝑊)𝑧) = ((𝑦(.r‘𝑊)𝑥)(.r‘𝑊)𝑧)) |
91 | 2, 42, 77, 81, 80, 82 | ringassd 20197 |
. . . 4
⊢ (((𝜑 ∧ 𝑆 ⊆ 𝑍) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ (Base‘𝑊) ∧ 𝑧 ∈ (Base‘𝑊))) → ((𝑦(.r‘𝑊)𝑥)(.r‘𝑊)𝑧) = (𝑦(.r‘𝑊)(𝑥(.r‘𝑊)𝑧))) |
92 | 90, 83, 91 | 3eqtr3rd 2777 |
. . 3
⊢ (((𝜑 ∧ 𝑆 ⊆ 𝑍) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ (Base‘𝑊) ∧ 𝑧 ∈ (Base‘𝑊))) → (𝑦(.r‘𝑊)(𝑥(.r‘𝑊)𝑧)) = (𝑥(.r‘𝑊)(𝑦(.r‘𝑊)𝑧))) |
93 | 66, 67, 68, 69, 70, 73, 76, 83, 92 | isassad 21798 |
. 2
⊢ ((𝜑 ∧ 𝑆 ⊆ 𝑍) → 𝐴 ∈ AssAlg) |
94 | 65, 93 | impbida 800 |
1
⊢ (𝜑 → (𝐴 ∈ AssAlg ↔ 𝑆 ⊆ 𝑍)) |