Metamath Proof Explorer

Theorem dvdsunit

Description: A divisor of a unit is a unit. (Contributed by Mario Carneiro, 18-Apr-2016)

Ref Expression
Hypotheses dvdsunit.1 
|- U = ( Unit ` R )
dvdsunit.3 
|- .|| = ( ||r ` R )
Assertion dvdsunit 
|- ( ( R e. CRing /\ Y .|| X /\ X e. U ) -> Y e. U )

Proof

Step Hyp Ref Expression
1 dvdsunit.1 
 |-  U = ( Unit ` R )
2 dvdsunit.3 
 |-  .|| = ( ||r ` R )
3 crngring 
 |-  ( R e. CRing -> R e. Ring )
4 eqid 
 |-  ( Base ` R ) = ( Base ` R )
5 4 2 dvdsrtr 
 |-  ( ( R e. Ring /\ Y .|| X /\ X .|| ( 1r ` R ) ) -> Y .|| ( 1r ` R ) )
6 5 3expia 
 |-  ( ( R e. Ring /\ Y .|| X ) -> ( X .|| ( 1r ` R ) -> Y .|| ( 1r ` R ) ) )
7 3 6 sylan 
 |-  ( ( R e. CRing /\ Y .|| X ) -> ( X .|| ( 1r ` R ) -> Y .|| ( 1r ` R ) ) )
8 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
9 1 8 2 crngunit 
 |-  ( R e. CRing -> ( X e. U <-> X .|| ( 1r ` R ) ) )
10 9 adantr 
 |-  ( ( R e. CRing /\ Y .|| X ) -> ( X e. U <-> X .|| ( 1r ` R ) ) )
11 1 8 2 crngunit 
 |-  ( R e. CRing -> ( Y e. U <-> Y .|| ( 1r ` R ) ) )
12 11 adantr 
 |-  ( ( R e. CRing /\ Y .|| X ) -> ( Y e. U <-> Y .|| ( 1r ` R ) ) )
13 7 10 12 3imtr4d 
 |-  ( ( R e. CRing /\ Y .|| X ) -> ( X e. U -> Y e. U ) )
14 13 3impia 
 |-  ( ( R e. CRing /\ Y .|| X /\ X e. U ) -> Y e. U )