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

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 ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℝ ) → ( 𝐴 . 𝐵 ) = 𝐴 𝐵 )

Proof

Step Hyp Ref Expression
1 df-dp2 ⊢ 𝑥 𝑦 = ( 𝑥 + ( 𝑦 / 1 0 ) )
2 oveq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 + ( 𝑦 / 1 0 ) ) = ( 𝐴 + ( 𝑦 / 1 0 ) ) )
3 1 2 eqtrid ⊢ ( 𝑥 = 𝐴 → 𝑥 𝑦 = ( 𝐴 + ( 𝑦 / 1 0 ) ) )
4 oveq1 ⊢ ( 𝑦 = 𝐵 → ( 𝑦 / 1 0 ) = ( 𝐵 / 1 0 ) )
5 4 oveq2d ⊢ ( 𝑦 = 𝐵 → ( 𝐴 + ( 𝑦 / 1 0 ) ) = ( 𝐴 + ( 𝐵 / 1 0 ) ) )
6 df-dp2 ⊢ 𝐴 𝐵 = ( 𝐴 + ( 𝐵 / 1 0 ) )
7 5 6 eqtr4di ⊢ ( 𝑦 = 𝐵 → ( 𝐴 + ( 𝑦 / 1 0 ) ) = 𝐴 𝐵 )
8 df-dp ⊢ . = ( 𝑥 ∈ ℕ0 , 𝑦 ∈ ℝ ↦ 𝑥 𝑦 )
9 6 ovexi ⊢ 𝐴 𝐵 ∈ V
10 3 7 8 9 ovmpo ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℝ ) → ( 𝐴 . 𝐵 ) = 𝐴 𝐵 )