Theorem prjspner01

Description: Any vector is equivalent to a vector whose zeroth coordinate is .0. or .1. (proof of the equivalence). (Contributed by SN, 13-Aug-2023)

	Ref	Expression
Hypotheses	prjspner01.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\}$$
	prjspner01.f	$$⊢F=\left(b\in B⟼if\left(b\left(0\right)=\underset{\dot{}}{0},b,I\left(b\left(0\right)\right)\underset{\dot{}}{·}b\right)\right)$$
	prjspner01.b	$$⊢B={\mathrm{Base}}_W\setminus \left\{0_W\right\}$$
	prjspner01.w	$$⊢W=K\mathrm{freeLMod}\left(0\dots N\right)$$
	prjspner01.t	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
	prjspner01.s	$$⊢S={\mathrm{Base}}_K$$
	prjspner01.0	$$⊢\underset{\dot{}}{0}=0_K$$
	prjspner01.i	$$⊢I={inv}_r\left(K\right)$$
	prjspner01.k	$$⊢\phi \to K\in \mathrm{DivRing}$$
	prjspner01.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
	prjspner01.x	$$⊢\phi \to X\in B$$
Assertion	prjspner01	$$⊢\phi \to X\underset{\dot{}}{\sim }F\left(X\right)$$

Proof

Step	Hyp	Ref	Expression
1		prjspner01.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		prjspner01.f	$$⊢F=\left(b\in B⟼if\left(b\left(0\right)=\underset{\dot{}}{0},b,I\left(b\left(0\right)\right)\underset{\dot{}}{·}b\right)\right)$$
3		prjspner01.b	$$⊢B={\mathrm{Base}}_W\setminus \left\{0_W\right\}$$
4		prjspner01.w	$$⊢W=K\mathrm{freeLMod}\left(0\dots N\right)$$
5		prjspner01.t	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
6		prjspner01.s	$$⊢S={\mathrm{Base}}_K$$
7		prjspner01.0	$$⊢\underset{\dot{}}{0}=0_K$$
8		prjspner01.i	$$⊢I={inv}_r\left(K\right)$$
9		prjspner01.k	$$⊢\phi \to K\in \mathrm{DivRing}$$
10		prjspner01.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
11		prjspner01.x	$$⊢\phi \to X\in B$$
12	1 4 3 6 5 9	prjspner	$$⊢\phi \to \underset{\dot{}}{\sim }\mathrm{Er}B$$
13	12 11	erref	$$⊢\phi \to X\underset{\dot{}}{\sim }X$$
14	13	adantr	$$⊢\left(\phi \wedge X\left(0\right)=\underset{\dot{}}{0}\right)\to X\underset{\dot{}}{\sim }X$$
15	12	adantr	$$⊢\left(\phi \wedge \neg X\left(0\right)=\underset{\dot{}}{0}\right)\to \underset{\dot{}}{\sim }\mathrm{Er}B$$
16	9	adantr	$$⊢\left(\phi \wedge \neg X\left(0\right)=\underset{\dot{}}{0}\right)\to K\in \mathrm{DivRing}$$
17	11	adantr	$$⊢\left(\phi \wedge \neg X\left(0\right)=\underset{\dot{}}{0}\right)\to X\in B$$
18		ovexd	$$⊢\phi \to \left(0\dots N\right)\in \mathrm{V}$$
19	11 3	eleqtrdi	$$⊢\phi \to X\in \left({\mathrm{Base}}_W\setminus \left\{0_W\right\}\right)$$
20	19	eldifad	$$⊢\phi \to X\in {\mathrm{Base}}_W$$
21		eqid	$$⊢{\mathrm{Base}}_W={\mathrm{Base}}_W$$
22	4 6 21	frlmbasf	$$⊢\left(\left(0\dots N\right)\in \mathrm{V}\wedge X\in {\mathrm{Base}}_W\right)\to X:\left(0\dots N\right)⟶S$$
23	18 20 22	syl2anc	$$⊢\phi \to X:\left(0\dots N\right)⟶S$$
24		0elfz	$$⊢N\in {\mathbb{N}}_0\to 0\in \left(0\dots N\right)$$
25	10 24	syl	$$⊢\phi \to 0\in \left(0\dots N\right)$$
26	23 25	ffvelcdmd	$$⊢\phi \to X\left(0\right)\in S$$
27		neqne	$$⊢\neg X\left(0\right)=\underset{\dot{}}{0}\to X\left(0\right)\ne \underset{\dot{}}{0}$$
28	6 7 8	drnginvrcl	$$⊢\left(K\in \mathrm{DivRing}\wedge X\left(0\right)\in S\wedge X\left(0\right)\ne \underset{\dot{}}{0}\right)\to I\left(X\left(0\right)\right)\in S$$
29	9 26 27 28	syl2an3an	$$⊢\left(\phi \wedge \neg X\left(0\right)=\underset{\dot{}}{0}\right)\to I\left(X\left(0\right)\right)\in S$$
30	6 7 8	drnginvrn0	$$⊢\left(K\in \mathrm{DivRing}\wedge X\left(0\right)\in S\wedge X\left(0\right)\ne \underset{\dot{}}{0}\right)\to I\left(X\left(0\right)\right)\ne \underset{\dot{}}{0}$$
31	9 26 27 30	syl2an3an	$$⊢\left(\phi \wedge \neg X\left(0\right)=\underset{\dot{}}{0}\right)\to I\left(X\left(0\right)\right)\ne \underset{\dot{}}{0}$$
32	1 4 3 6 5 7 16 17 29 31	prjspnvs	$$⊢\left(\phi \wedge \neg X\left(0\right)=\underset{\dot{}}{0}\right)\to \left(I\left(X\left(0\right)\right)\underset{\dot{}}{·}X\right)\underset{\dot{}}{\sim }X$$
33	15 32	ersym	$$⊢\left(\phi \wedge \neg X\left(0\right)=\underset{\dot{}}{0}\right)\to X\underset{\dot{}}{\sim }\left(I\left(X\left(0\right)\right)\underset{\dot{}}{·}X\right)$$
34	14 33	ifpimpda	$$⊢\phi \to if-\left(X\left(0\right)=\underset{\dot{}}{0},X\underset{\dot{}}{\sim }X,X\underset{\dot{}}{\sim }\left(I\left(X\left(0\right)\right)\underset{\dot{}}{·}X\right)\right)$$
35		brif2	$$⊢X\underset{\dot{}}{\sim }if\left(X\left(0\right)=\underset{\dot{}}{0},X,I\left(X\left(0\right)\right)\underset{\dot{}}{·}X\right)\leftrightarrow if-\left(X\left(0\right)=\underset{\dot{}}{0},X\underset{\dot{}}{\sim }X,X\underset{\dot{}}{\sim }\left(I\left(X\left(0\right)\right)\underset{\dot{}}{·}X\right)\right)$$
36	34 35	sylibr	$$⊢\phi \to X\underset{\dot{}}{\sim }if\left(X\left(0\right)=\underset{\dot{}}{0},X,I\left(X\left(0\right)\right)\underset{\dot{}}{·}X\right)$$
37		fveq1	$$⊢b=X\to b\left(0\right)=X\left(0\right)$$
38	37	eqeq1d	$$⊢b=X\to \left(b\left(0\right)=\underset{\dot{}}{0}\leftrightarrow X\left(0\right)=\underset{\dot{}}{0}\right)$$
39		id	$$⊢b=X\to b=X$$
40	37	fveq2d	$$⊢b=X\to I\left(b\left(0\right)\right)=I\left(X\left(0\right)\right)$$
41	40 39	oveq12d	$$⊢b=X\to I\left(b\left(0\right)\right)\underset{\dot{}}{·}b=I\left(X\left(0\right)\right)\underset{\dot{}}{·}X$$
42	38 39 41	ifbieq12d	$$⊢b=X\to if\left(b\left(0\right)=\underset{\dot{}}{0},b,I\left(b\left(0\right)\right)\underset{\dot{}}{·}b\right)=if\left(X\left(0\right)=\underset{\dot{}}{0},X,I\left(X\left(0\right)\right)\underset{\dot{}}{·}X\right)$$
43		ovexd	$$⊢\phi \to I\left(X\left(0\right)\right)\underset{\dot{}}{·}X\in \mathrm{V}$$
44	11 43	ifexd	$$⊢\phi \to if\left(X\left(0\right)=\underset{\dot{}}{0},X,I\left(X\left(0\right)\right)\underset{\dot{}}{·}X\right)\in \mathrm{V}$$
45	2 42 11 44	fvmptd3	$$⊢\phi \to F\left(X\right)=if\left(X\left(0\right)=\underset{\dot{}}{0},X,I\left(X\left(0\right)\right)\underset{\dot{}}{·}X\right)$$
46	36 45	breqtrrd	$$⊢\phi \to X\underset{\dot{}}{\sim }F\left(X\right)$$