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

Metamath Proof Explorer

Theorem ringinvnz1ne0

Description: In a unital ring, a left invertible element is different from zero iff .1. =/= .0. . (Contributed by FL, 18-Apr-2010) (Revised by AV, 24-Aug-2021)

Ref Expression
Hypotheses ringinvnzdiv.b 
|- B = ( Base ` R )
ringinvnzdiv.t 
|- .x. = ( .r ` R )
ringinvnzdiv.u 
|- .1. = ( 1r ` R )
ringinvnzdiv.z 
|- .0. = ( 0g ` R )
ringinvnzdiv.r 
|- ( ph -> R e. Ring )
ringinvnzdiv.x 
|- ( ph -> X e. B )
ringinvnzdiv.a 
|- ( ph -> E. a e. B ( a .x. X ) = .1. )
Assertion ringinvnz1ne0 
|- ( ph -> ( X =/= .0. <-> .1. =/= .0. ) )

Proof

Step Hyp Ref Expression
1 ringinvnzdiv.b 
 |-  B = ( Base ` R )
2 ringinvnzdiv.t 
 |-  .x. = ( .r ` R )
3 ringinvnzdiv.u 
 |-  .1. = ( 1r ` R )
4 ringinvnzdiv.z 
 |-  .0. = ( 0g ` R )
5 ringinvnzdiv.r 
 |-  ( ph -> R e. Ring )
6 ringinvnzdiv.x 
 |-  ( ph -> X e. B )
7 ringinvnzdiv.a 
 |-  ( ph -> E. a e. B ( a .x. X ) = .1. )
8 oveq2 
 |-  ( X = .0. -> ( a .x. X ) = ( a .x. .0. ) )
9 1 2 4 ringrz 
 |-  ( ( R e. Ring /\ a e. B ) -> ( a .x. .0. ) = .0. )
10 5 9 sylan 
 |-  ( ( ph /\ a e. B ) -> ( a .x. .0. ) = .0. )
11 eqeq12 
 |-  ( ( ( a .x. X ) = .1. /\ ( a .x. .0. ) = .0. ) -> ( ( a .x. X ) = ( a .x. .0. ) <-> .1. = .0. ) )
12 11 biimpd 
 |-  ( ( ( a .x. X ) = .1. /\ ( a .x. .0. ) = .0. ) -> ( ( a .x. X ) = ( a .x. .0. ) -> .1. = .0. ) )
13 12 ex 
 |-  ( ( a .x. X ) = .1. -> ( ( a .x. .0. ) = .0. -> ( ( a .x. X ) = ( a .x. .0. ) -> .1. = .0. ) ) )
14 10 13 mpan9 
 |-  ( ( ( ph /\ a e. B ) /\ ( a .x. X ) = .1. ) -> ( ( a .x. X ) = ( a .x. .0. ) -> .1. = .0. ) )
15 8 14 syl5 
 |-  ( ( ( ph /\ a e. B ) /\ ( a .x. X ) = .1. ) -> ( X = .0. -> .1. = .0. ) )
16 oveq2 
 |-  ( .1. = .0. -> ( X .x. .1. ) = ( X .x. .0. ) )
17 1 2 3 ringridm 
 |-  ( ( R e. Ring /\ X e. B ) -> ( X .x. .1. ) = X )
18 1 2 4 ringrz 
 |-  ( ( R e. Ring /\ X e. B ) -> ( X .x. .0. ) = .0. )
19 17 18 eqeq12d 
 |-  ( ( R e. Ring /\ X e. B ) -> ( ( X .x. .1. ) = ( X .x. .0. ) <-> X = .0. ) )
20 19 biimpd 
 |-  ( ( R e. Ring /\ X e. B ) -> ( ( X .x. .1. ) = ( X .x. .0. ) -> X = .0. ) )
21 5 6 20 syl2anc 
 |-  ( ph -> ( ( X .x. .1. ) = ( X .x. .0. ) -> X = .0. ) )
22 21 ad2antrr 
 |-  ( ( ( ph /\ a e. B ) /\ ( a .x. X ) = .1. ) -> ( ( X .x. .1. ) = ( X .x. .0. ) -> X = .0. ) )
23 16 22 syl5 
 |-  ( ( ( ph /\ a e. B ) /\ ( a .x. X ) = .1. ) -> ( .1. = .0. -> X = .0. ) )
24 15 23 impbid 
 |-  ( ( ( ph /\ a e. B ) /\ ( a .x. X ) = .1. ) -> ( X = .0. <-> .1. = .0. ) )
25 24 7 r19.29a 
 |-  ( ph -> ( X = .0. <-> .1. = .0. ) )
26 25 necon3bid 
 |-  ( ph -> ( X =/= .0. <-> .1. =/= .0. ) )