Theorem lspsnsubn0

Description: Unequal singleton spans imply nonzero vector subtraction. (Contributed by NM, 19-Mar-2015)

	Ref	Expression
Hypotheses	lspsnsubn0.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
	lspsnsubn0.o	⊢ 0 = ( 0g ‘ 𝑊 )
	lspsnsubn0.m	⊢ − = ( -g ‘ 𝑊 )
	lspsnsubn0.w	⊢ ( 𝜑 → 𝑊 ∈ LMod )
	lspsnsubn0.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
	lspsnsubn0.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
	lspsnsubn0.e	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ≠ ( 𝑁 ‘ { 𝑌 } ) )
Assertion	lspsnsubn0	⊢ ( 𝜑 → ( 𝑋 − 𝑌 ) ≠ 0 )

Proof

Step	Hyp	Ref	Expression
1		lspsnsubn0.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
2		lspsnsubn0.o	⊢ 0 = ( 0g ‘ 𝑊 )
3		lspsnsubn0.m	⊢ − = ( -g ‘ 𝑊 )
4		lspsnsubn0.w	⊢ ( 𝜑 → 𝑊 ∈ LMod )
5		lspsnsubn0.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
6		lspsnsubn0.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
7		lspsnsubn0.e	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ≠ ( 𝑁 ‘ { 𝑌 } ) )
8	1 2 3	lmodsubeq0	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( ( 𝑋 − 𝑌 ) = 0 ↔ 𝑋 = 𝑌 ) )
9	4 5 6 8	syl3anc	⊢ ( 𝜑 → ( ( 𝑋 − 𝑌 ) = 0 ↔ 𝑋 = 𝑌 ) )
10		sneq	⊢ ( 𝑋 = 𝑌 → { 𝑋 } = { 𝑌 } )
11	10	fveq2d	⊢ ( 𝑋 = 𝑌 → ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑌 } ) )
12	9 11	biimtrdi	⊢ ( 𝜑 → ( ( 𝑋 − 𝑌 ) = 0 → ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑌 } ) ) )
13	12	necon3d	⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝑋 } ) ≠ ( 𝑁 ‘ { 𝑌 } ) → ( 𝑋 − 𝑌 ) ≠ 0 ) )
14	7 13	mpd	⊢ ( 𝜑 → ( 𝑋 − 𝑌 ) ≠ 0 )