Metamath Proof Explorer

Theorem xrsmulgzz

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

Ref Expression
Assertion xrsmulgzz ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 ( .g ‘ ℝ*𝑠 ) 𝐵 ) = ( 𝐴 ·e 𝐵 ) )

Proof

Step Hyp Ref Expression
1 oveq1 ⊢ ( 𝑛 = 0 → ( 𝑛 ( .g ‘ ℝ*𝑠 ) 𝐵 ) = ( 0 ( .g ‘ ℝ*𝑠 ) 𝐵 ) )
2 oveq1 ⊢ ( 𝑛 = 0 → ( 𝑛 ·e 𝐵 ) = ( 0 ·e 𝐵 ) )
3 1 2 eqeq12d ⊢ ( 𝑛 = 0 → ( ( 𝑛 ( .g ‘ ℝ*𝑠 ) 𝐵 ) = ( 𝑛 ·e 𝐵 ) ↔ ( 0 ( .g ‘ ℝ*𝑠 ) 𝐵 ) = ( 0 ·e 𝐵 ) ) )
4 oveq1 ⊢ ( 𝑛 = 𝑚 → ( 𝑛 ( .g ‘ ℝ*𝑠 ) 𝐵 ) = ( 𝑚 ( .g ‘ ℝ*𝑠 ) 𝐵 ) )
5 oveq1 ⊢ ( 𝑛 = 𝑚 → ( 𝑛 ·e 𝐵 ) = ( 𝑚 ·e 𝐵 ) )
6 4 5 eqeq12d ⊢ ( 𝑛 = 𝑚 → ( ( 𝑛 ( .g ‘ ℝ*𝑠 ) 𝐵 ) = ( 𝑛 ·e 𝐵 ) ↔ ( 𝑚 ( .g ‘ ℝ*𝑠 ) 𝐵 ) = ( 𝑚 ·e 𝐵 ) ) )
7 oveq1 ⊢ ( 𝑛 = ( 𝑚 + 1 ) → ( 𝑛 ( .g ‘ ℝ*𝑠 ) 𝐵 ) = ( ( 𝑚 + 1 ) ( .g ‘ ℝ*𝑠 ) 𝐵 ) )
8 oveq1 ⊢ ( 𝑛 = ( 𝑚 + 1 ) → ( 𝑛 ·e 𝐵 ) = ( ( 𝑚 + 1 ) ·e 𝐵 ) )
9 7 8 eqeq12d ⊢ ( 𝑛 = ( 𝑚 + 1 ) → ( ( 𝑛 ( .g ‘ ℝ*𝑠 ) 𝐵 ) = ( 𝑛 ·e 𝐵 ) ↔ ( ( 𝑚 + 1 ) ( .g ‘ ℝ*𝑠 ) 𝐵 ) = ( ( 𝑚 + 1 ) ·e 𝐵 ) ) )
10 oveq1 ⊢ ( 𝑛 = - 𝑚 → ( 𝑛 ( .g ‘ ℝ*𝑠 ) 𝐵 ) = ( - 𝑚 ( .g ‘ ℝ*𝑠 ) 𝐵 ) )
11 oveq1 ⊢ ( 𝑛 = - 𝑚 → ( 𝑛 ·e 𝐵 ) = ( - 𝑚 ·e 𝐵 ) )
12 10 11 eqeq12d ⊢ ( 𝑛 = - 𝑚 → ( ( 𝑛 ( .g ‘ ℝ*𝑠 ) 𝐵 ) = ( 𝑛 ·e 𝐵 ) ↔ ( - 𝑚 ( .g ‘ ℝ*𝑠 ) 𝐵 ) = ( - 𝑚 ·e 𝐵 ) ) )
13 oveq1 ⊢ ( 𝑛 = 𝐴 → ( 𝑛 ( .g ‘ ℝ*𝑠 ) 𝐵 ) = ( 𝐴 ( .g ‘ ℝ*𝑠 ) 𝐵 ) )
14 oveq1 ⊢ ( 𝑛 = 𝐴 → ( 𝑛 ·e 𝐵 ) = ( 𝐴 ·e 𝐵 ) )
15 13 14 eqeq12d ⊢ ( 𝑛 = 𝐴 → ( ( 𝑛 ( .g ‘ ℝ*𝑠 ) 𝐵 ) = ( 𝑛 ·e 𝐵 ) ↔ ( 𝐴 ( .g ‘ ℝ*𝑠 ) 𝐵 ) = ( 𝐴 ·e 𝐵 ) ) )
16 xrsbas ⊢ ℝ* = ( Base ‘ ℝ*𝑠 )
17 xrs0 ⊢ 0 = ( 0g ‘ ℝ*𝑠 )
18 eqid ⊢ ( .g ‘ ℝ*𝑠 ) = ( .g ‘ ℝ*𝑠 )
19 16 17 18 mulg0 ⊢ ( 𝐵 ∈ ℝ* → ( 0 ( .g ‘ ℝ*𝑠 ) 𝐵 ) = 0 )
20 xmul02 ⊢ ( 𝐵 ∈ ℝ* → ( 0 ·e 𝐵 ) = 0 )
21 19 20 eqtr4d ⊢ ( 𝐵 ∈ ℝ* → ( 0 ( .g ‘ ℝ*𝑠 ) 𝐵 ) = ( 0 ·e 𝐵 ) )
22 simpr ⊢ ( ( ( 𝐵 ∈ ℝ* ∧ 𝑚 ∈ ℕ0 ) ∧ ( 𝑚 ( .g ‘ ℝ*𝑠 ) 𝐵 ) = ( 𝑚 ·e 𝐵 ) ) → ( 𝑚 ( .g ‘ ℝ*𝑠 ) 𝐵 ) = ( 𝑚 ·e 𝐵 ) )
23 22 oveq1d ⊢ ( ( ( 𝐵 ∈ ℝ* ∧ 𝑚 ∈ ℕ0 ) ∧ ( 𝑚 ( .g ‘ ℝ*𝑠 ) 𝐵 ) = ( 𝑚 ·e 𝐵 ) ) → ( ( 𝑚 ( .g ‘ ℝ*𝑠 ) 𝐵 ) +𝑒 𝐵 ) = ( ( 𝑚 ·e 𝐵 ) +𝑒 𝐵 ) )
24 simpr ⊢ ( ( ( 𝐵 ∈ ℝ* ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 ∈ ℕ ) → 𝑚 ∈ ℕ )
25 simpll ⊢ ( ( ( 𝐵 ∈ ℝ* ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 ∈ ℕ ) → 𝐵 ∈ ℝ* )
26 xrsadd ⊢ +𝑒 = ( +g ‘ ℝ*𝑠 )
27 16 18 26 mulgnnp1 ⊢ ( ( 𝑚 ∈ ℕ ∧ 𝐵 ∈ ℝ* ) → ( ( 𝑚 + 1 ) ( .g ‘ ℝ*𝑠 ) 𝐵 ) = ( ( 𝑚 ( .g ‘ ℝ*𝑠 ) 𝐵 ) +𝑒 𝐵 ) )
28 24 25 27 syl2anc ⊢ ( ( ( 𝐵 ∈ ℝ* ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 ∈ ℕ ) → ( ( 𝑚 + 1 ) ( .g ‘ ℝ*𝑠 ) 𝐵 ) = ( ( 𝑚 ( .g ‘ ℝ*𝑠 ) 𝐵 ) +𝑒 𝐵 ) )
29 simpr ⊢ ( ( ( 𝐵 ∈ ℝ* ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 = 0 ) → 𝑚 = 0 )
30 simpll ⊢ ( ( ( 𝐵 ∈ ℝ* ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 = 0 ) → 𝐵 ∈ ℝ* )
31 xaddlid ⊢ ( 𝐵 ∈ ℝ* → ( 0 +𝑒 𝐵 ) = 𝐵 )
32 31 adantl ⊢ ( ( 𝑚 = 0 ∧ 𝐵 ∈ ℝ* ) → ( 0 +𝑒 𝐵 ) = 𝐵 )
33 simpl ⊢ ( ( 𝑚 = 0 ∧ 𝐵 ∈ ℝ* ) → 𝑚 = 0 )
34 33 oveq1d ⊢ ( ( 𝑚 = 0 ∧ 𝐵 ∈ ℝ* ) → ( 𝑚 ( .g ‘ ℝ*𝑠 ) 𝐵 ) = ( 0 ( .g ‘ ℝ*𝑠 ) 𝐵 ) )
35 19 adantl ⊢ ( ( 𝑚 = 0 ∧ 𝐵 ∈ ℝ* ) → ( 0 ( .g ‘ ℝ*𝑠 ) 𝐵 ) = 0 )
36 34 35 eqtrd ⊢ ( ( 𝑚 = 0 ∧ 𝐵 ∈ ℝ* ) → ( 𝑚 ( .g ‘ ℝ*𝑠 ) 𝐵 ) = 0 )
37 36 oveq1d ⊢ ( ( 𝑚 = 0 ∧ 𝐵 ∈ ℝ* ) → ( ( 𝑚 ( .g ‘ ℝ*𝑠 ) 𝐵 ) +𝑒 𝐵 ) = ( 0 +𝑒 𝐵 ) )
38 33 oveq1d ⊢ ( ( 𝑚 = 0 ∧ 𝐵 ∈ ℝ* ) → ( 𝑚 + 1 ) = ( 0 + 1 ) )
39 0p1e1 ⊢ ( 0 + 1 ) = 1
40 38 39 eqtrdi ⊢ ( ( 𝑚 = 0 ∧ 𝐵 ∈ ℝ* ) → ( 𝑚 + 1 ) = 1 )
41 40 oveq1d ⊢ ( ( 𝑚 = 0 ∧ 𝐵 ∈ ℝ* ) → ( ( 𝑚 + 1 ) ( .g ‘ ℝ*𝑠 ) 𝐵 ) = ( 1 ( .g ‘ ℝ*𝑠 ) 𝐵 ) )
42 16 18 mulg1 ⊢ ( 𝐵 ∈ ℝ* → ( 1 ( .g ‘ ℝ*𝑠 ) 𝐵 ) = 𝐵 )
43 42 adantl ⊢ ( ( 𝑚 = 0 ∧ 𝐵 ∈ ℝ* ) → ( 1 ( .g ‘ ℝ*𝑠 ) 𝐵 ) = 𝐵 )
44 41 43 eqtrd ⊢ ( ( 𝑚 = 0 ∧ 𝐵 ∈ ℝ* ) → ( ( 𝑚 + 1 ) ( .g ‘ ℝ*𝑠 ) 𝐵 ) = 𝐵 )
45 32 37 44 3eqtr4rd ⊢ ( ( 𝑚 = 0 ∧ 𝐵 ∈ ℝ* ) → ( ( 𝑚 + 1 ) ( .g ‘ ℝ*𝑠 ) 𝐵 ) = ( ( 𝑚 ( .g ‘ ℝ*𝑠 ) 𝐵 ) +𝑒 𝐵 ) )
46 29 30 45 syl2anc ⊢ ( ( ( 𝐵 ∈ ℝ* ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 = 0 ) → ( ( 𝑚 + 1 ) ( .g ‘ ℝ*𝑠 ) 𝐵 ) = ( ( 𝑚 ( .g ‘ ℝ*𝑠 ) 𝐵 ) +𝑒 𝐵 ) )
47 simpr ⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝑚 ∈ ℕ0 ) → 𝑚 ∈ ℕ0 )
48 elnn0 ⊢ ( 𝑚 ∈ ℕ0 ↔ ( 𝑚 ∈ ℕ ∨ 𝑚 = 0 ) )
49 47 48 sylib ⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝑚 ∈ ℕ0 ) → ( 𝑚 ∈ ℕ ∨ 𝑚 = 0 ) )
50 28 46 49 mpjaodan ⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝑚 ∈ ℕ0 ) → ( ( 𝑚 + 1 ) ( .g ‘ ℝ*𝑠 ) 𝐵 ) = ( ( 𝑚 ( .g ‘ ℝ*𝑠 ) 𝐵 ) +𝑒 𝐵 ) )
51 50 adantr ⊢ ( ( ( 𝐵 ∈ ℝ* ∧ 𝑚 ∈ ℕ0 ) ∧ ( 𝑚 ( .g ‘ ℝ*𝑠 ) 𝐵 ) = ( 𝑚 ·e 𝐵 ) ) → ( ( 𝑚 + 1 ) ( .g ‘ ℝ*𝑠 ) 𝐵 ) = ( ( 𝑚 ( .g ‘ ℝ*𝑠 ) 𝐵 ) +𝑒 𝐵 ) )
52 nn0ssre ⊢ ℕ0 ⊆ ℝ
53 ressxr ⊢ ℝ ⊆ ℝ*
54 52 53 sstri ⊢ ℕ0 ⊆ ℝ*
55 47 adantr ⊢ ( ( ( 𝐵 ∈ ℝ* ∧ 𝑚 ∈ ℕ0 ) ∧ ( 𝑚 ( .g ‘ ℝ*𝑠 ) 𝐵 ) = ( 𝑚 ·e 𝐵 ) ) → 𝑚 ∈ ℕ0 )
56 54 55 sselid ⊢ ( ( ( 𝐵 ∈ ℝ* ∧ 𝑚 ∈ ℕ0 ) ∧ ( 𝑚 ( .g ‘ ℝ*𝑠 ) 𝐵 ) = ( 𝑚 ·e 𝐵 ) ) → 𝑚 ∈ ℝ* )
57 nn0ge0 ⊢ ( 𝑚 ∈ ℕ0 → 0 ≤ 𝑚 )
58 57 ad2antlr ⊢ ( ( ( 𝐵 ∈ ℝ* ∧ 𝑚 ∈ ℕ0 ) ∧ ( 𝑚 ( .g ‘ ℝ*𝑠 ) 𝐵 ) = ( 𝑚 ·e 𝐵 ) ) → 0 ≤ 𝑚 )
59 1xr ⊢ 1 ∈ ℝ*
60 59 a1i ⊢ ( ( ( 𝐵 ∈ ℝ* ∧ 𝑚 ∈ ℕ0 ) ∧ ( 𝑚 ( .g ‘ ℝ*𝑠 ) 𝐵 ) = ( 𝑚 ·e 𝐵 ) ) → 1 ∈ ℝ* )
61 0le1 ⊢ 0 ≤ 1
62 61 a1i ⊢ ( ( ( 𝐵 ∈ ℝ* ∧ 𝑚 ∈ ℕ0 ) ∧ ( 𝑚 ( .g ‘ ℝ*𝑠 ) 𝐵 ) = ( 𝑚 ·e 𝐵 ) ) → 0 ≤ 1 )
63 simpll ⊢ ( ( ( 𝐵 ∈ ℝ* ∧ 𝑚 ∈ ℕ0 ) ∧ ( 𝑚 ( .g ‘ ℝ*𝑠 ) 𝐵 ) = ( 𝑚 ·e 𝐵 ) ) → 𝐵 ∈ ℝ* )
64 xadddi2r ⊢ ( ( ( 𝑚 ∈ ℝ* ∧ 0 ≤ 𝑚 ) ∧ ( 1 ∈ ℝ* ∧ 0 ≤ 1 ) ∧ 𝐵 ∈ ℝ* ) → ( ( 𝑚 +𝑒 1 ) ·e 𝐵 ) = ( ( 𝑚 ·e 𝐵 ) +𝑒 ( 1 ·e 𝐵 ) ) )
65 56 58 60 62 63 64 syl221anc ⊢ ( ( ( 𝐵 ∈ ℝ* ∧ 𝑚 ∈ ℕ0 ) ∧ ( 𝑚 ( .g ‘ ℝ*𝑠 ) 𝐵 ) = ( 𝑚 ·e 𝐵 ) ) → ( ( 𝑚 +𝑒 1 ) ·e 𝐵 ) = ( ( 𝑚 ·e 𝐵 ) +𝑒 ( 1 ·e 𝐵 ) ) )
66 52 55 sselid ⊢ ( ( ( 𝐵 ∈ ℝ* ∧ 𝑚 ∈ ℕ0 ) ∧ ( 𝑚 ( .g ‘ ℝ*𝑠 ) 𝐵 ) = ( 𝑚 ·e 𝐵 ) ) → 𝑚 ∈ ℝ )
67 1re ⊢ 1 ∈ ℝ
68 67 a1i ⊢ ( ( ( 𝐵 ∈ ℝ* ∧ 𝑚 ∈ ℕ0 ) ∧ ( 𝑚 ( .g ‘ ℝ*𝑠 ) 𝐵 ) = ( 𝑚 ·e 𝐵 ) ) → 1 ∈ ℝ )
69 rexadd ⊢ ( ( 𝑚 ∈ ℝ ∧ 1 ∈ ℝ ) → ( 𝑚 +𝑒 1 ) = ( 𝑚 + 1 ) )
70 66 68 69 syl2anc ⊢ ( ( ( 𝐵 ∈ ℝ* ∧ 𝑚 ∈ ℕ0 ) ∧ ( 𝑚 ( .g ‘ ℝ*𝑠 ) 𝐵 ) = ( 𝑚 ·e 𝐵 ) ) → ( 𝑚 +𝑒 1 ) = ( 𝑚 + 1 ) )
71 70 oveq1d ⊢ ( ( ( 𝐵 ∈ ℝ* ∧ 𝑚 ∈ ℕ0 ) ∧ ( 𝑚 ( .g ‘ ℝ*𝑠 ) 𝐵 ) = ( 𝑚 ·e 𝐵 ) ) → ( ( 𝑚 +𝑒 1 ) ·e 𝐵 ) = ( ( 𝑚 + 1 ) ·e 𝐵 ) )
72 xmullid ⊢ ( 𝐵 ∈ ℝ* → ( 1 ·e 𝐵 ) = 𝐵 )
73 63 72 syl ⊢ ( ( ( 𝐵 ∈ ℝ* ∧ 𝑚 ∈ ℕ0 ) ∧ ( 𝑚 ( .g ‘ ℝ*𝑠 ) 𝐵 ) = ( 𝑚 ·e 𝐵 ) ) → ( 1 ·e 𝐵 ) = 𝐵 )
74 73 oveq2d ⊢ ( ( ( 𝐵 ∈ ℝ* ∧ 𝑚 ∈ ℕ0 ) ∧ ( 𝑚 ( .g ‘ ℝ*𝑠 ) 𝐵 ) = ( 𝑚 ·e 𝐵 ) ) → ( ( 𝑚 ·e 𝐵 ) +𝑒 ( 1 ·e 𝐵 ) ) = ( ( 𝑚 ·e 𝐵 ) +𝑒 𝐵 ) )
75 65 71 74 3eqtr3d ⊢ ( ( ( 𝐵 ∈ ℝ* ∧ 𝑚 ∈ ℕ0 ) ∧ ( 𝑚 ( .g ‘ ℝ*𝑠 ) 𝐵 ) = ( 𝑚 ·e 𝐵 ) ) → ( ( 𝑚 + 1 ) ·e 𝐵 ) = ( ( 𝑚 ·e 𝐵 ) +𝑒 𝐵 ) )
76 23 51 75 3eqtr4d ⊢ ( ( ( 𝐵 ∈ ℝ* ∧ 𝑚 ∈ ℕ0 ) ∧ ( 𝑚 ( .g ‘ ℝ*𝑠 ) 𝐵 ) = ( 𝑚 ·e 𝐵 ) ) → ( ( 𝑚 + 1 ) ( .g ‘ ℝ*𝑠 ) 𝐵 ) = ( ( 𝑚 + 1 ) ·e 𝐵 ) )
77 76 exp31 ⊢ ( 𝐵 ∈ ℝ* → ( 𝑚 ∈ ℕ0 → ( ( 𝑚 ( .g ‘ ℝ*𝑠 ) 𝐵 ) = ( 𝑚 ·e 𝐵 ) → ( ( 𝑚 + 1 ) ( .g ‘ ℝ*𝑠 ) 𝐵 ) = ( ( 𝑚 + 1 ) ·e 𝐵 ) ) ) )
78 xnegeq ⊢ ( ( 𝑚 ( .g ‘ ℝ*𝑠 ) 𝐵 ) = ( 𝑚 ·e 𝐵 ) → -𝑒 ( 𝑚 ( .g ‘ ℝ*𝑠 ) 𝐵 ) = -𝑒 ( 𝑚 ·e 𝐵 ) )
79 78 adantl ⊢ ( ( ( 𝐵 ∈ ℝ* ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑚 ( .g ‘ ℝ*𝑠 ) 𝐵 ) = ( 𝑚 ·e 𝐵 ) ) → -𝑒 ( 𝑚 ( .g ‘ ℝ*𝑠 ) 𝐵 ) = -𝑒 ( 𝑚 ·e 𝐵 ) )
80 eqid ⊢ ( invg ‘ ℝ*𝑠 ) = ( invg ‘ ℝ*𝑠 )
81 16 18 80 mulgnegnn ⊢ ( ( 𝑚 ∈ ℕ ∧ 𝐵 ∈ ℝ* ) → ( - 𝑚 ( .g ‘ ℝ*𝑠 ) 𝐵 ) = ( ( invg ‘ ℝ*𝑠 ) ‘ ( 𝑚 ( .g ‘ ℝ*𝑠 ) 𝐵 ) ) )
82 81 ancoms ⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝑚 ∈ ℕ ) → ( - 𝑚 ( .g ‘ ℝ*𝑠 ) 𝐵 ) = ( ( invg ‘ ℝ*𝑠 ) ‘ ( 𝑚 ( .g ‘ ℝ*𝑠 ) 𝐵 ) ) )
83 xrsex ⊢ ℝ*𝑠 ∈ V
84 83 a1i ⊢ ( 𝑚 ∈ ℕ → ℝ*𝑠 ∈ V )
85 ssidd ⊢ ( 𝑚 ∈ ℕ → ℝ* ⊆ ℝ* )
86 simp2 ⊢ ( ( 𝑚 ∈ ℕ ∧ 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) → 𝑥 ∈ ℝ* )
87 simp3 ⊢ ( ( 𝑚 ∈ ℕ ∧ 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) → 𝑦 ∈ ℝ* )
88 86 87 xaddcld ⊢ ( ( 𝑚 ∈ ℕ ∧ 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) → ( 𝑥 +𝑒 𝑦 ) ∈ ℝ* )
89 16 18 26 84 85 88 mulgnnsubcl ⊢ ( ( 𝑚 ∈ ℕ ∧ 𝑚 ∈ ℕ ∧ 𝐵 ∈ ℝ* ) → ( 𝑚 ( .g ‘ ℝ*𝑠 ) 𝐵 ) ∈ ℝ* )
90 89 3anidm12 ⊢ ( ( 𝑚 ∈ ℕ ∧ 𝐵 ∈ ℝ* ) → ( 𝑚 ( .g ‘ ℝ*𝑠 ) 𝐵 ) ∈ ℝ* )
91 90 ancoms ⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝑚 ∈ ℕ ) → ( 𝑚 ( .g ‘ ℝ*𝑠 ) 𝐵 ) ∈ ℝ* )
92 xrsinvgval ⊢ ( ( 𝑚 ( .g ‘ ℝ*𝑠 ) 𝐵 ) ∈ ℝ* → ( ( invg ‘ ℝ*𝑠 ) ‘ ( 𝑚 ( .g ‘ ℝ*𝑠 ) 𝐵 ) ) = -𝑒 ( 𝑚 ( .g ‘ ℝ*𝑠 ) 𝐵 ) )
93 91 92 syl ⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝑚 ∈ ℕ ) → ( ( invg ‘ ℝ*𝑠 ) ‘ ( 𝑚 ( .g ‘ ℝ*𝑠 ) 𝐵 ) ) = -𝑒 ( 𝑚 ( .g ‘ ℝ*𝑠 ) 𝐵 ) )
94 82 93 eqtrd ⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝑚 ∈ ℕ ) → ( - 𝑚 ( .g ‘ ℝ*𝑠 ) 𝐵 ) = -𝑒 ( 𝑚 ( .g ‘ ℝ*𝑠 ) 𝐵 ) )
95 94 adantr ⊢ ( ( ( 𝐵 ∈ ℝ* ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑚 ( .g ‘ ℝ*𝑠 ) 𝐵 ) = ( 𝑚 ·e 𝐵 ) ) → ( - 𝑚 ( .g ‘ ℝ*𝑠 ) 𝐵 ) = -𝑒 ( 𝑚 ( .g ‘ ℝ*𝑠 ) 𝐵 ) )
96 nnre ⊢ ( 𝑚 ∈ ℕ → 𝑚 ∈ ℝ )
97 96 adantl ⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝑚 ∈ ℕ ) → 𝑚 ∈ ℝ )
98 rexneg ⊢ ( 𝑚 ∈ ℝ → -𝑒 𝑚 = - 𝑚 )
99 97 98 syl ⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝑚 ∈ ℕ ) → -𝑒 𝑚 = - 𝑚 )
100 99 oveq1d ⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝑚 ∈ ℕ ) → ( -𝑒 𝑚 ·e 𝐵 ) = ( - 𝑚 ·e 𝐵 ) )
101 nnssre ⊢ ℕ ⊆ ℝ
102 101 53 sstri ⊢ ℕ ⊆ ℝ*
103 simpr ⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝑚 ∈ ℕ ) → 𝑚 ∈ ℕ )
104 102 103 sselid ⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝑚 ∈ ℕ ) → 𝑚 ∈ ℝ* )
105 simpl ⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝑚 ∈ ℕ ) → 𝐵 ∈ ℝ* )
106 xmulneg1 ⊢ ( ( 𝑚 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( -𝑒 𝑚 ·e 𝐵 ) = -𝑒 ( 𝑚 ·e 𝐵 ) )
107 104 105 106 syl2anc ⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝑚 ∈ ℕ ) → ( -𝑒 𝑚 ·e 𝐵 ) = -𝑒 ( 𝑚 ·e 𝐵 ) )
108 100 107 eqtr3d ⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝑚 ∈ ℕ ) → ( - 𝑚 ·e 𝐵 ) = -𝑒 ( 𝑚 ·e 𝐵 ) )
109 108 adantr ⊢ ( ( ( 𝐵 ∈ ℝ* ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑚 ( .g ‘ ℝ*𝑠 ) 𝐵 ) = ( 𝑚 ·e 𝐵 ) ) → ( - 𝑚 ·e 𝐵 ) = -𝑒 ( 𝑚 ·e 𝐵 ) )
110 79 95 109 3eqtr4d ⊢ ( ( ( 𝐵 ∈ ℝ* ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑚 ( .g ‘ ℝ*𝑠 ) 𝐵 ) = ( 𝑚 ·e 𝐵 ) ) → ( - 𝑚 ( .g ‘ ℝ*𝑠 ) 𝐵 ) = ( - 𝑚 ·e 𝐵 ) )
111 110 exp31 ⊢ ( 𝐵 ∈ ℝ* → ( 𝑚 ∈ ℕ → ( ( 𝑚 ( .g ‘ ℝ*𝑠 ) 𝐵 ) = ( 𝑚 ·e 𝐵 ) → ( - 𝑚 ( .g ‘ ℝ*𝑠 ) 𝐵 ) = ( - 𝑚 ·e 𝐵 ) ) ) )
112 3 6 9 12 15 21 77 111 zindd ⊢ ( 𝐵 ∈ ℝ* → ( 𝐴 ∈ ℤ → ( 𝐴 ( .g ‘ ℝ*𝑠 ) 𝐵 ) = ( 𝐴 ·e 𝐵 ) ) )
113 112 impcom ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 ( .g ‘ ℝ*𝑠 ) 𝐵 ) = ( 𝐴 ·e 𝐵 ) )