Metamath Proof Explorer


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 𝐵 )