Metamath Proof Explorer

Theorem xrge0mulgnn0

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

Ref Expression
Assertion xrge0mulgnn0 
|- ( ( A e. NN0 /\ B e. ( 0 [,] +oo ) ) -> ( A ( .g ` ( RR*s |`s ( 0 [,] +oo ) ) ) B ) = ( A *e B ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( RR*s |`s ( 0 [,] +oo ) ) = ( RR*s |`s ( 0 [,] +oo ) )
2 iccssxr 
 |-  ( 0 [,] +oo ) C_ RR*
3 xrsbas 
 |-  RR* = ( Base ` RR*s )
4 2 3 sseqtri 
 |-  ( 0 [,] +oo ) C_ ( Base ` RR*s )
5 eqid 
 |-  ( .g ` RR*s ) = ( .g ` RR*s )
6 eqid 
 |-  ( invg ` RR*s ) = ( invg ` RR*s )
7 xrs0 
 |-  0 = ( 0g ` RR*s )
8 xrge00 
 |-  0 = ( 0g ` ( RR*s |`s ( 0 [,] +oo ) ) )
9 7 8 eqtr3i 
 |-  ( 0g ` RR*s ) = ( 0g ` ( RR*s |`s ( 0 [,] +oo ) ) )
10 1 4 5 6 9 ressmulgnn0 
 |-  ( ( A e. NN0 /\ B e. ( 0 [,] +oo ) ) -> ( A ( .g ` ( RR*s |`s ( 0 [,] +oo ) ) ) B ) = ( A ( .g ` RR*s ) B ) )
11 nn0z 
 |-  ( A e. NN0 -> A e. ZZ )
12 eliccxr 
 |-  ( B e. ( 0 [,] +oo ) -> B e. RR* )
13 xrsmulgzz 
 |-  ( ( A e. ZZ /\ B e. RR* ) -> ( A ( .g ` RR*s ) B ) = ( A *e B ) )
14 11 12 13 syl2an 
 |-  ( ( A e. NN0 /\ B e. ( 0 [,] +oo ) ) -> ( A ( .g ` RR*s ) B ) = ( A *e B ) )
15 10 14 eqtrd 
 |-  ( ( A e. NN0 /\ B e. ( 0 [,] +oo ) ) -> ( A ( .g ` ( RR*s |`s ( 0 [,] +oo ) ) ) B ) = ( A *e B ) )