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 )