Theorem prjspval

Description: Value of the projective space function, which is also known as the projectivization of V . (Contributed by Steven Nguyen, 29-Apr-2023)

	Ref	Expression
Hypotheses	prjspval.b	$$⊢B={\mathrm{Base}}_V\setminus \left\{0_V\right\}$$
	prjspval.x	$$⊢\underset{\dot{}}{·}={\cdot }_V$$
	prjspval.s	$$⊢S=\mathrm{Scalar}\left(V\right)$$
	prjspval.k	$$⊢K={\mathrm{Base}}_S$$
Assertion	prjspval	$$⊢V\in \mathrm{LVec}\to \mathrm{\mathbb{P}𝕣𝕠𝕛}\left(V\right)=B/\left\{⟨x,y⟩|\left(\left(x\in B\wedge y\in B\right)\wedge \exists l\in Kx=l\underset{\dot{}}{·}y\right)\right\}$$

Proof

Step	Hyp	Ref	Expression
1		prjspval.b	$$⊢B={\mathrm{Base}}_V\setminus \left\{0_V\right\}$$
2		prjspval.x	$$⊢\underset{\dot{}}{·}={\cdot }_V$$
3		prjspval.s	$$⊢S=\mathrm{Scalar}\left(V\right)$$
4		prjspval.k	$$⊢K={\mathrm{Base}}_S$$
5		fvex	$$⊢{\mathrm{Base}}_v\in \mathrm{V}$$
6	5	difexi	$$⊢{\mathrm{Base}}_v\setminus \left\{0_v\right\}\in \mathrm{V}$$
7	6	a1i	$$⊢v=V\to {\mathrm{Base}}_v\setminus \left\{0_v\right\}\in \mathrm{V}$$
8		fveq2	$$⊢v=V\to {\mathrm{Base}}_v={\mathrm{Base}}_V$$
9		fveq2	$$⊢v=V\to 0_v=0_V$$
10	9	sneqd	$$⊢v=V\to \left\{0_v\right\}=\left\{0_V\right\}$$
11	8 10	difeq12d	$$⊢v=V\to {\mathrm{Base}}_v\setminus \left\{0_v\right\}={\mathrm{Base}}_V\setminus \left\{0_V\right\}$$
12	11 1	eqtr4di	$$⊢v=V\to {\mathrm{Base}}_v\setminus \left\{0_v\right\}=B$$
13	12	eqeq2d	$$⊢v=V\to \left(b={\mathrm{Base}}_v\setminus \left\{0_v\right\}\leftrightarrow b=B\right)$$
14	13	biimpd	$$⊢v=V\to \left(b={\mathrm{Base}}_v\setminus \left\{0_v\right\}\to b=B\right)$$
15	14	imp	$$⊢\left(v=V\wedge b={\mathrm{Base}}_v\setminus \left\{0_v\right\}\right)\to b=B$$
16	14	imdistani	$$⊢\left(v=V\wedge b={\mathrm{Base}}_v\setminus \left\{0_v\right\}\right)\to \left(v=V\wedge b=B\right)$$
17		eleq2	$$⊢b=B\to \left(x\in b\leftrightarrow x\in B\right)$$
18		eleq2	$$⊢b=B\to \left(y\in b\leftrightarrow y\in B\right)$$
19	17 18	anbi12d	$$⊢b=B\to \left(\left(x\in b\wedge y\in b\right)\leftrightarrow \left(x\in B\wedge y\in B\right)\right)$$
20		fveq2	$$⊢v=V\to \mathrm{Scalar}\left(v\right)=\mathrm{Scalar}\left(V\right)$$
21	20 3	eqtr4di	$$⊢v=V\to \mathrm{Scalar}\left(v\right)=S$$
22	21	fveq2d	$$⊢v=V\to {\mathrm{Base}}_{\mathrm{Scalar}\left(v\right)}={\mathrm{Base}}_S$$
23	22 4	eqtr4di	$$⊢v=V\to {\mathrm{Base}}_{\mathrm{Scalar}\left(v\right)}=K$$
24		fveq2	$$⊢v=V\to {\cdot }_v={\cdot }_V$$
25	24 2	eqtr4di	$$⊢v=V\to {\cdot }_v=\underset{\dot{}}{·}$$
26	25	oveqd	$$⊢v=V\to l{\cdot }_{v}y=l\underset{\dot{}}{·}y$$
27	26	eqeq2d	$$⊢v=V\to \left(x=l{\cdot }_{v}y\leftrightarrow x=l\underset{\dot{}}{·}y\right)$$
28	23 27	rexeqbidv	$$⊢v=V\to \left(\exists l\in {\mathrm{Base}}_{\mathrm{Scalar}\left(v\right)}x=l{\cdot }_{v}y\leftrightarrow \exists l\in Kx=l\underset{\dot{}}{·}y\right)$$
29	19 28	bi2anan9r	$$⊢\left(v=V\wedge b=B\right)\to \left(\left(\left(x\in b\wedge y\in b\right)\wedge \exists l\in {\mathrm{Base}}_{\mathrm{Scalar}\left(v\right)}x=l{\cdot }_{v}y\right)\leftrightarrow \left(\left(x\in B\wedge y\in B\right)\wedge \exists l\in Kx=l\underset{\dot{}}{·}y\right)\right)$$
30	16 29	syl	$$⊢\left(v=V\wedge b={\mathrm{Base}}_v\setminus \left\{0_v\right\}\right)\to \left(\left(\left(x\in b\wedge y\in b\right)\wedge \exists l\in {\mathrm{Base}}_{\mathrm{Scalar}\left(v\right)}x=l{\cdot }_{v}y\right)\leftrightarrow \left(\left(x\in B\wedge y\in B\right)\wedge \exists l\in Kx=l\underset{\dot{}}{·}y\right)\right)$$
31	30	opabbidv	$$⊢\left(v=V\wedge b={\mathrm{Base}}_v\setminus \left\{0_v\right\}\right)\to \left\{⟨x,y⟩|\left(\left(x\in b\wedge y\in b\right)\wedge \exists l\in {\mathrm{Base}}_{\mathrm{Scalar}\left(v\right)}x=l{\cdot }_{v}y\right)\right\}=\left\{⟨x,y⟩|\left(\left(x\in B\wedge y\in B\right)\wedge \exists l\in Kx=l\underset{\dot{}}{·}y\right)\right\}$$
32	15 31	qseq12d	$$⊢\left(v=V\wedge b={\mathrm{Base}}_v\setminus \left\{0_v\right\}\right)\to b/\left\{⟨x,y⟩|\left(\left(x\in b\wedge y\in b\right)\wedge \exists l\in {\mathrm{Base}}_{\mathrm{Scalar}\left(v\right)}x=l{\cdot }_{v}y\right)\right\}=B/\left\{⟨x,y⟩|\left(\left(x\in B\wedge y\in B\right)\wedge \exists l\in Kx=l\underset{\dot{}}{·}y\right)\right\}$$
33	7 32	csbied	$$⊢v=V\to ⦋\left({\mathrm{Base}}_v\setminus \left\{0_v\right\}\right)/b⦌\left(b/\left\{⟨x,y⟩|\left(\left(x\in b\wedge y\in b\right)\wedge \exists l\in {\mathrm{Base}}_{\mathrm{Scalar}\left(v\right)}x=l{\cdot }_{v}y\right)\right\}\right)=B/\left\{⟨x,y⟩|\left(\left(x\in B\wedge y\in B\right)\wedge \exists l\in Kx=l\underset{\dot{}}{·}y\right)\right\}$$
34		df-prjsp	$$⊢\mathrm{\mathbb{P}𝕣𝕠𝕛}=\left(v\in \mathrm{LVec}⟼⦋\left({\mathrm{Base}}_v\setminus \left\{0_v\right\}\right)/b⦌\left(b/\left\{⟨x,y⟩|\left(\left(x\in b\wedge y\in b\right)\wedge \exists l\in {\mathrm{Base}}_{\mathrm{Scalar}\left(v\right)}x=l{\cdot }_{v}y\right)\right\}\right)\right)$$
35		fvex	$$⊢{\mathrm{Base}}_V\in \mathrm{V}$$
36	35	difexi	$$⊢{\mathrm{Base}}_V\setminus \left\{0_V\right\}\in \mathrm{V}$$
37	1 36	eqeltri	$$⊢B\in \mathrm{V}$$
38	37	qsex	$$⊢B/\left\{⟨x,y⟩|\left(\left(x\in B\wedge y\in B\right)\wedge \exists l\in Kx=l\underset{\dot{}}{·}y\right)\right\}\in \mathrm{V}$$
39	33 34 38	fvmpt	$$⊢V\in \mathrm{LVec}\to \mathrm{\mathbb{P}𝕣𝕠𝕛}\left(V\right)=B/\left\{⟨x,y⟩|\left(\left(x\in B\wedge y\in B\right)\wedge \exists l\in Kx=l\underset{\dot{}}{·}y\right)\right\}$$