Metamath Proof Explorer

Theorem mapdindp2

Description: Vector independence lemma. (Contributed by NM, 1-May-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 mapdindp2 ( 𝜑 → ¬ 𝑤 ∈ ( 𝑁 ‘ { 𝑋 , ( 𝑌 + 𝑍 ) } ) )

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 preq2 ⊢ ( ( 𝑌 + 𝑍 ) = 0 → { 𝑋 , ( 𝑌 + 𝑍 ) } = { 𝑋 , 0 } )
14 13 fveq2d ⊢ ( ( 𝑌 + 𝑍 ) = 0 → ( 𝑁 ‘ { 𝑋 , ( 𝑌 + 𝑍 ) } ) = ( 𝑁 ‘ { 𝑋 , 0 } ) )
15 lveclmod ⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
16 5 15 syl ⊢ ( 𝜑 → 𝑊 ∈ LMod )
17 6 eldifad ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
18 1 3 4 16 17 lsppr0 ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 , 0 } ) = ( 𝑁 ‘ { 𝑋 } ) )
19 14 18 sylan9eqr ⊢ ( ( 𝜑 ∧ ( 𝑌 + 𝑍 ) = 0 ) → ( 𝑁 ‘ { 𝑋 , ( 𝑌 + 𝑍 ) } ) = ( 𝑁 ‘ { 𝑋 } ) )
20 7 eldifad ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
21 prssi ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → { 𝑋 , 𝑌 } ⊆ 𝑉 )
22 17 20 21 syl2anc ⊢ ( 𝜑 → { 𝑋 , 𝑌 } ⊆ 𝑉 )
23 snsspr1 ⊢ { 𝑋 } ⊆ { 𝑋 , 𝑌 }
24 23 a1i ⊢ ( 𝜑 → { 𝑋 } ⊆ { 𝑋 , 𝑌 } )
25 1 4 lspss ⊢ ( ( 𝑊 ∈ LMod ∧ { 𝑋 , 𝑌 } ⊆ 𝑉 ∧ { 𝑋 } ⊆ { 𝑋 , 𝑌 } ) → ( 𝑁 ‘ { 𝑋 } ) ⊆ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) )
26 16 22 24 25 syl3anc ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ⊆ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) )
27 26 adantr ⊢ ( ( 𝜑 ∧ ( 𝑌 + 𝑍 ) = 0 ) → ( 𝑁 ‘ { 𝑋 } ) ⊆ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) )
28 19 27 eqsstrd ⊢ ( ( 𝜑 ∧ ( 𝑌 + 𝑍 ) = 0 ) → ( 𝑁 ‘ { 𝑋 , ( 𝑌 + 𝑍 ) } ) ⊆ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) )
29 12 adantr ⊢ ( ( 𝜑 ∧ ( 𝑌 + 𝑍 ) = 0 ) → ¬ 𝑤 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) )
30 28 29 ssneldd ⊢ ( ( 𝜑 ∧ ( 𝑌 + 𝑍 ) = 0 ) → ¬ 𝑤 ∈ ( 𝑁 ‘ { 𝑋 , ( 𝑌 + 𝑍 ) } ) )
31 12 adantr ⊢ ( ( 𝜑 ∧ ( 𝑌 + 𝑍 ) ≠ 0 ) → ¬ 𝑤 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) )
32 5 adantr ⊢ ( ( 𝜑 ∧ ( 𝑌 + 𝑍 ) ≠ 0 ) → 𝑊 ∈ LVec )
33 6 adantr ⊢ ( ( 𝜑 ∧ ( 𝑌 + 𝑍 ) ≠ 0 ) → 𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
34 7 adantr ⊢ ( ( 𝜑 ∧ ( 𝑌 + 𝑍 ) ≠ 0 ) → 𝑌 ∈ ( 𝑉 ∖ { 0 } ) )
35 8 adantr ⊢ ( ( 𝜑 ∧ ( 𝑌 + 𝑍 ) ≠ 0 ) → 𝑍 ∈ ( 𝑉 ∖ { 0 } ) )
36 9 adantr ⊢ ( ( 𝜑 ∧ ( 𝑌 + 𝑍 ) ≠ 0 ) → 𝑤 ∈ ( 𝑉 ∖ { 0 } ) )
37 10 adantr ⊢ ( ( 𝜑 ∧ ( 𝑌 + 𝑍 ) ≠ 0 ) → ( 𝑁 ‘ { 𝑌 } ) = ( 𝑁 ‘ { 𝑍 } ) )
38 11 adantr ⊢ ( ( 𝜑 ∧ ( 𝑌 + 𝑍 ) ≠ 0 ) → ( 𝑁 ‘ { 𝑋 } ) ≠ ( 𝑁 ‘ { 𝑌 } ) )
39 simpr ⊢ ( ( 𝜑 ∧ ( 𝑌 + 𝑍 ) ≠ 0 ) → ( 𝑌 + 𝑍 ) ≠ 0 )
40 1 2 3 4 32 33 34 35 36 37 38 31 39 mapdindp0 ⊢ ( ( 𝜑 ∧ ( 𝑌 + 𝑍 ) ≠ 0 ) → ( 𝑁 ‘ { ( 𝑌 + 𝑍 ) } ) = ( 𝑁 ‘ { 𝑌 } ) )
41 40 oveq2d ⊢ ( ( 𝜑 ∧ ( 𝑌 + 𝑍 ) ≠ 0 ) → ( ( 𝑁 ‘ { 𝑋 } ) ( LSSum ‘ 𝑊 ) ( 𝑁 ‘ { ( 𝑌 + 𝑍 ) } ) ) = ( ( 𝑁 ‘ { 𝑋 } ) ( LSSum ‘ 𝑊 ) ( 𝑁 ‘ { 𝑌 } ) ) )
42 eqid ⊢ ( LSSum ‘ 𝑊 ) = ( LSSum ‘ 𝑊 )
43 8 eldifad ⊢ ( 𝜑 → 𝑍 ∈ 𝑉 )
44 1 2 lmodvacl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑉 ) → ( 𝑌 + 𝑍 ) ∈ 𝑉 )
45 16 20 43 44 syl3anc ⊢ ( 𝜑 → ( 𝑌 + 𝑍 ) ∈ 𝑉 )
46 1 4 42 16 17 45 lsmpr ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 , ( 𝑌 + 𝑍 ) } ) = ( ( 𝑁 ‘ { 𝑋 } ) ( LSSum ‘ 𝑊 ) ( 𝑁 ‘ { ( 𝑌 + 𝑍 ) } ) ) )
47 46 adantr ⊢ ( ( 𝜑 ∧ ( 𝑌 + 𝑍 ) ≠ 0 ) → ( 𝑁 ‘ { 𝑋 , ( 𝑌 + 𝑍 ) } ) = ( ( 𝑁 ‘ { 𝑋 } ) ( LSSum ‘ 𝑊 ) ( 𝑁 ‘ { ( 𝑌 + 𝑍 ) } ) ) )
48 1 4 42 16 17 20 lsmpr ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 , 𝑌 } ) = ( ( 𝑁 ‘ { 𝑋 } ) ( LSSum ‘ 𝑊 ) ( 𝑁 ‘ { 𝑌 } ) ) )
49 48 adantr ⊢ ( ( 𝜑 ∧ ( 𝑌 + 𝑍 ) ≠ 0 ) → ( 𝑁 ‘ { 𝑋 , 𝑌 } ) = ( ( 𝑁 ‘ { 𝑋 } ) ( LSSum ‘ 𝑊 ) ( 𝑁 ‘ { 𝑌 } ) ) )
50 41 47 49 3eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑌 + 𝑍 ) ≠ 0 ) → ( 𝑁 ‘ { 𝑋 , ( 𝑌 + 𝑍 ) } ) = ( 𝑁 ‘ { 𝑋 , 𝑌 } ) )
51 31 50 neleqtrrd ⊢ ( ( 𝜑 ∧ ( 𝑌 + 𝑍 ) ≠ 0 ) → ¬ 𝑤 ∈ ( 𝑁 ‘ { 𝑋 , ( 𝑌 + 𝑍 ) } ) )
52 30 51 pm2.61dane ⊢ ( 𝜑 → ¬ 𝑤 ∈ ( 𝑁 ‘ { 𝑋 , ( 𝑌 + 𝑍 ) } ) )