Theorem prjspnfv01

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

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

Proof

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