This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lmodindp1

Description: Two independent (non-colinear) vectors have nonzero sum. (Contributed by NM, 22-Apr-2015)

Ref Expression
Hypotheses lmodindp1.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
lmodindp1.p ⊢ + = ( +g ‘ 𝑊 )
lmodindp1.o ⊢ 0 = ( 0g ‘ 𝑊 )
lmodindp1.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
lmodindp1.w ⊢ ( 𝜑 → 𝑊 ∈ LMod )
lmodindp1.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
lmodindp1.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
lmodindp1.q ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ≠ ( 𝑁 ‘ { 𝑌 } ) )
Assertion lmodindp1 ( 𝜑 → ( 𝑋 + 𝑌 ) ≠ 0 )

Proof

Step Hyp Ref Expression
1 lmodindp1.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 lmodindp1.p ⊢ + = ( +g ‘ 𝑊 )
3 lmodindp1.o ⊢ 0 = ( 0g ‘ 𝑊 )
4 lmodindp1.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
5 lmodindp1.w ⊢ ( 𝜑 → 𝑊 ∈ LMod )
6 lmodindp1.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
7 lmodindp1.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
8 lmodindp1.q ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ≠ ( 𝑁 ‘ { 𝑌 } ) )
9 eqid ⊢ ( invg ‘ 𝑊 ) = ( invg ‘ 𝑊 )
10 1 9 4 lspsnneg ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → ( 𝑁 ‘ { ( ( invg ‘ 𝑊 ) ‘ 𝑋 ) } ) = ( 𝑁 ‘ { 𝑋 } ) )
11 5 6 10 syl2anc ⊢ ( 𝜑 → ( 𝑁 ‘ { ( ( invg ‘ 𝑊 ) ‘ 𝑋 ) } ) = ( 𝑁 ‘ { 𝑋 } ) )
12 11 eqcomd ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { ( ( invg ‘ 𝑊 ) ‘ 𝑋 ) } ) )
13 12 adantr ⊢ ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) = 0 ) → ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { ( ( invg ‘ 𝑊 ) ‘ 𝑋 ) } ) )
14 lmodgrp ⊢ ( 𝑊 ∈ LMod → 𝑊 ∈ Grp )
15 5 14 syl ⊢ ( 𝜑 → 𝑊 ∈ Grp )
16 1 2 3 9 grpinvid1 ⊢ ( ( 𝑊 ∈ Grp ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( ( ( invg ‘ 𝑊 ) ‘ 𝑋 ) = 𝑌 ↔ ( 𝑋 + 𝑌 ) = 0 ) )
17 15 6 7 16 syl3anc ⊢ ( 𝜑 → ( ( ( invg ‘ 𝑊 ) ‘ 𝑋 ) = 𝑌 ↔ ( 𝑋 + 𝑌 ) = 0 ) )
18 17 biimpar ⊢ ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) = 0 ) → ( ( invg ‘ 𝑊 ) ‘ 𝑋 ) = 𝑌 )
19 18 sneqd ⊢ ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) = 0 ) → { ( ( invg ‘ 𝑊 ) ‘ 𝑋 ) } = { 𝑌 } )
20 19 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) = 0 ) → ( 𝑁 ‘ { ( ( invg ‘ 𝑊 ) ‘ 𝑋 ) } ) = ( 𝑁 ‘ { 𝑌 } ) )
21 13 20 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) = 0 ) → ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑌 } ) )
22 21 ex ⊢ ( 𝜑 → ( ( 𝑋 + 𝑌 ) = 0 → ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑌 } ) ) )
23 22 necon3d ⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝑋 } ) ≠ ( 𝑁 ‘ { 𝑌 } ) → ( 𝑋 + 𝑌 ) ≠ 0 ) )
24 8 23 mpd ⊢ ( 𝜑 → ( 𝑋 + 𝑌 ) ≠ 0 )