Metamath Proof Explorer


Theorem prjspner

Description: The relation used to define PrjSp (and indirectly PrjSpn through df-prjspn ) is an equivalence relation. This is a lemma that converts the equivalence relation used in results like prjspertr and prjspersym (see prjspnerlem ). Several theorems are covered in one thanks to the theorems around df-er . (Contributed by SN, 14-Aug-2023)

Ref Expression
Hypotheses prjspner.e ˙ = x y | x B y B l S x = l · ˙ y
prjspner.w W = K freeLMod 0 N
prjspner.b B = Base W 0 W
prjspner.s S = Base K
prjspner.x · ˙ = W
prjspner.k φ K DivRing
Assertion prjspner φ ˙ Er B

Proof

Step Hyp Ref Expression
1 prjspner.e ˙ = x y | x B y B l S x = l · ˙ y
2 prjspner.w W = K freeLMod 0 N
3 prjspner.b B = Base W 0 W
4 prjspner.s S = Base K
5 prjspner.x · ˙ = W
6 prjspner.k φ K DivRing
7 ovexd φ 0 N V
8 2 frlmlvec K DivRing 0 N V W LVec
9 6 7 8 syl2anc φ W LVec
10 eqid x y | x B y B l Base Scalar W x = l · ˙ y = x y | x B y B l Base Scalar W x = l · ˙ y
11 eqid Scalar W = Scalar W
12 eqid Base Scalar W = Base Scalar W
13 10 3 11 5 12 prjsper W LVec x y | x B y B l Base Scalar W x = l · ˙ y Er B
14 9 13 syl φ x y | x B y B l Base Scalar W x = l · ˙ y Er B
15 1 2 3 4 5 prjspnerlem K DivRing ˙ = x y | x B y B l Base Scalar W x = l · ˙ y
16 ereq1 ˙ = x y | x B y B l Base Scalar W x = l · ˙ y ˙ Er B x y | x B y B l Base Scalar W x = l · ˙ y Er B
17 6 15 16 3syl φ ˙ Er B x y | x B y B l Base Scalar W x = l · ˙ y Er B
18 14 17 mpbird φ ˙ Er B