This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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. )