Metamath Proof Explorer

Theorem ringinvnzdiv

Description: In a unital ring, a left invertible element is not a zero divisor. (Contributed by FL, 18-Apr-2010) (Revised by Jeff Madsen, 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. )
ringinvnzdiv.y 
|- ( ph -> Y e. B )
Assertion ringinvnzdiv 
|- ( ph -> ( ( X .x. Y ) = .0. <-> Y = .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 ringinvnzdiv.y 
 |-  ( ph -> Y e. B )
9 1 2 3 ringlidm 
 |-  ( ( R e. Ring /\ Y e. B ) -> ( .1. .x. Y ) = Y )
10 5 8 9 syl2anc 
 |-  ( ph -> ( .1. .x. Y ) = Y )
11 10 eqcomd 
 |-  ( ph -> Y = ( .1. .x. Y ) )
12 11 ad3antrrr 
 |-  ( ( ( ( ph /\ a e. B ) /\ ( a .x. X ) = .1. ) /\ ( X .x. Y ) = .0. ) -> Y = ( .1. .x. Y ) )
13 oveq1 
 |-  ( .1. = ( a .x. X ) -> ( .1. .x. Y ) = ( ( a .x. X ) .x. Y ) )
14 13 eqcoms 
 |-  ( ( a .x. X ) = .1. -> ( .1. .x. Y ) = ( ( a .x. X ) .x. Y ) )
15 14 adantl 
 |-  ( ( ( ph /\ a e. B ) /\ ( a .x. X ) = .1. ) -> ( .1. .x. Y ) = ( ( a .x. X ) .x. Y ) )
16 5 adantr 
 |-  ( ( ph /\ a e. B ) -> R e. Ring )
17 simpr 
 |-  ( ( ph /\ a e. B ) -> a e. B )
18 6 adantr 
 |-  ( ( ph /\ a e. B ) -> X e. B )
19 8 adantr 
 |-  ( ( ph /\ a e. B ) -> Y e. B )
20 17 18 19 3jca 
 |-  ( ( ph /\ a e. B ) -> ( a e. B /\ X e. B /\ Y e. B ) )
21 16 20 jca 
 |-  ( ( ph /\ a e. B ) -> ( R e. Ring /\ ( a e. B /\ X e. B /\ Y e. B ) ) )
22 21 adantr 
 |-  ( ( ( ph /\ a e. B ) /\ ( a .x. X ) = .1. ) -> ( R e. Ring /\ ( a e. B /\ X e. B /\ Y e. B ) ) )
23 1 2 ringass 
 |-  ( ( R e. Ring /\ ( a e. B /\ X e. B /\ Y e. B ) ) -> ( ( a .x. X ) .x. Y ) = ( a .x. ( X .x. Y ) ) )
24 22 23 syl 
 |-  ( ( ( ph /\ a e. B ) /\ ( a .x. X ) = .1. ) -> ( ( a .x. X ) .x. Y ) = ( a .x. ( X .x. Y ) ) )
25 15 24 eqtrd 
 |-  ( ( ( ph /\ a e. B ) /\ ( a .x. X ) = .1. ) -> ( .1. .x. Y ) = ( a .x. ( X .x. Y ) ) )
26 25 adantr 
 |-  ( ( ( ( ph /\ a e. B ) /\ ( a .x. X ) = .1. ) /\ ( X .x. Y ) = .0. ) -> ( .1. .x. Y ) = ( a .x. ( X .x. Y ) ) )
27 oveq2 
 |-  ( ( X .x. Y ) = .0. -> ( a .x. ( X .x. Y ) ) = ( a .x. .0. ) )
28 1 2 4 ringrz 
 |-  ( ( R e. Ring /\ a e. B ) -> ( a .x. .0. ) = .0. )
29 5 28 sylan 
 |-  ( ( ph /\ a e. B ) -> ( a .x. .0. ) = .0. )
30 29 adantr 
 |-  ( ( ( ph /\ a e. B ) /\ ( a .x. X ) = .1. ) -> ( a .x. .0. ) = .0. )
31 27 30 sylan9eqr 
 |-  ( ( ( ( ph /\ a e. B ) /\ ( a .x. X ) = .1. ) /\ ( X .x. Y ) = .0. ) -> ( a .x. ( X .x. Y ) ) = .0. )
32 12 26 31 3eqtrd 
 |-  ( ( ( ( ph /\ a e. B ) /\ ( a .x. X ) = .1. ) /\ ( X .x. Y ) = .0. ) -> Y = .0. )
33 32 exp31 
 |-  ( ( ph /\ a e. B ) -> ( ( a .x. X ) = .1. -> ( ( X .x. Y ) = .0. -> Y = .0. ) ) )
34 33 rexlimdva 
 |-  ( ph -> ( E. a e. B ( a .x. X ) = .1. -> ( ( X .x. Y ) = .0. -> Y = .0. ) ) )
35 7 34 mpd 
 |-  ( ph -> ( ( X .x. Y ) = .0. -> Y = .0. ) )
36 oveq2 
 |-  ( Y = .0. -> ( X .x. Y ) = ( X .x. .0. ) )
37 1 2 4 ringrz 
 |-  ( ( R e. Ring /\ X e. B ) -> ( X .x. .0. ) = .0. )
38 5 6 37 syl2anc 
 |-  ( ph -> ( X .x. .0. ) = .0. )
39 36 38 sylan9eqr 
 |-  ( ( ph /\ Y = .0. ) -> ( X .x. Y ) = .0. )
40 39 ex 
 |-  ( ph -> ( Y = .0. -> ( X .x. Y ) = .0. ) )
41 35 40 impbid 
 |-  ( ph -> ( ( X .x. Y ) = .0. <-> Y = .0. ) )