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

Metamath Proof Explorer

Theorem ringunitnzdiv

Description: In a unitary ring, a unit is not a zero divisor. (Contributed by AV, 7-Mar-2025)

Ref Expression
Hypotheses ringunitnzdiv.b 
|- B = ( Base ` R )
ringunitnzdiv.z 
|- .0. = ( 0g ` R )
ringunitnzdiv.t 
|- .x. = ( .r ` R )
ringunitnzdiv.r 
|- ( ph -> R e. Ring )
ringunitnzdiv.y 
|- ( ph -> Y e. B )
ringunitnzdiv.x 
|- ( ph -> X e. ( Unit ` R ) )
Assertion ringunitnzdiv 
|- ( ph -> ( ( X .x. Y ) = .0. <-> Y = .0. ) )

Proof

Step Hyp Ref Expression
1 ringunitnzdiv.b 
 |-  B = ( Base ` R )
2 ringunitnzdiv.z 
 |-  .0. = ( 0g ` R )
3 ringunitnzdiv.t 
 |-  .x. = ( .r ` R )
4 ringunitnzdiv.r 
 |-  ( ph -> R e. Ring )
5 ringunitnzdiv.y 
 |-  ( ph -> Y e. B )
6 ringunitnzdiv.x 
 |-  ( ph -> X e. ( Unit ` R ) )
7 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
8 eqid 
 |-  ( Unit ` R ) = ( Unit ` R )
9 1 8 unitcl 
 |-  ( X e. ( Unit ` R ) -> X e. B )
10 6 9 syl 
 |-  ( ph -> X e. B )
11 eqid 
 |-  ( invr ` R ) = ( invr ` R )
12 8 11 1 ringinvcl 
 |-  ( ( R e. Ring /\ X e. ( Unit ` R ) ) -> ( ( invr ` R ) ` X ) e. B )
13 4 6 12 syl2anc 
 |-  ( ph -> ( ( invr ` R ) ` X ) e. B )
14 oveq1 
 |-  ( e = ( ( invr ` R ) ` X ) -> ( e .x. X ) = ( ( ( invr ` R ) ` X ) .x. X ) )
15 14 eqeq1d 
 |-  ( e = ( ( invr ` R ) ` X ) -> ( ( e .x. X ) = ( 1r ` R ) <-> ( ( ( invr ` R ) ` X ) .x. X ) = ( 1r ` R ) ) )
16 15 adantl 
 |-  ( ( ph /\ e = ( ( invr ` R ) ` X ) ) -> ( ( e .x. X ) = ( 1r ` R ) <-> ( ( ( invr ` R ) ` X ) .x. X ) = ( 1r ` R ) ) )
17 8 11 3 7 unitlinv 
 |-  ( ( R e. Ring /\ X e. ( Unit ` R ) ) -> ( ( ( invr ` R ) ` X ) .x. X ) = ( 1r ` R ) )
18 4 6 17 syl2anc 
 |-  ( ph -> ( ( ( invr ` R ) ` X ) .x. X ) = ( 1r ` R ) )
19 13 16 18 rspcedvd 
 |-  ( ph -> E. e e. B ( e .x. X ) = ( 1r ` R ) )
20 1 3 7 2 4 10 19 5 ringinvnzdiv 
 |-  ( ph -> ( ( X .x. Y ) = .0. <-> Y = .0. ) )