Metamath Proof Explorer

Theorem cnfldmulg

Description: The group multiple function in the field of complex numbers. (Contributed by Mario Carneiro, 14-Jun-2015)

Ref Expression
Assertion cnfldmulg ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 ( .g ‘ ℂfld ) 𝐵 ) = ( 𝐴 · 𝐵 ) )

Proof

Step Hyp Ref Expression
1 oveq1 ⊢ ( 𝑥 = 0 → ( 𝑥 ( .g ‘ ℂfld ) 𝐵 ) = ( 0 ( .g ‘ ℂfld ) 𝐵 ) )
2 oveq1 ⊢ ( 𝑥 = 0 → ( 𝑥 · 𝐵 ) = ( 0 · 𝐵 ) )
3 1 2 eqeq12d ⊢ ( 𝑥 = 0 → ( ( 𝑥 ( .g ‘ ℂfld ) 𝐵 ) = ( 𝑥 · 𝐵 ) ↔ ( 0 ( .g ‘ ℂfld ) 𝐵 ) = ( 0 · 𝐵 ) ) )
4 oveq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ( .g ‘ ℂfld ) 𝐵 ) = ( 𝑦 ( .g ‘ ℂfld ) 𝐵 ) )
5 oveq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 · 𝐵 ) = ( 𝑦 · 𝐵 ) )
6 4 5 eqeq12d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ( .g ‘ ℂfld ) 𝐵 ) = ( 𝑥 · 𝐵 ) ↔ ( 𝑦 ( .g ‘ ℂfld ) 𝐵 ) = ( 𝑦 · 𝐵 ) ) )
7 oveq1 ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( 𝑥 ( .g ‘ ℂfld ) 𝐵 ) = ( ( 𝑦 + 1 ) ( .g ‘ ℂfld ) 𝐵 ) )
8 oveq1 ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( 𝑥 · 𝐵 ) = ( ( 𝑦 + 1 ) · 𝐵 ) )
9 7 8 eqeq12d ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( ( 𝑥 ( .g ‘ ℂfld ) 𝐵 ) = ( 𝑥 · 𝐵 ) ↔ ( ( 𝑦 + 1 ) ( .g ‘ ℂfld ) 𝐵 ) = ( ( 𝑦 + 1 ) · 𝐵 ) ) )
10 oveq1 ⊢ ( 𝑥 = - 𝑦 → ( 𝑥 ( .g ‘ ℂfld ) 𝐵 ) = ( - 𝑦 ( .g ‘ ℂfld ) 𝐵 ) )
11 oveq1 ⊢ ( 𝑥 = - 𝑦 → ( 𝑥 · 𝐵 ) = ( - 𝑦 · 𝐵 ) )
12 10 11 eqeq12d ⊢ ( 𝑥 = - 𝑦 → ( ( 𝑥 ( .g ‘ ℂfld ) 𝐵 ) = ( 𝑥 · 𝐵 ) ↔ ( - 𝑦 ( .g ‘ ℂfld ) 𝐵 ) = ( - 𝑦 · 𝐵 ) ) )
13 oveq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 ( .g ‘ ℂfld ) 𝐵 ) = ( 𝐴 ( .g ‘ ℂfld ) 𝐵 ) )
14 oveq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 · 𝐵 ) = ( 𝐴 · 𝐵 ) )
15 13 14 eqeq12d ⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 ( .g ‘ ℂfld ) 𝐵 ) = ( 𝑥 · 𝐵 ) ↔ ( 𝐴 ( .g ‘ ℂfld ) 𝐵 ) = ( 𝐴 · 𝐵 ) ) )
16 cnfldbas ⊢ ℂ = ( Base ‘ ℂfld )
17 cnfld0 ⊢ 0 = ( 0g ‘ ℂfld )
18 eqid ⊢ ( .g ‘ ℂfld ) = ( .g ‘ ℂfld )
19 16 17 18 mulg0 ⊢ ( 𝐵 ∈ ℂ → ( 0 ( .g ‘ ℂfld ) 𝐵 ) = 0 )
20 mul02 ⊢ ( 𝐵 ∈ ℂ → ( 0 · 𝐵 ) = 0 )
21 19 20 eqtr4d ⊢ ( 𝐵 ∈ ℂ → ( 0 ( .g ‘ ℂfld ) 𝐵 ) = ( 0 · 𝐵 ) )
22 oveq1 ⊢ ( ( 𝑦 ( .g ‘ ℂfld ) 𝐵 ) = ( 𝑦 · 𝐵 ) → ( ( 𝑦 ( .g ‘ ℂfld ) 𝐵 ) + 𝐵 ) = ( ( 𝑦 · 𝐵 ) + 𝐵 ) )
23 cnring ⊢ ℂfld ∈ Ring
24 ringmnd ⊢ ( ℂfld ∈ Ring → ℂfld ∈ Mnd )
25 23 24 ax-mp ⊢ ℂfld ∈ Mnd
26 cnfldadd ⊢ + = ( +g ‘ ℂfld )
27 16 18 26 mulgnn0p1 ⊢ ( ( ℂfld ∈ Mnd ∧ 𝑦 ∈ ℕ0 ∧ 𝐵 ∈ ℂ ) → ( ( 𝑦 + 1 ) ( .g ‘ ℂfld ) 𝐵 ) = ( ( 𝑦 ( .g ‘ ℂfld ) 𝐵 ) + 𝐵 ) )
28 25 27 mp3an1 ⊢ ( ( 𝑦 ∈ ℕ0 ∧ 𝐵 ∈ ℂ ) → ( ( 𝑦 + 1 ) ( .g ‘ ℂfld ) 𝐵 ) = ( ( 𝑦 ( .g ‘ ℂfld ) 𝐵 ) + 𝐵 ) )
29 nn0cn ⊢ ( 𝑦 ∈ ℕ0 → 𝑦 ∈ ℂ )
30 29 adantr ⊢ ( ( 𝑦 ∈ ℕ0 ∧ 𝐵 ∈ ℂ ) → 𝑦 ∈ ℂ )
31 simpr ⊢ ( ( 𝑦 ∈ ℕ0 ∧ 𝐵 ∈ ℂ ) → 𝐵 ∈ ℂ )
32 30 31 adddirp1d ⊢ ( ( 𝑦 ∈ ℕ0 ∧ 𝐵 ∈ ℂ ) → ( ( 𝑦 + 1 ) · 𝐵 ) = ( ( 𝑦 · 𝐵 ) + 𝐵 ) )
33 28 32 eqeq12d ⊢ ( ( 𝑦 ∈ ℕ0 ∧ 𝐵 ∈ ℂ ) → ( ( ( 𝑦 + 1 ) ( .g ‘ ℂfld ) 𝐵 ) = ( ( 𝑦 + 1 ) · 𝐵 ) ↔ ( ( 𝑦 ( .g ‘ ℂfld ) 𝐵 ) + 𝐵 ) = ( ( 𝑦 · 𝐵 ) + 𝐵 ) ) )
34 22 33 syl5ibr ⊢ ( ( 𝑦 ∈ ℕ0 ∧ 𝐵 ∈ ℂ ) → ( ( 𝑦 ( .g ‘ ℂfld ) 𝐵 ) = ( 𝑦 · 𝐵 ) → ( ( 𝑦 + 1 ) ( .g ‘ ℂfld ) 𝐵 ) = ( ( 𝑦 + 1 ) · 𝐵 ) ) )
35 34 expcom ⊢ ( 𝐵 ∈ ℂ → ( 𝑦 ∈ ℕ0 → ( ( 𝑦 ( .g ‘ ℂfld ) 𝐵 ) = ( 𝑦 · 𝐵 ) → ( ( 𝑦 + 1 ) ( .g ‘ ℂfld ) 𝐵 ) = ( ( 𝑦 + 1 ) · 𝐵 ) ) ) )
36 fveq2 ⊢ ( ( 𝑦 ( .g ‘ ℂfld ) 𝐵 ) = ( 𝑦 · 𝐵 ) → ( ( invg ‘ ℂfld ) ‘ ( 𝑦 ( .g ‘ ℂfld ) 𝐵 ) ) = ( ( invg ‘ ℂfld ) ‘ ( 𝑦 · 𝐵 ) ) )
37 eqid ⊢ ( invg ‘ ℂfld ) = ( invg ‘ ℂfld )
38 16 18 37 mulgnegnn ⊢ ( ( 𝑦 ∈ ℕ ∧ 𝐵 ∈ ℂ ) → ( - 𝑦 ( .g ‘ ℂfld ) 𝐵 ) = ( ( invg ‘ ℂfld ) ‘ ( 𝑦 ( .g ‘ ℂfld ) 𝐵 ) ) )
39 nncn ⊢ ( 𝑦 ∈ ℕ → 𝑦 ∈ ℂ )
40 mulneg1 ⊢ ( ( 𝑦 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( - 𝑦 · 𝐵 ) = - ( 𝑦 · 𝐵 ) )
41 39 40 sylan ⊢ ( ( 𝑦 ∈ ℕ ∧ 𝐵 ∈ ℂ ) → ( - 𝑦 · 𝐵 ) = - ( 𝑦 · 𝐵 ) )
42 mulcl ⊢ ( ( 𝑦 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝑦 · 𝐵 ) ∈ ℂ )
43 39 42 sylan ⊢ ( ( 𝑦 ∈ ℕ ∧ 𝐵 ∈ ℂ ) → ( 𝑦 · 𝐵 ) ∈ ℂ )
44 cnfldneg ⊢ ( ( 𝑦 · 𝐵 ) ∈ ℂ → ( ( invg ‘ ℂfld ) ‘ ( 𝑦 · 𝐵 ) ) = - ( 𝑦 · 𝐵 ) )
45 43 44 syl ⊢ ( ( 𝑦 ∈ ℕ ∧ 𝐵 ∈ ℂ ) → ( ( invg ‘ ℂfld ) ‘ ( 𝑦 · 𝐵 ) ) = - ( 𝑦 · 𝐵 ) )
46 41 45 eqtr4d ⊢ ( ( 𝑦 ∈ ℕ ∧ 𝐵 ∈ ℂ ) → ( - 𝑦 · 𝐵 ) = ( ( invg ‘ ℂfld ) ‘ ( 𝑦 · 𝐵 ) ) )
47 38 46 eqeq12d ⊢ ( ( 𝑦 ∈ ℕ ∧ 𝐵 ∈ ℂ ) → ( ( - 𝑦 ( .g ‘ ℂfld ) 𝐵 ) = ( - 𝑦 · 𝐵 ) ↔ ( ( invg ‘ ℂfld ) ‘ ( 𝑦 ( .g ‘ ℂfld ) 𝐵 ) ) = ( ( invg ‘ ℂfld ) ‘ ( 𝑦 · 𝐵 ) ) ) )
48 36 47 syl5ibr ⊢ ( ( 𝑦 ∈ ℕ ∧ 𝐵 ∈ ℂ ) → ( ( 𝑦 ( .g ‘ ℂfld ) 𝐵 ) = ( 𝑦 · 𝐵 ) → ( - 𝑦 ( .g ‘ ℂfld ) 𝐵 ) = ( - 𝑦 · 𝐵 ) ) )
49 48 expcom ⊢ ( 𝐵 ∈ ℂ → ( 𝑦 ∈ ℕ → ( ( 𝑦 ( .g ‘ ℂfld ) 𝐵 ) = ( 𝑦 · 𝐵 ) → ( - 𝑦 ( .g ‘ ℂfld ) 𝐵 ) = ( - 𝑦 · 𝐵 ) ) ) )
50 3 6 9 12 15 21 35 49 zindd ⊢ ( 𝐵 ∈ ℂ → ( 𝐴 ∈ ℤ → ( 𝐴 ( .g ‘ ℂfld ) 𝐵 ) = ( 𝐴 · 𝐵 ) ) )
51 50 impcom ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 ( .g ‘ ℂfld ) 𝐵 ) = ( 𝐴 · 𝐵 ) )