Theorem lspsncmp

Description: Comparable spans of nonzero singletons are equal. (Contributed by NM, 27-Apr-2015)

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

Proof

Step	Hyp	Ref	Expression
1		lspsncmp.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
2		lspsncmp.o	⊢ 0 = ( 0g ‘ 𝑊 )
3		lspsncmp.n	⊢ 𝑁 = ( LSpan ‘ 𝑊 )
4		lspsncmp.w	⊢ ( 𝜑 → 𝑊 ∈ LVec )
5		lspsncmp.x	⊢ ( 𝜑 → 𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
6		lspsncmp.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
7	4	adantr	⊢ ( ( 𝜑 ∧ ( 𝑁 ‘ { 𝑋 } ) ⊆ ( 𝑁 ‘ { 𝑌 } ) ) → 𝑊 ∈ LVec )
8	6	adantr	⊢ ( ( 𝜑 ∧ ( 𝑁 ‘ { 𝑋 } ) ⊆ ( 𝑁 ‘ { 𝑌 } ) ) → 𝑌 ∈ 𝑉 )
9		eqid	⊢ ( LSubSp ‘ 𝑊 ) = ( LSubSp ‘ 𝑊 )
10		lveclmod	⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
11	4 10	syl	⊢ ( 𝜑 → 𝑊 ∈ LMod )
12	1 9 3	lspsncl	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑌 ∈ 𝑉 ) → ( 𝑁 ‘ { 𝑌 } ) ∈ ( LSubSp ‘ 𝑊 ) )
13	11 6 12	syl2anc	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑌 } ) ∈ ( LSubSp ‘ 𝑊 ) )
14	5	eldifad	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
15	1 9 3 11 13 14	ellspsn5b	⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝑁 ‘ { 𝑌 } ) ↔ ( 𝑁 ‘ { 𝑋 } ) ⊆ ( 𝑁 ‘ { 𝑌 } ) ) )
16	15	biimpar	⊢ ( ( 𝜑 ∧ ( 𝑁 ‘ { 𝑋 } ) ⊆ ( 𝑁 ‘ { 𝑌 } ) ) → 𝑋 ∈ ( 𝑁 ‘ { 𝑌 } ) )
17		eldifsni	⊢ ( 𝑋 ∈ ( 𝑉 ∖ { 0 } ) → 𝑋 ≠ 0 )
18	5 17	syl	⊢ ( 𝜑 → 𝑋 ≠ 0 )
19	18	adantr	⊢ ( ( 𝜑 ∧ ( 𝑁 ‘ { 𝑋 } ) ⊆ ( 𝑁 ‘ { 𝑌 } ) ) → 𝑋 ≠ 0 )
20	1 2 3 7 8 16 19	lspsneleq	⊢ ( ( 𝜑 ∧ ( 𝑁 ‘ { 𝑋 } ) ⊆ ( 𝑁 ‘ { 𝑌 } ) ) → ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑌 } ) )
21	20	ex	⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝑋 } ) ⊆ ( 𝑁 ‘ { 𝑌 } ) → ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑌 } ) ) )
22		eqimss	⊢ ( ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑌 } ) → ( 𝑁 ‘ { 𝑋 } ) ⊆ ( 𝑁 ‘ { 𝑌 } ) )
23	21 22	impbid1	⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝑋 } ) ⊆ ( 𝑁 ‘ { 𝑌 } ) ↔ ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑌 } ) ) )