Step | Hyp | Ref
| Expression |
1 | | oveq1 7278 |
. . . 4
⊢ (𝑥 = 0 → (𝑥(.g‘ℂfld)𝐵) =
(0(.g‘ℂfld)𝐵)) |
2 | | oveq1 7278 |
. . . 4
⊢ (𝑥 = 0 → (𝑥 · 𝐵) = (0 · 𝐵)) |
3 | 1, 2 | eqeq12d 2756 |
. . 3
⊢ (𝑥 = 0 → ((𝑥(.g‘ℂfld)𝐵) = (𝑥 · 𝐵) ↔
(0(.g‘ℂfld)𝐵) = (0 · 𝐵))) |
4 | | oveq1 7278 |
. . . 4
⊢ (𝑥 = 𝑦 → (𝑥(.g‘ℂfld)𝐵) = (𝑦(.g‘ℂfld)𝐵)) |
5 | | oveq1 7278 |
. . . 4
⊢ (𝑥 = 𝑦 → (𝑥 · 𝐵) = (𝑦 · 𝐵)) |
6 | 4, 5 | eqeq12d 2756 |
. . 3
⊢ (𝑥 = 𝑦 → ((𝑥(.g‘ℂfld)𝐵) = (𝑥 · 𝐵) ↔ (𝑦(.g‘ℂfld)𝐵) = (𝑦 · 𝐵))) |
7 | | oveq1 7278 |
. . . 4
⊢ (𝑥 = (𝑦 + 1) → (𝑥(.g‘ℂfld)𝐵) = ((𝑦 +
1)(.g‘ℂfld)𝐵)) |
8 | | oveq1 7278 |
. . . 4
⊢ (𝑥 = (𝑦 + 1) → (𝑥 · 𝐵) = ((𝑦 + 1) · 𝐵)) |
9 | 7, 8 | eqeq12d 2756 |
. . 3
⊢ (𝑥 = (𝑦 + 1) → ((𝑥(.g‘ℂfld)𝐵) = (𝑥 · 𝐵) ↔ ((𝑦 +
1)(.g‘ℂfld)𝐵) = ((𝑦 + 1) · 𝐵))) |
10 | | oveq1 7278 |
. . . 4
⊢ (𝑥 = -𝑦 → (𝑥(.g‘ℂfld)𝐵) = (-𝑦(.g‘ℂfld)𝐵)) |
11 | | oveq1 7278 |
. . . 4
⊢ (𝑥 = -𝑦 → (𝑥 · 𝐵) = (-𝑦 · 𝐵)) |
12 | 10, 11 | eqeq12d 2756 |
. . 3
⊢ (𝑥 = -𝑦 → ((𝑥(.g‘ℂfld)𝐵) = (𝑥 · 𝐵) ↔ (-𝑦(.g‘ℂfld)𝐵) = (-𝑦 · 𝐵))) |
13 | | oveq1 7278 |
. . . 4
⊢ (𝑥 = 𝐴 → (𝑥(.g‘ℂfld)𝐵) = (𝐴(.g‘ℂfld)𝐵)) |
14 | | oveq1 7278 |
. . . 4
⊢ (𝑥 = 𝐴 → (𝑥 · 𝐵) = (𝐴 · 𝐵)) |
15 | 13, 14 | eqeq12d 2756 |
. . 3
⊢ (𝑥 = 𝐴 → ((𝑥(.g‘ℂfld)𝐵) = (𝑥 · 𝐵) ↔ (𝐴(.g‘ℂfld)𝐵) = (𝐴 · 𝐵))) |
16 | | cnfldbas 20599 |
. . . . 5
⊢ ℂ =
(Base‘ℂfld) |
17 | | cnfld0 20620 |
. . . . 5
⊢ 0 =
(0g‘ℂfld) |
18 | | eqid 2740 |
. . . . 5
⊢
(.g‘ℂfld) =
(.g‘ℂfld) |
19 | 16, 17, 18 | mulg0 18705 |
. . . 4
⊢ (𝐵 ∈ ℂ →
(0(.g‘ℂfld)𝐵) = 0) |
20 | | mul02 11153 |
. . . 4
⊢ (𝐵 ∈ ℂ → (0
· 𝐵) =
0) |
21 | 19, 20 | eqtr4d 2783 |
. . 3
⊢ (𝐵 ∈ ℂ →
(0(.g‘ℂfld)𝐵) = (0 · 𝐵)) |
22 | | oveq1 7278 |
. . . . 5
⊢ ((𝑦(.g‘ℂfld)𝐵) = (𝑦 · 𝐵) → ((𝑦(.g‘ℂfld)𝐵) + 𝐵) = ((𝑦 · 𝐵) + 𝐵)) |
23 | | cnring 20618 |
. . . . . . . 8
⊢
ℂfld ∈ Ring |
24 | | ringmnd 19791 |
. . . . . . . 8
⊢
(ℂfld ∈ Ring → ℂfld ∈
Mnd) |
25 | 23, 24 | ax-mp 5 |
. . . . . . 7
⊢
ℂfld ∈ Mnd |
26 | | cnfldadd 20600 |
. . . . . . . 8
⊢ + =
(+g‘ℂfld) |
27 | 16, 18, 26 | mulgnn0p1 18713 |
. . . . . . 7
⊢
((ℂfld ∈ Mnd ∧ 𝑦 ∈ ℕ0 ∧ 𝐵 ∈ ℂ) → ((𝑦 +
1)(.g‘ℂfld)𝐵) = ((𝑦(.g‘ℂfld)𝐵) + 𝐵)) |
28 | 25, 27 | mp3an1 1447 |
. . . . . 6
⊢ ((𝑦 ∈ ℕ0
∧ 𝐵 ∈ ℂ)
→ ((𝑦 +
1)(.g‘ℂfld)𝐵) = ((𝑦(.g‘ℂfld)𝐵) + 𝐵)) |
29 | | nn0cn 12243 |
. . . . . . . 8
⊢ (𝑦 ∈ ℕ0
→ 𝑦 ∈
ℂ) |
30 | 29 | adantr 481 |
. . . . . . 7
⊢ ((𝑦 ∈ ℕ0
∧ 𝐵 ∈ ℂ)
→ 𝑦 ∈
ℂ) |
31 | | simpr 485 |
. . . . . . 7
⊢ ((𝑦 ∈ ℕ0
∧ 𝐵 ∈ ℂ)
→ 𝐵 ∈
ℂ) |
32 | 30, 31 | adddirp1d 11002 |
. . . . . 6
⊢ ((𝑦 ∈ ℕ0
∧ 𝐵 ∈ ℂ)
→ ((𝑦 + 1) ·
𝐵) = ((𝑦 · 𝐵) + 𝐵)) |
33 | 28, 32 | eqeq12d 2756 |
. . . . 5
⊢ ((𝑦 ∈ ℕ0
∧ 𝐵 ∈ ℂ)
→ (((𝑦 +
1)(.g‘ℂfld)𝐵) = ((𝑦 + 1) · 𝐵) ↔ ((𝑦(.g‘ℂfld)𝐵) + 𝐵) = ((𝑦 · 𝐵) + 𝐵))) |
34 | 22, 33 | syl5ibr 245 |
. . . 4
⊢ ((𝑦 ∈ ℕ0
∧ 𝐵 ∈ ℂ)
→ ((𝑦(.g‘ℂfld)𝐵) = (𝑦 · 𝐵) → ((𝑦 +
1)(.g‘ℂfld)𝐵) = ((𝑦 + 1) · 𝐵))) |
35 | 34 | expcom 414 |
. . 3
⊢ (𝐵 ∈ ℂ → (𝑦 ∈ ℕ0
→ ((𝑦(.g‘ℂfld)𝐵) = (𝑦 · 𝐵) → ((𝑦 +
1)(.g‘ℂfld)𝐵) = ((𝑦 + 1) · 𝐵)))) |
36 | | fveq2 6771 |
. . . . 5
⊢ ((𝑦(.g‘ℂfld)𝐵) = (𝑦 · 𝐵) →
((invg‘ℂfld)‘(𝑦(.g‘ℂfld)𝐵)) =
((invg‘ℂfld)‘(𝑦 · 𝐵))) |
37 | | eqid 2740 |
. . . . . . 7
⊢
(invg‘ℂfld) =
(invg‘ℂfld) |
38 | 16, 18, 37 | mulgnegnn 18712 |
. . . . . 6
⊢ ((𝑦 ∈ ℕ ∧ 𝐵 ∈ ℂ) → (-𝑦(.g‘ℂfld)𝐵) =
((invg‘ℂfld)‘(𝑦(.g‘ℂfld)𝐵))) |
39 | | nncn 11981 |
. . . . . . . 8
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℂ) |
40 | | mulneg1 11411 |
. . . . . . . 8
⊢ ((𝑦 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (-𝑦 · 𝐵) = -(𝑦 · 𝐵)) |
41 | 39, 40 | sylan 580 |
. . . . . . 7
⊢ ((𝑦 ∈ ℕ ∧ 𝐵 ∈ ℂ) → (-𝑦 · 𝐵) = -(𝑦 · 𝐵)) |
42 | | mulcl 10956 |
. . . . . . . . 9
⊢ ((𝑦 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝑦 · 𝐵) ∈ ℂ) |
43 | 39, 42 | sylan 580 |
. . . . . . . 8
⊢ ((𝑦 ∈ ℕ ∧ 𝐵 ∈ ℂ) → (𝑦 · 𝐵) ∈ ℂ) |
44 | | cnfldneg 20622 |
. . . . . . . 8
⊢ ((𝑦 · 𝐵) ∈ ℂ →
((invg‘ℂfld)‘(𝑦 · 𝐵)) = -(𝑦 · 𝐵)) |
45 | 43, 44 | syl 17 |
. . . . . . 7
⊢ ((𝑦 ∈ ℕ ∧ 𝐵 ∈ ℂ) →
((invg‘ℂfld)‘(𝑦 · 𝐵)) = -(𝑦 · 𝐵)) |
46 | 41, 45 | eqtr4d 2783 |
. . . . . 6
⊢ ((𝑦 ∈ ℕ ∧ 𝐵 ∈ ℂ) → (-𝑦 · 𝐵) =
((invg‘ℂfld)‘(𝑦 · 𝐵))) |
47 | 38, 46 | eqeq12d 2756 |
. . . . 5
⊢ ((𝑦 ∈ ℕ ∧ 𝐵 ∈ ℂ) → ((-𝑦(.g‘ℂfld)𝐵) = (-𝑦 · 𝐵) ↔
((invg‘ℂfld)‘(𝑦(.g‘ℂfld)𝐵)) =
((invg‘ℂfld)‘(𝑦 · 𝐵)))) |
48 | 36, 47 | syl5ibr 245 |
. . . 4
⊢ ((𝑦 ∈ ℕ ∧ 𝐵 ∈ ℂ) → ((𝑦(.g‘ℂfld)𝐵) = (𝑦 · 𝐵) → (-𝑦(.g‘ℂfld)𝐵) = (-𝑦 · 𝐵))) |
49 | 48 | expcom 414 |
. . 3
⊢ (𝐵 ∈ ℂ → (𝑦 ∈ ℕ → ((𝑦(.g‘ℂfld)𝐵) = (𝑦 · 𝐵) → (-𝑦(.g‘ℂfld)𝐵) = (-𝑦 · 𝐵)))) |
50 | 3, 6, 9, 12, 15, 21, 35, 49 | zindd 12421 |
. 2
⊢ (𝐵 ∈ ℂ → (𝐴 ∈ ℤ → (𝐴(.g‘ℂfld)𝐵) = (𝐴 · 𝐵))) |
51 | 50 | impcom 408 |
1
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℂ) → (𝐴(.g‘ℂfld)𝐵) = (𝐴 · 𝐵)) |