Theorem 0prjspnlem

Description: Lemma for 0prjspn . The given unit vector is a nonzero vector. (Contributed by Steven Nguyen, 16-Jul-2023)

	Ref	Expression
Hypotheses	0prjspnlem.b	$$⊢B={\mathrm{Base}}_W\setminus \left\{0_W\right\}$$
	0prjspnlem.w	$$⊢W=K\mathrm{freeLMod}\left(0\dots 0\right)$$
	0prjspnlem.1	$$⊢\underset{\dot{}}{1}=\left(K\mathrm{unitVec}\left(0\dots 0\right)\right)\left(0\right)$$
Assertion	0prjspnlem	$$⊢K\in \mathrm{DivRing}\to \underset{\dot{}}{1}\in B$$

Proof

Step	Hyp	Ref	Expression
1		0prjspnlem.b	$$⊢B={\mathrm{Base}}_W\setminus \left\{0_W\right\}$$
2		0prjspnlem.w	$$⊢W=K\mathrm{freeLMod}\left(0\dots 0\right)$$
3		0prjspnlem.1	$$⊢\underset{\dot{}}{1}=\left(K\mathrm{unitVec}\left(0\dots 0\right)\right)\left(0\right)$$
4		drngnzr	$$⊢K\in \mathrm{DivRing}\to K\in \mathrm{NzRing}$$
5		ovex	$$⊢\left(0\dots 0\right)\in \mathrm{V}$$
6		c0ex	$$⊢0\in \mathrm{V}$$
7	6	snid	$$⊢0\in \left\{0\right\}$$
8		fz0sn	$$⊢\left(0\dots 0\right)=\left\{0\right\}$$
9	7 8	eleqtrri	$$⊢0\in \left(0\dots 0\right)$$
10		nzrring	$$⊢K\in \mathrm{NzRing}\to K\in \mathrm{Ring}$$
11		eqid	$$⊢K\mathrm{unitVec}\left(0\dots 0\right)=K\mathrm{unitVec}\left(0\dots 0\right)$$
12		eqid	$$⊢{\mathrm{Base}}_W={\mathrm{Base}}_W$$
13	11 2 12	uvccl	$$⊢\left(K\in \mathrm{Ring}\wedge \left(0\dots 0\right)\in \mathrm{V}\wedge 0\in \left(0\dots 0\right)\right)\to \left(K\mathrm{unitVec}\left(0\dots 0\right)\right)\left(0\right)\in {\mathrm{Base}}_W$$
14	10 13	syl3an1	$$⊢\left(K\in \mathrm{NzRing}\wedge \left(0\dots 0\right)\in \mathrm{V}\wedge 0\in \left(0\dots 0\right)\right)\to \left(K\mathrm{unitVec}\left(0\dots 0\right)\right)\left(0\right)\in {\mathrm{Base}}_W$$
15		eqid	$$⊢0_W=0_W$$
16	11 2 12 15	uvcn0	$$⊢\left(K\in \mathrm{NzRing}\wedge \left(0\dots 0\right)\in \mathrm{V}\wedge 0\in \left(0\dots 0\right)\right)\to \left(K\mathrm{unitVec}\left(0\dots 0\right)\right)\left(0\right)\ne 0_W$$
17		eldifsn	$$⊢\left(K\mathrm{unitVec}\left(0\dots 0\right)\right)\left(0\right)\in \left({\mathrm{Base}}_W\setminus \left\{0_W\right\}\right)\leftrightarrow \left(\left(K\mathrm{unitVec}\left(0\dots 0\right)\right)\left(0\right)\in {\mathrm{Base}}_W\wedge \left(K\mathrm{unitVec}\left(0\dots 0\right)\right)\left(0\right)\ne 0_W\right)$$
18	14 16 17	sylanbrc	$$⊢\left(K\in \mathrm{NzRing}\wedge \left(0\dots 0\right)\in \mathrm{V}\wedge 0\in \left(0\dots 0\right)\right)\to \left(K\mathrm{unitVec}\left(0\dots 0\right)\right)\left(0\right)\in \left({\mathrm{Base}}_W\setminus \left\{0_W\right\}\right)$$
19	5 9 18	mp3an23	$$⊢K\in \mathrm{NzRing}\to \left(K\mathrm{unitVec}\left(0\dots 0\right)\right)\left(0\right)\in \left({\mathrm{Base}}_W\setminus \left\{0_W\right\}\right)$$
20	4 19	syl	$$⊢K\in \mathrm{DivRing}\to \left(K\mathrm{unitVec}\left(0\dots 0\right)\right)\left(0\right)\in \left({\mathrm{Base}}_W\setminus \left\{0_W\right\}\right)$$
21	20 3 1	3eltr4g	$$⊢K\in \mathrm{DivRing}\to \underset{\dot{}}{1}\in B$$