Theorem prjspnvs

Description: A nonzero multiple of a vector is equivalent to the vector. This is prjspvs with the equivalence relation converted by prjspnerlem . (Contributed by SN, 8-Aug-2024)

	Ref	Expression
Hypotheses	prjspnvs.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\}$$
	prjspnvs.w	$$⊢W=K\mathrm{freeLMod}\left(0\dots N\right)$$
	prjspnvs.b	$$⊢B={\mathrm{Base}}_W\setminus \left\{0_W\right\}$$
	prjspnvs.s	$$⊢S={\mathrm{Base}}_K$$
	prjspnvs.x	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
	prjspnvs.0	$$⊢\underset{\dot{}}{0}=0_K$$
	prjspnvs.k	$$⊢\phi \to K\in \mathrm{DivRing}$$
	prjspnvs.1	$$⊢\phi \to X\in B$$
	prjspnvs.2	$$⊢\phi \to C\in S$$
	prjspnvs.3	$$⊢\phi \to C\ne \underset{\dot{}}{0}$$
Assertion	prjspnvs	$$⊢\phi \to \left(C\underset{\dot{}}{·}X\right)\underset{\dot{}}{\sim }X$$

Proof

Step	Hyp	Ref	Expression
1		prjspnvs.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		prjspnvs.w	$$⊢W=K\mathrm{freeLMod}\left(0\dots N\right)$$
3		prjspnvs.b	$$⊢B={\mathrm{Base}}_W\setminus \left\{0_W\right\}$$
4		prjspnvs.s	$$⊢S={\mathrm{Base}}_K$$
5		prjspnvs.x	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
6		prjspnvs.0	$$⊢\underset{\dot{}}{0}=0_K$$
7		prjspnvs.k	$$⊢\phi \to K\in \mathrm{DivRing}$$
8		prjspnvs.1	$$⊢\phi \to X\in B$$
9		prjspnvs.2	$$⊢\phi \to C\in S$$
10		prjspnvs.3	$$⊢\phi \to C\ne \underset{\dot{}}{0}$$
11		ovexd	$$⊢\phi \to \left(0\dots N\right)\in \mathrm{V}$$
12	2	frlmlvec	$$⊢\left(K\in \mathrm{DivRing}\wedge \left(0\dots N\right)\in \mathrm{V}\right)\to W\in \mathrm{LVec}$$
13	7 11 12	syl2anc	$$⊢\phi \to W\in \mathrm{LVec}$$
14		nelsn	$$⊢C\ne \underset{\dot{}}{0}\to \neg C\in \left\{\underset{\dot{}}{0}\right\}$$
15	10 14	syl	$$⊢\phi \to \neg C\in \left\{\underset{\dot{}}{0}\right\}$$
16	9 15	eldifd	$$⊢\phi \to C\in \left(S\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
17	2	frlmsca	$$⊢\left(K\in \mathrm{DivRing}\wedge \left(0\dots N\right)\in \mathrm{V}\right)\to K=\mathrm{Scalar}\left(W\right)$$
18	7 11 17	syl2anc	$$⊢\phi \to K=\mathrm{Scalar}\left(W\right)$$
19	18	fveq2d	$$⊢\phi \to {\mathrm{Base}}_K={\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
20	4 19	eqtrid	$$⊢\phi \to S={\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
21	18	fveq2d	$$⊢\phi \to 0_K=0_{\mathrm{Scalar}\left(W\right)}$$
22	6 21	eqtrid	$$⊢\phi \to \underset{\dot{}}{0}=0_{\mathrm{Scalar}\left(W\right)}$$
23	22	sneqd	$$⊢\phi \to \left\{\underset{\dot{}}{0}\right\}=\left\{0_{\mathrm{Scalar}\left(W\right)}\right\}$$
24	20 23	difeq12d	$$⊢\phi \to S\setminus \left\{\underset{\dot{}}{0}\right\}={\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\setminus \left\{0_{\mathrm{Scalar}\left(W\right)}\right\}$$
25	16 24	eleqtrd	$$⊢\phi \to C\in \left({\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\setminus \left\{0_{\mathrm{Scalar}\left(W\right)}\right\}\right)$$
26		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\}$$
27		eqid	$$⊢\mathrm{Scalar}\left(W\right)=\mathrm{Scalar}\left(W\right)$$
28		eqid	$$⊢{\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
29		eqid	$$⊢0_{\mathrm{Scalar}\left(W\right)}=0_{\mathrm{Scalar}\left(W\right)}$$
30	26 3 27 5 28 29	prjspvs	$$⊢\left(W\in \mathrm{LVec}\wedge X\in B\wedge C\in \left({\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\setminus \left\{0_{\mathrm{Scalar}\left(W\right)}\right\}\right)\right)\to \left(C\underset{\dot{}}{·}X\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\}X$$
31	13 8 25 30	syl3anc	$$⊢\phi \to \left(C\underset{\dot{}}{·}X\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\}X$$
32	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\}$$
33	7 32	syl	$$⊢\phi \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\}$$
34	33	breqd	$$⊢\phi \to \left(\left(C\underset{\dot{}}{·}X\right)\underset{\dot{}}{\sim }X\leftrightarrow \left(C\underset{\dot{}}{·}X\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\}X\right)$$
35	31 34	mpbird	$$⊢\phi \to \left(C\underset{\dot{}}{·}X\right)\underset{\dot{}}{\sim }X$$