Theorem prjspval2

Description: Alternate definition of projective space. (Contributed by Steven Nguyen, 7-Jun-2023)

	Ref	Expression
Hypotheses	prjspval2.0	$$⊢\underset{\dot{}}{0}=0_V$$
	prjspval2.b	$$⊢B={\mathrm{Base}}_V\setminus \left\{\underset{\dot{}}{0}\right\}$$
	prjspval2.n	$$⊢N=\mathrm{LSpan}\left(V\right)$$
Assertion	prjspval2	$$⊢V\in \mathrm{LVec}\to \mathrm{\mathbb{P}𝕣𝕠𝕛}\left(V\right)=\bigcup _{z\in B}\left\{N\left(\left\{z\right\}\right)\setminus \left\{\underset{\dot{}}{0}\right\}\right\}$$

Proof

Step	Hyp	Ref	Expression
1		prjspval2.0	$$⊢\underset{\dot{}}{0}=0_V$$
2		prjspval2.b	$$⊢B={\mathrm{Base}}_V\setminus \left\{\underset{\dot{}}{0}\right\}$$
3		prjspval2.n	$$⊢N=\mathrm{LSpan}\left(V\right)$$
4	1	sneqi	$$⊢\left\{\underset{\dot{}}{0}\right\}=\left\{0_V\right\}$$
5	4	difeq2i	$$⊢{\mathrm{Base}}_V\setminus \left\{\underset{\dot{}}{0}\right\}={\mathrm{Base}}_V\setminus \left\{0_V\right\}$$
6	2 5	eqtri	$$⊢B={\mathrm{Base}}_V\setminus \left\{0_V\right\}$$
7		eqid	$$⊢{\cdot }_V={\cdot }_V$$
8		eqid	$$⊢\mathrm{Scalar}\left(V\right)=\mathrm{Scalar}\left(V\right)$$
9		eqid	$$⊢{\mathrm{Base}}_{\mathrm{Scalar}\left(V\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(V\right)}$$
10	6 7 8 9	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 {\mathrm{Base}}_{\mathrm{Scalar}\left(V\right)}x=l{\cdot }_{V}y\right)\right\}$$
11		dfqs3	$$⊢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\}=\bigcup _{z\in B}\left\{\left[z\right]\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\}$$
12	11	a1i	$$⊢V\in \mathrm{LVec}\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\}=\bigcup _{z\in B}\left\{\left[z\right]\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\}$$
13		eqid	$$⊢\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 {\mathrm{Base}}_{\mathrm{Scalar}\left(V\right)}x=l{\cdot }_{V}y\right)\right\}$$
14	13 6 8 7 9 3	prjspeclsp	$$⊢\left(V\in \mathrm{LVec}\wedge z\in B\right)\to \left[z\right]\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\}=N\left(\left\{z\right\}\right)\setminus \left\{0_V\right\}$$
15	4	difeq2i	$$⊢N\left(\left\{z\right\}\right)\setminus \left\{\underset{\dot{}}{0}\right\}=N\left(\left\{z\right\}\right)\setminus \left\{0_V\right\}$$
16	14 15	eqtr4di	$$⊢\left(V\in \mathrm{LVec}\wedge z\in B\right)\to \left[z\right]\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\}=N\left(\left\{z\right\}\right)\setminus \left\{\underset{\dot{}}{0}\right\}$$
17	16	sneqd	$$⊢\left(V\in \mathrm{LVec}\wedge z\in B\right)\to \left\{\left[z\right]\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\}=\left\{N\left(\left\{z\right\}\right)\setminus \left\{\underset{\dot{}}{0}\right\}\right\}$$
18	17	iuneq2dv	$$⊢V\in \mathrm{LVec}\to \bigcup _{z\in B}\left\{\left[z\right]\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\}=\bigcup _{z\in B}\left\{N\left(\left\{z\right\}\right)\setminus \left\{\underset{\dot{}}{0}\right\}\right\}$$
19	10 12 18	3eqtrd	$$⊢V\in \mathrm{LVec}\to \mathrm{\mathbb{P}𝕣𝕠𝕛}\left(V\right)=\bigcup _{z\in B}\left\{N\left(\left\{z\right\}\right)\setminus \left\{\underset{\dot{}}{0}\right\}\right\}$$