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	|- .~ = { <. x , y >. | ( ( x e. B /\ y e. B ) /\ E. l e. K x = ( l .x. y ) ) }
	prjspertr.b	|- B = ( ( Base ` V ) \ { ( 0g ` V ) } )
	prjspertr.s	|- S = ( Scalar ` V )
	prjspertr.x	|- .x. = ( .s ` V )
	prjspertr.k	|- K = ( Base ` S )
Assertion	prjsper	|- ( V e. LVec -> .~ Er B )

Proof

Step	Hyp	Ref	Expression
1		prjsprel.1	|- .~ = { <. x , y >. | ( ( x e. B /\ y e. B ) /\ E. l e. K x = ( l .x. y ) ) }
2		prjspertr.b	|- B = ( ( Base ` V ) \ { ( 0g ` V ) } )
3		prjspertr.s	|- S = ( Scalar ` V )
4		prjspertr.x	|- .x. = ( .s ` V )
5		prjspertr.k	|- K = ( Base ` S )
6	1	relopabiv	|- Rel .~
7	6	a1i	|- ( V e. LVec -> Rel .~ )
8	1 2 3 4 5	prjspersym	|- ( ( V e. LVec /\ a .~ b ) -> b .~ a )
9		lveclmod	|- ( V e. LVec -> V e. LMod )
10	1 2 3 4 5	prjspertr	|- ( ( V e. LMod /\ ( a .~ b /\ b .~ c ) ) -> a .~ c )
11	9 10	sylan	|- ( ( V e. LVec /\ ( a .~ b /\ b .~ c ) ) -> a .~ c )
12	1 2 3 4 5	prjsperref	|- ( V e. LMod -> ( a e. B <-> a .~ a ) )
13	9 12	syl	|- ( V e. LVec -> ( a e. B <-> a .~ a ) )
14	7 8 11 13	iserd	|- ( V e. LVec -> .~ Er B )