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

Metamath Proof Explorer

Theorem dvrass

Description: An associative law for division. ( divass analog.) (Contributed by Mario Carneiro, 4-Dec-2014)

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

Proof

Step Hyp Ref Expression
1 dvrass.b 
 |-  B = ( Base ` R )
2 dvrass.o 
 |-  U = ( Unit ` R )
3 dvrass.d 
 |-  ./ = ( /r ` R )
4 dvrass.t 
 |-  .x. = ( .r ` R )
5 simpl 
 |-  ( ( R e. Ring /\ ( X e. B /\ Y e. B /\ Z e. U ) ) -> R e. Ring )
6 simpr1 
 |-  ( ( R e. Ring /\ ( X e. B /\ Y e. B /\ Z e. U ) ) -> X e. B )
7 simpr2 
 |-  ( ( R e. Ring /\ ( X e. B /\ Y e. B /\ Z e. U ) ) -> Y e. B )
8 simpr3 
 |-  ( ( R e. Ring /\ ( X e. B /\ Y e. B /\ Z e. U ) ) -> Z e. U )
9 eqid 
 |-  ( invr ` R ) = ( invr ` R )
10 2 9 1 ringinvcl 
 |-  ( ( R e. Ring /\ Z e. U ) -> ( ( invr ` R ) ` Z ) e. B )
11 5 8 10 syl2anc 
 |-  ( ( R e. Ring /\ ( X e. B /\ Y e. B /\ Z e. U ) ) -> ( ( invr ` R ) ` Z ) e. B )
12 1 4 ringass 
 |-  ( ( R e. Ring /\ ( X e. B /\ Y e. B /\ ( ( invr ` R ) ` Z ) e. B ) ) -> ( ( X .x. Y ) .x. ( ( invr ` R ) ` Z ) ) = ( X .x. ( Y .x. ( ( invr ` R ) ` Z ) ) ) )
13 5 6 7 11 12 syl13anc 
 |-  ( ( R e. Ring /\ ( X e. B /\ Y e. B /\ Z e. U ) ) -> ( ( X .x. Y ) .x. ( ( invr ` R ) ` Z ) ) = ( X .x. ( Y .x. ( ( invr ` R ) ` Z ) ) ) )
14 1 4 ringcl 
 |-  ( ( R e. Ring /\ X e. B /\ Y e. B ) -> ( X .x. Y ) e. B )
15 14 3adant3r3 
 |-  ( ( R e. Ring /\ ( X e. B /\ Y e. B /\ Z e. U ) ) -> ( X .x. Y ) e. B )
16 1 4 2 9 3 dvrval 
 |-  ( ( ( X .x. Y ) e. B /\ Z e. U ) -> ( ( X .x. Y ) ./ Z ) = ( ( X .x. Y ) .x. ( ( invr ` R ) ` Z ) ) )
17 15 8 16 syl2anc 
 |-  ( ( R e. Ring /\ ( X e. B /\ Y e. B /\ Z e. U ) ) -> ( ( X .x. Y ) ./ Z ) = ( ( X .x. Y ) .x. ( ( invr ` R ) ` Z ) ) )
18 1 4 2 9 3 dvrval 
 |-  ( ( Y e. B /\ Z e. U ) -> ( Y ./ Z ) = ( Y .x. ( ( invr ` R ) ` Z ) ) )
19 7 8 18 syl2anc 
 |-  ( ( R e. Ring /\ ( X e. B /\ Y e. B /\ Z e. U ) ) -> ( Y ./ Z ) = ( Y .x. ( ( invr ` R ) ` Z ) ) )
20 19 oveq2d 
 |-  ( ( R e. Ring /\ ( X e. B /\ Y e. B /\ Z e. U ) ) -> ( X .x. ( Y ./ Z ) ) = ( X .x. ( Y .x. ( ( invr ` R ) ` Z ) ) ) )
21 13 17 20 3eqtr4d 
 |-  ( ( R e. Ring /\ ( X e. B /\ Y e. B /\ Z e. U ) ) -> ( ( X .x. Y ) ./ Z ) = ( X .x. ( Y ./ Z ) ) )