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	$$⊢\underset{\dot{}}{\sim }=\left\{⟨x,y⟩|\left(\left(x\in B\wedge y\in B\right)\wedge \exists l\in Sx=l\underset{\dot{}}{·}y\right)\right\}$$
	prjspner.w	$$⊢W=K\mathrm{freeLMod}\left(0\dots N\right)$$
	prjspner.b	$$⊢B={\mathrm{Base}}_W\setminus \left\{0_W\right\}$$
	prjspner.s	$$⊢S={\mathrm{Base}}_K$$
	prjspner.x	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
	prjspner.k	$$⊢\phi \to K\in \mathrm{DivRing}$$
Assertion	prjspner	$$⊢\phi \to \underset{\dot{}}{\sim }\mathrm{Er}B$$

Proof

Step	Hyp	Ref	Expression
1		prjspner.e	$$⊢\underset{\dot{}}{\sim }=\left\{⟨x,y⟩|\left(\left(x\in B\wedge y\in B\right)\wedge \exists l\in Sx=l\underset{\dot{}}{·}y\right)\right\}$$
2		prjspner.w	$$⊢W=K\mathrm{freeLMod}\left(0\dots N\right)$$
3		prjspner.b	$$⊢B={\mathrm{Base}}_W\setminus \left\{0_W\right\}$$
4		prjspner.s	$$⊢S={\mathrm{Base}}_K$$
5		prjspner.x	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
6		prjspner.k	$$⊢\phi \to K\in \mathrm{DivRing}$$
7		ovexd	$$⊢\phi \to \left(0\dots N\right)\in \mathrm{V}$$
8	2	frlmlvec	$$⊢\left(K\in \mathrm{DivRing}\wedge \left(0\dots N\right)\in \mathrm{V}\right)\to W\in \mathrm{LVec}$$
9	6 7 8	syl2anc	$$⊢\phi \to W\in \mathrm{LVec}$$
10		eqid	$$⊢\left\{⟨x,y⟩|\left(\left(x\in B\wedge y\in B\right)\wedge \exists l\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}x=l\underset{\dot{}}{·}y\right)\right\}=\left\{⟨x,y⟩|\left(\left(x\in B\wedge y\in B\right)\wedge \exists l\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}x=l\underset{\dot{}}{·}y\right)\right\}$$
11		eqid	$$⊢\mathrm{Scalar}\left(W\right)=\mathrm{Scalar}\left(W\right)$$
12		eqid	$$⊢{\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
13	10 3 11 5 12	prjsper	$$⊢W\in \mathrm{LVec}\to \left\{⟨x,y⟩|\left(\left(x\in B\wedge y\in B\right)\wedge \exists l\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}x=l\underset{\dot{}}{·}y\right)\right\}\mathrm{Er}B$$
14	9 13	syl	$$⊢\phi \to \left\{⟨x,y⟩|\left(\left(x\in B\wedge y\in B\right)\wedge \exists l\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}x=l\underset{\dot{}}{·}y\right)\right\}\mathrm{Er}B$$
15	1 2 3 4 5	prjspnerlem	$$⊢K\in \mathrm{DivRing}\to \underset{\dot{}}{\sim }=\left\{⟨x,y⟩|\left(\left(x\in B\wedge y\in B\right)\wedge \exists l\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}x=l\underset{\dot{}}{·}y\right)\right\}$$
16		ereq1	$$⊢\underset{\dot{}}{\sim }=\left\{⟨x,y⟩|\left(\left(x\in B\wedge y\in B\right)\wedge \exists l\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}x=l\underset{\dot{}}{·}y\right)\right\}\to \left(\underset{\dot{}}{\sim }\mathrm{Er}B\leftrightarrow \left\{⟨x,y⟩|\left(\left(x\in B\wedge y\in B\right)\wedge \exists l\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}x=l\underset{\dot{}}{·}y\right)\right\}\mathrm{Er}B\right)$$
17	6 15 16	3syl	$$⊢\phi \to \left(\underset{\dot{}}{\sim }\mathrm{Er}B\leftrightarrow \left\{⟨x,y⟩|\left(\left(x\in B\wedge y\in B\right)\wedge \exists l\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}x=l\underset{\dot{}}{·}y\right)\right\}\mathrm{Er}B\right)$$
18	14 17	mpbird	$$⊢\phi \to \underset{\dot{}}{\sim }\mathrm{Er}B$$