Metamath Proof Explorer

Theorem unitdvcl

Description: The units are closed under division. (Contributed by Mario Carneiro, 2-Jul-2014)

Ref Expression
Hypotheses unitdvcl.o 
|- U = ( Unit ` R )
unitdvcl.d 
|- ./ = ( /r ` R )
Assertion unitdvcl 
|- ( ( R e. Ring /\ X e. U /\ Y e. U ) -> ( X ./ Y ) e. U )

Proof

Step Hyp Ref Expression
1 unitdvcl.o 
 |-  U = ( Unit ` R )
2 unitdvcl.d 
 |-  ./ = ( /r ` R )
3 eqid 
 |-  ( Base ` R ) = ( Base ` R )
4 3 1 unitcl 
 |-  ( X e. U -> X e. ( Base ` R ) )
5 eqid 
 |-  ( .r ` R ) = ( .r ` R )
6 eqid 
 |-  ( invr ` R ) = ( invr ` R )
7 3 5 1 6 2 dvrval 
 |-  ( ( X e. ( Base ` R ) /\ Y e. U ) -> ( X ./ Y ) = ( X ( .r ` R ) ( ( invr ` R ) ` Y ) ) )
8 4 7 sylan 
 |-  ( ( X e. U /\ Y e. U ) -> ( X ./ Y ) = ( X ( .r ` R ) ( ( invr ` R ) ` Y ) ) )
9 8 3adant1 
 |-  ( ( R e. Ring /\ X e. U /\ Y e. U ) -> ( X ./ Y ) = ( X ( .r ` R ) ( ( invr ` R ) ` Y ) ) )
10 1 6 unitinvcl 
 |-  ( ( R e. Ring /\ Y e. U ) -> ( ( invr ` R ) ` Y ) e. U )
11 10 3adant2 
 |-  ( ( R e. Ring /\ X e. U /\ Y e. U ) -> ( ( invr ` R ) ` Y ) e. U )
12 1 5 unitmulcl 
 |-  ( ( R e. Ring /\ X e. U /\ ( ( invr ` R ) ` Y ) e. U ) -> ( X ( .r ` R ) ( ( invr ` R ) ` Y ) ) e. U )
13 11 12 syld3an3 
 |-  ( ( R e. Ring /\ X e. U /\ Y e. U ) -> ( X ( .r ` R ) ( ( invr ` R ) ` Y ) ) e. U )
14 9 13 eqeltrd 
 |-  ( ( R e. Ring /\ X e. U /\ Y e. U ) -> ( X ./ Y ) e. U )