Metamath Proof Explorer

Theorem lbsextlem2

Description: Lemma for lbsext . Since A is a chain (actually, we only need it to be closed under binary union), the union T of the spans of each individual element of A is a subspace, and it contains all of U. A (except for our target vector x - we are trying to make x a linear combination of all the other vectors in some set from A ). (Contributed by Mario Carneiro, 25-Jun-2014)

Ref Expression
Hypotheses 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 lbsextlem2 ( 𝜑 → ( 𝑇 ∈ 𝑃 ∧ ( ∪ 𝐴 ∖ { 𝑥 } ) ⊆ 𝑇 ) )

Proof

Step Hyp Ref Expression
1 lbsext.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 lbsext.j ⊢ 𝐽 = ( LBasis ‘ 𝑊 )
3 lbsext.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
4 lbsext.w ⊢ ( 𝜑 → 𝑊 ∈ LVec )
5 lbsext.c ⊢ ( 𝜑 → 𝐶 ⊆ 𝑉 )
6 lbsext.x ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐶 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝐶 ∖ { 𝑥 } ) ) )
7 lbsext.s ⊢ 𝑆 = { 𝑧 ∈ 𝒫 𝑉 ∣ ( 𝐶 ⊆ 𝑧 ∧ ∀ 𝑥 ∈ 𝑧 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝑧 ∖ { 𝑥 } ) ) ) }
8 lbsext.p ⊢ 𝑃 = ( LSubSp ‘ 𝑊 )
9 lbsext.a ⊢ ( 𝜑 → 𝐴 ⊆ 𝑆 )
10 lbsext.z ⊢ ( 𝜑 → 𝐴 ≠ ∅ )
11 lbsext.r ⊢ ( 𝜑 → [⊊] Or 𝐴 )
12 lbsext.t ⊢ 𝑇 = ∪ 𝑢 ∈ 𝐴 ( 𝑁 ‘ ( 𝑢 ∖ { 𝑥 } ) )
13 eqidd ⊢ ( 𝜑 → ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 ) )
14 eqidd ⊢ ( 𝜑 → ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
15 1 a1i ⊢ ( 𝜑 → 𝑉 = ( Base ‘ 𝑊 ) )
16 eqidd ⊢ ( 𝜑 → ( +g ‘ 𝑊 ) = ( +g ‘ 𝑊 ) )
17 eqidd ⊢ ( 𝜑 → ( ·𝑠 ‘ 𝑊 ) = ( ·𝑠 ‘ 𝑊 ) )
18 8 a1i ⊢ ( 𝜑 → 𝑃 = ( LSubSp ‘ 𝑊 ) )
19 lveclmod ⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
20 4 19 syl ⊢ ( 𝜑 → 𝑊 ∈ LMod )
21 7 ssrab3 ⊢ 𝑆 ⊆ 𝒫 𝑉
22 9 21 sstrdi ⊢ ( 𝜑 → 𝐴 ⊆ 𝒫 𝑉 )
23 22 sselda ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝐴 ) → 𝑢 ∈ 𝒫 𝑉 )
24 23 elpwid ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝐴 ) → 𝑢 ⊆ 𝑉 )
25 24 ssdifssd ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝐴 ) → ( 𝑢 ∖ { 𝑥 } ) ⊆ 𝑉 )
26 1 3 lspssv ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑢 ∖ { 𝑥 } ) ⊆ 𝑉 ) → ( 𝑁 ‘ ( 𝑢 ∖ { 𝑥 } ) ) ⊆ 𝑉 )
27 20 25 26 syl2an2r ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝐴 ) → ( 𝑁 ‘ ( 𝑢 ∖ { 𝑥 } ) ) ⊆ 𝑉 )
28 27 ralrimiva ⊢ ( 𝜑 → ∀ 𝑢 ∈ 𝐴 ( 𝑁 ‘ ( 𝑢 ∖ { 𝑥 } ) ) ⊆ 𝑉 )
29 iunss ⊢ ( ∪ 𝑢 ∈ 𝐴 ( 𝑁 ‘ ( 𝑢 ∖ { 𝑥 } ) ) ⊆ 𝑉 ↔ ∀ 𝑢 ∈ 𝐴 ( 𝑁 ‘ ( 𝑢 ∖ { 𝑥 } ) ) ⊆ 𝑉 )
30 28 29 sylibr ⊢ ( 𝜑 → ∪ 𝑢 ∈ 𝐴 ( 𝑁 ‘ ( 𝑢 ∖ { 𝑥 } ) ) ⊆ 𝑉 )
31 12 30 eqsstrid ⊢ ( 𝜑 → 𝑇 ⊆ 𝑉 )
32 12 a1i ⊢ ( 𝜑 → 𝑇 = ∪ 𝑢 ∈ 𝐴 ( 𝑁 ‘ ( 𝑢 ∖ { 𝑥 } ) ) )
33 1 8 3 lspcl ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑢 ∖ { 𝑥 } ) ⊆ 𝑉 ) → ( 𝑁 ‘ ( 𝑢 ∖ { 𝑥 } ) ) ∈ 𝑃 )
34 20 25 33 syl2an2r ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝐴 ) → ( 𝑁 ‘ ( 𝑢 ∖ { 𝑥 } ) ) ∈ 𝑃 )
35 8 lssn0 ⊢ ( ( 𝑁 ‘ ( 𝑢 ∖ { 𝑥 } ) ) ∈ 𝑃 → ( 𝑁 ‘ ( 𝑢 ∖ { 𝑥 } ) ) ≠ ∅ )
36 34 35 syl ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝐴 ) → ( 𝑁 ‘ ( 𝑢 ∖ { 𝑥 } ) ) ≠ ∅ )
37 36 ralrimiva ⊢ ( 𝜑 → ∀ 𝑢 ∈ 𝐴 ( 𝑁 ‘ ( 𝑢 ∖ { 𝑥 } ) ) ≠ ∅ )
38 r19.2z ⊢ ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑢 ∈ 𝐴 ( 𝑁 ‘ ( 𝑢 ∖ { 𝑥 } ) ) ≠ ∅ ) → ∃ 𝑢 ∈ 𝐴 ( 𝑁 ‘ ( 𝑢 ∖ { 𝑥 } ) ) ≠ ∅ )
39 10 37 38 syl2anc ⊢ ( 𝜑 → ∃ 𝑢 ∈ 𝐴 ( 𝑁 ‘ ( 𝑢 ∖ { 𝑥 } ) ) ≠ ∅ )
40 iunn0 ⊢ ( ∃ 𝑢 ∈ 𝐴 ( 𝑁 ‘ ( 𝑢 ∖ { 𝑥 } ) ) ≠ ∅ ↔ ∪ 𝑢 ∈ 𝐴 ( 𝑁 ‘ ( 𝑢 ∖ { 𝑥 } ) ) ≠ ∅ )
41 39 40 sylib ⊢ ( 𝜑 → ∪ 𝑢 ∈ 𝐴 ( 𝑁 ‘ ( 𝑢 ∖ { 𝑥 } ) ) ≠ ∅ )
42 32 41 eqnetrd ⊢ ( 𝜑 → 𝑇 ≠ ∅ )
43 12 eleq2i ⊢ ( 𝑣 ∈ 𝑇 ↔ 𝑣 ∈ ∪ 𝑢 ∈ 𝐴 ( 𝑁 ‘ ( 𝑢 ∖ { 𝑥 } ) ) )
44 eliun ⊢ ( 𝑣 ∈ ∪ 𝑢 ∈ 𝐴 ( 𝑁 ‘ ( 𝑢 ∖ { 𝑥 } ) ) ↔ ∃ 𝑢 ∈ 𝐴 𝑣 ∈ ( 𝑁 ‘ ( 𝑢 ∖ { 𝑥 } ) ) )
45 difeq1 ⊢ ( 𝑢 = 𝑚 → ( 𝑢 ∖ { 𝑥 } ) = ( 𝑚 ∖ { 𝑥 } ) )
46 45 fveq2d ⊢ ( 𝑢 = 𝑚 → ( 𝑁 ‘ ( 𝑢 ∖ { 𝑥 } ) ) = ( 𝑁 ‘ ( 𝑚 ∖ { 𝑥 } ) ) )
47 46 eleq2d ⊢ ( 𝑢 = 𝑚 → ( 𝑣 ∈ ( 𝑁 ‘ ( 𝑢 ∖ { 𝑥 } ) ) ↔ 𝑣 ∈ ( 𝑁 ‘ ( 𝑚 ∖ { 𝑥 } ) ) ) )
48 47 cbvrexvw ⊢ ( ∃ 𝑢 ∈ 𝐴 𝑣 ∈ ( 𝑁 ‘ ( 𝑢 ∖ { 𝑥 } ) ) ↔ ∃ 𝑚 ∈ 𝐴 𝑣 ∈ ( 𝑁 ‘ ( 𝑚 ∖ { 𝑥 } ) ) )
49 43 44 48 3bitri ⊢ ( 𝑣 ∈ 𝑇 ↔ ∃ 𝑚 ∈ 𝐴 𝑣 ∈ ( 𝑁 ‘ ( 𝑚 ∖ { 𝑥 } ) ) )
50 12 eleq2i ⊢ ( 𝑤 ∈ 𝑇 ↔ 𝑤 ∈ ∪ 𝑢 ∈ 𝐴 ( 𝑁 ‘ ( 𝑢 ∖ { 𝑥 } ) ) )
51 eliun ⊢ ( 𝑤 ∈ ∪ 𝑢 ∈ 𝐴 ( 𝑁 ‘ ( 𝑢 ∖ { 𝑥 } ) ) ↔ ∃ 𝑢 ∈ 𝐴 𝑤 ∈ ( 𝑁 ‘ ( 𝑢 ∖ { 𝑥 } ) ) )
52 difeq1 ⊢ ( 𝑢 = 𝑛 → ( 𝑢 ∖ { 𝑥 } ) = ( 𝑛 ∖ { 𝑥 } ) )
53 52 fveq2d ⊢ ( 𝑢 = 𝑛 → ( 𝑁 ‘ ( 𝑢 ∖ { 𝑥 } ) ) = ( 𝑁 ‘ ( 𝑛 ∖ { 𝑥 } ) ) )
54 53 eleq2d ⊢ ( 𝑢 = 𝑛 → ( 𝑤 ∈ ( 𝑁 ‘ ( 𝑢 ∖ { 𝑥 } ) ) ↔ 𝑤 ∈ ( 𝑁 ‘ ( 𝑛 ∖ { 𝑥 } ) ) ) )
55 54 cbvrexvw ⊢ ( ∃ 𝑢 ∈ 𝐴 𝑤 ∈ ( 𝑁 ‘ ( 𝑢 ∖ { 𝑥 } ) ) ↔ ∃ 𝑛 ∈ 𝐴 𝑤 ∈ ( 𝑁 ‘ ( 𝑛 ∖ { 𝑥 } ) ) )
56 50 51 55 3bitri ⊢ ( 𝑤 ∈ 𝑇 ↔ ∃ 𝑛 ∈ 𝐴 𝑤 ∈ ( 𝑁 ‘ ( 𝑛 ∖ { 𝑥 } ) ) )
57 49 56 anbi12i ⊢ ( ( 𝑣 ∈ 𝑇 ∧ 𝑤 ∈ 𝑇 ) ↔ ( ∃ 𝑚 ∈ 𝐴 𝑣 ∈ ( 𝑁 ‘ ( 𝑚 ∖ { 𝑥 } ) ) ∧ ∃ 𝑛 ∈ 𝐴 𝑤 ∈ ( 𝑁 ‘ ( 𝑛 ∖ { 𝑥 } ) ) ) )
58 reeanv ⊢ ( ∃ 𝑚 ∈ 𝐴 ∃ 𝑛 ∈ 𝐴 ( 𝑣 ∈ ( 𝑁 ‘ ( 𝑚 ∖ { 𝑥 } ) ) ∧ 𝑤 ∈ ( 𝑁 ‘ ( 𝑛 ∖ { 𝑥 } ) ) ) ↔ ( ∃ 𝑚 ∈ 𝐴 𝑣 ∈ ( 𝑁 ‘ ( 𝑚 ∖ { 𝑥 } ) ) ∧ ∃ 𝑛 ∈ 𝐴 𝑤 ∈ ( 𝑁 ‘ ( 𝑛 ∖ { 𝑥 } ) ) ) )
59 57 58 bitr4i ⊢ ( ( 𝑣 ∈ 𝑇 ∧ 𝑤 ∈ 𝑇 ) ↔ ∃ 𝑚 ∈ 𝐴 ∃ 𝑛 ∈ 𝐴 ( 𝑣 ∈ ( 𝑁 ‘ ( 𝑚 ∖ { 𝑥 } ) ) ∧ 𝑤 ∈ ( 𝑁 ‘ ( 𝑛 ∖ { 𝑥 } ) ) ) )
60 simp1l ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( 𝑚 ∈ 𝐴 ∧ 𝑛 ∈ 𝐴 ) ∧ ( 𝑣 ∈ ( 𝑁 ‘ ( 𝑚 ∖ { 𝑥 } ) ) ∧ 𝑤 ∈ ( 𝑁 ‘ ( 𝑛 ∖ { 𝑥 } ) ) ) ) → 𝜑 )
61 60 11 syl ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( 𝑚 ∈ 𝐴 ∧ 𝑛 ∈ 𝐴 ) ∧ ( 𝑣 ∈ ( 𝑁 ‘ ( 𝑚 ∖ { 𝑥 } ) ) ∧ 𝑤 ∈ ( 𝑁 ‘ ( 𝑛 ∖ { 𝑥 } ) ) ) ) → [⊊] Or 𝐴 )
62 simp2 ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( 𝑚 ∈ 𝐴 ∧ 𝑛 ∈ 𝐴 ) ∧ ( 𝑣 ∈ ( 𝑁 ‘ ( 𝑚 ∖ { 𝑥 } ) ) ∧ 𝑤 ∈ ( 𝑁 ‘ ( 𝑛 ∖ { 𝑥 } ) ) ) ) → ( 𝑚 ∈ 𝐴 ∧ 𝑛 ∈ 𝐴 ) )
63 sorpssun ⊢ ( ( [⊊] Or 𝐴 ∧ ( 𝑚 ∈ 𝐴 ∧ 𝑛 ∈ 𝐴 ) ) → ( 𝑚 ∪ 𝑛 ) ∈ 𝐴 )
64 61 62 63 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( 𝑚 ∈ 𝐴 ∧ 𝑛 ∈ 𝐴 ) ∧ ( 𝑣 ∈ ( 𝑁 ‘ ( 𝑚 ∖ { 𝑥 } ) ) ∧ 𝑤 ∈ ( 𝑁 ‘ ( 𝑛 ∖ { 𝑥 } ) ) ) ) → ( 𝑚 ∪ 𝑛 ) ∈ 𝐴 )
65 60 20 syl ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( 𝑚 ∈ 𝐴 ∧ 𝑛 ∈ 𝐴 ) ∧ ( 𝑣 ∈ ( 𝑁 ‘ ( 𝑚 ∖ { 𝑥 } ) ) ∧ 𝑤 ∈ ( 𝑁 ‘ ( 𝑛 ∖ { 𝑥 } ) ) ) ) → 𝑊 ∈ LMod )
66 elssuni ⊢ ( ( 𝑚 ∪ 𝑛 ) ∈ 𝐴 → ( 𝑚 ∪ 𝑛 ) ⊆ ∪ 𝐴 )
67 64 66 syl ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( 𝑚 ∈ 𝐴 ∧ 𝑛 ∈ 𝐴 ) ∧ ( 𝑣 ∈ ( 𝑁 ‘ ( 𝑚 ∖ { 𝑥 } ) ) ∧ 𝑤 ∈ ( 𝑁 ‘ ( 𝑛 ∖ { 𝑥 } ) ) ) ) → ( 𝑚 ∪ 𝑛 ) ⊆ ∪ 𝐴 )
68 sspwuni ⊢ ( 𝐴 ⊆ 𝒫 𝑉 ↔ ∪ 𝐴 ⊆ 𝑉 )
69 22 68 sylib ⊢ ( 𝜑 → ∪ 𝐴 ⊆ 𝑉 )
70 60 69 syl ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( 𝑚 ∈ 𝐴 ∧ 𝑛 ∈ 𝐴 ) ∧ ( 𝑣 ∈ ( 𝑁 ‘ ( 𝑚 ∖ { 𝑥 } ) ) ∧ 𝑤 ∈ ( 𝑁 ‘ ( 𝑛 ∖ { 𝑥 } ) ) ) ) → ∪ 𝐴 ⊆ 𝑉 )
71 67 70 sstrd ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( 𝑚 ∈ 𝐴 ∧ 𝑛 ∈ 𝐴 ) ∧ ( 𝑣 ∈ ( 𝑁 ‘ ( 𝑚 ∖ { 𝑥 } ) ) ∧ 𝑤 ∈ ( 𝑁 ‘ ( 𝑛 ∖ { 𝑥 } ) ) ) ) → ( 𝑚 ∪ 𝑛 ) ⊆ 𝑉 )
72 71 ssdifssd ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( 𝑚 ∈ 𝐴 ∧ 𝑛 ∈ 𝐴 ) ∧ ( 𝑣 ∈ ( 𝑁 ‘ ( 𝑚 ∖ { 𝑥 } ) ) ∧ 𝑤 ∈ ( 𝑁 ‘ ( 𝑛 ∖ { 𝑥 } ) ) ) ) → ( ( 𝑚 ∪ 𝑛 ) ∖ { 𝑥 } ) ⊆ 𝑉 )
73 1 8 3 lspcl ⊢ ( ( 𝑊 ∈ LMod ∧ ( ( 𝑚 ∪ 𝑛 ) ∖ { 𝑥 } ) ⊆ 𝑉 ) → ( 𝑁 ‘ ( ( 𝑚 ∪ 𝑛 ) ∖ { 𝑥 } ) ) ∈ 𝑃 )
74 65 72 73 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( 𝑚 ∈ 𝐴 ∧ 𝑛 ∈ 𝐴 ) ∧ ( 𝑣 ∈ ( 𝑁 ‘ ( 𝑚 ∖ { 𝑥 } ) ) ∧ 𝑤 ∈ ( 𝑁 ‘ ( 𝑛 ∖ { 𝑥 } ) ) ) ) → ( 𝑁 ‘ ( ( 𝑚 ∪ 𝑛 ) ∖ { 𝑥 } ) ) ∈ 𝑃 )
75 simp1r ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( 𝑚 ∈ 𝐴 ∧ 𝑛 ∈ 𝐴 ) ∧ ( 𝑣 ∈ ( 𝑁 ‘ ( 𝑚 ∖ { 𝑥 } ) ) ∧ 𝑤 ∈ ( 𝑁 ‘ ( 𝑛 ∖ { 𝑥 } ) ) ) ) → 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
76 ssun1 ⊢ 𝑚 ⊆ ( 𝑚 ∪ 𝑛 )
77 ssdif ⊢ ( 𝑚 ⊆ ( 𝑚 ∪ 𝑛 ) → ( 𝑚 ∖ { 𝑥 } ) ⊆ ( ( 𝑚 ∪ 𝑛 ) ∖ { 𝑥 } ) )
78 76 77 mp1i ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( 𝑚 ∈ 𝐴 ∧ 𝑛 ∈ 𝐴 ) ∧ ( 𝑣 ∈ ( 𝑁 ‘ ( 𝑚 ∖ { 𝑥 } ) ) ∧ 𝑤 ∈ ( 𝑁 ‘ ( 𝑛 ∖ { 𝑥 } ) ) ) ) → ( 𝑚 ∖ { 𝑥 } ) ⊆ ( ( 𝑚 ∪ 𝑛 ) ∖ { 𝑥 } ) )
79 1 3 lspss ⊢ ( ( 𝑊 ∈ LMod ∧ ( ( 𝑚 ∪ 𝑛 ) ∖ { 𝑥 } ) ⊆ 𝑉 ∧ ( 𝑚 ∖ { 𝑥 } ) ⊆ ( ( 𝑚 ∪ 𝑛 ) ∖ { 𝑥 } ) ) → ( 𝑁 ‘ ( 𝑚 ∖ { 𝑥 } ) ) ⊆ ( 𝑁 ‘ ( ( 𝑚 ∪ 𝑛 ) ∖ { 𝑥 } ) ) )
80 65 72 78 79 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( 𝑚 ∈ 𝐴 ∧ 𝑛 ∈ 𝐴 ) ∧ ( 𝑣 ∈ ( 𝑁 ‘ ( 𝑚 ∖ { 𝑥 } ) ) ∧ 𝑤 ∈ ( 𝑁 ‘ ( 𝑛 ∖ { 𝑥 } ) ) ) ) → ( 𝑁 ‘ ( 𝑚 ∖ { 𝑥 } ) ) ⊆ ( 𝑁 ‘ ( ( 𝑚 ∪ 𝑛 ) ∖ { 𝑥 } ) ) )
81 simp3l ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( 𝑚 ∈ 𝐴 ∧ 𝑛 ∈ 𝐴 ) ∧ ( 𝑣 ∈ ( 𝑁 ‘ ( 𝑚 ∖ { 𝑥 } ) ) ∧ 𝑤 ∈ ( 𝑁 ‘ ( 𝑛 ∖ { 𝑥 } ) ) ) ) → 𝑣 ∈ ( 𝑁 ‘ ( 𝑚 ∖ { 𝑥 } ) ) )
82 80 81 sseldd ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( 𝑚 ∈ 𝐴 ∧ 𝑛 ∈ 𝐴 ) ∧ ( 𝑣 ∈ ( 𝑁 ‘ ( 𝑚 ∖ { 𝑥 } ) ) ∧ 𝑤 ∈ ( 𝑁 ‘ ( 𝑛 ∖ { 𝑥 } ) ) ) ) → 𝑣 ∈ ( 𝑁 ‘ ( ( 𝑚 ∪ 𝑛 ) ∖ { 𝑥 } ) ) )
83 ssun2 ⊢ 𝑛 ⊆ ( 𝑚 ∪ 𝑛 )
84 ssdif ⊢ ( 𝑛 ⊆ ( 𝑚 ∪ 𝑛 ) → ( 𝑛 ∖ { 𝑥 } ) ⊆ ( ( 𝑚 ∪ 𝑛 ) ∖ { 𝑥 } ) )
85 83 84 mp1i ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( 𝑚 ∈ 𝐴 ∧ 𝑛 ∈ 𝐴 ) ∧ ( 𝑣 ∈ ( 𝑁 ‘ ( 𝑚 ∖ { 𝑥 } ) ) ∧ 𝑤 ∈ ( 𝑁 ‘ ( 𝑛 ∖ { 𝑥 } ) ) ) ) → ( 𝑛 ∖ { 𝑥 } ) ⊆ ( ( 𝑚 ∪ 𝑛 ) ∖ { 𝑥 } ) )
86 1 3 lspss ⊢ ( ( 𝑊 ∈ LMod ∧ ( ( 𝑚 ∪ 𝑛 ) ∖ { 𝑥 } ) ⊆ 𝑉 ∧ ( 𝑛 ∖ { 𝑥 } ) ⊆ ( ( 𝑚 ∪ 𝑛 ) ∖ { 𝑥 } ) ) → ( 𝑁 ‘ ( 𝑛 ∖ { 𝑥 } ) ) ⊆ ( 𝑁 ‘ ( ( 𝑚 ∪ 𝑛 ) ∖ { 𝑥 } ) ) )
87 65 72 85 86 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( 𝑚 ∈ 𝐴 ∧ 𝑛 ∈ 𝐴 ) ∧ ( 𝑣 ∈ ( 𝑁 ‘ ( 𝑚 ∖ { 𝑥 } ) ) ∧ 𝑤 ∈ ( 𝑁 ‘ ( 𝑛 ∖ { 𝑥 } ) ) ) ) → ( 𝑁 ‘ ( 𝑛 ∖ { 𝑥 } ) ) ⊆ ( 𝑁 ‘ ( ( 𝑚 ∪ 𝑛 ) ∖ { 𝑥 } ) ) )
88 simp3r ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( 𝑚 ∈ 𝐴 ∧ 𝑛 ∈ 𝐴 ) ∧ ( 𝑣 ∈ ( 𝑁 ‘ ( 𝑚 ∖ { 𝑥 } ) ) ∧ 𝑤 ∈ ( 𝑁 ‘ ( 𝑛 ∖ { 𝑥 } ) ) ) ) → 𝑤 ∈ ( 𝑁 ‘ ( 𝑛 ∖ { 𝑥 } ) ) )
89 87 88 sseldd ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( 𝑚 ∈ 𝐴 ∧ 𝑛 ∈ 𝐴 ) ∧ ( 𝑣 ∈ ( 𝑁 ‘ ( 𝑚 ∖ { 𝑥 } ) ) ∧ 𝑤 ∈ ( 𝑁 ‘ ( 𝑛 ∖ { 𝑥 } ) ) ) ) → 𝑤 ∈ ( 𝑁 ‘ ( ( 𝑚 ∪ 𝑛 ) ∖ { 𝑥 } ) ) )
90 eqid ⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
91 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ ( Scalar ‘ 𝑊 ) )
92 eqid ⊢ ( +g ‘ 𝑊 ) = ( +g ‘ 𝑊 )
93 eqid ⊢ ( ·𝑠 ‘ 𝑊 ) = ( ·𝑠 ‘ 𝑊 )
94 90 91 92 93 8 lsscl ⊢ ( ( ( 𝑁 ‘ ( ( 𝑚 ∪ 𝑛 ) ∖ { 𝑥 } ) ) ∈ 𝑃 ∧ ( 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑣 ∈ ( 𝑁 ‘ ( ( 𝑚 ∪ 𝑛 ) ∖ { 𝑥 } ) ) ∧ 𝑤 ∈ ( 𝑁 ‘ ( ( 𝑚 ∪ 𝑛 ) ∖ { 𝑥 } ) ) ) ) → ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ( +g ‘ 𝑊 ) 𝑤 ) ∈ ( 𝑁 ‘ ( ( 𝑚 ∪ 𝑛 ) ∖ { 𝑥 } ) ) )
95 74 75 82 89 94 syl13anc ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( 𝑚 ∈ 𝐴 ∧ 𝑛 ∈ 𝐴 ) ∧ ( 𝑣 ∈ ( 𝑁 ‘ ( 𝑚 ∖ { 𝑥 } ) ) ∧ 𝑤 ∈ ( 𝑁 ‘ ( 𝑛 ∖ { 𝑥 } ) ) ) ) → ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ( +g ‘ 𝑊 ) 𝑤 ) ∈ ( 𝑁 ‘ ( ( 𝑚 ∪ 𝑛 ) ∖ { 𝑥 } ) ) )
96 difeq1 ⊢ ( 𝑢 = ( 𝑚 ∪ 𝑛 ) → ( 𝑢 ∖ { 𝑥 } ) = ( ( 𝑚 ∪ 𝑛 ) ∖ { 𝑥 } ) )
97 96 fveq2d ⊢ ( 𝑢 = ( 𝑚 ∪ 𝑛 ) → ( 𝑁 ‘ ( 𝑢 ∖ { 𝑥 } ) ) = ( 𝑁 ‘ ( ( 𝑚 ∪ 𝑛 ) ∖ { 𝑥 } ) ) )
98 97 eliuni ⊢ ( ( ( 𝑚 ∪ 𝑛 ) ∈ 𝐴 ∧ ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ( +g ‘ 𝑊 ) 𝑤 ) ∈ ( 𝑁 ‘ ( ( 𝑚 ∪ 𝑛 ) ∖ { 𝑥 } ) ) ) → ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ( +g ‘ 𝑊 ) 𝑤 ) ∈ ∪ 𝑢 ∈ 𝐴 ( 𝑁 ‘ ( 𝑢 ∖ { 𝑥 } ) ) )
99 64 95 98 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( 𝑚 ∈ 𝐴 ∧ 𝑛 ∈ 𝐴 ) ∧ ( 𝑣 ∈ ( 𝑁 ‘ ( 𝑚 ∖ { 𝑥 } ) ) ∧ 𝑤 ∈ ( 𝑁 ‘ ( 𝑛 ∖ { 𝑥 } ) ) ) ) → ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ( +g ‘ 𝑊 ) 𝑤 ) ∈ ∪ 𝑢 ∈ 𝐴 ( 𝑁 ‘ ( 𝑢 ∖ { 𝑥 } ) ) )
100 99 12 eleqtrrdi ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( 𝑚 ∈ 𝐴 ∧ 𝑛 ∈ 𝐴 ) ∧ ( 𝑣 ∈ ( 𝑁 ‘ ( 𝑚 ∖ { 𝑥 } ) ) ∧ 𝑤 ∈ ( 𝑁 ‘ ( 𝑛 ∖ { 𝑥 } ) ) ) ) → ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ( +g ‘ 𝑊 ) 𝑤 ) ∈ 𝑇 )
101 100 3expia ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( 𝑚 ∈ 𝐴 ∧ 𝑛 ∈ 𝐴 ) ) → ( ( 𝑣 ∈ ( 𝑁 ‘ ( 𝑚 ∖ { 𝑥 } ) ) ∧ 𝑤 ∈ ( 𝑁 ‘ ( 𝑛 ∖ { 𝑥 } ) ) ) → ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ( +g ‘ 𝑊 ) 𝑤 ) ∈ 𝑇 ) )
102 101 rexlimdvva ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) → ( ∃ 𝑚 ∈ 𝐴 ∃ 𝑛 ∈ 𝐴 ( 𝑣 ∈ ( 𝑁 ‘ ( 𝑚 ∖ { 𝑥 } ) ) ∧ 𝑤 ∈ ( 𝑁 ‘ ( 𝑛 ∖ { 𝑥 } ) ) ) → ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ( +g ‘ 𝑊 ) 𝑤 ) ∈ 𝑇 ) )
103 59 102 syl5bi ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) → ( ( 𝑣 ∈ 𝑇 ∧ 𝑤 ∈ 𝑇 ) → ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ( +g ‘ 𝑊 ) 𝑤 ) ∈ 𝑇 ) )
104 103 exp4b ⊢ ( 𝜑 → ( 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) → ( 𝑣 ∈ 𝑇 → ( 𝑤 ∈ 𝑇 → ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ( +g ‘ 𝑊 ) 𝑤 ) ∈ 𝑇 ) ) ) )
105 104 3imp2 ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑣 ∈ 𝑇 ∧ 𝑤 ∈ 𝑇 ) ) → ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ( +g ‘ 𝑊 ) 𝑤 ) ∈ 𝑇 )
106 13 14 15 16 17 18 31 42 105 islssd ⊢ ( 𝜑 → 𝑇 ∈ 𝑃 )
107 eldifi ⊢ ( 𝑦 ∈ ( ∪ 𝐴 ∖ { 𝑥 } ) → 𝑦 ∈ ∪ 𝐴 )
108 107 adantl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ∪ 𝐴 ∖ { 𝑥 } ) ) → 𝑦 ∈ ∪ 𝐴 )
109 eldifn ⊢ ( 𝑦 ∈ ( ∪ 𝐴 ∖ { 𝑥 } ) → ¬ 𝑦 ∈ { 𝑥 } )
110 109 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ∪ 𝐴 ∖ { 𝑥 } ) ) ∧ 𝑢 ∈ 𝐴 ) → ¬ 𝑦 ∈ { 𝑥 } )
111 eldif ⊢ ( 𝑦 ∈ ( 𝑢 ∖ { 𝑥 } ) ↔ ( 𝑦 ∈ 𝑢 ∧ ¬ 𝑦 ∈ { 𝑥 } ) )
112 1 3 lspssid ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑢 ∖ { 𝑥 } ) ⊆ 𝑉 ) → ( 𝑢 ∖ { 𝑥 } ) ⊆ ( 𝑁 ‘ ( 𝑢 ∖ { 𝑥 } ) ) )
113 20 25 112 syl2an2r ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝐴 ) → ( 𝑢 ∖ { 𝑥 } ) ⊆ ( 𝑁 ‘ ( 𝑢 ∖ { 𝑥 } ) ) )
114 113 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ∪ 𝐴 ∖ { 𝑥 } ) ) ∧ 𝑢 ∈ 𝐴 ) → ( 𝑢 ∖ { 𝑥 } ) ⊆ ( 𝑁 ‘ ( 𝑢 ∖ { 𝑥 } ) ) )
115 114 sseld ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ∪ 𝐴 ∖ { 𝑥 } ) ) ∧ 𝑢 ∈ 𝐴 ) → ( 𝑦 ∈ ( 𝑢 ∖ { 𝑥 } ) → 𝑦 ∈ ( 𝑁 ‘ ( 𝑢 ∖ { 𝑥 } ) ) ) )
116 111 115 syl5bir ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ∪ 𝐴 ∖ { 𝑥 } ) ) ∧ 𝑢 ∈ 𝐴 ) → ( ( 𝑦 ∈ 𝑢 ∧ ¬ 𝑦 ∈ { 𝑥 } ) → 𝑦 ∈ ( 𝑁 ‘ ( 𝑢 ∖ { 𝑥 } ) ) ) )
117 110 116 mpan2d ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ∪ 𝐴 ∖ { 𝑥 } ) ) ∧ 𝑢 ∈ 𝐴 ) → ( 𝑦 ∈ 𝑢 → 𝑦 ∈ ( 𝑁 ‘ ( 𝑢 ∖ { 𝑥 } ) ) ) )
118 117 reximdva ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ∪ 𝐴 ∖ { 𝑥 } ) ) → ( ∃ 𝑢 ∈ 𝐴 𝑦 ∈ 𝑢 → ∃ 𝑢 ∈ 𝐴 𝑦 ∈ ( 𝑁 ‘ ( 𝑢 ∖ { 𝑥 } ) ) ) )
119 eluni2 ⊢ ( 𝑦 ∈ ∪ 𝐴 ↔ ∃ 𝑢 ∈ 𝐴 𝑦 ∈ 𝑢 )
120 eliun ⊢ ( 𝑦 ∈ ∪ 𝑢 ∈ 𝐴 ( 𝑁 ‘ ( 𝑢 ∖ { 𝑥 } ) ) ↔ ∃ 𝑢 ∈ 𝐴 𝑦 ∈ ( 𝑁 ‘ ( 𝑢 ∖ { 𝑥 } ) ) )
121 118 119 120 3imtr4g ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ∪ 𝐴 ∖ { 𝑥 } ) ) → ( 𝑦 ∈ ∪ 𝐴 → 𝑦 ∈ ∪ 𝑢 ∈ 𝐴 ( 𝑁 ‘ ( 𝑢 ∖ { 𝑥 } ) ) ) )
122 108 121 mpd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ∪ 𝐴 ∖ { 𝑥 } ) ) → 𝑦 ∈ ∪ 𝑢 ∈ 𝐴 ( 𝑁 ‘ ( 𝑢 ∖ { 𝑥 } ) ) )
123 122 ex ⊢ ( 𝜑 → ( 𝑦 ∈ ( ∪ 𝐴 ∖ { 𝑥 } ) → 𝑦 ∈ ∪ 𝑢 ∈ 𝐴 ( 𝑁 ‘ ( 𝑢 ∖ { 𝑥 } ) ) ) )
124 123 ssrdv ⊢ ( 𝜑 → ( ∪ 𝐴 ∖ { 𝑥 } ) ⊆ ∪ 𝑢 ∈ 𝐴 ( 𝑁 ‘ ( 𝑢 ∖ { 𝑥 } ) ) )
125 124 12 sseqtrrdi ⊢ ( 𝜑 → ( ∪ 𝐴 ∖ { 𝑥 } ) ⊆ 𝑇 )
126 106 125 jca ⊢ ( 𝜑 → ( 𝑇 ∈ 𝑃 ∧ ( ∪ 𝐴 ∖ { 𝑥 } ) ⊆ 𝑇 ) )