Step | Hyp | Ref
| Expression |
1 | | eqidd 2188 |
. 2
⊢ ((𝑊 ∈ LMod ∧ 𝐴 ⊆ 𝑆 ∧ ∃𝑤 𝑤 ∈ 𝐴) → (Scalar‘𝑊) = (Scalar‘𝑊)) |
2 | | eqidd 2188 |
. 2
⊢ ((𝑊 ∈ LMod ∧ 𝐴 ⊆ 𝑆 ∧ ∃𝑤 𝑤 ∈ 𝐴) → (Base‘(Scalar‘𝑊)) =
(Base‘(Scalar‘𝑊))) |
3 | | eqidd 2188 |
. 2
⊢ ((𝑊 ∈ LMod ∧ 𝐴 ⊆ 𝑆 ∧ ∃𝑤 𝑤 ∈ 𝐴) → (Base‘𝑊) = (Base‘𝑊)) |
4 | | eqidd 2188 |
. 2
⊢ ((𝑊 ∈ LMod ∧ 𝐴 ⊆ 𝑆 ∧ ∃𝑤 𝑤 ∈ 𝐴) → (+g‘𝑊) = (+g‘𝑊)) |
5 | | eqidd 2188 |
. 2
⊢ ((𝑊 ∈ LMod ∧ 𝐴 ⊆ 𝑆 ∧ ∃𝑤 𝑤 ∈ 𝐴) → (
·𝑠 ‘𝑊) = ( ·𝑠
‘𝑊)) |
6 | | lssintcl.s |
. . 3
⊢ 𝑆 = (LSubSp‘𝑊) |
7 | 6 | a1i 9 |
. 2
⊢ ((𝑊 ∈ LMod ∧ 𝐴 ⊆ 𝑆 ∧ ∃𝑤 𝑤 ∈ 𝐴) → 𝑆 = (LSubSp‘𝑊)) |
8 | | intssuni2m 3880 |
. . . 4
⊢ ((𝐴 ⊆ 𝑆 ∧ ∃𝑤 𝑤 ∈ 𝐴) → ∩ 𝐴 ⊆ ∪ 𝑆) |
9 | 8 | 3adant1 1016 |
. . 3
⊢ ((𝑊 ∈ LMod ∧ 𝐴 ⊆ 𝑆 ∧ ∃𝑤 𝑤 ∈ 𝐴) → ∩ 𝐴 ⊆ ∪ 𝑆) |
10 | | eqid 2187 |
. . . . . . . . 9
⊢
(Base‘𝑊) =
(Base‘𝑊) |
11 | 10, 6 | lssssg 13549 |
. . . . . . . 8
⊢ ((𝑊 ∈ LMod ∧ 𝑦 ∈ 𝑆) → 𝑦 ⊆ (Base‘𝑊)) |
12 | | velpw 3594 |
. . . . . . . 8
⊢ (𝑦 ∈ 𝒫
(Base‘𝑊) ↔ 𝑦 ⊆ (Base‘𝑊)) |
13 | 11, 12 | sylibr 134 |
. . . . . . 7
⊢ ((𝑊 ∈ LMod ∧ 𝑦 ∈ 𝑆) → 𝑦 ∈ 𝒫 (Base‘𝑊)) |
14 | 13 | ex 115 |
. . . . . 6
⊢ (𝑊 ∈ LMod → (𝑦 ∈ 𝑆 → 𝑦 ∈ 𝒫 (Base‘𝑊))) |
15 | 14 | ssrdv 3173 |
. . . . 5
⊢ (𝑊 ∈ LMod → 𝑆 ⊆ 𝒫
(Base‘𝑊)) |
16 | | sspwuni 3983 |
. . . . 5
⊢ (𝑆 ⊆ 𝒫
(Base‘𝑊) ↔ ∪ 𝑆
⊆ (Base‘𝑊)) |
17 | 15, 16 | sylib 122 |
. . . 4
⊢ (𝑊 ∈ LMod → ∪ 𝑆
⊆ (Base‘𝑊)) |
18 | 17 | 3ad2ant1 1019 |
. . 3
⊢ ((𝑊 ∈ LMod ∧ 𝐴 ⊆ 𝑆 ∧ ∃𝑤 𝑤 ∈ 𝐴) → ∪ 𝑆 ⊆ (Base‘𝑊)) |
19 | 9, 18 | sstrd 3177 |
. 2
⊢ ((𝑊 ∈ LMod ∧ 𝐴 ⊆ 𝑆 ∧ ∃𝑤 𝑤 ∈ 𝐴) → ∩ 𝐴 ⊆ (Base‘𝑊)) |
20 | | simpl1 1001 |
. . . . . 6
⊢ (((𝑊 ∈ LMod ∧ 𝐴 ⊆ 𝑆 ∧ ∃𝑤 𝑤 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → 𝑊 ∈ LMod) |
21 | | simp2 999 |
. . . . . . 7
⊢ ((𝑊 ∈ LMod ∧ 𝐴 ⊆ 𝑆 ∧ ∃𝑤 𝑤 ∈ 𝐴) → 𝐴 ⊆ 𝑆) |
22 | 21 | sselda 3167 |
. . . . . 6
⊢ (((𝑊 ∈ LMod ∧ 𝐴 ⊆ 𝑆 ∧ ∃𝑤 𝑤 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ 𝑆) |
23 | | eqid 2187 |
. . . . . . 7
⊢
(0g‘𝑊) = (0g‘𝑊) |
24 | 23, 6 | lss0cl 13558 |
. . . . . 6
⊢ ((𝑊 ∈ LMod ∧ 𝑦 ∈ 𝑆) → (0g‘𝑊) ∈ 𝑦) |
25 | 20, 22, 24 | syl2anc 411 |
. . . . 5
⊢ (((𝑊 ∈ LMod ∧ 𝐴 ⊆ 𝑆 ∧ ∃𝑤 𝑤 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → (0g‘𝑊) ∈ 𝑦) |
26 | 25 | ralrimiva 2560 |
. . . 4
⊢ ((𝑊 ∈ LMod ∧ 𝐴 ⊆ 𝑆 ∧ ∃𝑤 𝑤 ∈ 𝐴) → ∀𝑦 ∈ 𝐴 (0g‘𝑊) ∈ 𝑦) |
27 | 10, 23 | lmod0vcl 13506 |
. . . . . 6
⊢ (𝑊 ∈ LMod →
(0g‘𝑊)
∈ (Base‘𝑊)) |
28 | | elintg 3864 |
. . . . . 6
⊢
((0g‘𝑊) ∈ (Base‘𝑊) → ((0g‘𝑊) ∈ ∩ 𝐴
↔ ∀𝑦 ∈
𝐴
(0g‘𝑊)
∈ 𝑦)) |
29 | 27, 28 | syl 14 |
. . . . 5
⊢ (𝑊 ∈ LMod →
((0g‘𝑊)
∈ ∩ 𝐴 ↔ ∀𝑦 ∈ 𝐴 (0g‘𝑊) ∈ 𝑦)) |
30 | 29 | 3ad2ant1 1019 |
. . . 4
⊢ ((𝑊 ∈ LMod ∧ 𝐴 ⊆ 𝑆 ∧ ∃𝑤 𝑤 ∈ 𝐴) → ((0g‘𝑊) ∈ ∩ 𝐴
↔ ∀𝑦 ∈
𝐴
(0g‘𝑊)
∈ 𝑦)) |
31 | 26, 30 | mpbird 167 |
. . 3
⊢ ((𝑊 ∈ LMod ∧ 𝐴 ⊆ 𝑆 ∧ ∃𝑤 𝑤 ∈ 𝐴) → (0g‘𝑊) ∈ ∩ 𝐴) |
32 | | elex2 2765 |
. . 3
⊢
((0g‘𝑊) ∈ ∩ 𝐴 → ∃𝑤 𝑤 ∈ ∩ 𝐴) |
33 | 31, 32 | syl 14 |
. 2
⊢ ((𝑊 ∈ LMod ∧ 𝐴 ⊆ 𝑆 ∧ ∃𝑤 𝑤 ∈ 𝐴) → ∃𝑤 𝑤 ∈ ∩ 𝐴) |
34 | 20 | adantlr 477 |
. . . . 5
⊢ ((((𝑊 ∈ LMod ∧ 𝐴 ⊆ 𝑆 ∧ ∃𝑤 𝑤 ∈ 𝐴) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑎 ∈ ∩ 𝐴 ∧ 𝑏 ∈ ∩ 𝐴)) ∧ 𝑦 ∈ 𝐴) → 𝑊 ∈ LMod) |
35 | 22 | adantlr 477 |
. . . . 5
⊢ ((((𝑊 ∈ LMod ∧ 𝐴 ⊆ 𝑆 ∧ ∃𝑤 𝑤 ∈ 𝐴) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑎 ∈ ∩ 𝐴 ∧ 𝑏 ∈ ∩ 𝐴)) ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ 𝑆) |
36 | | simplr1 1040 |
. . . . 5
⊢ ((((𝑊 ∈ LMod ∧ 𝐴 ⊆ 𝑆 ∧ ∃𝑤 𝑤 ∈ 𝐴) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑎 ∈ ∩ 𝐴 ∧ 𝑏 ∈ ∩ 𝐴)) ∧ 𝑦 ∈ 𝐴) → 𝑥 ∈ (Base‘(Scalar‘𝑊))) |
37 | | simplr2 1041 |
. . . . . 6
⊢ ((((𝑊 ∈ LMod ∧ 𝐴 ⊆ 𝑆 ∧ ∃𝑤 𝑤 ∈ 𝐴) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑎 ∈ ∩ 𝐴 ∧ 𝑏 ∈ ∩ 𝐴)) ∧ 𝑦 ∈ 𝐴) → 𝑎 ∈ ∩ 𝐴) |
38 | | simpr 110 |
. . . . . 6
⊢ ((((𝑊 ∈ LMod ∧ 𝐴 ⊆ 𝑆 ∧ ∃𝑤 𝑤 ∈ 𝐴) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑎 ∈ ∩ 𝐴 ∧ 𝑏 ∈ ∩ 𝐴)) ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ 𝐴) |
39 | | elinti 3865 |
. . . . . 6
⊢ (𝑎 ∈ ∩ 𝐴
→ (𝑦 ∈ 𝐴 → 𝑎 ∈ 𝑦)) |
40 | 37, 38, 39 | sylc 62 |
. . . . 5
⊢ ((((𝑊 ∈ LMod ∧ 𝐴 ⊆ 𝑆 ∧ ∃𝑤 𝑤 ∈ 𝐴) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑎 ∈ ∩ 𝐴 ∧ 𝑏 ∈ ∩ 𝐴)) ∧ 𝑦 ∈ 𝐴) → 𝑎 ∈ 𝑦) |
41 | | simplr3 1042 |
. . . . . 6
⊢ ((((𝑊 ∈ LMod ∧ 𝐴 ⊆ 𝑆 ∧ ∃𝑤 𝑤 ∈ 𝐴) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑎 ∈ ∩ 𝐴 ∧ 𝑏 ∈ ∩ 𝐴)) ∧ 𝑦 ∈ 𝐴) → 𝑏 ∈ ∩ 𝐴) |
42 | | elinti 3865 |
. . . . . 6
⊢ (𝑏 ∈ ∩ 𝐴
→ (𝑦 ∈ 𝐴 → 𝑏 ∈ 𝑦)) |
43 | 41, 38, 42 | sylc 62 |
. . . . 5
⊢ ((((𝑊 ∈ LMod ∧ 𝐴 ⊆ 𝑆 ∧ ∃𝑤 𝑤 ∈ 𝐴) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑎 ∈ ∩ 𝐴 ∧ 𝑏 ∈ ∩ 𝐴)) ∧ 𝑦 ∈ 𝐴) → 𝑏 ∈ 𝑦) |
44 | | eqid 2187 |
. . . . . 6
⊢
(Scalar‘𝑊) =
(Scalar‘𝑊) |
45 | | eqid 2187 |
. . . . . 6
⊢
(Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊)) |
46 | | eqid 2187 |
. . . . . 6
⊢
(+g‘𝑊) = (+g‘𝑊) |
47 | | eqid 2187 |
. . . . . 6
⊢ (
·𝑠 ‘𝑊) = ( ·𝑠
‘𝑊) |
48 | 44, 45, 46, 47, 6 | lssclg 13553 |
. . . . 5
⊢ ((𝑊 ∈ LMod ∧ 𝑦 ∈ 𝑆 ∧ (𝑥 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑎 ∈ 𝑦 ∧ 𝑏 ∈ 𝑦)) → ((𝑥( ·𝑠
‘𝑊)𝑎)(+g‘𝑊)𝑏) ∈ 𝑦) |
49 | 34, 35, 36, 40, 43, 48 | syl113anc 1260 |
. . . 4
⊢ ((((𝑊 ∈ LMod ∧ 𝐴 ⊆ 𝑆 ∧ ∃𝑤 𝑤 ∈ 𝐴) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑎 ∈ ∩ 𝐴 ∧ 𝑏 ∈ ∩ 𝐴)) ∧ 𝑦 ∈ 𝐴) → ((𝑥( ·𝑠
‘𝑊)𝑎)(+g‘𝑊)𝑏) ∈ 𝑦) |
50 | 49 | ralrimiva 2560 |
. . 3
⊢ (((𝑊 ∈ LMod ∧ 𝐴 ⊆ 𝑆 ∧ ∃𝑤 𝑤 ∈ 𝐴) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑎 ∈ ∩ 𝐴 ∧ 𝑏 ∈ ∩ 𝐴)) → ∀𝑦 ∈ 𝐴 ((𝑥( ·𝑠
‘𝑊)𝑎)(+g‘𝑊)𝑏) ∈ 𝑦) |
51 | | vex 2752 |
. . . . . . . . 9
⊢ 𝑥 ∈ V |
52 | 51 | a1i 9 |
. . . . . . . 8
⊢ (𝑊 ∈ LMod → 𝑥 ∈ V) |
53 | | vscaslid 12636 |
. . . . . . . . 9
⊢ (
·𝑠 = Slot (
·𝑠 ‘ndx) ∧ (
·𝑠 ‘ndx) ∈
ℕ) |
54 | 53 | slotex 12503 |
. . . . . . . 8
⊢ (𝑊 ∈ LMod → (
·𝑠 ‘𝑊) ∈ V) |
55 | | vex 2752 |
. . . . . . . . 9
⊢ 𝑎 ∈ V |
56 | 55 | a1i 9 |
. . . . . . . 8
⊢ (𝑊 ∈ LMod → 𝑎 ∈ V) |
57 | | ovexg 5922 |
. . . . . . . 8
⊢ ((𝑥 ∈ V ∧ (
·𝑠 ‘𝑊) ∈ V ∧ 𝑎 ∈ V) → (𝑥( ·𝑠
‘𝑊)𝑎) ∈ V) |
58 | 52, 54, 56, 57 | syl3anc 1248 |
. . . . . . 7
⊢ (𝑊 ∈ LMod → (𝑥(
·𝑠 ‘𝑊)𝑎) ∈ V) |
59 | | plusgslid 12586 |
. . . . . . . 8
⊢
(+g = Slot (+g‘ndx) ∧
(+g‘ndx) ∈ ℕ) |
60 | 59 | slotex 12503 |
. . . . . . 7
⊢ (𝑊 ∈ LMod →
(+g‘𝑊)
∈ V) |
61 | | vex 2752 |
. . . . . . . 8
⊢ 𝑏 ∈ V |
62 | 61 | a1i 9 |
. . . . . . 7
⊢ (𝑊 ∈ LMod → 𝑏 ∈ V) |
63 | | ovexg 5922 |
. . . . . . 7
⊢ (((𝑥(
·𝑠 ‘𝑊)𝑎) ∈ V ∧ (+g‘𝑊) ∈ V ∧ 𝑏 ∈ V) → ((𝑥(
·𝑠 ‘𝑊)𝑎)(+g‘𝑊)𝑏) ∈ V) |
64 | 58, 60, 62, 63 | syl3anc 1248 |
. . . . . 6
⊢ (𝑊 ∈ LMod → ((𝑥(
·𝑠 ‘𝑊)𝑎)(+g‘𝑊)𝑏) ∈ V) |
65 | | elintg 3864 |
. . . . . 6
⊢ (((𝑥(
·𝑠 ‘𝑊)𝑎)(+g‘𝑊)𝑏) ∈ V → (((𝑥( ·𝑠
‘𝑊)𝑎)(+g‘𝑊)𝑏) ∈ ∩ 𝐴 ↔ ∀𝑦 ∈ 𝐴 ((𝑥( ·𝑠
‘𝑊)𝑎)(+g‘𝑊)𝑏) ∈ 𝑦)) |
66 | 64, 65 | syl 14 |
. . . . 5
⊢ (𝑊 ∈ LMod → (((𝑥(
·𝑠 ‘𝑊)𝑎)(+g‘𝑊)𝑏) ∈ ∩ 𝐴 ↔ ∀𝑦 ∈ 𝐴 ((𝑥( ·𝑠
‘𝑊)𝑎)(+g‘𝑊)𝑏) ∈ 𝑦)) |
67 | 66 | 3ad2ant1 1019 |
. . . 4
⊢ ((𝑊 ∈ LMod ∧ 𝐴 ⊆ 𝑆 ∧ ∃𝑤 𝑤 ∈ 𝐴) → (((𝑥( ·𝑠
‘𝑊)𝑎)(+g‘𝑊)𝑏) ∈ ∩ 𝐴 ↔ ∀𝑦 ∈ 𝐴 ((𝑥( ·𝑠
‘𝑊)𝑎)(+g‘𝑊)𝑏) ∈ 𝑦)) |
68 | 67 | adantr 276 |
. . 3
⊢ (((𝑊 ∈ LMod ∧ 𝐴 ⊆ 𝑆 ∧ ∃𝑤 𝑤 ∈ 𝐴) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑎 ∈ ∩ 𝐴 ∧ 𝑏 ∈ ∩ 𝐴)) → (((𝑥( ·𝑠
‘𝑊)𝑎)(+g‘𝑊)𝑏) ∈ ∩ 𝐴 ↔ ∀𝑦 ∈ 𝐴 ((𝑥( ·𝑠
‘𝑊)𝑎)(+g‘𝑊)𝑏) ∈ 𝑦)) |
69 | 50, 68 | mpbird 167 |
. 2
⊢ (((𝑊 ∈ LMod ∧ 𝐴 ⊆ 𝑆 ∧ ∃𝑤 𝑤 ∈ 𝐴) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑎 ∈ ∩ 𝐴 ∧ 𝑏 ∈ ∩ 𝐴)) → ((𝑥( ·𝑠
‘𝑊)𝑎)(+g‘𝑊)𝑏) ∈ ∩ 𝐴) |
70 | | simp1 998 |
. 2
⊢ ((𝑊 ∈ LMod ∧ 𝐴 ⊆ 𝑆 ∧ ∃𝑤 𝑤 ∈ 𝐴) → 𝑊 ∈ LMod) |
71 | 1, 2, 3, 4, 5, 7, 19, 33, 69, 70 | islssmd 13548 |
1
⊢ ((𝑊 ∈ LMod ∧ 𝐴 ⊆ 𝑆 ∧ ∃𝑤 𝑤 ∈ 𝐴) → ∩ 𝐴 ∈ 𝑆) |