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