Metamath Proof Explorer

Theorem dpval

Description: Define the value of the decimal point operator. See df-dp . (Contributed by David A. Wheeler, 15-May-2015)

Ref Expression
Assertion dpval 
|- ( ( A e. NN0 /\ B e. RR ) -> ( A . B ) = _ A B )

Proof

Step Hyp Ref Expression
1 df-dp2 
 |-  _ x y = ( x + ( y / ; 1 0 ) )
2 oveq1 
 |-  ( x = A -> ( x + ( y / ; 1 0 ) ) = ( A + ( y / ; 1 0 ) ) )
3 1 2 eqtrid 
 |-  ( x = A -> _ x y = ( A + ( y / ; 1 0 ) ) )
4 oveq1 
 |-  ( y = B -> ( y / ; 1 0 ) = ( B / ; 1 0 ) )
5 4 oveq2d 
 |-  ( y = B -> ( A + ( y / ; 1 0 ) ) = ( A + ( B / ; 1 0 ) ) )
6 df-dp2 
 |-  _ A B = ( A + ( B / ; 1 0 ) )
7 5 6 eqtr4di 
 |-  ( y = B -> ( A + ( y / ; 1 0 ) ) = _ A B )
8 df-dp 
 |-  . = ( x e. NN0 , y e. RR |-> _ x y )
9 6 ovexi 
 |-  _ A B e. _V
10 3 7 8 9 ovmpo 
 |-  ( ( A e. NN0 /\ B e. RR ) -> ( A . B ) = _ A B )