Metamath Proof Explorer

Theorem lsatfixedN

Description: Show equality with the span of the sum of two vectors, one of which ( X ) is fixed in advance. Compare lspfixed . (Contributed by NM, 29-May-2015) (New usage is discouraged.)

Ref Expression
Hypotheses lsatfixed.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
lsatfixed.p ⊢ + = ( +g ‘ 𝑊 )
lsatfixed.o ⊢ 0 = ( 0g ‘ 𝑊 )
lsatfixed.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
lsatfixed.a ⊢ 𝐴 = ( LSAtoms ‘ 𝑊 )
lsatfixed.w ⊢ ( 𝜑 → 𝑊 ∈ LVec )
lsatfixed.q ⊢ ( 𝜑 → 𝑄 ∈ 𝐴 )
lsatfixed.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
lsatfixed.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
lsatfixed.e ⊢ ( 𝜑 → 𝑄 ≠ ( 𝑁 ‘ { 𝑋 } ) )
lsatfixed.f ⊢ ( 𝜑 → 𝑄 ≠ ( 𝑁 ‘ { 𝑌 } ) )
lsatfixed.g ⊢ ( 𝜑 → 𝑄 ⊆ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) )
Assertion lsatfixedN ( 𝜑 → ∃ 𝑧 ∈ ( ( 𝑁 ‘ { 𝑌 } ) ∖ { 0 } ) 𝑄 = ( 𝑁 ‘ { ( 𝑋 + 𝑧 ) } ) )

Proof

Step Hyp Ref Expression
1 lsatfixed.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 lsatfixed.p ⊢ + = ( +g ‘ 𝑊 )
3 lsatfixed.o ⊢ 0 = ( 0g ‘ 𝑊 )
4 lsatfixed.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
5 lsatfixed.a ⊢ 𝐴 = ( LSAtoms ‘ 𝑊 )
6 lsatfixed.w ⊢ ( 𝜑 → 𝑊 ∈ LVec )
7 lsatfixed.q ⊢ ( 𝜑 → 𝑄 ∈ 𝐴 )
8 lsatfixed.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
9 lsatfixed.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
10 lsatfixed.e ⊢ ( 𝜑 → 𝑄 ≠ ( 𝑁 ‘ { 𝑋 } ) )
11 lsatfixed.f ⊢ ( 𝜑 → 𝑄 ≠ ( 𝑁 ‘ { 𝑌 } ) )
12 lsatfixed.g ⊢ ( 𝜑 → 𝑄 ⊆ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) )
13 1 4 3 5 islsat ⊢ ( 𝑊 ∈ LVec → ( 𝑄 ∈ 𝐴 ↔ ∃ 𝑤 ∈ ( 𝑉 ∖ { 0 } ) 𝑄 = ( 𝑁 ‘ { 𝑤 } ) ) )
14 6 13 syl ⊢ ( 𝜑 → ( 𝑄 ∈ 𝐴 ↔ ∃ 𝑤 ∈ ( 𝑉 ∖ { 0 } ) 𝑄 = ( 𝑁 ‘ { 𝑤 } ) ) )
15 7 14 mpbid ⊢ ( 𝜑 → ∃ 𝑤 ∈ ( 𝑉 ∖ { 0 } ) 𝑄 = ( 𝑁 ‘ { 𝑤 } ) )
16 6 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝑉 ∖ { 0 } ) ∧ 𝑄 = ( 𝑁 ‘ { 𝑤 } ) ) → 𝑊 ∈ LVec )
17 8 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝑉 ∖ { 0 } ) ∧ 𝑄 = ( 𝑁 ‘ { 𝑤 } ) ) → 𝑋 ∈ 𝑉 )
18 9 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝑉 ∖ { 0 } ) ∧ 𝑄 = ( 𝑁 ‘ { 𝑤 } ) ) → 𝑌 ∈ 𝑉 )
19 simp2 ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝑉 ∖ { 0 } ) ∧ 𝑄 = ( 𝑁 ‘ { 𝑤 } ) ) → 𝑤 ∈ ( 𝑉 ∖ { 0 } ) )
20 simp3 ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝑉 ∖ { 0 } ) ∧ 𝑄 = ( 𝑁 ‘ { 𝑤 } ) ) → 𝑄 = ( 𝑁 ‘ { 𝑤 } ) )
21 20 eqcomd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝑉 ∖ { 0 } ) ∧ 𝑄 = ( 𝑁 ‘ { 𝑤 } ) ) → ( 𝑁 ‘ { 𝑤 } ) = 𝑄 )
22 10 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝑉 ∖ { 0 } ) ∧ 𝑄 = ( 𝑁 ‘ { 𝑤 } ) ) → 𝑄 ≠ ( 𝑁 ‘ { 𝑋 } ) )
23 21 22 eqnetrd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝑉 ∖ { 0 } ) ∧ 𝑄 = ( 𝑁 ‘ { 𝑤 } ) ) → ( 𝑁 ‘ { 𝑤 } ) ≠ ( 𝑁 ‘ { 𝑋 } ) )
24 1 3 4 16 19 17 23 lspsnne1 ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝑉 ∖ { 0 } ) ∧ 𝑄 = ( 𝑁 ‘ { 𝑤 } ) ) → ¬ 𝑤 ∈ ( 𝑁 ‘ { 𝑋 } ) )
25 11 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝑉 ∖ { 0 } ) ∧ 𝑄 = ( 𝑁 ‘ { 𝑤 } ) ) → 𝑄 ≠ ( 𝑁 ‘ { 𝑌 } ) )
26 21 25 eqnetrd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝑉 ∖ { 0 } ) ∧ 𝑄 = ( 𝑁 ‘ { 𝑤 } ) ) → ( 𝑁 ‘ { 𝑤 } ) ≠ ( 𝑁 ‘ { 𝑌 } ) )
27 1 3 4 16 19 18 26 lspsnne1 ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝑉 ∖ { 0 } ) ∧ 𝑄 = ( 𝑁 ‘ { 𝑤 } ) ) → ¬ 𝑤 ∈ ( 𝑁 ‘ { 𝑌 } ) )
28 12 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝑉 ∖ { 0 } ) ∧ 𝑄 = ( 𝑁 ‘ { 𝑤 } ) ) → 𝑄 ⊆ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) )
29 21 28 eqsstrd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝑉 ∖ { 0 } ) ∧ 𝑄 = ( 𝑁 ‘ { 𝑤 } ) ) → ( 𝑁 ‘ { 𝑤 } ) ⊆ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) )
30 eqid ⊢ ( LSubSp ‘ 𝑊 ) = ( LSubSp ‘ 𝑊 )
31 lveclmod ⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
32 6 31 syl ⊢ ( 𝜑 → 𝑊 ∈ LMod )
33 32 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝑉 ∖ { 0 } ) ∧ 𝑄 = ( 𝑁 ‘ { 𝑤 } ) ) → 𝑊 ∈ LMod )
34 1 30 4 32 8 9 lspprcl ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∈ ( LSubSp ‘ 𝑊 ) )
35 34 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝑉 ∖ { 0 } ) ∧ 𝑄 = ( 𝑁 ‘ { 𝑤 } ) ) → ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∈ ( LSubSp ‘ 𝑊 ) )
36 19 eldifad ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝑉 ∖ { 0 } ) ∧ 𝑄 = ( 𝑁 ‘ { 𝑤 } ) ) → 𝑤 ∈ 𝑉 )
37 1 30 4 33 35 36 ellspsn5b ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝑉 ∖ { 0 } ) ∧ 𝑄 = ( 𝑁 ‘ { 𝑤 } ) ) → ( 𝑤 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ↔ ( 𝑁 ‘ { 𝑤 } ) ⊆ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) )
38 29 37 mpbird ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝑉 ∖ { 0 } ) ∧ 𝑄 = ( 𝑁 ‘ { 𝑤 } ) ) → 𝑤 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) )
39 1 2 3 4 16 17 18 24 27 38 lspfixed ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝑉 ∖ { 0 } ) ∧ 𝑄 = ( 𝑁 ‘ { 𝑤 } ) ) → ∃ 𝑧 ∈ ( ( 𝑁 ‘ { 𝑌 } ) ∖ { 0 } ) 𝑤 ∈ ( 𝑁 ‘ { ( 𝑋 + 𝑧 ) } ) )
40 simpl1 ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝑉 ∖ { 0 } ) ∧ 𝑄 = ( 𝑁 ‘ { 𝑤 } ) ) ∧ 𝑧 ∈ ( ( 𝑁 ‘ { 𝑌 } ) ∖ { 0 } ) ) → 𝜑 )
41 40 6 syl ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝑉 ∖ { 0 } ) ∧ 𝑄 = ( 𝑁 ‘ { 𝑤 } ) ) ∧ 𝑧 ∈ ( ( 𝑁 ‘ { 𝑌 } ) ∖ { 0 } ) ) → 𝑊 ∈ LVec )
42 simpl2 ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝑉 ∖ { 0 } ) ∧ 𝑄 = ( 𝑁 ‘ { 𝑤 } ) ) ∧ 𝑧 ∈ ( ( 𝑁 ‘ { 𝑌 } ) ∖ { 0 } ) ) → 𝑤 ∈ ( 𝑉 ∖ { 0 } ) )
43 40 32 syl ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝑉 ∖ { 0 } ) ∧ 𝑄 = ( 𝑁 ‘ { 𝑤 } ) ) ∧ 𝑧 ∈ ( ( 𝑁 ‘ { 𝑌 } ) ∖ { 0 } ) ) → 𝑊 ∈ LMod )
44 40 8 syl ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝑉 ∖ { 0 } ) ∧ 𝑄 = ( 𝑁 ‘ { 𝑤 } ) ) ∧ 𝑧 ∈ ( ( 𝑁 ‘ { 𝑌 } ) ∖ { 0 } ) ) → 𝑋 ∈ 𝑉 )
45 9 snssd ⊢ ( 𝜑 → { 𝑌 } ⊆ 𝑉 )
46 1 4 lspssv ⊢ ( ( 𝑊 ∈ LMod ∧ { 𝑌 } ⊆ 𝑉 ) → ( 𝑁 ‘ { 𝑌 } ) ⊆ 𝑉 )
47 32 45 46 syl2anc ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑌 } ) ⊆ 𝑉 )
48 47 ssdifssd ⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝑌 } ) ∖ { 0 } ) ⊆ 𝑉 )
49 48 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝑉 ∖ { 0 } ) ∧ 𝑄 = ( 𝑁 ‘ { 𝑤 } ) ) → ( ( 𝑁 ‘ { 𝑌 } ) ∖ { 0 } ) ⊆ 𝑉 )
50 49 sselda ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝑉 ∖ { 0 } ) ∧ 𝑄 = ( 𝑁 ‘ { 𝑤 } ) ) ∧ 𝑧 ∈ ( ( 𝑁 ‘ { 𝑌 } ) ∖ { 0 } ) ) → 𝑧 ∈ 𝑉 )
51 1 2 lmodvacl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) → ( 𝑋 + 𝑧 ) ∈ 𝑉 )
52 43 44 50 51 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝑉 ∖ { 0 } ) ∧ 𝑄 = ( 𝑁 ‘ { 𝑤 } ) ) ∧ 𝑧 ∈ ( ( 𝑁 ‘ { 𝑌 } ) ∖ { 0 } ) ) → ( 𝑋 + 𝑧 ) ∈ 𝑉 )
53 1 3 4 41 42 52 lspsncmp ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝑉 ∖ { 0 } ) ∧ 𝑄 = ( 𝑁 ‘ { 𝑤 } ) ) ∧ 𝑧 ∈ ( ( 𝑁 ‘ { 𝑌 } ) ∖ { 0 } ) ) → ( ( 𝑁 ‘ { 𝑤 } ) ⊆ ( 𝑁 ‘ { ( 𝑋 + 𝑧 ) } ) ↔ ( 𝑁 ‘ { 𝑤 } ) = ( 𝑁 ‘ { ( 𝑋 + 𝑧 ) } ) ) )
54 1 30 4 lspsncl ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑋 + 𝑧 ) ∈ 𝑉 ) → ( 𝑁 ‘ { ( 𝑋 + 𝑧 ) } ) ∈ ( LSubSp ‘ 𝑊 ) )
55 43 52 54 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝑉 ∖ { 0 } ) ∧ 𝑄 = ( 𝑁 ‘ { 𝑤 } ) ) ∧ 𝑧 ∈ ( ( 𝑁 ‘ { 𝑌 } ) ∖ { 0 } ) ) → ( 𝑁 ‘ { ( 𝑋 + 𝑧 ) } ) ∈ ( LSubSp ‘ 𝑊 ) )
56 42 eldifad ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝑉 ∖ { 0 } ) ∧ 𝑄 = ( 𝑁 ‘ { 𝑤 } ) ) ∧ 𝑧 ∈ ( ( 𝑁 ‘ { 𝑌 } ) ∖ { 0 } ) ) → 𝑤 ∈ 𝑉 )
57 1 30 4 43 55 56 ellspsn5b ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝑉 ∖ { 0 } ) ∧ 𝑄 = ( 𝑁 ‘ { 𝑤 } ) ) ∧ 𝑧 ∈ ( ( 𝑁 ‘ { 𝑌 } ) ∖ { 0 } ) ) → ( 𝑤 ∈ ( 𝑁 ‘ { ( 𝑋 + 𝑧 ) } ) ↔ ( 𝑁 ‘ { 𝑤 } ) ⊆ ( 𝑁 ‘ { ( 𝑋 + 𝑧 ) } ) ) )
58 simpl3 ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝑉 ∖ { 0 } ) ∧ 𝑄 = ( 𝑁 ‘ { 𝑤 } ) ) ∧ 𝑧 ∈ ( ( 𝑁 ‘ { 𝑌 } ) ∖ { 0 } ) ) → 𝑄 = ( 𝑁 ‘ { 𝑤 } ) )
59 58 eqeq1d ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝑉 ∖ { 0 } ) ∧ 𝑄 = ( 𝑁 ‘ { 𝑤 } ) ) ∧ 𝑧 ∈ ( ( 𝑁 ‘ { 𝑌 } ) ∖ { 0 } ) ) → ( 𝑄 = ( 𝑁 ‘ { ( 𝑋 + 𝑧 ) } ) ↔ ( 𝑁 ‘ { 𝑤 } ) = ( 𝑁 ‘ { ( 𝑋 + 𝑧 ) } ) ) )
60 53 57 59 3bitr4rd ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝑉 ∖ { 0 } ) ∧ 𝑄 = ( 𝑁 ‘ { 𝑤 } ) ) ∧ 𝑧 ∈ ( ( 𝑁 ‘ { 𝑌 } ) ∖ { 0 } ) ) → ( 𝑄 = ( 𝑁 ‘ { ( 𝑋 + 𝑧 ) } ) ↔ 𝑤 ∈ ( 𝑁 ‘ { ( 𝑋 + 𝑧 ) } ) ) )
61 60 rexbidva ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝑉 ∖ { 0 } ) ∧ 𝑄 = ( 𝑁 ‘ { 𝑤 } ) ) → ( ∃ 𝑧 ∈ ( ( 𝑁 ‘ { 𝑌 } ) ∖ { 0 } ) 𝑄 = ( 𝑁 ‘ { ( 𝑋 + 𝑧 ) } ) ↔ ∃ 𝑧 ∈ ( ( 𝑁 ‘ { 𝑌 } ) ∖ { 0 } ) 𝑤 ∈ ( 𝑁 ‘ { ( 𝑋 + 𝑧 ) } ) ) )
62 39 61 mpbird ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝑉 ∖ { 0 } ) ∧ 𝑄 = ( 𝑁 ‘ { 𝑤 } ) ) → ∃ 𝑧 ∈ ( ( 𝑁 ‘ { 𝑌 } ) ∖ { 0 } ) 𝑄 = ( 𝑁 ‘ { ( 𝑋 + 𝑧 ) } ) )
63 62 rexlimdv3a ⊢ ( 𝜑 → ( ∃ 𝑤 ∈ ( 𝑉 ∖ { 0 } ) 𝑄 = ( 𝑁 ‘ { 𝑤 } ) → ∃ 𝑧 ∈ ( ( 𝑁 ‘ { 𝑌 } ) ∖ { 0 } ) 𝑄 = ( 𝑁 ‘ { ( 𝑋 + 𝑧 ) } ) ) )
64 15 63 mpd ⊢ ( 𝜑 → ∃ 𝑧 ∈ ( ( 𝑁 ‘ { 𝑌 } ) ∖ { 0 } ) 𝑄 = ( 𝑁 ‘ { ( 𝑋 + 𝑧 ) } ) )