Theorem lspsnnecom

Description: Swap two vectors with different spans. (Contributed by NM, 20-May-2015)

	Ref	Expression
Hypotheses	lspsnnecom.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
	lspsnnecom.o	⊢ 0 = ( 0g ‘ 𝑊 )
	lspsnnecom.n	⊢ 𝑁 = ( LSpan ‘ 𝑊 )
	lspsnnecom.w	⊢ ( 𝜑 → 𝑊 ∈ LVec )
	lspsnnecom.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
	lspsnnecom.y	⊢ ( 𝜑 → 𝑌 ∈ ( 𝑉 ∖ { 0 } ) )
	lspsnnecom.e	⊢ ( 𝜑 → ¬ 𝑋 ∈ ( 𝑁 ‘ { 𝑌 } ) )
Assertion	lspsnnecom	⊢ ( 𝜑 → ¬ 𝑌 ∈ ( 𝑁 ‘ { 𝑋 } ) )

Proof

Step	Hyp	Ref	Expression
1		lspsnnecom.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
2		lspsnnecom.o	⊢ 0 = ( 0g ‘ 𝑊 )
3		lspsnnecom.n	⊢ 𝑁 = ( LSpan ‘ 𝑊 )
4		lspsnnecom.w	⊢ ( 𝜑 → 𝑊 ∈ LVec )
5		lspsnnecom.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
6		lspsnnecom.y	⊢ ( 𝜑 → 𝑌 ∈ ( 𝑉 ∖ { 0 } ) )
7		lspsnnecom.e	⊢ ( 𝜑 → ¬ 𝑋 ∈ ( 𝑁 ‘ { 𝑌 } ) )
8		lveclmod	⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
9	4 8	syl	⊢ ( 𝜑 → 𝑊 ∈ LMod )
10	6	eldifad	⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
11	1 3 9 5 10 7	lspsnne2	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ≠ ( 𝑁 ‘ { 𝑌 } ) )
12	11	necomd	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑌 } ) ≠ ( 𝑁 ‘ { 𝑋 } ) )
13	1 2 3 4 6 5 12	lspsnne1	⊢ ( 𝜑 → ¬ 𝑌 ∈ ( 𝑁 ‘ { 𝑋 } ) )