Step | Hyp | Ref
| Expression |
1 | | simpl1 1057 |
. . . . . 6
⊢ (((𝑊 ∈ AssAlg ∧ 1 ∈ 𝐴 ∧ 𝐴 ⊆ 𝑉) ∧ 𝑆 ∈ AssAlg) → 𝑊 ∈ AssAlg) |
2 | | assaring 19141 |
. . . . . 6
⊢ (𝑊 ∈ AssAlg → 𝑊 ∈ Ring) |
3 | 1, 2 | syl 17 |
. . . . 5
⊢ (((𝑊 ∈ AssAlg ∧ 1 ∈ 𝐴 ∧ 𝐴 ⊆ 𝑉) ∧ 𝑆 ∈ AssAlg) → 𝑊 ∈ Ring) |
4 | | issubassa.s |
. . . . . 6
⊢ 𝑆 = (𝑊 ↾s 𝐴) |
5 | | assaring 19141 |
. . . . . . 7
⊢ (𝑆 ∈ AssAlg → 𝑆 ∈ Ring) |
6 | 5 | adantl 481 |
. . . . . 6
⊢ (((𝑊 ∈ AssAlg ∧ 1 ∈ 𝐴 ∧ 𝐴 ⊆ 𝑉) ∧ 𝑆 ∈ AssAlg) → 𝑆 ∈ Ring) |
7 | 4, 6 | syl5eqelr 2693 |
. . . . 5
⊢ (((𝑊 ∈ AssAlg ∧ 1 ∈ 𝐴 ∧ 𝐴 ⊆ 𝑉) ∧ 𝑆 ∈ AssAlg) → (𝑊 ↾s 𝐴) ∈ Ring) |
8 | 3, 7 | jca 553 |
. . . 4
⊢ (((𝑊 ∈ AssAlg ∧ 1 ∈ 𝐴 ∧ 𝐴 ⊆ 𝑉) ∧ 𝑆 ∈ AssAlg) → (𝑊 ∈ Ring ∧ (𝑊 ↾s 𝐴) ∈ Ring)) |
9 | | simpl3 1059 |
. . . . 5
⊢ (((𝑊 ∈ AssAlg ∧ 1 ∈ 𝐴 ∧ 𝐴 ⊆ 𝑉) ∧ 𝑆 ∈ AssAlg) → 𝐴 ⊆ 𝑉) |
10 | | simpl2 1058 |
. . . . 5
⊢ (((𝑊 ∈ AssAlg ∧ 1 ∈ 𝐴 ∧ 𝐴 ⊆ 𝑉) ∧ 𝑆 ∈ AssAlg) → 1 ∈ 𝐴) |
11 | 9, 10 | jca 553 |
. . . 4
⊢ (((𝑊 ∈ AssAlg ∧ 1 ∈ 𝐴 ∧ 𝐴 ⊆ 𝑉) ∧ 𝑆 ∈ AssAlg) → (𝐴 ⊆ 𝑉 ∧ 1 ∈ 𝐴)) |
12 | | issubassa.v |
. . . . 5
⊢ 𝑉 = (Base‘𝑊) |
13 | | issubassa.o |
. . . . 5
⊢ 1 =
(1r‘𝑊) |
14 | 12, 13 | issubrg 18603 |
. . . 4
⊢ (𝐴 ∈ (SubRing‘𝑊) ↔ ((𝑊 ∈ Ring ∧ (𝑊 ↾s 𝐴) ∈ Ring) ∧ (𝐴 ⊆ 𝑉 ∧ 1 ∈ 𝐴))) |
15 | 8, 11, 14 | sylanbrc 695 |
. . 3
⊢ (((𝑊 ∈ AssAlg ∧ 1 ∈ 𝐴 ∧ 𝐴 ⊆ 𝑉) ∧ 𝑆 ∈ AssAlg) → 𝐴 ∈ (SubRing‘𝑊)) |
16 | | assalmod 19140 |
. . . . 5
⊢ (𝑆 ∈ AssAlg → 𝑆 ∈ LMod) |
17 | 16 | adantl 481 |
. . . 4
⊢ (((𝑊 ∈ AssAlg ∧ 1 ∈ 𝐴 ∧ 𝐴 ⊆ 𝑉) ∧ 𝑆 ∈ AssAlg) → 𝑆 ∈ LMod) |
18 | | assalmod 19140 |
. . . . 5
⊢ (𝑊 ∈ AssAlg → 𝑊 ∈ LMod) |
19 | | issubassa.l |
. . . . . 6
⊢ 𝐿 = (LSubSp‘𝑊) |
20 | 4, 12, 19 | islss3 18780 |
. . . . 5
⊢ (𝑊 ∈ LMod → (𝐴 ∈ 𝐿 ↔ (𝐴 ⊆ 𝑉 ∧ 𝑆 ∈ LMod))) |
21 | 1, 18, 20 | 3syl 18 |
. . . 4
⊢ (((𝑊 ∈ AssAlg ∧ 1 ∈ 𝐴 ∧ 𝐴 ⊆ 𝑉) ∧ 𝑆 ∈ AssAlg) → (𝐴 ∈ 𝐿 ↔ (𝐴 ⊆ 𝑉 ∧ 𝑆 ∈ LMod))) |
22 | 9, 17, 21 | mpbir2and 959 |
. . 3
⊢ (((𝑊 ∈ AssAlg ∧ 1 ∈ 𝐴 ∧ 𝐴 ⊆ 𝑉) ∧ 𝑆 ∈ AssAlg) → 𝐴 ∈ 𝐿) |
23 | 15, 22 | jca 553 |
. 2
⊢ (((𝑊 ∈ AssAlg ∧ 1 ∈ 𝐴 ∧ 𝐴 ⊆ 𝑉) ∧ 𝑆 ∈ AssAlg) → (𝐴 ∈ (SubRing‘𝑊) ∧ 𝐴 ∈ 𝐿)) |
24 | 12 | subrgss 18604 |
. . . . . 6
⊢ (𝐴 ∈ (SubRing‘𝑊) → 𝐴 ⊆ 𝑉) |
25 | 24 | ad2antrl 760 |
. . . . 5
⊢ ((𝑊 ∈ AssAlg ∧ (𝐴 ∈ (SubRing‘𝑊) ∧ 𝐴 ∈ 𝐿)) → 𝐴 ⊆ 𝑉) |
26 | 4, 12 | ressbas2 15758 |
. . . . 5
⊢ (𝐴 ⊆ 𝑉 → 𝐴 = (Base‘𝑆)) |
27 | 25, 26 | syl 17 |
. . . 4
⊢ ((𝑊 ∈ AssAlg ∧ (𝐴 ∈ (SubRing‘𝑊) ∧ 𝐴 ∈ 𝐿)) → 𝐴 = (Base‘𝑆)) |
28 | | eqid 2610 |
. . . . . 6
⊢
(Scalar‘𝑊) =
(Scalar‘𝑊) |
29 | 4, 28 | resssca 15854 |
. . . . 5
⊢ (𝐴 ∈ (SubRing‘𝑊) → (Scalar‘𝑊) = (Scalar‘𝑆)) |
30 | 29 | ad2antrl 760 |
. . . 4
⊢ ((𝑊 ∈ AssAlg ∧ (𝐴 ∈ (SubRing‘𝑊) ∧ 𝐴 ∈ 𝐿)) → (Scalar‘𝑊) = (Scalar‘𝑆)) |
31 | | eqidd 2611 |
. . . 4
⊢ ((𝑊 ∈ AssAlg ∧ (𝐴 ∈ (SubRing‘𝑊) ∧ 𝐴 ∈ 𝐿)) → (Base‘(Scalar‘𝑊)) =
(Base‘(Scalar‘𝑊))) |
32 | | eqid 2610 |
. . . . . 6
⊢ (
·𝑠 ‘𝑊) = ( ·𝑠
‘𝑊) |
33 | 4, 32 | ressvsca 15855 |
. . . . 5
⊢ (𝐴 ∈ (SubRing‘𝑊) → (
·𝑠 ‘𝑊) = ( ·𝑠
‘𝑆)) |
34 | 33 | ad2antrl 760 |
. . . 4
⊢ ((𝑊 ∈ AssAlg ∧ (𝐴 ∈ (SubRing‘𝑊) ∧ 𝐴 ∈ 𝐿)) → (
·𝑠 ‘𝑊) = ( ·𝑠
‘𝑆)) |
35 | | eqid 2610 |
. . . . . 6
⊢
(.r‘𝑊) = (.r‘𝑊) |
36 | 4, 35 | ressmulr 15829 |
. . . . 5
⊢ (𝐴 ∈ (SubRing‘𝑊) →
(.r‘𝑊) =
(.r‘𝑆)) |
37 | 36 | ad2antrl 760 |
. . . 4
⊢ ((𝑊 ∈ AssAlg ∧ (𝐴 ∈ (SubRing‘𝑊) ∧ 𝐴 ∈ 𝐿)) → (.r‘𝑊) = (.r‘𝑆)) |
38 | | simpr 476 |
. . . . 5
⊢ ((𝐴 ∈ (SubRing‘𝑊) ∧ 𝐴 ∈ 𝐿) → 𝐴 ∈ 𝐿) |
39 | 4, 19 | lsslmod 18781 |
. . . . 5
⊢ ((𝑊 ∈ LMod ∧ 𝐴 ∈ 𝐿) → 𝑆 ∈ LMod) |
40 | 18, 38, 39 | syl2an 493 |
. . . 4
⊢ ((𝑊 ∈ AssAlg ∧ (𝐴 ∈ (SubRing‘𝑊) ∧ 𝐴 ∈ 𝐿)) → 𝑆 ∈ LMod) |
41 | 4 | subrgring 18606 |
. . . . 5
⊢ (𝐴 ∈ (SubRing‘𝑊) → 𝑆 ∈ Ring) |
42 | 41 | ad2antrl 760 |
. . . 4
⊢ ((𝑊 ∈ AssAlg ∧ (𝐴 ∈ (SubRing‘𝑊) ∧ 𝐴 ∈ 𝐿)) → 𝑆 ∈ Ring) |
43 | 28 | assasca 19142 |
. . . . 5
⊢ (𝑊 ∈ AssAlg →
(Scalar‘𝑊) ∈
CRing) |
44 | 43 | adantr 480 |
. . . 4
⊢ ((𝑊 ∈ AssAlg ∧ (𝐴 ∈ (SubRing‘𝑊) ∧ 𝐴 ∈ 𝐿)) → (Scalar‘𝑊) ∈ CRing) |
45 | | simpll 786 |
. . . . 5
⊢ (((𝑊 ∈ AssAlg ∧ (𝐴 ∈ (SubRing‘𝑊) ∧ 𝐴 ∈ 𝐿)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → 𝑊 ∈ AssAlg) |
46 | | simpr1 1060 |
. . . . 5
⊢ (((𝑊 ∈ AssAlg ∧ (𝐴 ∈ (SubRing‘𝑊) ∧ 𝐴 ∈ 𝐿)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → 𝑥 ∈ (Base‘(Scalar‘𝑊))) |
47 | 25 | adantr 480 |
. . . . . 6
⊢ (((𝑊 ∈ AssAlg ∧ (𝐴 ∈ (SubRing‘𝑊) ∧ 𝐴 ∈ 𝐿)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → 𝐴 ⊆ 𝑉) |
48 | | simpr2 1061 |
. . . . . 6
⊢ (((𝑊 ∈ AssAlg ∧ (𝐴 ∈ (SubRing‘𝑊) ∧ 𝐴 ∈ 𝐿)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → 𝑦 ∈ 𝐴) |
49 | 47, 48 | sseldd 3569 |
. . . . 5
⊢ (((𝑊 ∈ AssAlg ∧ (𝐴 ∈ (SubRing‘𝑊) ∧ 𝐴 ∈ 𝐿)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → 𝑦 ∈ 𝑉) |
50 | | simpr3 1062 |
. . . . . 6
⊢ (((𝑊 ∈ AssAlg ∧ (𝐴 ∈ (SubRing‘𝑊) ∧ 𝐴 ∈ 𝐿)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → 𝑧 ∈ 𝐴) |
51 | 47, 50 | sseldd 3569 |
. . . . 5
⊢ (((𝑊 ∈ AssAlg ∧ (𝐴 ∈ (SubRing‘𝑊) ∧ 𝐴 ∈ 𝐿)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → 𝑧 ∈ 𝑉) |
52 | | eqid 2610 |
. . . . . 6
⊢
(Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊)) |
53 | 12, 28, 52, 32, 35 | assaass 19138 |
. . . . 5
⊢ ((𝑊 ∈ AssAlg ∧ (𝑥 ∈
(Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → ((𝑥( ·𝑠
‘𝑊)𝑦)(.r‘𝑊)𝑧) = (𝑥( ·𝑠
‘𝑊)(𝑦(.r‘𝑊)𝑧))) |
54 | 45, 46, 49, 51, 53 | syl13anc 1320 |
. . . 4
⊢ (((𝑊 ∈ AssAlg ∧ (𝐴 ∈ (SubRing‘𝑊) ∧ 𝐴 ∈ 𝐿)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → ((𝑥( ·𝑠
‘𝑊)𝑦)(.r‘𝑊)𝑧) = (𝑥( ·𝑠
‘𝑊)(𝑦(.r‘𝑊)𝑧))) |
55 | 12, 28, 52, 32, 35 | assaassr 19139 |
. . . . 5
⊢ ((𝑊 ∈ AssAlg ∧ (𝑥 ∈
(Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝑦(.r‘𝑊)(𝑥( ·𝑠
‘𝑊)𝑧)) = (𝑥( ·𝑠
‘𝑊)(𝑦(.r‘𝑊)𝑧))) |
56 | 45, 46, 49, 51, 55 | syl13anc 1320 |
. . . 4
⊢ (((𝑊 ∈ AssAlg ∧ (𝐴 ∈ (SubRing‘𝑊) ∧ 𝐴 ∈ 𝐿)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → (𝑦(.r‘𝑊)(𝑥( ·𝑠
‘𝑊)𝑧)) = (𝑥( ·𝑠
‘𝑊)(𝑦(.r‘𝑊)𝑧))) |
57 | 27, 30, 31, 34, 37, 40, 42, 44, 54, 56 | isassad 19144 |
. . 3
⊢ ((𝑊 ∈ AssAlg ∧ (𝐴 ∈ (SubRing‘𝑊) ∧ 𝐴 ∈ 𝐿)) → 𝑆 ∈ AssAlg) |
58 | 57 | 3ad2antl1 1216 |
. 2
⊢ (((𝑊 ∈ AssAlg ∧ 1 ∈ 𝐴 ∧ 𝐴 ⊆ 𝑉) ∧ (𝐴 ∈ (SubRing‘𝑊) ∧ 𝐴 ∈ 𝐿)) → 𝑆 ∈ AssAlg) |
59 | 23, 58 | impbida 873 |
1
⊢ ((𝑊 ∈ AssAlg ∧ 1 ∈ 𝐴 ∧ 𝐴 ⊆ 𝑉) → (𝑆 ∈ AssAlg ↔ (𝐴 ∈ (SubRing‘𝑊) ∧ 𝐴 ∈ 𝐿))) |