Theorem prjspnerlem

Description: A lemma showing that the equivalence relation used in prjspnval2 and the equivalence relation used in prjspval are equal, but only with the antecedent K e. DivRing . (Contributed by SN, 15-Jul-2023)

	Ref	Expression
Hypotheses	prjspnerlem.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\}$$
	prjspnerlem.w	$$⊢W=K\mathrm{freeLMod}\left(0\dots N\right)$$
	prjspnerlem.b	$$⊢B={\mathrm{Base}}_W\setminus \left\{0_W\right\}$$
	prjspnerlem.s	$$⊢S={\mathrm{Base}}_K$$
	prjspnerlem.x	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
Assertion	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\}$$

Proof

Step	Hyp	Ref	Expression
1		prjspnerlem.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		prjspnerlem.w	$$⊢W=K\mathrm{freeLMod}\left(0\dots N\right)$$
3		prjspnerlem.b	$$⊢B={\mathrm{Base}}_W\setminus \left\{0_W\right\}$$
4		prjspnerlem.s	$$⊢S={\mathrm{Base}}_K$$
5		prjspnerlem.x	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
6		ovex	$$⊢\left(0\dots N\right)\in \mathrm{V}$$
7	2	frlmsca	$$⊢\left(K\in \mathrm{DivRing}\wedge \left(0\dots N\right)\in \mathrm{V}\right)\to K=\mathrm{Scalar}\left(W\right)$$
8	6 7	mpan2	$$⊢K\in \mathrm{DivRing}\to K=\mathrm{Scalar}\left(W\right)$$
9	8	fveq2d	$$⊢K\in \mathrm{DivRing}\to {\mathrm{Base}}_K={\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
10	4 9	syl5eq	$$⊢K\in \mathrm{DivRing}\to S={\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
11	10	rexeqdv	$$⊢K\in \mathrm{DivRing}\to \left(\exists l\in Sx=l\underset{\dot{}}{·}y\leftrightarrow \exists l\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}x=l\underset{\dot{}}{·}y\right)$$
12	11	anbi2d	$$⊢K\in \mathrm{DivRing}\to \left(\left(\left(x\in B\wedge y\in B\right)\wedge \exists l\in Sx=l\underset{\dot{}}{·}y\right)\leftrightarrow \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)$$
13	12	opabbidv	$$⊢K\in \mathrm{DivRing}\to \left\{⟨x,y⟩|\left(\left(x\in B\wedge y\in B\right)\wedge \exists l\in Sx=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\}$$
14	1 13	syl5eq	$$⊢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\}$$