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