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 = ( ( Base ` W ) \ { ( 0g ` W ) } )
	0prjspnlem.w	|- W = ( K freeLMod ( 0 ... 0 ) )
	0prjspnlem.1	|- .1. = ( ( K unitVec ( 0 ... 0 ) ) ` 0 )
Assertion	0prjspnlem	|- ( K e. DivRing -> .1. e. B )

Proof

Step	Hyp	Ref	Expression
1		0prjspnlem.b	|- B = ( ( Base ` W ) \ { ( 0g ` W ) } )
2		0prjspnlem.w	|- W = ( K freeLMod ( 0 ... 0 ) )
3		0prjspnlem.1	|- .1. = ( ( K unitVec ( 0 ... 0 ) ) ` 0 )
4		drngnzr	|- ( K e. DivRing -> K e. NzRing )
5		ovex	|- ( 0 ... 0 ) e. _V
6		c0ex	|- 0 e. _V
7	6	snid	|- 0 e. { 0 }
8		fz0sn	|- ( 0 ... 0 ) = { 0 }
9	7 8	eleqtrri	|- 0 e. ( 0 ... 0 )
10		nzrring	|- ( K e. NzRing -> K e. Ring )
11		eqid	|- ( K unitVec ( 0 ... 0 ) ) = ( K unitVec ( 0 ... 0 ) )
12		eqid	|- ( Base ` W ) = ( Base ` W )
13	11 2 12	uvccl	|- ( ( K e. Ring /\ ( 0 ... 0 ) e. _V /\ 0 e. ( 0 ... 0 ) ) -> ( ( K unitVec ( 0 ... 0 ) ) ` 0 ) e. ( Base ` W ) )
14	10 13	syl3an1	|- ( ( K e. NzRing /\ ( 0 ... 0 ) e. _V /\ 0 e. ( 0 ... 0 ) ) -> ( ( K unitVec ( 0 ... 0 ) ) ` 0 ) e. ( Base ` W ) )
15		eqid	|- ( 0g ` W ) = ( 0g ` W )
16	11 2 12 15	uvcn0	|- ( ( K e. NzRing /\ ( 0 ... 0 ) e. _V /\ 0 e. ( 0 ... 0 ) ) -> ( ( K unitVec ( 0 ... 0 ) ) ` 0 ) =/= ( 0g ` W ) )
17		eldifsn	|- ( ( ( K unitVec ( 0 ... 0 ) ) ` 0 ) e. ( ( Base ` W ) \ { ( 0g ` W ) } ) <-> ( ( ( K unitVec ( 0 ... 0 ) ) ` 0 ) e. ( Base ` W ) /\ ( ( K unitVec ( 0 ... 0 ) ) ` 0 ) =/= ( 0g ` W ) ) )
18	14 16 17	sylanbrc	|- ( ( K e. NzRing /\ ( 0 ... 0 ) e. _V /\ 0 e. ( 0 ... 0 ) ) -> ( ( K unitVec ( 0 ... 0 ) ) ` 0 ) e. ( ( Base ` W ) \ { ( 0g ` W ) } ) )
19	5 9 18	mp3an23	|- ( K e. NzRing -> ( ( K unitVec ( 0 ... 0 ) ) ` 0 ) e. ( ( Base ` W ) \ { ( 0g ` W ) } ) )
20	4 19	syl	|- ( K e. DivRing -> ( ( K unitVec ( 0 ... 0 ) ) ` 0 ) e. ( ( Base ` W ) \ { ( 0g ` W ) } ) )
21	20 3 1	3eltr4g	|- ( K e. DivRing -> .1. e. B )