Theorem prjsper

Description: The relation used to define PrjSp is an equivalence relation. (Contributed by Steven Nguyen, 1-May-2023)

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

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	1	relopabiv	⊢ Rel ∼
7	6	a1i	⊢ ( 𝑉 ∈ LVec → Rel ∼ )
8	1 2 3 4 5	prjspersym	⊢ ( ( 𝑉 ∈ LVec ∧ 𝑎 ∼ 𝑏 ) → 𝑏 ∼ 𝑎 )
9		lveclmod	⊢ ( 𝑉 ∈ LVec → 𝑉 ∈ LMod )
10	1 2 3 4 5	prjspertr	⊢ ( ( 𝑉 ∈ LMod ∧ ( 𝑎 ∼ 𝑏 ∧ 𝑏 ∼ 𝑐 ) ) → 𝑎 ∼ 𝑐 )
11	9 10	sylan	⊢ ( ( 𝑉 ∈ LVec ∧ ( 𝑎 ∼ 𝑏 ∧ 𝑏 ∼ 𝑐 ) ) → 𝑎 ∼ 𝑐 )
12	1 2 3 4 5	prjsperref	⊢ ( 𝑉 ∈ LMod → ( 𝑎 ∈ 𝐵 ↔ 𝑎 ∼ 𝑎 ) )
13	9 12	syl	⊢ ( 𝑉 ∈ LVec → ( 𝑎 ∈ 𝐵 ↔ 𝑎 ∼ 𝑎 ) )
14	7 8 11 13	iserd	⊢ ( 𝑉 ∈ LVec → ∼ Er 𝐵 )