Theorem uvcn0

Description: A unit vector is nonzero. (Contributed by Steven Nguyen, 16-Jul-2023)

	Ref	Expression
Hypotheses	uvcn0.u	|- U = ( R unitVec I )
	uvcn0.y	|- Y = ( R freeLMod I )
	uvcn0.b	|- B = ( Base ` Y )
	uvcn0.0	|- .0. = ( 0g ` Y )
Assertion	uvcn0	|- ( ( R e. NzRing /\ I e. W /\ J e. I ) -> ( U ` J ) =/= .0. )

Proof

Step	Hyp	Ref	Expression
1		uvcn0.u	|- U = ( R unitVec I )
2		uvcn0.y	|- Y = ( R freeLMod I )
3		uvcn0.b	|- B = ( Base ` Y )
4		uvcn0.0	|- .0. = ( 0g ` Y )
5		eqid	|- ( 1r ` R ) = ( 1r ` R )
6		eqid	|- ( 0g ` R ) = ( 0g ` R )
7	5 6	nzrnz	|- ( R e. NzRing -> ( 1r ` R ) =/= ( 0g ` R ) )
8	7	3ad2ant1	|- ( ( R e. NzRing /\ I e. W /\ J e. I ) -> ( 1r ` R ) =/= ( 0g ` R ) )
9		simp1	|- ( ( R e. NzRing /\ I e. W /\ J e. I ) -> R e. NzRing )
10		simp2	|- ( ( R e. NzRing /\ I e. W /\ J e. I ) -> I e. W )
11		simp3	|- ( ( R e. NzRing /\ I e. W /\ J e. I ) -> J e. I )
12	1 9 10 11 5	uvcvv1	|- ( ( R e. NzRing /\ I e. W /\ J e. I ) -> ( ( U ` J ) ` J ) = ( 1r ` R ) )
13		nzrring	|- ( R e. NzRing -> R e. Ring )
14	13	3ad2ant1	|- ( ( R e. NzRing /\ I e. W /\ J e. I ) -> R e. Ring )
15	2 6 14 10 11	frlm0vald	|- ( ( R e. NzRing /\ I e. W /\ J e. I ) -> ( ( 0g ` Y ) ` J ) = ( 0g ` R ) )
16	8 12 15	3netr4d	|- ( ( R e. NzRing /\ I e. W /\ J e. I ) -> ( ( U ` J ) ` J ) =/= ( ( 0g ` Y ) ` J ) )
17		fveq1	|- ( ( U ` J ) = ( 0g ` Y ) -> ( ( U ` J ) ` J ) = ( ( 0g ` Y ) ` J ) )
18	17	necon3i	|- ( ( ( U ` J ) ` J ) =/= ( ( 0g ` Y ) ` J ) -> ( U ` J ) =/= ( 0g ` Y ) )
19	16 18	syl	|- ( ( R e. NzRing /\ I e. W /\ J e. I ) -> ( U ` J ) =/= ( 0g ` Y ) )
20	4	a1i	|- ( ( R e. NzRing /\ I e. W /\ J e. I ) -> .0. = ( 0g ` Y ) )
21	19 20	neeqtrrd	|- ( ( R e. NzRing /\ I e. W /\ J e. I ) -> ( U ` J ) =/= .0. )