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

Metamath Proof Explorer

Theorem dvrcl

Description: Closure of division operation. (Contributed by Mario Carneiro, 2-Jul-2014)

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

Proof

Step Hyp Ref Expression
1 dvrcl.b 
 |-  B = ( Base ` R )
2 dvrcl.o 
 |-  U = ( Unit ` R )
3 dvrcl.d 
 |-  ./ = ( /r ` R )
4 eqid 
 |-  ( .r ` R ) = ( .r ` R )
5 eqid 
 |-  ( invr ` R ) = ( invr ` R )
6 1 4 2 5 3 dvrval 
 |-  ( ( X e. B /\ Y e. U ) -> ( X ./ Y ) = ( X ( .r ` R ) ( ( invr ` R ) ` Y ) ) )
7 6 3adant1 
 |-  ( ( R e. Ring /\ X e. B /\ Y e. U ) -> ( X ./ Y ) = ( X ( .r ` R ) ( ( invr ` R ) ` Y ) ) )
8 2 5 1 ringinvcl 
 |-  ( ( R e. Ring /\ Y e. U ) -> ( ( invr ` R ) ` Y ) e. B )
9 8 3adant2 
 |-  ( ( R e. Ring /\ X e. B /\ Y e. U ) -> ( ( invr ` R ) ` Y ) e. B )
10 1 4 ringcl 
 |-  ( ( R e. Ring /\ X e. B /\ ( ( invr ` R ) ` Y ) e. B ) -> ( X ( .r ` R ) ( ( invr ` R ) ` Y ) ) e. B )
11 9 10 syld3an3 
 |-  ( ( R e. Ring /\ X e. B /\ Y e. U ) -> ( X ( .r ` R ) ( ( invr ` R ) ` Y ) ) e. B )
12 7 11 eqeltrd 
 |-  ( ( R e. Ring /\ X e. B /\ Y e. U ) -> ( X ./ Y ) e. B )