Step | Hyp | Ref
| Expression |
1 | | simpl1 1184 |
. . . . 5
⊢ (((𝑊 ∈ AssAlg ∧ 1 ∈ 𝐴 ∧ 𝐴 ⊆ 𝑉) ∧ 𝑆 ∈ AssAlg) → 𝑊 ∈ AssAlg) |
2 | | assaring 19782 |
. . . . 5
⊢ (𝑊 ∈ AssAlg → 𝑊 ∈ Ring) |
3 | 1, 2 | syl 17 |
. . . 4
⊢ (((𝑊 ∈ AssAlg ∧ 1 ∈ 𝐴 ∧ 𝐴 ⊆ 𝑉) ∧ 𝑆 ∈ AssAlg) → 𝑊 ∈ Ring) |
4 | | issubassa.s |
. . . . 5
⊢ 𝑆 = (𝑊 ↾s 𝐴) |
5 | | assaring 19782 |
. . . . . 6
⊢ (𝑆 ∈ AssAlg → 𝑆 ∈ Ring) |
6 | 5 | adantl 482 |
. . . . 5
⊢ (((𝑊 ∈ AssAlg ∧ 1 ∈ 𝐴 ∧ 𝐴 ⊆ 𝑉) ∧ 𝑆 ∈ AssAlg) → 𝑆 ∈ Ring) |
7 | 4, 6 | syl5eqelr 2888 |
. . . 4
⊢ (((𝑊 ∈ AssAlg ∧ 1 ∈ 𝐴 ∧ 𝐴 ⊆ 𝑉) ∧ 𝑆 ∈ AssAlg) → (𝑊 ↾s 𝐴) ∈ Ring) |
8 | | simpl3 1186 |
. . . . 5
⊢ (((𝑊 ∈ AssAlg ∧ 1 ∈ 𝐴 ∧ 𝐴 ⊆ 𝑉) ∧ 𝑆 ∈ AssAlg) → 𝐴 ⊆ 𝑉) |
9 | | simpl2 1185 |
. . . . 5
⊢ (((𝑊 ∈ AssAlg ∧ 1 ∈ 𝐴 ∧ 𝐴 ⊆ 𝑉) ∧ 𝑆 ∈ AssAlg) → 1 ∈ 𝐴) |
10 | 8, 9 | jca 512 |
. . . 4
⊢ (((𝑊 ∈ AssAlg ∧ 1 ∈ 𝐴 ∧ 𝐴 ⊆ 𝑉) ∧ 𝑆 ∈ AssAlg) → (𝐴 ⊆ 𝑉 ∧ 1 ∈ 𝐴)) |
11 | | issubassa.v |
. . . . 5
⊢ 𝑉 = (Base‘𝑊) |
12 | | issubassa.o |
. . . . 5
⊢ 1 =
(1r‘𝑊) |
13 | 11, 12 | issubrg 19225 |
. . . 4
⊢ (𝐴 ∈ (SubRing‘𝑊) ↔ ((𝑊 ∈ Ring ∧ (𝑊 ↾s 𝐴) ∈ Ring) ∧ (𝐴 ⊆ 𝑉 ∧ 1 ∈ 𝐴))) |
14 | 3, 7, 10, 13 | syl21anbrc 1337 |
. . 3
⊢ (((𝑊 ∈ AssAlg ∧ 1 ∈ 𝐴 ∧ 𝐴 ⊆ 𝑉) ∧ 𝑆 ∈ AssAlg) → 𝐴 ∈ (SubRing‘𝑊)) |
15 | | assalmod 19781 |
. . . . 5
⊢ (𝑆 ∈ AssAlg → 𝑆 ∈ LMod) |
16 | 15 | adantl 482 |
. . . 4
⊢ (((𝑊 ∈ AssAlg ∧ 1 ∈ 𝐴 ∧ 𝐴 ⊆ 𝑉) ∧ 𝑆 ∈ AssAlg) → 𝑆 ∈ LMod) |
17 | | assalmod 19781 |
. . . . 5
⊢ (𝑊 ∈ AssAlg → 𝑊 ∈ LMod) |
18 | | issubassa.l |
. . . . . 6
⊢ 𝐿 = (LSubSp‘𝑊) |
19 | 4, 11, 18 | islss3 19421 |
. . . . 5
⊢ (𝑊 ∈ LMod → (𝐴 ∈ 𝐿 ↔ (𝐴 ⊆ 𝑉 ∧ 𝑆 ∈ LMod))) |
20 | 1, 17, 19 | 3syl 18 |
. . . 4
⊢ (((𝑊 ∈ AssAlg ∧ 1 ∈ 𝐴 ∧ 𝐴 ⊆ 𝑉) ∧ 𝑆 ∈ AssAlg) → (𝐴 ∈ 𝐿 ↔ (𝐴 ⊆ 𝑉 ∧ 𝑆 ∈ LMod))) |
21 | 8, 16, 20 | mpbir2and 709 |
. . 3
⊢ (((𝑊 ∈ AssAlg ∧ 1 ∈ 𝐴 ∧ 𝐴 ⊆ 𝑉) ∧ 𝑆 ∈ AssAlg) → 𝐴 ∈ 𝐿) |
22 | 14, 21 | jca 512 |
. 2
⊢ (((𝑊 ∈ AssAlg ∧ 1 ∈ 𝐴 ∧ 𝐴 ⊆ 𝑉) ∧ 𝑆 ∈ AssAlg) → (𝐴 ∈ (SubRing‘𝑊) ∧ 𝐴 ∈ 𝐿)) |
23 | 11 | subrgss 19226 |
. . . . . 6
⊢ (𝐴 ∈ (SubRing‘𝑊) → 𝐴 ⊆ 𝑉) |
24 | 23 | ad2antrl 724 |
. . . . 5
⊢ ((𝑊 ∈ AssAlg ∧ (𝐴 ∈ (SubRing‘𝑊) ∧ 𝐴 ∈ 𝐿)) → 𝐴 ⊆ 𝑉) |
25 | 4, 11 | ressbas2 16384 |
. . . . 5
⊢ (𝐴 ⊆ 𝑉 → 𝐴 = (Base‘𝑆)) |
26 | 24, 25 | syl 17 |
. . . 4
⊢ ((𝑊 ∈ AssAlg ∧ (𝐴 ∈ (SubRing‘𝑊) ∧ 𝐴 ∈ 𝐿)) → 𝐴 = (Base‘𝑆)) |
27 | | eqid 2795 |
. . . . . 6
⊢
(Scalar‘𝑊) =
(Scalar‘𝑊) |
28 | 4, 27 | resssca 16479 |
. . . . 5
⊢ (𝐴 ∈ (SubRing‘𝑊) → (Scalar‘𝑊) = (Scalar‘𝑆)) |
29 | 28 | ad2antrl 724 |
. . . 4
⊢ ((𝑊 ∈ AssAlg ∧ (𝐴 ∈ (SubRing‘𝑊) ∧ 𝐴 ∈ 𝐿)) → (Scalar‘𝑊) = (Scalar‘𝑆)) |
30 | | eqidd 2796 |
. . . 4
⊢ ((𝑊 ∈ AssAlg ∧ (𝐴 ∈ (SubRing‘𝑊) ∧ 𝐴 ∈ 𝐿)) → (Base‘(Scalar‘𝑊)) =
(Base‘(Scalar‘𝑊))) |
31 | | eqid 2795 |
. . . . . 6
⊢ (
·𝑠 ‘𝑊) = ( ·𝑠
‘𝑊) |
32 | 4, 31 | ressvsca 16480 |
. . . . 5
⊢ (𝐴 ∈ (SubRing‘𝑊) → (
·𝑠 ‘𝑊) = ( ·𝑠
‘𝑆)) |
33 | 32 | ad2antrl 724 |
. . . 4
⊢ ((𝑊 ∈ AssAlg ∧ (𝐴 ∈ (SubRing‘𝑊) ∧ 𝐴 ∈ 𝐿)) → (
·𝑠 ‘𝑊) = ( ·𝑠
‘𝑆)) |
34 | | eqid 2795 |
. . . . . 6
⊢
(.r‘𝑊) = (.r‘𝑊) |
35 | 4, 34 | ressmulr 16454 |
. . . . 5
⊢ (𝐴 ∈ (SubRing‘𝑊) →
(.r‘𝑊) =
(.r‘𝑆)) |
36 | 35 | ad2antrl 724 |
. . . 4
⊢ ((𝑊 ∈ AssAlg ∧ (𝐴 ∈ (SubRing‘𝑊) ∧ 𝐴 ∈ 𝐿)) → (.r‘𝑊) = (.r‘𝑆)) |
37 | | simpr 485 |
. . . . 5
⊢ ((𝐴 ∈ (SubRing‘𝑊) ∧ 𝐴 ∈ 𝐿) → 𝐴 ∈ 𝐿) |
38 | 4, 18 | lsslmod 19422 |
. . . . 5
⊢ ((𝑊 ∈ LMod ∧ 𝐴 ∈ 𝐿) → 𝑆 ∈ LMod) |
39 | 17, 37, 38 | syl2an 595 |
. . . 4
⊢ ((𝑊 ∈ AssAlg ∧ (𝐴 ∈ (SubRing‘𝑊) ∧ 𝐴 ∈ 𝐿)) → 𝑆 ∈ LMod) |
40 | 4 | subrgring 19228 |
. . . . 5
⊢ (𝐴 ∈ (SubRing‘𝑊) → 𝑆 ∈ Ring) |
41 | 40 | ad2antrl 724 |
. . . 4
⊢ ((𝑊 ∈ AssAlg ∧ (𝐴 ∈ (SubRing‘𝑊) ∧ 𝐴 ∈ 𝐿)) → 𝑆 ∈ Ring) |
42 | 27 | assasca 19783 |
. . . . 5
⊢ (𝑊 ∈ AssAlg →
(Scalar‘𝑊) ∈
CRing) |
43 | 42 | adantr 481 |
. . . 4
⊢ ((𝑊 ∈ AssAlg ∧ (𝐴 ∈ (SubRing‘𝑊) ∧ 𝐴 ∈ 𝐿)) → (Scalar‘𝑊) ∈ CRing) |
44 | | simpll 763 |
. . . . 5
⊢ (((𝑊 ∈ AssAlg ∧ (𝐴 ∈ (SubRing‘𝑊) ∧ 𝐴 ∈ 𝐿)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → 𝑊 ∈ AssAlg) |
45 | | simpr1 1187 |
. . . . 5
⊢ (((𝑊 ∈ AssAlg ∧ (𝐴 ∈ (SubRing‘𝑊) ∧ 𝐴 ∈ 𝐿)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → 𝑥 ∈ (Base‘(Scalar‘𝑊))) |
46 | 24 | adantr 481 |
. . . . . 6
⊢ (((𝑊 ∈ AssAlg ∧ (𝐴 ∈ (SubRing‘𝑊) ∧ 𝐴 ∈ 𝐿)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → 𝐴 ⊆ 𝑉) |
47 | | simpr2 1188 |
. . . . . 6
⊢ (((𝑊 ∈ AssAlg ∧ (𝐴 ∈ (SubRing‘𝑊) ∧ 𝐴 ∈ 𝐿)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → 𝑦 ∈ 𝐴) |
48 | 46, 47 | sseldd 3890 |
. . . . 5
⊢ (((𝑊 ∈ AssAlg ∧ (𝐴 ∈ (SubRing‘𝑊) ∧ 𝐴 ∈ 𝐿)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → 𝑦 ∈ 𝑉) |
49 | | simpr3 1189 |
. . . . . 6
⊢ (((𝑊 ∈ AssAlg ∧ (𝐴 ∈ (SubRing‘𝑊) ∧ 𝐴 ∈ 𝐿)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → 𝑧 ∈ 𝐴) |
50 | 46, 49 | sseldd 3890 |
. . . . 5
⊢ (((𝑊 ∈ AssAlg ∧ (𝐴 ∈ (SubRing‘𝑊) ∧ 𝐴 ∈ 𝐿)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → 𝑧 ∈ 𝑉) |
51 | | eqid 2795 |
. . . . . 6
⊢
(Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊)) |
52 | 11, 27, 51, 31, 34 | assaass 19779 |
. . . . 5
⊢ ((𝑊 ∈ AssAlg ∧ (𝑥 ∈
(Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → ((𝑥( ·𝑠
‘𝑊)𝑦)(.r‘𝑊)𝑧) = (𝑥( ·𝑠
‘𝑊)(𝑦(.r‘𝑊)𝑧))) |
53 | 44, 45, 48, 50, 52 | syl13anc 1365 |
. . . 4
⊢ (((𝑊 ∈ AssAlg ∧ (𝐴 ∈ (SubRing‘𝑊) ∧ 𝐴 ∈ 𝐿)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → ((𝑥( ·𝑠
‘𝑊)𝑦)(.r‘𝑊)𝑧) = (𝑥( ·𝑠
‘𝑊)(𝑦(.r‘𝑊)𝑧))) |
54 | 11, 27, 51, 31, 34 | assaassr 19780 |
. . . . 5
⊢ ((𝑊 ∈ AssAlg ∧ (𝑥 ∈
(Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝑦(.r‘𝑊)(𝑥( ·𝑠
‘𝑊)𝑧)) = (𝑥( ·𝑠
‘𝑊)(𝑦(.r‘𝑊)𝑧))) |
55 | 44, 45, 48, 50, 54 | syl13anc 1365 |
. . . 4
⊢ (((𝑊 ∈ AssAlg ∧ (𝐴 ∈ (SubRing‘𝑊) ∧ 𝐴 ∈ 𝐿)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → (𝑦(.r‘𝑊)(𝑥( ·𝑠
‘𝑊)𝑧)) = (𝑥( ·𝑠
‘𝑊)(𝑦(.r‘𝑊)𝑧))) |
56 | 26, 29, 30, 33, 36, 39, 41, 43, 53, 55 | isassad 19785 |
. . 3
⊢ ((𝑊 ∈ AssAlg ∧ (𝐴 ∈ (SubRing‘𝑊) ∧ 𝐴 ∈ 𝐿)) → 𝑆 ∈ AssAlg) |
57 | 56 | 3ad2antl1 1178 |
. 2
⊢ (((𝑊 ∈ AssAlg ∧ 1 ∈ 𝐴 ∧ 𝐴 ⊆ 𝑉) ∧ (𝐴 ∈ (SubRing‘𝑊) ∧ 𝐴 ∈ 𝐿)) → 𝑆 ∈ AssAlg) |
58 | 22, 57 | impbida 797 |
1
⊢ ((𝑊 ∈ AssAlg ∧ 1 ∈ 𝐴 ∧ 𝐴 ⊆ 𝑉) → (𝑆 ∈ AssAlg ↔ (𝐴 ∈ (SubRing‘𝑊) ∧ 𝐴 ∈ 𝐿))) |