Metamath Proof Explorer

Theorem mapdindp0

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 ⊢ ( 𝜑 → ¬ 𝑤 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) )
mapdindp1.yz ⊢ ( 𝜑 → ( 𝑌 + 𝑍 ) ≠ 0 )
Assertion mapdindp0 ( 𝜑 → ( 𝑁 ‘ { ( 𝑌 + 𝑍 ) } ) = ( 𝑁 ‘ { 𝑌 } ) )

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 mapdindp1.yz ⊢ ( 𝜑 → ( 𝑌 + 𝑍 ) ≠ 0 )
14 eqid ⊢ ( LSubSp ‘ 𝑊 ) = ( LSubSp ‘ 𝑊 )
15 lveclmod ⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
16 5 15 syl ⊢ ( 𝜑 → 𝑊 ∈ LMod )
17 7 eldifad ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
18 1 14 4 lspsncl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑌 ∈ 𝑉 ) → ( 𝑁 ‘ { 𝑌 } ) ∈ ( LSubSp ‘ 𝑊 ) )
19 16 17 18 syl2anc ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑌 } ) ∈ ( LSubSp ‘ 𝑊 ) )
20 10 19 eqeltrrd ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑍 } ) ∈ ( LSubSp ‘ 𝑊 ) )
21 eqid ⊢ ( LSSum ‘ 𝑊 ) = ( LSSum ‘ 𝑊 )
22 14 21 lsmcl ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑁 ‘ { 𝑌 } ) ∈ ( LSubSp ‘ 𝑊 ) ∧ ( 𝑁 ‘ { 𝑍 } ) ∈ ( LSubSp ‘ 𝑊 ) ) → ( ( 𝑁 ‘ { 𝑌 } ) ( LSSum ‘ 𝑊 ) ( 𝑁 ‘ { 𝑍 } ) ) ∈ ( LSubSp ‘ 𝑊 ) )
23 16 19 20 22 syl3anc ⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝑌 } ) ( LSSum ‘ 𝑊 ) ( 𝑁 ‘ { 𝑍 } ) ) ∈ ( LSubSp ‘ 𝑊 ) )
24 14 lsssssubg ⊢ ( 𝑊 ∈ LMod → ( LSubSp ‘ 𝑊 ) ⊆ ( SubGrp ‘ 𝑊 ) )
25 16 24 syl ⊢ ( 𝜑 → ( LSubSp ‘ 𝑊 ) ⊆ ( SubGrp ‘ 𝑊 ) )
26 25 19 sseldd ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑌 } ) ∈ ( SubGrp ‘ 𝑊 ) )
27 10 26 eqeltrrd ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑍 } ) ∈ ( SubGrp ‘ 𝑊 ) )
28 1 4 lspsnid ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑌 ∈ 𝑉 ) → 𝑌 ∈ ( 𝑁 ‘ { 𝑌 } ) )
29 16 17 28 syl2anc ⊢ ( 𝜑 → 𝑌 ∈ ( 𝑁 ‘ { 𝑌 } ) )
30 8 eldifad ⊢ ( 𝜑 → 𝑍 ∈ 𝑉 )
31 1 4 lspsnid ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑍 ∈ 𝑉 ) → 𝑍 ∈ ( 𝑁 ‘ { 𝑍 } ) )
32 16 30 31 syl2anc ⊢ ( 𝜑 → 𝑍 ∈ ( 𝑁 ‘ { 𝑍 } ) )
33 2 21 lsmelvali ⊢ ( ( ( ( 𝑁 ‘ { 𝑌 } ) ∈ ( SubGrp ‘ 𝑊 ) ∧ ( 𝑁 ‘ { 𝑍 } ) ∈ ( SubGrp ‘ 𝑊 ) ) ∧ ( 𝑌 ∈ ( 𝑁 ‘ { 𝑌 } ) ∧ 𝑍 ∈ ( 𝑁 ‘ { 𝑍 } ) ) ) → ( 𝑌 + 𝑍 ) ∈ ( ( 𝑁 ‘ { 𝑌 } ) ( LSSum ‘ 𝑊 ) ( 𝑁 ‘ { 𝑍 } ) ) )
34 26 27 29 32 33 syl22anc ⊢ ( 𝜑 → ( 𝑌 + 𝑍 ) ∈ ( ( 𝑁 ‘ { 𝑌 } ) ( LSSum ‘ 𝑊 ) ( 𝑁 ‘ { 𝑍 } ) ) )
35 14 4 16 23 34 ellspsn5 ⊢ ( 𝜑 → ( 𝑁 ‘ { ( 𝑌 + 𝑍 ) } ) ⊆ ( ( 𝑁 ‘ { 𝑌 } ) ( LSSum ‘ 𝑊 ) ( 𝑁 ‘ { 𝑍 } ) ) )
36 10 oveq2d ⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝑌 } ) ( LSSum ‘ 𝑊 ) ( 𝑁 ‘ { 𝑌 } ) ) = ( ( 𝑁 ‘ { 𝑌 } ) ( LSSum ‘ 𝑊 ) ( 𝑁 ‘ { 𝑍 } ) ) )
37 21 lsmidm ⊢ ( ( 𝑁 ‘ { 𝑌 } ) ∈ ( SubGrp ‘ 𝑊 ) → ( ( 𝑁 ‘ { 𝑌 } ) ( LSSum ‘ 𝑊 ) ( 𝑁 ‘ { 𝑌 } ) ) = ( 𝑁 ‘ { 𝑌 } ) )
38 26 37 syl ⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝑌 } ) ( LSSum ‘ 𝑊 ) ( 𝑁 ‘ { 𝑌 } ) ) = ( 𝑁 ‘ { 𝑌 } ) )
39 36 38 eqtr3d ⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝑌 } ) ( LSSum ‘ 𝑊 ) ( 𝑁 ‘ { 𝑍 } ) ) = ( 𝑁 ‘ { 𝑌 } ) )
40 35 39 sseqtrd ⊢ ( 𝜑 → ( 𝑁 ‘ { ( 𝑌 + 𝑍 ) } ) ⊆ ( 𝑁 ‘ { 𝑌 } ) )
41 1 2 lmodvacl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑉 ) → ( 𝑌 + 𝑍 ) ∈ 𝑉 )
42 16 17 30 41 syl3anc ⊢ ( 𝜑 → ( 𝑌 + 𝑍 ) ∈ 𝑉 )
43 eldifsn ⊢ ( ( 𝑌 + 𝑍 ) ∈ ( 𝑉 ∖ { 0 } ) ↔ ( ( 𝑌 + 𝑍 ) ∈ 𝑉 ∧ ( 𝑌 + 𝑍 ) ≠ 0 ) )
44 42 13 43 sylanbrc ⊢ ( 𝜑 → ( 𝑌 + 𝑍 ) ∈ ( 𝑉 ∖ { 0 } ) )
45 1 3 4 5 44 17 lspsncmp ⊢ ( 𝜑 → ( ( 𝑁 ‘ { ( 𝑌 + 𝑍 ) } ) ⊆ ( 𝑁 ‘ { 𝑌 } ) ↔ ( 𝑁 ‘ { ( 𝑌 + 𝑍 ) } ) = ( 𝑁 ‘ { 𝑌 } ) ) )
46 40 45 mpbid ⊢ ( 𝜑 → ( 𝑁 ‘ { ( 𝑌 + 𝑍 ) } ) = ( 𝑁 ‘ { 𝑌 } ) )