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	$$⊢\underset{\dot{}}{\sim }=\left\{⟨x,y⟩|\left(\left(x\in B\wedge y\in B\right)\wedge \exists l\in Kx=l\underset{\dot{}}{·}y\right)\right\}$$
	prjspertr.b	$$⊢B={\mathrm{Base}}_V\setminus \left\{0_V\right\}$$
	prjspertr.s	$$⊢S=\mathrm{Scalar}\left(V\right)$$
	prjspertr.x	$$⊢\underset{\dot{}}{·}={\cdot }_V$$
	prjspertr.k	$$⊢K={\mathrm{Base}}_S$$
Assertion	prjsper	$$⊢V\in \mathrm{LVec}\to \underset{\dot{}}{\sim }\mathrm{Er}B$$

Proof

Step	Hyp	Ref	Expression
1		prjsprel.1	$$⊢\underset{\dot{}}{\sim }=\left\{⟨x,y⟩|\left(\left(x\in B\wedge y\in B\right)\wedge \exists l\in Kx=l\underset{\dot{}}{·}y\right)\right\}$$
2		prjspertr.b	$$⊢B={\mathrm{Base}}_V\setminus \left\{0_V\right\}$$
3		prjspertr.s	$$⊢S=\mathrm{Scalar}\left(V\right)$$
4		prjspertr.x	$$⊢\underset{\dot{}}{·}={\cdot }_V$$
5		prjspertr.k	$$⊢K={\mathrm{Base}}_S$$
6	1	relopabiv	$$⊢\mathrm{Rel}\underset{\dot{}}{\sim }$$
7	6	a1i	$$⊢V\in \mathrm{LVec}\to \mathrm{Rel}\underset{\dot{}}{\sim }$$
8	1 2 3 4 5	prjspersym	$$⊢\left(V\in \mathrm{LVec}\wedge a\underset{\dot{}}{\sim }b\right)\to b\underset{\dot{}}{\sim }a$$
9		lveclmod	$$⊢V\in \mathrm{LVec}\to V\in \mathrm{LMod}$$
10	1 2 3 4 5	prjspertr	$$⊢\left(V\in \mathrm{LMod}\wedge \left(a\underset{\dot{}}{\sim }b\wedge b\underset{\dot{}}{\sim }c\right)\right)\to a\underset{\dot{}}{\sim }c$$
11	9 10	sylan	$$⊢\left(V\in \mathrm{LVec}\wedge \left(a\underset{\dot{}}{\sim }b\wedge b\underset{\dot{}}{\sim }c\right)\right)\to a\underset{\dot{}}{\sim }c$$
12	1 2 3 4 5	prjsperref	$$⊢V\in \mathrm{LMod}\to \left(a\in B\leftrightarrow a\underset{\dot{}}{\sim }a\right)$$
13	9 12	syl	$$⊢V\in \mathrm{LVec}\to \left(a\in B\leftrightarrow a\underset{\dot{}}{\sim }a\right)$$
14	7 8 11 13	iserd	$$⊢V\in \mathrm{LVec}\to \underset{\dot{}}{\sim }\mathrm{Er}B$$