| Step | Hyp | Ref
| Expression |
| 1 | | eqidd 2738 |
. 2
⊢ ((𝑊 ∈ LMod ∧ 𝐴 ⊆ 𝑆 ∧ 𝐴 ≠ ∅) → (Scalar‘𝑊) = (Scalar‘𝑊)) |
| 2 | | eqidd 2738 |
. 2
⊢ ((𝑊 ∈ LMod ∧ 𝐴 ⊆ 𝑆 ∧ 𝐴 ≠ ∅) →
(Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊))) |
| 3 | | eqidd 2738 |
. 2
⊢ ((𝑊 ∈ LMod ∧ 𝐴 ⊆ 𝑆 ∧ 𝐴 ≠ ∅) → (Base‘𝑊) = (Base‘𝑊)) |
| 4 | | eqidd 2738 |
. 2
⊢ ((𝑊 ∈ LMod ∧ 𝐴 ⊆ 𝑆 ∧ 𝐴 ≠ ∅) →
(+g‘𝑊) =
(+g‘𝑊)) |
| 5 | | eqidd 2738 |
. 2
⊢ ((𝑊 ∈ LMod ∧ 𝐴 ⊆ 𝑆 ∧ 𝐴 ≠ ∅) → (
·𝑠 ‘𝑊) = ( ·𝑠
‘𝑊)) |
| 6 | | lssintcl.s |
. . 3
⊢ 𝑆 = (LSubSp‘𝑊) |
| 7 | 6 | a1i 11 |
. 2
⊢ ((𝑊 ∈ LMod ∧ 𝐴 ⊆ 𝑆 ∧ 𝐴 ≠ ∅) → 𝑆 = (LSubSp‘𝑊)) |
| 8 | | intssuni2 4973 |
. . . 4
⊢ ((𝐴 ⊆ 𝑆 ∧ 𝐴 ≠ ∅) → ∩ 𝐴
⊆ ∪ 𝑆) |
| 9 | 8 | 3adant1 1131 |
. . 3
⊢ ((𝑊 ∈ LMod ∧ 𝐴 ⊆ 𝑆 ∧ 𝐴 ≠ ∅) → ∩ 𝐴
⊆ ∪ 𝑆) |
| 10 | | eqid 2737 |
. . . . . . 7
⊢
(Base‘𝑊) =
(Base‘𝑊) |
| 11 | 10, 6 | lssss 20934 |
. . . . . 6
⊢ (𝑦 ∈ 𝑆 → 𝑦 ⊆ (Base‘𝑊)) |
| 12 | | velpw 4605 |
. . . . . 6
⊢ (𝑦 ∈ 𝒫
(Base‘𝑊) ↔ 𝑦 ⊆ (Base‘𝑊)) |
| 13 | 11, 12 | sylibr 234 |
. . . . 5
⊢ (𝑦 ∈ 𝑆 → 𝑦 ∈ 𝒫 (Base‘𝑊)) |
| 14 | 13 | ssriv 3987 |
. . . 4
⊢ 𝑆 ⊆ 𝒫
(Base‘𝑊) |
| 15 | | sspwuni 5100 |
. . . 4
⊢ (𝑆 ⊆ 𝒫
(Base‘𝑊) ↔ ∪ 𝑆
⊆ (Base‘𝑊)) |
| 16 | 14, 15 | mpbi 230 |
. . 3
⊢ ∪ 𝑆
⊆ (Base‘𝑊) |
| 17 | 9, 16 | sstrdi 3996 |
. 2
⊢ ((𝑊 ∈ LMod ∧ 𝐴 ⊆ 𝑆 ∧ 𝐴 ≠ ∅) → ∩ 𝐴
⊆ (Base‘𝑊)) |
| 18 | | simpl1 1192 |
. . . . . 6
⊢ (((𝑊 ∈ LMod ∧ 𝐴 ⊆ 𝑆 ∧ 𝐴 ≠ ∅) ∧ 𝑦 ∈ 𝐴) → 𝑊 ∈ LMod) |
| 19 | | simp2 1138 |
. . . . . . 7
⊢ ((𝑊 ∈ LMod ∧ 𝐴 ⊆ 𝑆 ∧ 𝐴 ≠ ∅) → 𝐴 ⊆ 𝑆) |
| 20 | 19 | sselda 3983 |
. . . . . 6
⊢ (((𝑊 ∈ LMod ∧ 𝐴 ⊆ 𝑆 ∧ 𝐴 ≠ ∅) ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ 𝑆) |
| 21 | | eqid 2737 |
. . . . . . 7
⊢
(0g‘𝑊) = (0g‘𝑊) |
| 22 | 21, 6 | lss0cl 20945 |
. . . . . 6
⊢ ((𝑊 ∈ LMod ∧ 𝑦 ∈ 𝑆) → (0g‘𝑊) ∈ 𝑦) |
| 23 | 18, 20, 22 | syl2anc 584 |
. . . . 5
⊢ (((𝑊 ∈ LMod ∧ 𝐴 ⊆ 𝑆 ∧ 𝐴 ≠ ∅) ∧ 𝑦 ∈ 𝐴) → (0g‘𝑊) ∈ 𝑦) |
| 24 | 23 | ralrimiva 3146 |
. . . 4
⊢ ((𝑊 ∈ LMod ∧ 𝐴 ⊆ 𝑆 ∧ 𝐴 ≠ ∅) → ∀𝑦 ∈ 𝐴 (0g‘𝑊) ∈ 𝑦) |
| 25 | | fvex 6919 |
. . . . 5
⊢
(0g‘𝑊) ∈ V |
| 26 | 25 | elint2 4953 |
. . . 4
⊢
((0g‘𝑊) ∈ ∩ 𝐴 ↔ ∀𝑦 ∈ 𝐴 (0g‘𝑊) ∈ 𝑦) |
| 27 | 24, 26 | sylibr 234 |
. . 3
⊢ ((𝑊 ∈ LMod ∧ 𝐴 ⊆ 𝑆 ∧ 𝐴 ≠ ∅) →
(0g‘𝑊)
∈ ∩ 𝐴) |
| 28 | 27 | ne0d 4342 |
. 2
⊢ ((𝑊 ∈ LMod ∧ 𝐴 ⊆ 𝑆 ∧ 𝐴 ≠ ∅) → ∩ 𝐴
≠ ∅) |
| 29 | 20 | adantlr 715 |
. . . . 5
⊢ ((((𝑊 ∈ LMod ∧ 𝐴 ⊆ 𝑆 ∧ 𝐴 ≠ ∅) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑎 ∈ ∩ 𝐴 ∧ 𝑏 ∈ ∩ 𝐴)) ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ 𝑆) |
| 30 | | simplr1 1216 |
. . . . 5
⊢ ((((𝑊 ∈ LMod ∧ 𝐴 ⊆ 𝑆 ∧ 𝐴 ≠ ∅) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑎 ∈ ∩ 𝐴 ∧ 𝑏 ∈ ∩ 𝐴)) ∧ 𝑦 ∈ 𝐴) → 𝑥 ∈ (Base‘(Scalar‘𝑊))) |
| 31 | | simplr2 1217 |
. . . . . 6
⊢ ((((𝑊 ∈ LMod ∧ 𝐴 ⊆ 𝑆 ∧ 𝐴 ≠ ∅) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑎 ∈ ∩ 𝐴 ∧ 𝑏 ∈ ∩ 𝐴)) ∧ 𝑦 ∈ 𝐴) → 𝑎 ∈ ∩ 𝐴) |
| 32 | | simpr 484 |
. . . . . 6
⊢ ((((𝑊 ∈ LMod ∧ 𝐴 ⊆ 𝑆 ∧ 𝐴 ≠ ∅) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑎 ∈ ∩ 𝐴 ∧ 𝑏 ∈ ∩ 𝐴)) ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ 𝐴) |
| 33 | | elinti 4955 |
. . . . . 6
⊢ (𝑎 ∈ ∩ 𝐴
→ (𝑦 ∈ 𝐴 → 𝑎 ∈ 𝑦)) |
| 34 | 31, 32, 33 | sylc 65 |
. . . . 5
⊢ ((((𝑊 ∈ LMod ∧ 𝐴 ⊆ 𝑆 ∧ 𝐴 ≠ ∅) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑎 ∈ ∩ 𝐴 ∧ 𝑏 ∈ ∩ 𝐴)) ∧ 𝑦 ∈ 𝐴) → 𝑎 ∈ 𝑦) |
| 35 | | simplr3 1218 |
. . . . . 6
⊢ ((((𝑊 ∈ LMod ∧ 𝐴 ⊆ 𝑆 ∧ 𝐴 ≠ ∅) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑎 ∈ ∩ 𝐴 ∧ 𝑏 ∈ ∩ 𝐴)) ∧ 𝑦 ∈ 𝐴) → 𝑏 ∈ ∩ 𝐴) |
| 36 | | elinti 4955 |
. . . . . 6
⊢ (𝑏 ∈ ∩ 𝐴
→ (𝑦 ∈ 𝐴 → 𝑏 ∈ 𝑦)) |
| 37 | 35, 32, 36 | sylc 65 |
. . . . 5
⊢ ((((𝑊 ∈ LMod ∧ 𝐴 ⊆ 𝑆 ∧ 𝐴 ≠ ∅) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑎 ∈ ∩ 𝐴 ∧ 𝑏 ∈ ∩ 𝐴)) ∧ 𝑦 ∈ 𝐴) → 𝑏 ∈ 𝑦) |
| 38 | | eqid 2737 |
. . . . . 6
⊢
(Scalar‘𝑊) =
(Scalar‘𝑊) |
| 39 | | eqid 2737 |
. . . . . 6
⊢
(Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊)) |
| 40 | | eqid 2737 |
. . . . . 6
⊢
(+g‘𝑊) = (+g‘𝑊) |
| 41 | | eqid 2737 |
. . . . . 6
⊢ (
·𝑠 ‘𝑊) = ( ·𝑠
‘𝑊) |
| 42 | 38, 39, 40, 41, 6 | lsscl 20940 |
. . . . 5
⊢ ((𝑦 ∈ 𝑆 ∧ (𝑥 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑎 ∈ 𝑦 ∧ 𝑏 ∈ 𝑦)) → ((𝑥( ·𝑠
‘𝑊)𝑎)(+g‘𝑊)𝑏) ∈ 𝑦) |
| 43 | 29, 30, 34, 37, 42 | syl13anc 1374 |
. . . 4
⊢ ((((𝑊 ∈ LMod ∧ 𝐴 ⊆ 𝑆 ∧ 𝐴 ≠ ∅) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑎 ∈ ∩ 𝐴 ∧ 𝑏 ∈ ∩ 𝐴)) ∧ 𝑦 ∈ 𝐴) → ((𝑥( ·𝑠
‘𝑊)𝑎)(+g‘𝑊)𝑏) ∈ 𝑦) |
| 44 | 43 | ralrimiva 3146 |
. . 3
⊢ (((𝑊 ∈ LMod ∧ 𝐴 ⊆ 𝑆 ∧ 𝐴 ≠ ∅) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑎 ∈ ∩ 𝐴 ∧ 𝑏 ∈ ∩ 𝐴)) → ∀𝑦 ∈ 𝐴 ((𝑥( ·𝑠
‘𝑊)𝑎)(+g‘𝑊)𝑏) ∈ 𝑦) |
| 45 | | ovex 7464 |
. . . 4
⊢ ((𝑥(
·𝑠 ‘𝑊)𝑎)(+g‘𝑊)𝑏) ∈ V |
| 46 | 45 | elint2 4953 |
. . 3
⊢ (((𝑥(
·𝑠 ‘𝑊)𝑎)(+g‘𝑊)𝑏) ∈ ∩ 𝐴 ↔ ∀𝑦 ∈ 𝐴 ((𝑥( ·𝑠
‘𝑊)𝑎)(+g‘𝑊)𝑏) ∈ 𝑦) |
| 47 | 44, 46 | sylibr 234 |
. 2
⊢ (((𝑊 ∈ LMod ∧ 𝐴 ⊆ 𝑆 ∧ 𝐴 ≠ ∅) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑎 ∈ ∩ 𝐴 ∧ 𝑏 ∈ ∩ 𝐴)) → ((𝑥( ·𝑠
‘𝑊)𝑎)(+g‘𝑊)𝑏) ∈ ∩ 𝐴) |
| 48 | 1, 2, 3, 4, 5, 7, 17, 28, 47 | islssd 20933 |
1
⊢ ((𝑊 ∈ LMod ∧ 𝐴 ⊆ 𝑆 ∧ 𝐴 ≠ ∅) → ∩ 𝐴
∈ 𝑆) |