MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  lbsextlem2 Structured version   Visualization version   GIF version

Theorem lbsextlem2 19860
Description: Lemma for lbsext 19864. Since 𝐴 is a chain (actually, we only need it to be closed under binary union), the union 𝑇 of the spans of each individual element of 𝐴 is a subspace, and it contains all of 𝐴 (except for our target vector 𝑥- we are trying to make 𝑥 a linear combination of all the other vectors in some set from 𝐴). (Contributed by Mario Carneiro, 25-Jun-2014.)
Hypotheses
Ref Expression
lbsext.v 𝑉 = (Base‘𝑊)
lbsext.j 𝐽 = (LBasis‘𝑊)
lbsext.n 𝑁 = (LSpan‘𝑊)
lbsext.w (𝜑𝑊 ∈ LVec)
lbsext.c (𝜑𝐶𝑉)
lbsext.x (𝜑 → ∀𝑥𝐶 ¬ 𝑥 ∈ (𝑁‘(𝐶 ∖ {𝑥})))
lbsext.s 𝑆 = {𝑧 ∈ 𝒫 𝑉 ∣ (𝐶𝑧 ∧ ∀𝑥𝑧 ¬ 𝑥 ∈ (𝑁‘(𝑧 ∖ {𝑥})))}
lbsext.p 𝑃 = (LSubSp‘𝑊)
lbsext.a (𝜑𝐴𝑆)
lbsext.z (𝜑𝐴 ≠ ∅)
lbsext.r (𝜑 → [] Or 𝐴)
lbsext.t 𝑇 = 𝑢𝐴 (𝑁‘(𝑢 ∖ {𝑥}))
Assertion
Ref Expression
lbsextlem2 (𝜑 → (𝑇𝑃 ∧ ( 𝐴 ∖ {𝑥}) ⊆ 𝑇))
Distinct variable groups:   𝑥,𝐽   𝑥,𝑢,𝜑   𝑢,𝑆,𝑥   𝑥,𝑧,𝐶   𝑧,𝑢,𝑁,𝑥   𝑢,𝑉,𝑥,𝑧   𝑢,𝑊,𝑥   𝑢,𝐴,𝑥,𝑧
Allowed substitution hints:   𝜑(𝑧)   𝐶(𝑢)   𝑃(𝑥,𝑧,𝑢)   𝑆(𝑧)   𝑇(𝑥,𝑧,𝑢)   𝐽(𝑧,𝑢)   𝑊(𝑧)

Proof of Theorem lbsextlem2
Dummy variables 𝑚 𝑛 𝑟 𝑣 𝑤 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqidd 2819 . . 3 (𝜑 → (Scalar‘𝑊) = (Scalar‘𝑊))
2 eqidd 2819 . . 3 (𝜑 → (Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊)))
3 lbsext.v . . . 4 𝑉 = (Base‘𝑊)
43a1i 11 . . 3 (𝜑𝑉 = (Base‘𝑊))
5 eqidd 2819 . . 3 (𝜑 → (+g𝑊) = (+g𝑊))
6 eqidd 2819 . . 3 (𝜑 → ( ·𝑠𝑊) = ( ·𝑠𝑊))
7 lbsext.p . . . 4 𝑃 = (LSubSp‘𝑊)
87a1i 11 . . 3 (𝜑𝑃 = (LSubSp‘𝑊))
9 lbsext.t . . . 4 𝑇 = 𝑢𝐴 (𝑁‘(𝑢 ∖ {𝑥}))
10 lbsext.w . . . . . . . 8 (𝜑𝑊 ∈ LVec)
11 lveclmod 19807 . . . . . . . 8 (𝑊 ∈ LVec → 𝑊 ∈ LMod)
1210, 11syl 17 . . . . . . 7 (𝜑𝑊 ∈ LMod)
13 lbsext.a . . . . . . . . . . 11 (𝜑𝐴𝑆)
14 lbsext.s . . . . . . . . . . . 12 𝑆 = {𝑧 ∈ 𝒫 𝑉 ∣ (𝐶𝑧 ∧ ∀𝑥𝑧 ¬ 𝑥 ∈ (𝑁‘(𝑧 ∖ {𝑥})))}
1514ssrab3 4054 . . . . . . . . . . 11 𝑆 ⊆ 𝒫 𝑉
1613, 15sstrdi 3976 . . . . . . . . . 10 (𝜑𝐴 ⊆ 𝒫 𝑉)
1716sselda 3964 . . . . . . . . 9 ((𝜑𝑢𝐴) → 𝑢 ∈ 𝒫 𝑉)
1817elpwid 4549 . . . . . . . 8 ((𝜑𝑢𝐴) → 𝑢𝑉)
1918ssdifssd 4116 . . . . . . 7 ((𝜑𝑢𝐴) → (𝑢 ∖ {𝑥}) ⊆ 𝑉)
20 lbsext.n . . . . . . . 8 𝑁 = (LSpan‘𝑊)
213, 20lspssv 19684 . . . . . . 7 ((𝑊 ∈ LMod ∧ (𝑢 ∖ {𝑥}) ⊆ 𝑉) → (𝑁‘(𝑢 ∖ {𝑥})) ⊆ 𝑉)
2212, 19, 21syl2an2r 681 . . . . . 6 ((𝜑𝑢𝐴) → (𝑁‘(𝑢 ∖ {𝑥})) ⊆ 𝑉)
2322ralrimiva 3179 . . . . 5 (𝜑 → ∀𝑢𝐴 (𝑁‘(𝑢 ∖ {𝑥})) ⊆ 𝑉)
24 iunss 4960 . . . . 5 ( 𝑢𝐴 (𝑁‘(𝑢 ∖ {𝑥})) ⊆ 𝑉 ↔ ∀𝑢𝐴 (𝑁‘(𝑢 ∖ {𝑥})) ⊆ 𝑉)
2523, 24sylibr 235 . . . 4 (𝜑 𝑢𝐴 (𝑁‘(𝑢 ∖ {𝑥})) ⊆ 𝑉)
269, 25eqsstrid 4012 . . 3 (𝜑𝑇𝑉)
279a1i 11 . . . 4 (𝜑𝑇 = 𝑢𝐴 (𝑁‘(𝑢 ∖ {𝑥})))
28 lbsext.z . . . . . 6 (𝜑𝐴 ≠ ∅)
293, 7, 20lspcl 19677 . . . . . . . . 9 ((𝑊 ∈ LMod ∧ (𝑢 ∖ {𝑥}) ⊆ 𝑉) → (𝑁‘(𝑢 ∖ {𝑥})) ∈ 𝑃)
3012, 19, 29syl2an2r 681 . . . . . . . 8 ((𝜑𝑢𝐴) → (𝑁‘(𝑢 ∖ {𝑥})) ∈ 𝑃)
317lssn0 19641 . . . . . . . 8 ((𝑁‘(𝑢 ∖ {𝑥})) ∈ 𝑃 → (𝑁‘(𝑢 ∖ {𝑥})) ≠ ∅)
3230, 31syl 17 . . . . . . 7 ((𝜑𝑢𝐴) → (𝑁‘(𝑢 ∖ {𝑥})) ≠ ∅)
3332ralrimiva 3179 . . . . . 6 (𝜑 → ∀𝑢𝐴 (𝑁‘(𝑢 ∖ {𝑥})) ≠ ∅)
34 r19.2z 4436 . . . . . 6 ((𝐴 ≠ ∅ ∧ ∀𝑢𝐴 (𝑁‘(𝑢 ∖ {𝑥})) ≠ ∅) → ∃𝑢𝐴 (𝑁‘(𝑢 ∖ {𝑥})) ≠ ∅)
3528, 33, 34syl2anc 584 . . . . 5 (𝜑 → ∃𝑢𝐴 (𝑁‘(𝑢 ∖ {𝑥})) ≠ ∅)
36 iunn0 4980 . . . . 5 (∃𝑢𝐴 (𝑁‘(𝑢 ∖ {𝑥})) ≠ ∅ ↔ 𝑢𝐴 (𝑁‘(𝑢 ∖ {𝑥})) ≠ ∅)
3735, 36sylib 219 . . . 4 (𝜑 𝑢𝐴 (𝑁‘(𝑢 ∖ {𝑥})) ≠ ∅)
3827, 37eqnetrd 3080 . . 3 (𝜑𝑇 ≠ ∅)
399eleq2i 2901 . . . . . . . . 9 (𝑣𝑇𝑣 𝑢𝐴 (𝑁‘(𝑢 ∖ {𝑥})))
40 eliun 4914 . . . . . . . . 9 (𝑣 𝑢𝐴 (𝑁‘(𝑢 ∖ {𝑥})) ↔ ∃𝑢𝐴 𝑣 ∈ (𝑁‘(𝑢 ∖ {𝑥})))
41 difeq1 4089 . . . . . . . . . . . 12 (𝑢 = 𝑚 → (𝑢 ∖ {𝑥}) = (𝑚 ∖ {𝑥}))
4241fveq2d 6667 . . . . . . . . . . 11 (𝑢 = 𝑚 → (𝑁‘(𝑢 ∖ {𝑥})) = (𝑁‘(𝑚 ∖ {𝑥})))
4342eleq2d 2895 . . . . . . . . . 10 (𝑢 = 𝑚 → (𝑣 ∈ (𝑁‘(𝑢 ∖ {𝑥})) ↔ 𝑣 ∈ (𝑁‘(𝑚 ∖ {𝑥}))))
4443cbvrexvw 3448 . . . . . . . . 9 (∃𝑢𝐴 𝑣 ∈ (𝑁‘(𝑢 ∖ {𝑥})) ↔ ∃𝑚𝐴 𝑣 ∈ (𝑁‘(𝑚 ∖ {𝑥})))
4539, 40, 443bitri 298 . . . . . . . 8 (𝑣𝑇 ↔ ∃𝑚𝐴 𝑣 ∈ (𝑁‘(𝑚 ∖ {𝑥})))
469eleq2i 2901 . . . . . . . . 9 (𝑤𝑇𝑤 𝑢𝐴 (𝑁‘(𝑢 ∖ {𝑥})))
47 eliun 4914 . . . . . . . . 9 (𝑤 𝑢𝐴 (𝑁‘(𝑢 ∖ {𝑥})) ↔ ∃𝑢𝐴 𝑤 ∈ (𝑁‘(𝑢 ∖ {𝑥})))
48 difeq1 4089 . . . . . . . . . . . 12 (𝑢 = 𝑛 → (𝑢 ∖ {𝑥}) = (𝑛 ∖ {𝑥}))
4948fveq2d 6667 . . . . . . . . . . 11 (𝑢 = 𝑛 → (𝑁‘(𝑢 ∖ {𝑥})) = (𝑁‘(𝑛 ∖ {𝑥})))
5049eleq2d 2895 . . . . . . . . . 10 (𝑢 = 𝑛 → (𝑤 ∈ (𝑁‘(𝑢 ∖ {𝑥})) ↔ 𝑤 ∈ (𝑁‘(𝑛 ∖ {𝑥}))))
5150cbvrexvw 3448 . . . . . . . . 9 (∃𝑢𝐴 𝑤 ∈ (𝑁‘(𝑢 ∖ {𝑥})) ↔ ∃𝑛𝐴 𝑤 ∈ (𝑁‘(𝑛 ∖ {𝑥})))
5246, 47, 513bitri 298 . . . . . . . 8 (𝑤𝑇 ↔ ∃𝑛𝐴 𝑤 ∈ (𝑁‘(𝑛 ∖ {𝑥})))
5345, 52anbi12i 626 . . . . . . 7 ((𝑣𝑇𝑤𝑇) ↔ (∃𝑚𝐴 𝑣 ∈ (𝑁‘(𝑚 ∖ {𝑥})) ∧ ∃𝑛𝐴 𝑤 ∈ (𝑁‘(𝑛 ∖ {𝑥}))))
54 reeanv 3365 . . . . . . 7 (∃𝑚𝐴𝑛𝐴 (𝑣 ∈ (𝑁‘(𝑚 ∖ {𝑥})) ∧ 𝑤 ∈ (𝑁‘(𝑛 ∖ {𝑥}))) ↔ (∃𝑚𝐴 𝑣 ∈ (𝑁‘(𝑚 ∖ {𝑥})) ∧ ∃𝑛𝐴 𝑤 ∈ (𝑁‘(𝑛 ∖ {𝑥}))))
5553, 54bitr4i 279 . . . . . 6 ((𝑣𝑇𝑤𝑇) ↔ ∃𝑚𝐴𝑛𝐴 (𝑣 ∈ (𝑁‘(𝑚 ∖ {𝑥})) ∧ 𝑤 ∈ (𝑁‘(𝑛 ∖ {𝑥}))))
56 simp1l 1189 . . . . . . . . . . . 12 (((𝜑𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑚𝐴𝑛𝐴) ∧ (𝑣 ∈ (𝑁‘(𝑚 ∖ {𝑥})) ∧ 𝑤 ∈ (𝑁‘(𝑛 ∖ {𝑥})))) → 𝜑)
57 lbsext.r . . . . . . . . . . . 12 (𝜑 → [] Or 𝐴)
5856, 57syl 17 . . . . . . . . . . 11 (((𝜑𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑚𝐴𝑛𝐴) ∧ (𝑣 ∈ (𝑁‘(𝑚 ∖ {𝑥})) ∧ 𝑤 ∈ (𝑁‘(𝑛 ∖ {𝑥})))) → [] Or 𝐴)
59 simp2 1129 . . . . . . . . . . 11 (((𝜑𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑚𝐴𝑛𝐴) ∧ (𝑣 ∈ (𝑁‘(𝑚 ∖ {𝑥})) ∧ 𝑤 ∈ (𝑁‘(𝑛 ∖ {𝑥})))) → (𝑚𝐴𝑛𝐴))
60 sorpssun 7445 . . . . . . . . . . 11 (( [] Or 𝐴 ∧ (𝑚𝐴𝑛𝐴)) → (𝑚𝑛) ∈ 𝐴)
6158, 59, 60syl2anc 584 . . . . . . . . . 10 (((𝜑𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑚𝐴𝑛𝐴) ∧ (𝑣 ∈ (𝑁‘(𝑚 ∖ {𝑥})) ∧ 𝑤 ∈ (𝑁‘(𝑛 ∖ {𝑥})))) → (𝑚𝑛) ∈ 𝐴)
6256, 12syl 17 . . . . . . . . . . . 12 (((𝜑𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑚𝐴𝑛𝐴) ∧ (𝑣 ∈ (𝑁‘(𝑚 ∖ {𝑥})) ∧ 𝑤 ∈ (𝑁‘(𝑛 ∖ {𝑥})))) → 𝑊 ∈ LMod)
63 elssuni 4859 . . . . . . . . . . . . . . 15 ((𝑚𝑛) ∈ 𝐴 → (𝑚𝑛) ⊆ 𝐴)
6461, 63syl 17 . . . . . . . . . . . . . 14 (((𝜑𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑚𝐴𝑛𝐴) ∧ (𝑣 ∈ (𝑁‘(𝑚 ∖ {𝑥})) ∧ 𝑤 ∈ (𝑁‘(𝑛 ∖ {𝑥})))) → (𝑚𝑛) ⊆ 𝐴)
65 sspwuni 5013 . . . . . . . . . . . . . . . 16 (𝐴 ⊆ 𝒫 𝑉 𝐴𝑉)
6616, 65sylib 219 . . . . . . . . . . . . . . 15 (𝜑 𝐴𝑉)
6756, 66syl 17 . . . . . . . . . . . . . 14 (((𝜑𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑚𝐴𝑛𝐴) ∧ (𝑣 ∈ (𝑁‘(𝑚 ∖ {𝑥})) ∧ 𝑤 ∈ (𝑁‘(𝑛 ∖ {𝑥})))) → 𝐴𝑉)
6864, 67sstrd 3974 . . . . . . . . . . . . 13 (((𝜑𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑚𝐴𝑛𝐴) ∧ (𝑣 ∈ (𝑁‘(𝑚 ∖ {𝑥})) ∧ 𝑤 ∈ (𝑁‘(𝑛 ∖ {𝑥})))) → (𝑚𝑛) ⊆ 𝑉)
6968ssdifssd 4116 . . . . . . . . . . . 12 (((𝜑𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑚𝐴𝑛𝐴) ∧ (𝑣 ∈ (𝑁‘(𝑚 ∖ {𝑥})) ∧ 𝑤 ∈ (𝑁‘(𝑛 ∖ {𝑥})))) → ((𝑚𝑛) ∖ {𝑥}) ⊆ 𝑉)
703, 7, 20lspcl 19677 . . . . . . . . . . . 12 ((𝑊 ∈ LMod ∧ ((𝑚𝑛) ∖ {𝑥}) ⊆ 𝑉) → (𝑁‘((𝑚𝑛) ∖ {𝑥})) ∈ 𝑃)
7162, 69, 70syl2anc 584 . . . . . . . . . . 11 (((𝜑𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑚𝐴𝑛𝐴) ∧ (𝑣 ∈ (𝑁‘(𝑚 ∖ {𝑥})) ∧ 𝑤 ∈ (𝑁‘(𝑛 ∖ {𝑥})))) → (𝑁‘((𝑚𝑛) ∖ {𝑥})) ∈ 𝑃)
72 simp1r 1190 . . . . . . . . . . 11 (((𝜑𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑚𝐴𝑛𝐴) ∧ (𝑣 ∈ (𝑁‘(𝑚 ∖ {𝑥})) ∧ 𝑤 ∈ (𝑁‘(𝑛 ∖ {𝑥})))) → 𝑟 ∈ (Base‘(Scalar‘𝑊)))
73 ssun1 4145 . . . . . . . . . . . . . 14 𝑚 ⊆ (𝑚𝑛)
74 ssdif 4113 . . . . . . . . . . . . . 14 (𝑚 ⊆ (𝑚𝑛) → (𝑚 ∖ {𝑥}) ⊆ ((𝑚𝑛) ∖ {𝑥}))
7573, 74mp1i 13 . . . . . . . . . . . . 13 (((𝜑𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑚𝐴𝑛𝐴) ∧ (𝑣 ∈ (𝑁‘(𝑚 ∖ {𝑥})) ∧ 𝑤 ∈ (𝑁‘(𝑛 ∖ {𝑥})))) → (𝑚 ∖ {𝑥}) ⊆ ((𝑚𝑛) ∖ {𝑥}))
763, 20lspss 19685 . . . . . . . . . . . . 13 ((𝑊 ∈ LMod ∧ ((𝑚𝑛) ∖ {𝑥}) ⊆ 𝑉 ∧ (𝑚 ∖ {𝑥}) ⊆ ((𝑚𝑛) ∖ {𝑥})) → (𝑁‘(𝑚 ∖ {𝑥})) ⊆ (𝑁‘((𝑚𝑛) ∖ {𝑥})))
7762, 69, 75, 76syl3anc 1363 . . . . . . . . . . . 12 (((𝜑𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑚𝐴𝑛𝐴) ∧ (𝑣 ∈ (𝑁‘(𝑚 ∖ {𝑥})) ∧ 𝑤 ∈ (𝑁‘(𝑛 ∖ {𝑥})))) → (𝑁‘(𝑚 ∖ {𝑥})) ⊆ (𝑁‘((𝑚𝑛) ∖ {𝑥})))
78 simp3l 1193 . . . . . . . . . . . 12 (((𝜑𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑚𝐴𝑛𝐴) ∧ (𝑣 ∈ (𝑁‘(𝑚 ∖ {𝑥})) ∧ 𝑤 ∈ (𝑁‘(𝑛 ∖ {𝑥})))) → 𝑣 ∈ (𝑁‘(𝑚 ∖ {𝑥})))
7977, 78sseldd 3965 . . . . . . . . . . 11 (((𝜑𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑚𝐴𝑛𝐴) ∧ (𝑣 ∈ (𝑁‘(𝑚 ∖ {𝑥})) ∧ 𝑤 ∈ (𝑁‘(𝑛 ∖ {𝑥})))) → 𝑣 ∈ (𝑁‘((𝑚𝑛) ∖ {𝑥})))
80 ssun2 4146 . . . . . . . . . . . . . 14 𝑛 ⊆ (𝑚𝑛)
81 ssdif 4113 . . . . . . . . . . . . . 14 (𝑛 ⊆ (𝑚𝑛) → (𝑛 ∖ {𝑥}) ⊆ ((𝑚𝑛) ∖ {𝑥}))
8280, 81mp1i 13 . . . . . . . . . . . . 13 (((𝜑𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑚𝐴𝑛𝐴) ∧ (𝑣 ∈ (𝑁‘(𝑚 ∖ {𝑥})) ∧ 𝑤 ∈ (𝑁‘(𝑛 ∖ {𝑥})))) → (𝑛 ∖ {𝑥}) ⊆ ((𝑚𝑛) ∖ {𝑥}))
833, 20lspss 19685 . . . . . . . . . . . . 13 ((𝑊 ∈ LMod ∧ ((𝑚𝑛) ∖ {𝑥}) ⊆ 𝑉 ∧ (𝑛 ∖ {𝑥}) ⊆ ((𝑚𝑛) ∖ {𝑥})) → (𝑁‘(𝑛 ∖ {𝑥})) ⊆ (𝑁‘((𝑚𝑛) ∖ {𝑥})))
8462, 69, 82, 83syl3anc 1363 . . . . . . . . . . . 12 (((𝜑𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑚𝐴𝑛𝐴) ∧ (𝑣 ∈ (𝑁‘(𝑚 ∖ {𝑥})) ∧ 𝑤 ∈ (𝑁‘(𝑛 ∖ {𝑥})))) → (𝑁‘(𝑛 ∖ {𝑥})) ⊆ (𝑁‘((𝑚𝑛) ∖ {𝑥})))
85 simp3r 1194 . . . . . . . . . . . 12 (((𝜑𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑚𝐴𝑛𝐴) ∧ (𝑣 ∈ (𝑁‘(𝑚 ∖ {𝑥})) ∧ 𝑤 ∈ (𝑁‘(𝑛 ∖ {𝑥})))) → 𝑤 ∈ (𝑁‘(𝑛 ∖ {𝑥})))
8684, 85sseldd 3965 . . . . . . . . . . 11 (((𝜑𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑚𝐴𝑛𝐴) ∧ (𝑣 ∈ (𝑁‘(𝑚 ∖ {𝑥})) ∧ 𝑤 ∈ (𝑁‘(𝑛 ∖ {𝑥})))) → 𝑤 ∈ (𝑁‘((𝑚𝑛) ∖ {𝑥})))
87 eqid 2818 . . . . . . . . . . . 12 (Scalar‘𝑊) = (Scalar‘𝑊)
88 eqid 2818 . . . . . . . . . . . 12 (Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊))
89 eqid 2818 . . . . . . . . . . . 12 (+g𝑊) = (+g𝑊)
90 eqid 2818 . . . . . . . . . . . 12 ( ·𝑠𝑊) = ( ·𝑠𝑊)
9187, 88, 89, 90, 7lsscl 19643 . . . . . . . . . . 11 (((𝑁‘((𝑚𝑛) ∖ {𝑥})) ∈ 𝑃 ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑣 ∈ (𝑁‘((𝑚𝑛) ∖ {𝑥})) ∧ 𝑤 ∈ (𝑁‘((𝑚𝑛) ∖ {𝑥})))) → ((𝑟( ·𝑠𝑊)𝑣)(+g𝑊)𝑤) ∈ (𝑁‘((𝑚𝑛) ∖ {𝑥})))
9271, 72, 79, 86, 91syl13anc 1364 . . . . . . . . . 10 (((𝜑𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑚𝐴𝑛𝐴) ∧ (𝑣 ∈ (𝑁‘(𝑚 ∖ {𝑥})) ∧ 𝑤 ∈ (𝑁‘(𝑛 ∖ {𝑥})))) → ((𝑟( ·𝑠𝑊)𝑣)(+g𝑊)𝑤) ∈ (𝑁‘((𝑚𝑛) ∖ {𝑥})))
93 difeq1 4089 . . . . . . . . . . . 12 (𝑢 = (𝑚𝑛) → (𝑢 ∖ {𝑥}) = ((𝑚𝑛) ∖ {𝑥}))
9493fveq2d 6667 . . . . . . . . . . 11 (𝑢 = (𝑚𝑛) → (𝑁‘(𝑢 ∖ {𝑥})) = (𝑁‘((𝑚𝑛) ∖ {𝑥})))
9594eliuni 4916 . . . . . . . . . 10 (((𝑚𝑛) ∈ 𝐴 ∧ ((𝑟( ·𝑠𝑊)𝑣)(+g𝑊)𝑤) ∈ (𝑁‘((𝑚𝑛) ∖ {𝑥}))) → ((𝑟( ·𝑠𝑊)𝑣)(+g𝑊)𝑤) ∈ 𝑢𝐴 (𝑁‘(𝑢 ∖ {𝑥})))
9661, 92, 95syl2anc 584 . . . . . . . . 9 (((𝜑𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑚𝐴𝑛𝐴) ∧ (𝑣 ∈ (𝑁‘(𝑚 ∖ {𝑥})) ∧ 𝑤 ∈ (𝑁‘(𝑛 ∖ {𝑥})))) → ((𝑟( ·𝑠𝑊)𝑣)(+g𝑊)𝑤) ∈ 𝑢𝐴 (𝑁‘(𝑢 ∖ {𝑥})))
9796, 9eleqtrrdi 2921 . . . . . . . 8 (((𝜑𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑚𝐴𝑛𝐴) ∧ (𝑣 ∈ (𝑁‘(𝑚 ∖ {𝑥})) ∧ 𝑤 ∈ (𝑁‘(𝑛 ∖ {𝑥})))) → ((𝑟( ·𝑠𝑊)𝑣)(+g𝑊)𝑤) ∈ 𝑇)
98973expia 1113 . . . . . . 7 (((𝜑𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑚𝐴𝑛𝐴)) → ((𝑣 ∈ (𝑁‘(𝑚 ∖ {𝑥})) ∧ 𝑤 ∈ (𝑁‘(𝑛 ∖ {𝑥}))) → ((𝑟( ·𝑠𝑊)𝑣)(+g𝑊)𝑤) ∈ 𝑇))
9998rexlimdvva 3291 . . . . . 6 ((𝜑𝑟 ∈ (Base‘(Scalar‘𝑊))) → (∃𝑚𝐴𝑛𝐴 (𝑣 ∈ (𝑁‘(𝑚 ∖ {𝑥})) ∧ 𝑤 ∈ (𝑁‘(𝑛 ∖ {𝑥}))) → ((𝑟( ·𝑠𝑊)𝑣)(+g𝑊)𝑤) ∈ 𝑇))
10055, 99syl5bi 243 . . . . 5 ((𝜑𝑟 ∈ (Base‘(Scalar‘𝑊))) → ((𝑣𝑇𝑤𝑇) → ((𝑟( ·𝑠𝑊)𝑣)(+g𝑊)𝑤) ∈ 𝑇))
101100exp4b 431 . . . 4 (𝜑 → (𝑟 ∈ (Base‘(Scalar‘𝑊)) → (𝑣𝑇 → (𝑤𝑇 → ((𝑟( ·𝑠𝑊)𝑣)(+g𝑊)𝑤) ∈ 𝑇))))
1021013imp2 1341 . . 3 ((𝜑 ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑣𝑇𝑤𝑇)) → ((𝑟( ·𝑠𝑊)𝑣)(+g𝑊)𝑤) ∈ 𝑇)
1031, 2, 4, 5, 6, 8, 26, 38, 102islssd 19636 . 2 (𝜑𝑇𝑃)
104 eldifi 4100 . . . . . . 7 (𝑦 ∈ ( 𝐴 ∖ {𝑥}) → 𝑦 𝐴)
105104adantl 482 . . . . . 6 ((𝜑𝑦 ∈ ( 𝐴 ∖ {𝑥})) → 𝑦 𝐴)
106 eldifn 4101 . . . . . . . . . 10 (𝑦 ∈ ( 𝐴 ∖ {𝑥}) → ¬ 𝑦 ∈ {𝑥})
107106ad2antlr 723 . . . . . . . . 9 (((𝜑𝑦 ∈ ( 𝐴 ∖ {𝑥})) ∧ 𝑢𝐴) → ¬ 𝑦 ∈ {𝑥})
108 eldif 3943 . . . . . . . . . 10 (𝑦 ∈ (𝑢 ∖ {𝑥}) ↔ (𝑦𝑢 ∧ ¬ 𝑦 ∈ {𝑥}))
1093, 20lspssid 19686 . . . . . . . . . . . . 13 ((𝑊 ∈ LMod ∧ (𝑢 ∖ {𝑥}) ⊆ 𝑉) → (𝑢 ∖ {𝑥}) ⊆ (𝑁‘(𝑢 ∖ {𝑥})))
11012, 19, 109syl2an2r 681 . . . . . . . . . . . 12 ((𝜑𝑢𝐴) → (𝑢 ∖ {𝑥}) ⊆ (𝑁‘(𝑢 ∖ {𝑥})))
111110adantlr 711 . . . . . . . . . . 11 (((𝜑𝑦 ∈ ( 𝐴 ∖ {𝑥})) ∧ 𝑢𝐴) → (𝑢 ∖ {𝑥}) ⊆ (𝑁‘(𝑢 ∖ {𝑥})))
112111sseld 3963 . . . . . . . . . 10 (((𝜑𝑦 ∈ ( 𝐴 ∖ {𝑥})) ∧ 𝑢𝐴) → (𝑦 ∈ (𝑢 ∖ {𝑥}) → 𝑦 ∈ (𝑁‘(𝑢 ∖ {𝑥}))))
113108, 112syl5bir 244 . . . . . . . . 9 (((𝜑𝑦 ∈ ( 𝐴 ∖ {𝑥})) ∧ 𝑢𝐴) → ((𝑦𝑢 ∧ ¬ 𝑦 ∈ {𝑥}) → 𝑦 ∈ (𝑁‘(𝑢 ∖ {𝑥}))))
114107, 113mpan2d 690 . . . . . . . 8 (((𝜑𝑦 ∈ ( 𝐴 ∖ {𝑥})) ∧ 𝑢𝐴) → (𝑦𝑢𝑦 ∈ (𝑁‘(𝑢 ∖ {𝑥}))))
115114reximdva 3271 . . . . . . 7 ((𝜑𝑦 ∈ ( 𝐴 ∖ {𝑥})) → (∃𝑢𝐴 𝑦𝑢 → ∃𝑢𝐴 𝑦 ∈ (𝑁‘(𝑢 ∖ {𝑥}))))
116 eluni2 4834 . . . . . . 7 (𝑦 𝐴 ↔ ∃𝑢𝐴 𝑦𝑢)
117 eliun 4914 . . . . . . 7 (𝑦 𝑢𝐴 (𝑁‘(𝑢 ∖ {𝑥})) ↔ ∃𝑢𝐴 𝑦 ∈ (𝑁‘(𝑢 ∖ {𝑥})))
118115, 116, 1173imtr4g 297 . . . . . 6 ((𝜑𝑦 ∈ ( 𝐴 ∖ {𝑥})) → (𝑦 𝐴𝑦 𝑢𝐴 (𝑁‘(𝑢 ∖ {𝑥}))))
119105, 118mpd 15 . . . . 5 ((𝜑𝑦 ∈ ( 𝐴 ∖ {𝑥})) → 𝑦 𝑢𝐴 (𝑁‘(𝑢 ∖ {𝑥})))
120119ex 413 . . . 4 (𝜑 → (𝑦 ∈ ( 𝐴 ∖ {𝑥}) → 𝑦 𝑢𝐴 (𝑁‘(𝑢 ∖ {𝑥}))))
121120ssrdv 3970 . . 3 (𝜑 → ( 𝐴 ∖ {𝑥}) ⊆ 𝑢𝐴 (𝑁‘(𝑢 ∖ {𝑥})))
122121, 9sseqtrrdi 4015 . 2 (𝜑 → ( 𝐴 ∖ {𝑥}) ⊆ 𝑇)
123103, 122jca 512 1 (𝜑 → (𝑇𝑃 ∧ ( 𝐴 ∖ {𝑥}) ⊆ 𝑇))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 396  w3a 1079   = wceq 1528  wcel 2105  wne 3013  wral 3135  wrex 3136  {crab 3139  cdif 3930  cun 3931  wss 3933  c0 4288  𝒫 cpw 4535  {csn 4557   cuni 4830   ciun 4910   Or wor 5466  cfv 6348  (class class class)co 7145   [] crpss 7437  Basecbs 16471  +gcplusg 16553  Scalarcsca 16556   ·𝑠 cvsca 16557  LModclmod 19563  LSubSpclss 19632  LSpanclspn 19672  LBasisclbs 19775  LVecclvec 19803
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-rep 5181  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7450  ax-cnex 10581  ax-resscn 10582  ax-1cn 10583  ax-icn 10584  ax-addcl 10585  ax-addrcl 10586  ax-mulcl 10587  ax-mulrcl 10588  ax-mulcom 10589  ax-addass 10590  ax-mulass 10591  ax-distr 10592  ax-i2m1 10593  ax-1ne0 10594  ax-1rid 10595  ax-rnegex 10596  ax-rrecex 10597  ax-cnre 10598  ax-pre-lttri 10599  ax-pre-lttrn 10600  ax-pre-ltadd 10601  ax-pre-mulgt0 10602
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-nel 3121  df-ral 3140  df-rex 3141  df-reu 3142  df-rmo 3143  df-rab 3144  df-v 3494  df-sbc 3770  df-csb 3881  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-pss 3951  df-nul 4289  df-if 4464  df-pw 4537  df-sn 4558  df-pr 4560  df-tp 4562  df-op 4564  df-uni 4831  df-int 4868  df-iun 4912  df-br 5058  df-opab 5120  df-mpt 5138  df-tr 5164  df-id 5453  df-eprel 5458  df-po 5467  df-so 5468  df-fr 5507  df-we 5509  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-pred 6141  df-ord 6187  df-on 6188  df-lim 6189  df-suc 6190  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-riota 7103  df-ov 7148  df-oprab 7149  df-mpo 7150  df-rpss 7438  df-om 7570  df-1st 7678  df-2nd 7679  df-wrecs 7936  df-recs 7997  df-rdg 8035  df-er 8278  df-en 8498  df-dom 8499  df-sdom 8500  df-pnf 10665  df-mnf 10666  df-xr 10667  df-ltxr 10668  df-le 10669  df-sub 10860  df-neg 10861  df-nn 11627  df-2 11688  df-ndx 16474  df-slot 16475  df-base 16477  df-sets 16478  df-plusg 16566  df-0g 16703  df-mgm 17840  df-sgrp 17889  df-mnd 17900  df-grp 18044  df-minusg 18045  df-sbg 18046  df-mgp 19169  df-ur 19181  df-ring 19228  df-lmod 19565  df-lss 19633  df-lsp 19673  df-lvec 19804
This theorem is referenced by:  lbsextlem3  19861
  Copyright terms: Public domain W3C validator