Theorem xrge0mulgnn0

Description: The group multiple function in the extended nonnegative real numbers. (Contributed by Thierry Arnoux, 14-Jun-2017)

	Ref	Expression
Assertion	xrge0mulgnn0	⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ( 0 [,] +∞ ) ) → ( 𝐴 ( .g ‘ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ) 𝐵 ) = ( 𝐴 ·e 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) = ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) )
2		iccssxr	⊢ ( 0 [,] +∞ ) ⊆ ℝ*
3		xrsbas	⊢ ℝ* = ( Base ‘ ℝ*𝑠 )
4	2 3	sseqtri	⊢ ( 0 [,] +∞ ) ⊆ ( Base ‘ ℝ*𝑠 )
5		eqid	⊢ ( .g ‘ ℝ*𝑠 ) = ( .g ‘ ℝ*𝑠 )
6		eqid	⊢ ( invg ‘ ℝ*𝑠 ) = ( invg ‘ ℝ*𝑠 )
7		xrs0	⊢ 0 = ( 0g ‘ ℝ*𝑠 )
8		xrge00	⊢ 0 = ( 0g ‘ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) )
9	7 8	eqtr3i	⊢ ( 0g ‘ ℝ*𝑠 ) = ( 0g ‘ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) )
10	1 4 5 6 9	ressmulgnn0	⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ( 0 [,] +∞ ) ) → ( 𝐴 ( .g ‘ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ) 𝐵 ) = ( 𝐴 ( .g ‘ ℝ*𝑠 ) 𝐵 ) )
11		nn0z	⊢ ( 𝐴 ∈ ℕ0 → 𝐴 ∈ ℤ )
12		eliccxr	⊢ ( 𝐵 ∈ ( 0 [,] +∞ ) → 𝐵 ∈ ℝ* )
13		xrsmulgzz	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 ( .g ‘ ℝ*𝑠 ) 𝐵 ) = ( 𝐴 ·e 𝐵 ) )
14	11 12 13	syl2an	⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ( 0 [,] +∞ ) ) → ( 𝐴 ( .g ‘ ℝ*𝑠 ) 𝐵 ) = ( 𝐴 ·e 𝐵 ) )
15	10 14	eqtrd	⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ( 0 [,] +∞ ) ) → ( 𝐴 ( .g ‘ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ) 𝐵 ) = ( 𝐴 ·e 𝐵 ) )