| Step | Hyp | Ref
| Expression |
| 1 | | oveq1 7438 |
. . . 4
⊢ (𝑥 = 0 → (𝑥(.g‘ℂfld)𝐵) =
(0(.g‘ℂfld)𝐵)) |
| 2 | | oveq1 7438 |
. . . 4
⊢ (𝑥 = 0 → (𝑥 · 𝐵) = (0 · 𝐵)) |
| 3 | 1, 2 | eqeq12d 2753 |
. . 3
⊢ (𝑥 = 0 → ((𝑥(.g‘ℂfld)𝐵) = (𝑥 · 𝐵) ↔
(0(.g‘ℂfld)𝐵) = (0 · 𝐵))) |
| 4 | | oveq1 7438 |
. . . 4
⊢ (𝑥 = 𝑦 → (𝑥(.g‘ℂfld)𝐵) = (𝑦(.g‘ℂfld)𝐵)) |
| 5 | | oveq1 7438 |
. . . 4
⊢ (𝑥 = 𝑦 → (𝑥 · 𝐵) = (𝑦 · 𝐵)) |
| 6 | 4, 5 | eqeq12d 2753 |
. . 3
⊢ (𝑥 = 𝑦 → ((𝑥(.g‘ℂfld)𝐵) = (𝑥 · 𝐵) ↔ (𝑦(.g‘ℂfld)𝐵) = (𝑦 · 𝐵))) |
| 7 | | oveq1 7438 |
. . . 4
⊢ (𝑥 = (𝑦 + 1) → (𝑥(.g‘ℂfld)𝐵) = ((𝑦 +
1)(.g‘ℂfld)𝐵)) |
| 8 | | oveq1 7438 |
. . . 4
⊢ (𝑥 = (𝑦 + 1) → (𝑥 · 𝐵) = ((𝑦 + 1) · 𝐵)) |
| 9 | 7, 8 | eqeq12d 2753 |
. . 3
⊢ (𝑥 = (𝑦 + 1) → ((𝑥(.g‘ℂfld)𝐵) = (𝑥 · 𝐵) ↔ ((𝑦 +
1)(.g‘ℂfld)𝐵) = ((𝑦 + 1) · 𝐵))) |
| 10 | | oveq1 7438 |
. . . 4
⊢ (𝑥 = -𝑦 → (𝑥(.g‘ℂfld)𝐵) = (-𝑦(.g‘ℂfld)𝐵)) |
| 11 | | oveq1 7438 |
. . . 4
⊢ (𝑥 = -𝑦 → (𝑥 · 𝐵) = (-𝑦 · 𝐵)) |
| 12 | 10, 11 | eqeq12d 2753 |
. . 3
⊢ (𝑥 = -𝑦 → ((𝑥(.g‘ℂfld)𝐵) = (𝑥 · 𝐵) ↔ (-𝑦(.g‘ℂfld)𝐵) = (-𝑦 · 𝐵))) |
| 13 | | oveq1 7438 |
. . . 4
⊢ (𝑥 = 𝐴 → (𝑥(.g‘ℂfld)𝐵) = (𝐴(.g‘ℂfld)𝐵)) |
| 14 | | oveq1 7438 |
. . . 4
⊢ (𝑥 = 𝐴 → (𝑥 · 𝐵) = (𝐴 · 𝐵)) |
| 15 | 13, 14 | eqeq12d 2753 |
. . 3
⊢ (𝑥 = 𝐴 → ((𝑥(.g‘ℂfld)𝐵) = (𝑥 · 𝐵) ↔ (𝐴(.g‘ℂfld)𝐵) = (𝐴 · 𝐵))) |
| 16 | | cnfldbas 21368 |
. . . . 5
⊢ ℂ =
(Base‘ℂfld) |
| 17 | | cnfld0 21405 |
. . . . 5
⊢ 0 =
(0g‘ℂfld) |
| 18 | | eqid 2737 |
. . . . 5
⊢
(.g‘ℂfld) =
(.g‘ℂfld) |
| 19 | 16, 17, 18 | mulg0 19092 |
. . . 4
⊢ (𝐵 ∈ ℂ →
(0(.g‘ℂfld)𝐵) = 0) |
| 20 | | mul02 11439 |
. . . 4
⊢ (𝐵 ∈ ℂ → (0
· 𝐵) =
0) |
| 21 | 19, 20 | eqtr4d 2780 |
. . 3
⊢ (𝐵 ∈ ℂ →
(0(.g‘ℂfld)𝐵) = (0 · 𝐵)) |
| 22 | | oveq1 7438 |
. . . . 5
⊢ ((𝑦(.g‘ℂfld)𝐵) = (𝑦 · 𝐵) → ((𝑦(.g‘ℂfld)𝐵) + 𝐵) = ((𝑦 · 𝐵) + 𝐵)) |
| 23 | | cnring 21403 |
. . . . . . . 8
⊢
ℂfld ∈ Ring |
| 24 | | ringmnd 20240 |
. . . . . . . 8
⊢
(ℂfld ∈ Ring → ℂfld ∈
Mnd) |
| 25 | 23, 24 | ax-mp 5 |
. . . . . . 7
⊢
ℂfld ∈ Mnd |
| 26 | | cnfldadd 21370 |
. . . . . . . 8
⊢ + =
(+g‘ℂfld) |
| 27 | 16, 18, 26 | mulgnn0p1 19103 |
. . . . . . 7
⊢
((ℂfld ∈ Mnd ∧ 𝑦 ∈ ℕ0 ∧ 𝐵 ∈ ℂ) → ((𝑦 +
1)(.g‘ℂfld)𝐵) = ((𝑦(.g‘ℂfld)𝐵) + 𝐵)) |
| 28 | 25, 27 | mp3an1 1450 |
. . . . . 6
⊢ ((𝑦 ∈ ℕ0
∧ 𝐵 ∈ ℂ)
→ ((𝑦 +
1)(.g‘ℂfld)𝐵) = ((𝑦(.g‘ℂfld)𝐵) + 𝐵)) |
| 29 | | nn0cn 12536 |
. . . . . . . 8
⊢ (𝑦 ∈ ℕ0
→ 𝑦 ∈
ℂ) |
| 30 | 29 | adantr 480 |
. . . . . . 7
⊢ ((𝑦 ∈ ℕ0
∧ 𝐵 ∈ ℂ)
→ 𝑦 ∈
ℂ) |
| 31 | | simpr 484 |
. . . . . . 7
⊢ ((𝑦 ∈ ℕ0
∧ 𝐵 ∈ ℂ)
→ 𝐵 ∈
ℂ) |
| 32 | 30, 31 | adddirp1d 11287 |
. . . . . 6
⊢ ((𝑦 ∈ ℕ0
∧ 𝐵 ∈ ℂ)
→ ((𝑦 + 1) ·
𝐵) = ((𝑦 · 𝐵) + 𝐵)) |
| 33 | 28, 32 | eqeq12d 2753 |
. . . . 5
⊢ ((𝑦 ∈ ℕ0
∧ 𝐵 ∈ ℂ)
→ (((𝑦 +
1)(.g‘ℂfld)𝐵) = ((𝑦 + 1) · 𝐵) ↔ ((𝑦(.g‘ℂfld)𝐵) + 𝐵) = ((𝑦 · 𝐵) + 𝐵))) |
| 34 | 22, 33 | imbitrrid 246 |
. . . 4
⊢ ((𝑦 ∈ ℕ0
∧ 𝐵 ∈ ℂ)
→ ((𝑦(.g‘ℂfld)𝐵) = (𝑦 · 𝐵) → ((𝑦 +
1)(.g‘ℂfld)𝐵) = ((𝑦 + 1) · 𝐵))) |
| 35 | 34 | expcom 413 |
. . 3
⊢ (𝐵 ∈ ℂ → (𝑦 ∈ ℕ0
→ ((𝑦(.g‘ℂfld)𝐵) = (𝑦 · 𝐵) → ((𝑦 +
1)(.g‘ℂfld)𝐵) = ((𝑦 + 1) · 𝐵)))) |
| 36 | | fveq2 6906 |
. . . . 5
⊢ ((𝑦(.g‘ℂfld)𝐵) = (𝑦 · 𝐵) →
((invg‘ℂfld)‘(𝑦(.g‘ℂfld)𝐵)) =
((invg‘ℂfld)‘(𝑦 · 𝐵))) |
| 37 | | eqid 2737 |
. . . . . . 7
⊢
(invg‘ℂfld) =
(invg‘ℂfld) |
| 38 | 16, 18, 37 | mulgnegnn 19102 |
. . . . . 6
⊢ ((𝑦 ∈ ℕ ∧ 𝐵 ∈ ℂ) → (-𝑦(.g‘ℂfld)𝐵) =
((invg‘ℂfld)‘(𝑦(.g‘ℂfld)𝐵))) |
| 39 | | nncn 12274 |
. . . . . . . 8
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℂ) |
| 40 | | mulneg1 11699 |
. . . . . . . 8
⊢ ((𝑦 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (-𝑦 · 𝐵) = -(𝑦 · 𝐵)) |
| 41 | 39, 40 | sylan 580 |
. . . . . . 7
⊢ ((𝑦 ∈ ℕ ∧ 𝐵 ∈ ℂ) → (-𝑦 · 𝐵) = -(𝑦 · 𝐵)) |
| 42 | | mulcl 11239 |
. . . . . . . . 9
⊢ ((𝑦 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝑦 · 𝐵) ∈ ℂ) |
| 43 | 39, 42 | sylan 580 |
. . . . . . . 8
⊢ ((𝑦 ∈ ℕ ∧ 𝐵 ∈ ℂ) → (𝑦 · 𝐵) ∈ ℂ) |
| 44 | | cnfldneg 21408 |
. . . . . . . 8
⊢ ((𝑦 · 𝐵) ∈ ℂ →
((invg‘ℂfld)‘(𝑦 · 𝐵)) = -(𝑦 · 𝐵)) |
| 45 | 43, 44 | syl 17 |
. . . . . . 7
⊢ ((𝑦 ∈ ℕ ∧ 𝐵 ∈ ℂ) →
((invg‘ℂfld)‘(𝑦 · 𝐵)) = -(𝑦 · 𝐵)) |
| 46 | 41, 45 | eqtr4d 2780 |
. . . . . 6
⊢ ((𝑦 ∈ ℕ ∧ 𝐵 ∈ ℂ) → (-𝑦 · 𝐵) =
((invg‘ℂfld)‘(𝑦 · 𝐵))) |
| 47 | 38, 46 | eqeq12d 2753 |
. . . . 5
⊢ ((𝑦 ∈ ℕ ∧ 𝐵 ∈ ℂ) → ((-𝑦(.g‘ℂfld)𝐵) = (-𝑦 · 𝐵) ↔
((invg‘ℂfld)‘(𝑦(.g‘ℂfld)𝐵)) =
((invg‘ℂfld)‘(𝑦 · 𝐵)))) |
| 48 | 36, 47 | imbitrrid 246 |
. . . 4
⊢ ((𝑦 ∈ ℕ ∧ 𝐵 ∈ ℂ) → ((𝑦(.g‘ℂfld)𝐵) = (𝑦 · 𝐵) → (-𝑦(.g‘ℂfld)𝐵) = (-𝑦 · 𝐵))) |
| 49 | 48 | expcom 413 |
. . 3
⊢ (𝐵 ∈ ℂ → (𝑦 ∈ ℕ → ((𝑦(.g‘ℂfld)𝐵) = (𝑦 · 𝐵) → (-𝑦(.g‘ℂfld)𝐵) = (-𝑦 · 𝐵)))) |
| 50 | 3, 6, 9, 12, 15, 21, 35, 49 | zindd 12719 |
. 2
⊢ (𝐵 ∈ ℂ → (𝐴 ∈ ℤ → (𝐴(.g‘ℂfld)𝐵) = (𝐴 · 𝐵))) |
| 51 | 50 | impcom 407 |
1
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℂ) → (𝐴(.g‘ℂfld)𝐵) = (𝐴 · 𝐵)) |