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

Metamath Proof Explorer

Theorem dvrfval

Description: Division operation in a ring. (Contributed by Mario Carneiro, 2-Jul-2014) (Revised by Mario Carneiro, 2-Dec-2014) (Proof shortened by AV, 2-Mar-2024)

Ref Expression
Hypotheses dvrval.b 
|- B = ( Base ` R )
dvrval.t 
|- .x. = ( .r ` R )
dvrval.u 
|- U = ( Unit ` R )
dvrval.i 
|- I = ( invr ` R )
dvrval.d 
|- ./ = ( /r ` R )
Assertion dvrfval 
|- ./ = ( x e. B , y e. U |-> ( x .x. ( I ` y ) ) )

Proof

Step Hyp Ref Expression
1 dvrval.b 
 |-  B = ( Base ` R )
2 dvrval.t 
 |-  .x. = ( .r ` R )
3 dvrval.u 
 |-  U = ( Unit ` R )
4 dvrval.i 
 |-  I = ( invr ` R )
5 dvrval.d 
 |-  ./ = ( /r ` R )
6 fveq2 
 |-  ( r = R -> ( Base ` r ) = ( Base ` R ) )
7 6 1 eqtr4di 
 |-  ( r = R -> ( Base ` r ) = B )
8 fveq2 
 |-  ( r = R -> ( Unit ` r ) = ( Unit ` R ) )
9 8 3 eqtr4di 
 |-  ( r = R -> ( Unit ` r ) = U )
10 fveq2 
 |-  ( r = R -> ( .r ` r ) = ( .r ` R ) )
11 10 2 eqtr4di 
 |-  ( r = R -> ( .r ` r ) = .x. )
12 eqidd 
 |-  ( r = R -> x = x )
13 fveq2 
 |-  ( r = R -> ( invr ` r ) = ( invr ` R ) )
14 13 4 eqtr4di 
 |-  ( r = R -> ( invr ` r ) = I )
15 14 fveq1d 
 |-  ( r = R -> ( ( invr ` r ) ` y ) = ( I ` y ) )
16 11 12 15 oveq123d 
 |-  ( r = R -> ( x ( .r ` r ) ( ( invr ` r ) ` y ) ) = ( x .x. ( I ` y ) ) )
17 7 9 16 mpoeq123dv 
 |-  ( r = R -> ( x e. ( Base ` r ) , y e. ( Unit ` r ) |-> ( x ( .r ` r ) ( ( invr ` r ) ` y ) ) ) = ( x e. B , y e. U |-> ( x .x. ( I ` y ) ) ) )
18 df-dvr 
 |-  /r = ( r e. _V |-> ( x e. ( Base ` r ) , y e. ( Unit ` r ) |-> ( x ( .r ` r ) ( ( invr ` r ) ` y ) ) ) )
19 1 fvexi 
 |-  B e. _V
20 3 fvexi 
 |-  U e. _V
21 19 20 mpoex 
 |-  ( x e. B , y e. U |-> ( x .x. ( I ` y ) ) ) e. _V
22 17 18 21 fvmpt 
 |-  ( R e. _V -> ( /r ` R ) = ( x e. B , y e. U |-> ( x .x. ( I ` y ) ) ) )
23 fvprc 
 |-  ( -. R e. _V -> ( /r ` R ) = (/) )
24 fvprc 
 |-  ( -. R e. _V -> ( Base ` R ) = (/) )
25 1 24 eqtrid 
 |-  ( -. R e. _V -> B = (/) )
26 25 orcd 
 |-  ( -. R e. _V -> ( B = (/) \/ U = (/) ) )
27 0mpo0 
 |-  ( ( B = (/) \/ U = (/) ) -> ( x e. B , y e. U |-> ( x .x. ( I ` y ) ) ) = (/) )
28 26 27 syl 
 |-  ( -. R e. _V -> ( x e. B , y e. U |-> ( x .x. ( I ` y ) ) ) = (/) )
29 23 28 eqtr4d 
 |-  ( -. R e. _V -> ( /r ` R ) = ( x e. B , y e. U |-> ( x .x. ( I ` y ) ) ) )
30 22 29 pm2.61i 
 |-  ( /r ` R ) = ( x e. B , y e. U |-> ( x .x. ( I ` y ) ) )
31 5 30 eqtri 
 |-  ./ = ( x e. B , y e. U |-> ( x .x. ( I ` y ) ) )