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 ⊢ A ∈ ℤ ∧ B ∈ ℂ → A ⋅ ℂ fld B = A ⁢ B

Proof

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