Metamath Proof Explorer

Theorem mapdindp3

Description: Vector independence lemma. (Contributed by NM, 29-Apr-2015)

Ref Expression
Hypotheses mapdindp1.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
mapdindp1.p ⊢ + = ( +g ‘ 𝑊 )
mapdindp1.o ⊢ 0 = ( 0g ‘ 𝑊 )
mapdindp1.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
mapdindp1.w ⊢ ( 𝜑 → 𝑊 ∈ LVec )
mapdindp1.x ⊢ ( 𝜑 → 𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
mapdindp1.y ⊢ ( 𝜑 → 𝑌 ∈ ( 𝑉 ∖ { 0 } ) )
mapdindp1.z ⊢ ( 𝜑 → 𝑍 ∈ ( 𝑉 ∖ { 0 } ) )
mapdindp1.W ⊢ ( 𝜑 → 𝑤 ∈ ( 𝑉 ∖ { 0 } ) )
mapdindp1.e ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑌 } ) = ( 𝑁 ‘ { 𝑍 } ) )
mapdindp1.ne ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ≠ ( 𝑁 ‘ { 𝑌 } ) )
mapdindp1.f ⊢ ( 𝜑 → ¬ 𝑤 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) )
Assertion mapdindp3 ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ≠ ( 𝑁 ‘ { ( 𝑤 + 𝑌 ) } ) )

Proof

Step Hyp Ref Expression
1 mapdindp1.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 mapdindp1.p ⊢ + = ( +g ‘ 𝑊 )
3 mapdindp1.o ⊢ 0 = ( 0g ‘ 𝑊 )
4 mapdindp1.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
5 mapdindp1.w ⊢ ( 𝜑 → 𝑊 ∈ LVec )
6 mapdindp1.x ⊢ ( 𝜑 → 𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
7 mapdindp1.y ⊢ ( 𝜑 → 𝑌 ∈ ( 𝑉 ∖ { 0 } ) )
8 mapdindp1.z ⊢ ( 𝜑 → 𝑍 ∈ ( 𝑉 ∖ { 0 } ) )
9 mapdindp1.W ⊢ ( 𝜑 → 𝑤 ∈ ( 𝑉 ∖ { 0 } ) )
10 mapdindp1.e ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑌 } ) = ( 𝑁 ‘ { 𝑍 } ) )
11 mapdindp1.ne ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ≠ ( 𝑁 ‘ { 𝑌 } ) )
12 mapdindp1.f ⊢ ( 𝜑 → ¬ 𝑤 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) )
13 lveclmod ⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
14 5 13 syl ⊢ ( 𝜑 → 𝑊 ∈ LMod )
15 9 eldifad ⊢ ( 𝜑 → 𝑤 ∈ 𝑉 )
16 7 eldifad ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
17 1 2 4 lspvadd ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑤 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( 𝑁 ‘ { ( 𝑤 + 𝑌 ) } ) ⊆ ( 𝑁 ‘ { 𝑤 , 𝑌 } ) )
18 14 15 16 17 syl3anc ⊢ ( 𝜑 → ( 𝑁 ‘ { ( 𝑤 + 𝑌 ) } ) ⊆ ( 𝑁 ‘ { 𝑤 , 𝑌 } ) )
19 1 3 4 5 6 16 15 11 12 lspindp1 ⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝑤 } ) ≠ ( 𝑁 ‘ { 𝑌 } ) ∧ ¬ 𝑋 ∈ ( 𝑁 ‘ { 𝑤 , 𝑌 } ) ) )
20 19 simprd ⊢ ( 𝜑 → ¬ 𝑋 ∈ ( 𝑁 ‘ { 𝑤 , 𝑌 } ) )
21 18 20 ssneldd ⊢ ( 𝜑 → ¬ 𝑋 ∈ ( 𝑁 ‘ { ( 𝑤 + 𝑌 ) } ) )
22 6 eldifad ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
23 1 4 lspsnid ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → 𝑋 ∈ ( 𝑁 ‘ { 𝑋 } ) )
24 14 22 23 syl2anc ⊢ ( 𝜑 → 𝑋 ∈ ( 𝑁 ‘ { 𝑋 } ) )
25 eleq2 ⊢ ( ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { ( 𝑤 + 𝑌 ) } ) → ( 𝑋 ∈ ( 𝑁 ‘ { 𝑋 } ) ↔ 𝑋 ∈ ( 𝑁 ‘ { ( 𝑤 + 𝑌 ) } ) ) )
26 24 25 syl5ibcom ⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { ( 𝑤 + 𝑌 ) } ) → 𝑋 ∈ ( 𝑁 ‘ { ( 𝑤 + 𝑌 ) } ) ) )
27 26 necon3bd ⊢ ( 𝜑 → ( ¬ 𝑋 ∈ ( 𝑁 ‘ { ( 𝑤 + 𝑌 ) } ) → ( 𝑁 ‘ { 𝑋 } ) ≠ ( 𝑁 ‘ { ( 𝑤 + 𝑌 ) } ) ) )
28 21 27 mpd ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ≠ ( 𝑁 ‘ { ( 𝑤 + 𝑌 ) } ) )