Theorem lspsnne1

Description: Two ways to express that vectors have different spans. (Contributed by NM, 28-May-2015)

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

Proof

Step	Hyp	Ref	Expression
1		lspsnne1.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
2		lspsnne1.o	⊢ 0 = ( 0g ‘ 𝑊 )
3		lspsnne1.n	⊢ 𝑁 = ( LSpan ‘ 𝑊 )
4		lspsnne1.w	⊢ ( 𝜑 → 𝑊 ∈ LVec )
5		lspsnne1.x	⊢ ( 𝜑 → 𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
6		lspsnne1.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
7		lspsnne1.e	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ≠ ( 𝑁 ‘ { 𝑌 } ) )
8		eqid	⊢ ( LSubSp ‘ 𝑊 ) = ( LSubSp ‘ 𝑊 )
9		lveclmod	⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
10	4 9	syl	⊢ ( 𝜑 → 𝑊 ∈ LMod )
11	1 8 3	lspsncl	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑌 ∈ 𝑉 ) → ( 𝑁 ‘ { 𝑌 } ) ∈ ( LSubSp ‘ 𝑊 ) )
12	10 6 11	syl2anc	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑌 } ) ∈ ( LSubSp ‘ 𝑊 ) )
13	5	eldifad	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
14	1 8 3 10 12 13	ellspsn5b	⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝑁 ‘ { 𝑌 } ) ↔ ( 𝑁 ‘ { 𝑋 } ) ⊆ ( 𝑁 ‘ { 𝑌 } ) ) )
15	14	notbid	⊢ ( 𝜑 → ( ¬ 𝑋 ∈ ( 𝑁 ‘ { 𝑌 } ) ↔ ¬ ( 𝑁 ‘ { 𝑋 } ) ⊆ ( 𝑁 ‘ { 𝑌 } ) ) )
16	1 2 3 4 5 6	lspsncmp	⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝑋 } ) ⊆ ( 𝑁 ‘ { 𝑌 } ) ↔ ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑌 } ) ) )
17	16	necon3bbid	⊢ ( 𝜑 → ( ¬ ( 𝑁 ‘ { 𝑋 } ) ⊆ ( 𝑁 ‘ { 𝑌 } ) ↔ ( 𝑁 ‘ { 𝑋 } ) ≠ ( 𝑁 ‘ { 𝑌 } ) ) )
18	15 17	bitrd	⊢ ( 𝜑 → ( ¬ 𝑋 ∈ ( 𝑁 ‘ { 𝑌 } ) ↔ ( 𝑁 ‘ { 𝑋 } ) ≠ ( 𝑁 ‘ { 𝑌 } ) ) )
19	7 18	mpbird	⊢ ( 𝜑 → ¬ 𝑋 ∈ ( 𝑁 ‘ { 𝑌 } ) )