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