Step | Hyp | Ref
| Expression |
1 | | eqidd 2778 |
. . 3
⊢ (𝜑 → (Scalar‘𝑊) = (Scalar‘𝑊)) |
2 | | eqidd 2778 |
. . 3
⊢ (𝜑 →
(Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊))) |
3 | | lbsext.v |
. . . 4
⊢ 𝑉 = (Base‘𝑊) |
4 | 3 | a1i 11 |
. . 3
⊢ (𝜑 → 𝑉 = (Base‘𝑊)) |
5 | | eqidd 2778 |
. . 3
⊢ (𝜑 → (+g‘𝑊) = (+g‘𝑊)) |
6 | | eqidd 2778 |
. . 3
⊢ (𝜑 → (
·𝑠 ‘𝑊) = ( ·𝑠
‘𝑊)) |
7 | | lbsext.p |
. . . 4
⊢ 𝑃 = (LSubSp‘𝑊) |
8 | 7 | a1i 11 |
. . 3
⊢ (𝜑 → 𝑃 = (LSubSp‘𝑊)) |
9 | | lbsext.t |
. . . 4
⊢ 𝑇 = ∪ 𝑢 ∈ 𝐴 (𝑁‘(𝑢 ∖ {𝑥})) |
10 | | lbsext.w |
. . . . . . . 8
⊢ (𝜑 → 𝑊 ∈ LVec) |
11 | | lveclmod 19501 |
. . . . . . . 8
⊢ (𝑊 ∈ LVec → 𝑊 ∈ LMod) |
12 | 10, 11 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑊 ∈ LMod) |
13 | | lbsext.a |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ⊆ 𝑆) |
14 | | lbsext.s |
. . . . . . . . . . . 12
⊢ 𝑆 = {𝑧 ∈ 𝒫 𝑉 ∣ (𝐶 ⊆ 𝑧 ∧ ∀𝑥 ∈ 𝑧 ¬ 𝑥 ∈ (𝑁‘(𝑧 ∖ {𝑥})))} |
15 | | ssrab2 3907 |
. . . . . . . . . . . 12
⊢ {𝑧 ∈ 𝒫 𝑉 ∣ (𝐶 ⊆ 𝑧 ∧ ∀𝑥 ∈ 𝑧 ¬ 𝑥 ∈ (𝑁‘(𝑧 ∖ {𝑥})))} ⊆ 𝒫 𝑉 |
16 | 14, 15 | eqsstri 3853 |
. . . . . . . . . . 11
⊢ 𝑆 ⊆ 𝒫 𝑉 |
17 | 13, 16 | syl6ss 3832 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 ⊆ 𝒫 𝑉) |
18 | 17 | sselda 3820 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑢 ∈ 𝐴) → 𝑢 ∈ 𝒫 𝑉) |
19 | 18 | elpwid 4390 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑢 ∈ 𝐴) → 𝑢 ⊆ 𝑉) |
20 | 19 | ssdifssd 3970 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑢 ∈ 𝐴) → (𝑢 ∖ {𝑥}) ⊆ 𝑉) |
21 | | lbsext.n |
. . . . . . . 8
⊢ 𝑁 = (LSpan‘𝑊) |
22 | 3, 21 | lspssv 19378 |
. . . . . . 7
⊢ ((𝑊 ∈ LMod ∧ (𝑢 ∖ {𝑥}) ⊆ 𝑉) → (𝑁‘(𝑢 ∖ {𝑥})) ⊆ 𝑉) |
23 | 12, 20, 22 | syl2an2r 675 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑢 ∈ 𝐴) → (𝑁‘(𝑢 ∖ {𝑥})) ⊆ 𝑉) |
24 | 23 | ralrimiva 3147 |
. . . . 5
⊢ (𝜑 → ∀𝑢 ∈ 𝐴 (𝑁‘(𝑢 ∖ {𝑥})) ⊆ 𝑉) |
25 | | iunss 4794 |
. . . . 5
⊢ (∪ 𝑢 ∈ 𝐴 (𝑁‘(𝑢 ∖ {𝑥})) ⊆ 𝑉 ↔ ∀𝑢 ∈ 𝐴 (𝑁‘(𝑢 ∖ {𝑥})) ⊆ 𝑉) |
26 | 24, 25 | sylibr 226 |
. . . 4
⊢ (𝜑 → ∪ 𝑢 ∈ 𝐴 (𝑁‘(𝑢 ∖ {𝑥})) ⊆ 𝑉) |
27 | 9, 26 | syl5eqss 3867 |
. . 3
⊢ (𝜑 → 𝑇 ⊆ 𝑉) |
28 | 9 | a1i 11 |
. . . 4
⊢ (𝜑 → 𝑇 = ∪ 𝑢 ∈ 𝐴 (𝑁‘(𝑢 ∖ {𝑥}))) |
29 | | lbsext.z |
. . . . . 6
⊢ (𝜑 → 𝐴 ≠ ∅) |
30 | 3, 7, 21 | lspcl 19371 |
. . . . . . . . 9
⊢ ((𝑊 ∈ LMod ∧ (𝑢 ∖ {𝑥}) ⊆ 𝑉) → (𝑁‘(𝑢 ∖ {𝑥})) ∈ 𝑃) |
31 | 12, 20, 30 | syl2an2r 675 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑢 ∈ 𝐴) → (𝑁‘(𝑢 ∖ {𝑥})) ∈ 𝑃) |
32 | 7 | lssn0 19333 |
. . . . . . . 8
⊢ ((𝑁‘(𝑢 ∖ {𝑥})) ∈ 𝑃 → (𝑁‘(𝑢 ∖ {𝑥})) ≠ ∅) |
33 | 31, 32 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑢 ∈ 𝐴) → (𝑁‘(𝑢 ∖ {𝑥})) ≠ ∅) |
34 | 33 | ralrimiva 3147 |
. . . . . 6
⊢ (𝜑 → ∀𝑢 ∈ 𝐴 (𝑁‘(𝑢 ∖ {𝑥})) ≠ ∅) |
35 | | r19.2z 4282 |
. . . . . 6
⊢ ((𝐴 ≠ ∅ ∧
∀𝑢 ∈ 𝐴 (𝑁‘(𝑢 ∖ {𝑥})) ≠ ∅) → ∃𝑢 ∈ 𝐴 (𝑁‘(𝑢 ∖ {𝑥})) ≠ ∅) |
36 | 29, 34, 35 | syl2anc 579 |
. . . . 5
⊢ (𝜑 → ∃𝑢 ∈ 𝐴 (𝑁‘(𝑢 ∖ {𝑥})) ≠ ∅) |
37 | | iunn0 4813 |
. . . . 5
⊢
(∃𝑢 ∈
𝐴 (𝑁‘(𝑢 ∖ {𝑥})) ≠ ∅ ↔ ∪ 𝑢 ∈ 𝐴 (𝑁‘(𝑢 ∖ {𝑥})) ≠ ∅) |
38 | 36, 37 | sylib 210 |
. . . 4
⊢ (𝜑 → ∪ 𝑢 ∈ 𝐴 (𝑁‘(𝑢 ∖ {𝑥})) ≠ ∅) |
39 | 28, 38 | eqnetrd 3035 |
. . 3
⊢ (𝜑 → 𝑇 ≠ ∅) |
40 | 9 | eleq2i 2850 |
. . . . . . . . 9
⊢ (𝑣 ∈ 𝑇 ↔ 𝑣 ∈ ∪
𝑢 ∈ 𝐴 (𝑁‘(𝑢 ∖ {𝑥}))) |
41 | | eliun 4757 |
. . . . . . . . 9
⊢ (𝑣 ∈ ∪ 𝑢 ∈ 𝐴 (𝑁‘(𝑢 ∖ {𝑥})) ↔ ∃𝑢 ∈ 𝐴 𝑣 ∈ (𝑁‘(𝑢 ∖ {𝑥}))) |
42 | | difeq1 3943 |
. . . . . . . . . . . 12
⊢ (𝑢 = 𝑚 → (𝑢 ∖ {𝑥}) = (𝑚 ∖ {𝑥})) |
43 | 42 | fveq2d 6450 |
. . . . . . . . . . 11
⊢ (𝑢 = 𝑚 → (𝑁‘(𝑢 ∖ {𝑥})) = (𝑁‘(𝑚 ∖ {𝑥}))) |
44 | 43 | eleq2d 2844 |
. . . . . . . . . 10
⊢ (𝑢 = 𝑚 → (𝑣 ∈ (𝑁‘(𝑢 ∖ {𝑥})) ↔ 𝑣 ∈ (𝑁‘(𝑚 ∖ {𝑥})))) |
45 | 44 | cbvrexv 3367 |
. . . . . . . . 9
⊢
(∃𝑢 ∈
𝐴 𝑣 ∈ (𝑁‘(𝑢 ∖ {𝑥})) ↔ ∃𝑚 ∈ 𝐴 𝑣 ∈ (𝑁‘(𝑚 ∖ {𝑥}))) |
46 | 40, 41, 45 | 3bitri 289 |
. . . . . . . 8
⊢ (𝑣 ∈ 𝑇 ↔ ∃𝑚 ∈ 𝐴 𝑣 ∈ (𝑁‘(𝑚 ∖ {𝑥}))) |
47 | 9 | eleq2i 2850 |
. . . . . . . . 9
⊢ (𝑤 ∈ 𝑇 ↔ 𝑤 ∈ ∪
𝑢 ∈ 𝐴 (𝑁‘(𝑢 ∖ {𝑥}))) |
48 | | eliun 4757 |
. . . . . . . . 9
⊢ (𝑤 ∈ ∪ 𝑢 ∈ 𝐴 (𝑁‘(𝑢 ∖ {𝑥})) ↔ ∃𝑢 ∈ 𝐴 𝑤 ∈ (𝑁‘(𝑢 ∖ {𝑥}))) |
49 | | difeq1 3943 |
. . . . . . . . . . . 12
⊢ (𝑢 = 𝑛 → (𝑢 ∖ {𝑥}) = (𝑛 ∖ {𝑥})) |
50 | 49 | fveq2d 6450 |
. . . . . . . . . . 11
⊢ (𝑢 = 𝑛 → (𝑁‘(𝑢 ∖ {𝑥})) = (𝑁‘(𝑛 ∖ {𝑥}))) |
51 | 50 | eleq2d 2844 |
. . . . . . . . . 10
⊢ (𝑢 = 𝑛 → (𝑤 ∈ (𝑁‘(𝑢 ∖ {𝑥})) ↔ 𝑤 ∈ (𝑁‘(𝑛 ∖ {𝑥})))) |
52 | 51 | cbvrexv 3367 |
. . . . . . . . 9
⊢
(∃𝑢 ∈
𝐴 𝑤 ∈ (𝑁‘(𝑢 ∖ {𝑥})) ↔ ∃𝑛 ∈ 𝐴 𝑤 ∈ (𝑁‘(𝑛 ∖ {𝑥}))) |
53 | 47, 48, 52 | 3bitri 289 |
. . . . . . . 8
⊢ (𝑤 ∈ 𝑇 ↔ ∃𝑛 ∈ 𝐴 𝑤 ∈ (𝑁‘(𝑛 ∖ {𝑥}))) |
54 | 46, 53 | anbi12i 620 |
. . . . . . 7
⊢ ((𝑣 ∈ 𝑇 ∧ 𝑤 ∈ 𝑇) ↔ (∃𝑚 ∈ 𝐴 𝑣 ∈ (𝑁‘(𝑚 ∖ {𝑥})) ∧ ∃𝑛 ∈ 𝐴 𝑤 ∈ (𝑁‘(𝑛 ∖ {𝑥})))) |
55 | | reeanv 3292 |
. . . . . . 7
⊢
(∃𝑚 ∈
𝐴 ∃𝑛 ∈ 𝐴 (𝑣 ∈ (𝑁‘(𝑚 ∖ {𝑥})) ∧ 𝑤 ∈ (𝑁‘(𝑛 ∖ {𝑥}))) ↔ (∃𝑚 ∈ 𝐴 𝑣 ∈ (𝑁‘(𝑚 ∖ {𝑥})) ∧ ∃𝑛 ∈ 𝐴 𝑤 ∈ (𝑁‘(𝑛 ∖ {𝑥})))) |
56 | 54, 55 | bitr4i 270 |
. . . . . 6
⊢ ((𝑣 ∈ 𝑇 ∧ 𝑤 ∈ 𝑇) ↔ ∃𝑚 ∈ 𝐴 ∃𝑛 ∈ 𝐴 (𝑣 ∈ (𝑁‘(𝑚 ∖ {𝑥})) ∧ 𝑤 ∈ (𝑁‘(𝑛 ∖ {𝑥})))) |
57 | | simp1l 1211 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑚 ∈ 𝐴 ∧ 𝑛 ∈ 𝐴) ∧ (𝑣 ∈ (𝑁‘(𝑚 ∖ {𝑥})) ∧ 𝑤 ∈ (𝑁‘(𝑛 ∖ {𝑥})))) → 𝜑) |
58 | | lbsext.r |
. . . . . . . . . . . 12
⊢ (𝜑 → [⊊] Or 𝐴) |
59 | 57, 58 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑚 ∈ 𝐴 ∧ 𝑛 ∈ 𝐴) ∧ (𝑣 ∈ (𝑁‘(𝑚 ∖ {𝑥})) ∧ 𝑤 ∈ (𝑁‘(𝑛 ∖ {𝑥})))) → [⊊] Or 𝐴) |
60 | | simp2 1128 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑚 ∈ 𝐴 ∧ 𝑛 ∈ 𝐴) ∧ (𝑣 ∈ (𝑁‘(𝑚 ∖ {𝑥})) ∧ 𝑤 ∈ (𝑁‘(𝑛 ∖ {𝑥})))) → (𝑚 ∈ 𝐴 ∧ 𝑛 ∈ 𝐴)) |
61 | | sorpssun 7221 |
. . . . . . . . . . 11
⊢ ((
[⊊] Or 𝐴
∧ (𝑚 ∈ 𝐴 ∧ 𝑛 ∈ 𝐴)) → (𝑚 ∪ 𝑛) ∈ 𝐴) |
62 | 59, 60, 61 | syl2anc 579 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑚 ∈ 𝐴 ∧ 𝑛 ∈ 𝐴) ∧ (𝑣 ∈ (𝑁‘(𝑚 ∖ {𝑥})) ∧ 𝑤 ∈ (𝑁‘(𝑛 ∖ {𝑥})))) → (𝑚 ∪ 𝑛) ∈ 𝐴) |
63 | 57, 12 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑚 ∈ 𝐴 ∧ 𝑛 ∈ 𝐴) ∧ (𝑣 ∈ (𝑁‘(𝑚 ∖ {𝑥})) ∧ 𝑤 ∈ (𝑁‘(𝑛 ∖ {𝑥})))) → 𝑊 ∈ LMod) |
64 | | elssuni 4702 |
. . . . . . . . . . . . . . 15
⊢ ((𝑚 ∪ 𝑛) ∈ 𝐴 → (𝑚 ∪ 𝑛) ⊆ ∪ 𝐴) |
65 | 62, 64 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑚 ∈ 𝐴 ∧ 𝑛 ∈ 𝐴) ∧ (𝑣 ∈ (𝑁‘(𝑚 ∖ {𝑥})) ∧ 𝑤 ∈ (𝑁‘(𝑛 ∖ {𝑥})))) → (𝑚 ∪ 𝑛) ⊆ ∪ 𝐴) |
66 | | sspwuni 4845 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ⊆ 𝒫 𝑉 ↔ ∪ 𝐴
⊆ 𝑉) |
67 | 17, 66 | sylib 210 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ∪ 𝐴
⊆ 𝑉) |
68 | 57, 67 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑚 ∈ 𝐴 ∧ 𝑛 ∈ 𝐴) ∧ (𝑣 ∈ (𝑁‘(𝑚 ∖ {𝑥})) ∧ 𝑤 ∈ (𝑁‘(𝑛 ∖ {𝑥})))) → ∪
𝐴 ⊆ 𝑉) |
69 | 65, 68 | sstrd 3830 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑚 ∈ 𝐴 ∧ 𝑛 ∈ 𝐴) ∧ (𝑣 ∈ (𝑁‘(𝑚 ∖ {𝑥})) ∧ 𝑤 ∈ (𝑁‘(𝑛 ∖ {𝑥})))) → (𝑚 ∪ 𝑛) ⊆ 𝑉) |
70 | 69 | ssdifssd 3970 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑚 ∈ 𝐴 ∧ 𝑛 ∈ 𝐴) ∧ (𝑣 ∈ (𝑁‘(𝑚 ∖ {𝑥})) ∧ 𝑤 ∈ (𝑁‘(𝑛 ∖ {𝑥})))) → ((𝑚 ∪ 𝑛) ∖ {𝑥}) ⊆ 𝑉) |
71 | 3, 7, 21 | lspcl 19371 |
. . . . . . . . . . . 12
⊢ ((𝑊 ∈ LMod ∧ ((𝑚 ∪ 𝑛) ∖ {𝑥}) ⊆ 𝑉) → (𝑁‘((𝑚 ∪ 𝑛) ∖ {𝑥})) ∈ 𝑃) |
72 | 63, 70, 71 | syl2anc 579 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑚 ∈ 𝐴 ∧ 𝑛 ∈ 𝐴) ∧ (𝑣 ∈ (𝑁‘(𝑚 ∖ {𝑥})) ∧ 𝑤 ∈ (𝑁‘(𝑛 ∖ {𝑥})))) → (𝑁‘((𝑚 ∪ 𝑛) ∖ {𝑥})) ∈ 𝑃) |
73 | | simp1r 1212 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑚 ∈ 𝐴 ∧ 𝑛 ∈ 𝐴) ∧ (𝑣 ∈ (𝑁‘(𝑚 ∖ {𝑥})) ∧ 𝑤 ∈ (𝑁‘(𝑛 ∖ {𝑥})))) → 𝑟 ∈ (Base‘(Scalar‘𝑊))) |
74 | | ssun1 3998 |
. . . . . . . . . . . . . 14
⊢ 𝑚 ⊆ (𝑚 ∪ 𝑛) |
75 | | ssdif 3967 |
. . . . . . . . . . . . . 14
⊢ (𝑚 ⊆ (𝑚 ∪ 𝑛) → (𝑚 ∖ {𝑥}) ⊆ ((𝑚 ∪ 𝑛) ∖ {𝑥})) |
76 | 74, 75 | mp1i 13 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑚 ∈ 𝐴 ∧ 𝑛 ∈ 𝐴) ∧ (𝑣 ∈ (𝑁‘(𝑚 ∖ {𝑥})) ∧ 𝑤 ∈ (𝑁‘(𝑛 ∖ {𝑥})))) → (𝑚 ∖ {𝑥}) ⊆ ((𝑚 ∪ 𝑛) ∖ {𝑥})) |
77 | 3, 21 | lspss 19379 |
. . . . . . . . . . . . 13
⊢ ((𝑊 ∈ LMod ∧ ((𝑚 ∪ 𝑛) ∖ {𝑥}) ⊆ 𝑉 ∧ (𝑚 ∖ {𝑥}) ⊆ ((𝑚 ∪ 𝑛) ∖ {𝑥})) → (𝑁‘(𝑚 ∖ {𝑥})) ⊆ (𝑁‘((𝑚 ∪ 𝑛) ∖ {𝑥}))) |
78 | 63, 70, 76, 77 | syl3anc 1439 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑚 ∈ 𝐴 ∧ 𝑛 ∈ 𝐴) ∧ (𝑣 ∈ (𝑁‘(𝑚 ∖ {𝑥})) ∧ 𝑤 ∈ (𝑁‘(𝑛 ∖ {𝑥})))) → (𝑁‘(𝑚 ∖ {𝑥})) ⊆ (𝑁‘((𝑚 ∪ 𝑛) ∖ {𝑥}))) |
79 | | simp3l 1215 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑚 ∈ 𝐴 ∧ 𝑛 ∈ 𝐴) ∧ (𝑣 ∈ (𝑁‘(𝑚 ∖ {𝑥})) ∧ 𝑤 ∈ (𝑁‘(𝑛 ∖ {𝑥})))) → 𝑣 ∈ (𝑁‘(𝑚 ∖ {𝑥}))) |
80 | 78, 79 | sseldd 3821 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑚 ∈ 𝐴 ∧ 𝑛 ∈ 𝐴) ∧ (𝑣 ∈ (𝑁‘(𝑚 ∖ {𝑥})) ∧ 𝑤 ∈ (𝑁‘(𝑛 ∖ {𝑥})))) → 𝑣 ∈ (𝑁‘((𝑚 ∪ 𝑛) ∖ {𝑥}))) |
81 | | ssun2 3999 |
. . . . . . . . . . . . . 14
⊢ 𝑛 ⊆ (𝑚 ∪ 𝑛) |
82 | | ssdif 3967 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ⊆ (𝑚 ∪ 𝑛) → (𝑛 ∖ {𝑥}) ⊆ ((𝑚 ∪ 𝑛) ∖ {𝑥})) |
83 | 81, 82 | mp1i 13 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑚 ∈ 𝐴 ∧ 𝑛 ∈ 𝐴) ∧ (𝑣 ∈ (𝑁‘(𝑚 ∖ {𝑥})) ∧ 𝑤 ∈ (𝑁‘(𝑛 ∖ {𝑥})))) → (𝑛 ∖ {𝑥}) ⊆ ((𝑚 ∪ 𝑛) ∖ {𝑥})) |
84 | 3, 21 | lspss 19379 |
. . . . . . . . . . . . 13
⊢ ((𝑊 ∈ LMod ∧ ((𝑚 ∪ 𝑛) ∖ {𝑥}) ⊆ 𝑉 ∧ (𝑛 ∖ {𝑥}) ⊆ ((𝑚 ∪ 𝑛) ∖ {𝑥})) → (𝑁‘(𝑛 ∖ {𝑥})) ⊆ (𝑁‘((𝑚 ∪ 𝑛) ∖ {𝑥}))) |
85 | 63, 70, 83, 84 | syl3anc 1439 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑚 ∈ 𝐴 ∧ 𝑛 ∈ 𝐴) ∧ (𝑣 ∈ (𝑁‘(𝑚 ∖ {𝑥})) ∧ 𝑤 ∈ (𝑁‘(𝑛 ∖ {𝑥})))) → (𝑁‘(𝑛 ∖ {𝑥})) ⊆ (𝑁‘((𝑚 ∪ 𝑛) ∖ {𝑥}))) |
86 | | simp3r 1216 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑚 ∈ 𝐴 ∧ 𝑛 ∈ 𝐴) ∧ (𝑣 ∈ (𝑁‘(𝑚 ∖ {𝑥})) ∧ 𝑤 ∈ (𝑁‘(𝑛 ∖ {𝑥})))) → 𝑤 ∈ (𝑁‘(𝑛 ∖ {𝑥}))) |
87 | 85, 86 | sseldd 3821 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑚 ∈ 𝐴 ∧ 𝑛 ∈ 𝐴) ∧ (𝑣 ∈ (𝑁‘(𝑚 ∖ {𝑥})) ∧ 𝑤 ∈ (𝑁‘(𝑛 ∖ {𝑥})))) → 𝑤 ∈ (𝑁‘((𝑚 ∪ 𝑛) ∖ {𝑥}))) |
88 | | eqid 2777 |
. . . . . . . . . . . 12
⊢
(Scalar‘𝑊) =
(Scalar‘𝑊) |
89 | | eqid 2777 |
. . . . . . . . . . . 12
⊢
(Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊)) |
90 | | eqid 2777 |
. . . . . . . . . . . 12
⊢
(+g‘𝑊) = (+g‘𝑊) |
91 | | eqid 2777 |
. . . . . . . . . . . 12
⊢ (
·𝑠 ‘𝑊) = ( ·𝑠
‘𝑊) |
92 | 88, 89, 90, 91, 7 | lsscl 19335 |
. . . . . . . . . . 11
⊢ (((𝑁‘((𝑚 ∪ 𝑛) ∖ {𝑥})) ∈ 𝑃 ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑣 ∈ (𝑁‘((𝑚 ∪ 𝑛) ∖ {𝑥})) ∧ 𝑤 ∈ (𝑁‘((𝑚 ∪ 𝑛) ∖ {𝑥})))) → ((𝑟( ·𝑠
‘𝑊)𝑣)(+g‘𝑊)𝑤) ∈ (𝑁‘((𝑚 ∪ 𝑛) ∖ {𝑥}))) |
93 | 72, 73, 80, 87, 92 | syl13anc 1440 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑚 ∈ 𝐴 ∧ 𝑛 ∈ 𝐴) ∧ (𝑣 ∈ (𝑁‘(𝑚 ∖ {𝑥})) ∧ 𝑤 ∈ (𝑁‘(𝑛 ∖ {𝑥})))) → ((𝑟( ·𝑠
‘𝑊)𝑣)(+g‘𝑊)𝑤) ∈ (𝑁‘((𝑚 ∪ 𝑛) ∖ {𝑥}))) |
94 | | difeq1 3943 |
. . . . . . . . . . . 12
⊢ (𝑢 = (𝑚 ∪ 𝑛) → (𝑢 ∖ {𝑥}) = ((𝑚 ∪ 𝑛) ∖ {𝑥})) |
95 | 94 | fveq2d 6450 |
. . . . . . . . . . 11
⊢ (𝑢 = (𝑚 ∪ 𝑛) → (𝑁‘(𝑢 ∖ {𝑥})) = (𝑁‘((𝑚 ∪ 𝑛) ∖ {𝑥}))) |
96 | 95 | eliuni 4759 |
. . . . . . . . . 10
⊢ (((𝑚 ∪ 𝑛) ∈ 𝐴 ∧ ((𝑟( ·𝑠
‘𝑊)𝑣)(+g‘𝑊)𝑤) ∈ (𝑁‘((𝑚 ∪ 𝑛) ∖ {𝑥}))) → ((𝑟( ·𝑠
‘𝑊)𝑣)(+g‘𝑊)𝑤) ∈ ∪
𝑢 ∈ 𝐴 (𝑁‘(𝑢 ∖ {𝑥}))) |
97 | 62, 93, 96 | syl2anc 579 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑚 ∈ 𝐴 ∧ 𝑛 ∈ 𝐴) ∧ (𝑣 ∈ (𝑁‘(𝑚 ∖ {𝑥})) ∧ 𝑤 ∈ (𝑁‘(𝑛 ∖ {𝑥})))) → ((𝑟( ·𝑠
‘𝑊)𝑣)(+g‘𝑊)𝑤) ∈ ∪
𝑢 ∈ 𝐴 (𝑁‘(𝑢 ∖ {𝑥}))) |
98 | 97, 9 | syl6eleqr 2869 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑚 ∈ 𝐴 ∧ 𝑛 ∈ 𝐴) ∧ (𝑣 ∈ (𝑁‘(𝑚 ∖ {𝑥})) ∧ 𝑤 ∈ (𝑁‘(𝑛 ∖ {𝑥})))) → ((𝑟( ·𝑠
‘𝑊)𝑣)(+g‘𝑊)𝑤) ∈ 𝑇) |
99 | 98 | 3expia 1111 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑚 ∈ 𝐴 ∧ 𝑛 ∈ 𝐴)) → ((𝑣 ∈ (𝑁‘(𝑚 ∖ {𝑥})) ∧ 𝑤 ∈ (𝑁‘(𝑛 ∖ {𝑥}))) → ((𝑟( ·𝑠
‘𝑊)𝑣)(+g‘𝑊)𝑤) ∈ 𝑇)) |
100 | 99 | rexlimdvva 3220 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) → (∃𝑚 ∈ 𝐴 ∃𝑛 ∈ 𝐴 (𝑣 ∈ (𝑁‘(𝑚 ∖ {𝑥})) ∧ 𝑤 ∈ (𝑁‘(𝑛 ∖ {𝑥}))) → ((𝑟( ·𝑠
‘𝑊)𝑣)(+g‘𝑊)𝑤) ∈ 𝑇)) |
101 | 56, 100 | syl5bi 234 |
. . . . 5
⊢ ((𝜑 ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) → ((𝑣 ∈ 𝑇 ∧ 𝑤 ∈ 𝑇) → ((𝑟( ·𝑠
‘𝑊)𝑣)(+g‘𝑊)𝑤) ∈ 𝑇)) |
102 | 101 | exp4b 423 |
. . . 4
⊢ (𝜑 → (𝑟 ∈ (Base‘(Scalar‘𝑊)) → (𝑣 ∈ 𝑇 → (𝑤 ∈ 𝑇 → ((𝑟( ·𝑠
‘𝑊)𝑣)(+g‘𝑊)𝑤) ∈ 𝑇)))) |
103 | 102 | 3imp2 1411 |
. . 3
⊢ ((𝜑 ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑣 ∈ 𝑇 ∧ 𝑤 ∈ 𝑇)) → ((𝑟( ·𝑠
‘𝑊)𝑣)(+g‘𝑊)𝑤) ∈ 𝑇) |
104 | 1, 2, 4, 5, 6, 8, 27, 39, 103 | islssd 19328 |
. 2
⊢ (𝜑 → 𝑇 ∈ 𝑃) |
105 | | eldifi 3954 |
. . . . . . 7
⊢ (𝑦 ∈ (∪ 𝐴
∖ {𝑥}) → 𝑦 ∈ ∪ 𝐴) |
106 | 105 | adantl 475 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ (∪ 𝐴 ∖ {𝑥})) → 𝑦 ∈ ∪ 𝐴) |
107 | | eldifn 3955 |
. . . . . . . . . 10
⊢ (𝑦 ∈ (∪ 𝐴
∖ {𝑥}) → ¬
𝑦 ∈ {𝑥}) |
108 | 107 | ad2antlr 717 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ (∪ 𝐴 ∖ {𝑥})) ∧ 𝑢 ∈ 𝐴) → ¬ 𝑦 ∈ {𝑥}) |
109 | | eldif 3801 |
. . . . . . . . . 10
⊢ (𝑦 ∈ (𝑢 ∖ {𝑥}) ↔ (𝑦 ∈ 𝑢 ∧ ¬ 𝑦 ∈ {𝑥})) |
110 | 3, 21 | lspssid 19380 |
. . . . . . . . . . . . 13
⊢ ((𝑊 ∈ LMod ∧ (𝑢 ∖ {𝑥}) ⊆ 𝑉) → (𝑢 ∖ {𝑥}) ⊆ (𝑁‘(𝑢 ∖ {𝑥}))) |
111 | 12, 20, 110 | syl2an2r 675 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑢 ∈ 𝐴) → (𝑢 ∖ {𝑥}) ⊆ (𝑁‘(𝑢 ∖ {𝑥}))) |
112 | 111 | adantlr 705 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ (∪ 𝐴 ∖ {𝑥})) ∧ 𝑢 ∈ 𝐴) → (𝑢 ∖ {𝑥}) ⊆ (𝑁‘(𝑢 ∖ {𝑥}))) |
113 | 112 | sseld 3819 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ (∪ 𝐴 ∖ {𝑥})) ∧ 𝑢 ∈ 𝐴) → (𝑦 ∈ (𝑢 ∖ {𝑥}) → 𝑦 ∈ (𝑁‘(𝑢 ∖ {𝑥})))) |
114 | 109, 113 | syl5bir 235 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ (∪ 𝐴 ∖ {𝑥})) ∧ 𝑢 ∈ 𝐴) → ((𝑦 ∈ 𝑢 ∧ ¬ 𝑦 ∈ {𝑥}) → 𝑦 ∈ (𝑁‘(𝑢 ∖ {𝑥})))) |
115 | 108, 114 | mpan2d 684 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ (∪ 𝐴 ∖ {𝑥})) ∧ 𝑢 ∈ 𝐴) → (𝑦 ∈ 𝑢 → 𝑦 ∈ (𝑁‘(𝑢 ∖ {𝑥})))) |
116 | 115 | reximdva 3197 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ (∪ 𝐴 ∖ {𝑥})) → (∃𝑢 ∈ 𝐴 𝑦 ∈ 𝑢 → ∃𝑢 ∈ 𝐴 𝑦 ∈ (𝑁‘(𝑢 ∖ {𝑥})))) |
117 | | eluni2 4675 |
. . . . . . 7
⊢ (𝑦 ∈ ∪ 𝐴
↔ ∃𝑢 ∈
𝐴 𝑦 ∈ 𝑢) |
118 | | eliun 4757 |
. . . . . . 7
⊢ (𝑦 ∈ ∪ 𝑢 ∈ 𝐴 (𝑁‘(𝑢 ∖ {𝑥})) ↔ ∃𝑢 ∈ 𝐴 𝑦 ∈ (𝑁‘(𝑢 ∖ {𝑥}))) |
119 | 116, 117,
118 | 3imtr4g 288 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ (∪ 𝐴 ∖ {𝑥})) → (𝑦 ∈ ∪ 𝐴 → 𝑦 ∈ ∪
𝑢 ∈ 𝐴 (𝑁‘(𝑢 ∖ {𝑥})))) |
120 | 106, 119 | mpd 15 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (∪ 𝐴 ∖ {𝑥})) → 𝑦 ∈ ∪
𝑢 ∈ 𝐴 (𝑁‘(𝑢 ∖ {𝑥}))) |
121 | 120 | ex 403 |
. . . 4
⊢ (𝜑 → (𝑦 ∈ (∪ 𝐴 ∖ {𝑥}) → 𝑦 ∈ ∪
𝑢 ∈ 𝐴 (𝑁‘(𝑢 ∖ {𝑥})))) |
122 | 121 | ssrdv 3826 |
. . 3
⊢ (𝜑 → (∪ 𝐴
∖ {𝑥}) ⊆
∪ 𝑢 ∈ 𝐴 (𝑁‘(𝑢 ∖ {𝑥}))) |
123 | 122, 9 | syl6sseqr 3870 |
. 2
⊢ (𝜑 → (∪ 𝐴
∖ {𝑥}) ⊆ 𝑇) |
124 | 104, 123 | jca 507 |
1
⊢ (𝜑 → (𝑇 ∈ 𝑃 ∧ (∪ 𝐴 ∖ {𝑥}) ⊆ 𝑇)) |