Theorem prjsprellsp

Description: Two vectors are equivalent iff their spans are equal. (Contributed by Steven Nguyen, 31-May-2023)

	Ref	Expression
Hypotheses	prjsprel.1	⊢ ∼ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ 𝐾 𝑥 = ( 𝑙 · 𝑦 ) ) }
	prjspertr.b	⊢ 𝐵 = ( ( Base ‘ 𝑉 ) ∖ { ( 0g ‘ 𝑉 ) } )
	prjspertr.s	⊢ 𝑆 = ( Scalar ‘ 𝑉 )
	prjspertr.x	⊢ · = ( ·𝑠 ‘ 𝑉 )
	prjspertr.k	⊢ 𝐾 = ( Base ‘ 𝑆 )
	prjsprellsp.n	⊢ 𝑁 = ( LSpan ‘ 𝑉 )
Assertion	prjsprellsp	⊢ ( ( 𝑉 ∈ LVec ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑋 ∼ 𝑌 ↔ ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑌 } ) ) )

Proof

Step	Hyp	Ref	Expression
1		prjsprel.1	⊢ ∼ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ 𝐾 𝑥 = ( 𝑙 · 𝑦 ) ) }
2		prjspertr.b	⊢ 𝐵 = ( ( Base ‘ 𝑉 ) ∖ { ( 0g ‘ 𝑉 ) } )
3		prjspertr.s	⊢ 𝑆 = ( Scalar ‘ 𝑉 )
4		prjspertr.x	⊢ · = ( ·𝑠 ‘ 𝑉 )
5		prjspertr.k	⊢ 𝐾 = ( Base ‘ 𝑆 )
6		prjsprellsp.n	⊢ 𝑁 = ( LSpan ‘ 𝑉 )
7		ibar	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ∃ 𝑚 ∈ ( 𝐾 ∖ { ( 0g ‘ 𝑆 ) } ) 𝑋 = ( 𝑚 · 𝑌 ) ↔ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ∃ 𝑚 ∈ ( 𝐾 ∖ { ( 0g ‘ 𝑆 ) } ) 𝑋 = ( 𝑚 · 𝑌 ) ) ) )
8	7	bicomd	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ∃ 𝑚 ∈ ( 𝐾 ∖ { ( 0g ‘ 𝑆 ) } ) 𝑋 = ( 𝑚 · 𝑌 ) ) ↔ ∃ 𝑚 ∈ ( 𝐾 ∖ { ( 0g ‘ 𝑆 ) } ) 𝑋 = ( 𝑚 · 𝑌 ) ) )
9	8	adantl	⊢ ( ( 𝑉 ∈ LVec ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ∃ 𝑚 ∈ ( 𝐾 ∖ { ( 0g ‘ 𝑆 ) } ) 𝑋 = ( 𝑚 · 𝑌 ) ) ↔ ∃ 𝑚 ∈ ( 𝐾 ∖ { ( 0g ‘ 𝑆 ) } ) 𝑋 = ( 𝑚 · 𝑌 ) ) )
10		eqid	⊢ ( 0g ‘ 𝑆 ) = ( 0g ‘ 𝑆 )
11	1 2 3 4 5 10	prjspreln0	⊢ ( 𝑉 ∈ LVec → ( 𝑋 ∼ 𝑌 ↔ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ∃ 𝑚 ∈ ( 𝐾 ∖ { ( 0g ‘ 𝑆 ) } ) 𝑋 = ( 𝑚 · 𝑌 ) ) ) )
12	11	adantr	⊢ ( ( 𝑉 ∈ LVec ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑋 ∼ 𝑌 ↔ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ∃ 𝑚 ∈ ( 𝐾 ∖ { ( 0g ‘ 𝑆 ) } ) 𝑋 = ( 𝑚 · 𝑌 ) ) ) )
13		eqid	⊢ ( Base ‘ 𝑉 ) = ( Base ‘ 𝑉 )
14		simpl	⊢ ( ( 𝑉 ∈ LVec ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → 𝑉 ∈ LVec )
15		eldifi	⊢ ( 𝑋 ∈ ( ( Base ‘ 𝑉 ) ∖ { ( 0g ‘ 𝑉 ) } ) → 𝑋 ∈ ( Base ‘ 𝑉 ) )
16	15 2	eleq2s	⊢ ( 𝑋 ∈ 𝐵 → 𝑋 ∈ ( Base ‘ 𝑉 ) )
17	16	ad2antrl	⊢ ( ( 𝑉 ∈ LVec ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → 𝑋 ∈ ( Base ‘ 𝑉 ) )
18		eldifi	⊢ ( 𝑌 ∈ ( ( Base ‘ 𝑉 ) ∖ { ( 0g ‘ 𝑉 ) } ) → 𝑌 ∈ ( Base ‘ 𝑉 ) )
19	18 2	eleq2s	⊢ ( 𝑌 ∈ 𝐵 → 𝑌 ∈ ( Base ‘ 𝑉 ) )
20	19	ad2antll	⊢ ( ( 𝑉 ∈ LVec ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → 𝑌 ∈ ( Base ‘ 𝑉 ) )
21	13 3 5 10 4 6 14 17 20	lspsneq	⊢ ( ( 𝑉 ∈ LVec ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑌 } ) ↔ ∃ 𝑚 ∈ ( 𝐾 ∖ { ( 0g ‘ 𝑆 ) } ) 𝑋 = ( 𝑚 · 𝑌 ) ) )
22	9 12 21	3bitr4d	⊢ ( ( 𝑉 ∈ LVec ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑋 ∼ 𝑌 ↔ ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑌 } ) ) )