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 e. B /\ y e. B ) /\ E. l e. S x = ( l .x. y ) ) }
	prjspner.w	|- W = ( K freeLMod ( 0 ... N ) )
	prjspner.b	|- B = ( ( Base ` W ) \ { ( 0g ` W ) } )
	prjspner.s	|- S = ( Base ` K )
	prjspner.x	|- .x. = ( .s ` W )
	prjspner.k	|- ( ph -> K e. DivRing )
Assertion	prjspner	|- ( ph -> .~ Er B )

Proof

Step	Hyp	Ref	Expression
1		prjspner.e	|- .~ = { <. x , y >. | ( ( x e. B /\ y e. B ) /\ E. l e. S x = ( l .x. y ) ) }
2		prjspner.w	|- W = ( K freeLMod ( 0 ... N ) )
3		prjspner.b	|- B = ( ( Base ` W ) \ { ( 0g ` W ) } )
4		prjspner.s	|- S = ( Base ` K )
5		prjspner.x	|- .x. = ( .s ` W )
6		prjspner.k	|- ( ph -> K e. DivRing )
7		ovexd	|- ( ph -> ( 0 ... N ) e. _V )
8	2	frlmlvec	|- ( ( K e. DivRing /\ ( 0 ... N ) e. _V ) -> W e. LVec )
9	6 7 8	syl2anc	|- ( ph -> W e. LVec )
10		eqid	|- { <. x , y >. | ( ( x e. B /\ y e. B ) /\ E. l e. ( Base ` ( Scalar ` W ) ) x = ( l .x. y ) ) } = { <. x , y >. | ( ( x e. B /\ y e. B ) /\ E. l e. ( Base ` ( Scalar ` W ) ) x = ( l .x. y ) ) }
11		eqid	|- ( Scalar ` W ) = ( Scalar ` W )
12		eqid	|- ( Base ` ( Scalar ` W ) ) = ( Base ` ( Scalar ` W ) )
13	10 3 11 5 12	prjsper	|- ( W e. LVec -> { <. x , y >. | ( ( x e. B /\ y e. B ) /\ E. l e. ( Base ` ( Scalar ` W ) ) x = ( l .x. y ) ) } Er B )
14	9 13	syl	|- ( ph -> { <. x , y >. | ( ( x e. B /\ y e. B ) /\ E. l e. ( Base ` ( Scalar ` W ) ) x = ( l .x. y ) ) } Er B )
15	1 2 3 4 5	prjspnerlem	|- ( K e. DivRing -> .~ = { <. x , y >. | ( ( x e. B /\ y e. B ) /\ E. l e. ( Base ` ( Scalar ` W ) ) x = ( l .x. y ) ) } )
16		ereq1	|- ( .~ = { <. x , y >. | ( ( x e. B /\ y e. B ) /\ E. l e. ( Base ` ( Scalar ` W ) ) x = ( l .x. y ) ) } -> ( .~ Er B <-> { <. x , y >. | ( ( x e. B /\ y e. B ) /\ E. l e. ( Base ` ( Scalar ` W ) ) x = ( l .x. y ) ) } Er B ) )
17	6 15 16	3syl	|- ( ph -> ( .~ Er B <-> { <. x , y >. | ( ( x e. B /\ y e. B ) /\ E. l e. ( Base ` ( Scalar ` W ) ) x = ( l .x. y ) ) } Er B ) )
18	14 17	mpbird	|- ( ph -> .~ Er B )