| Step | Hyp | Ref
| Expression |
| 1 | | expcl 14120 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℕ0)
→ (𝐴↑𝑥) ∈
ℂ) |
| 2 | 1 | fmpttd 7135 |
. 2
⊢ (𝐴 ∈ ℂ → (𝑥 ∈ ℕ0
↦ (𝐴↑𝑥)):ℕ0⟶ℂ) |
| 3 | | expadd 14145 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℕ0
∧ 𝑧 ∈
ℕ0) → (𝐴↑(𝑦 + 𝑧)) = ((𝐴↑𝑦) · (𝐴↑𝑧))) |
| 4 | 3 | 3expb 1121 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℕ0
∧ 𝑧 ∈
ℕ0)) → (𝐴↑(𝑦 + 𝑧)) = ((𝐴↑𝑦) · (𝐴↑𝑧))) |
| 5 | | nn0addcl 12561 |
. . . . . 6
⊢ ((𝑦 ∈ ℕ0
∧ 𝑧 ∈
ℕ0) → (𝑦 + 𝑧) ∈
ℕ0) |
| 6 | 5 | adantl 481 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℕ0
∧ 𝑧 ∈
ℕ0)) → (𝑦 + 𝑧) ∈
ℕ0) |
| 7 | | oveq2 7439 |
. . . . . 6
⊢ (𝑥 = (𝑦 + 𝑧) → (𝐴↑𝑥) = (𝐴↑(𝑦 + 𝑧))) |
| 8 | | eqid 2737 |
. . . . . 6
⊢ (𝑥 ∈ ℕ0
↦ (𝐴↑𝑥)) = (𝑥 ∈ ℕ0 ↦ (𝐴↑𝑥)) |
| 9 | | ovex 7464 |
. . . . . 6
⊢ (𝐴↑(𝑦 + 𝑧)) ∈ V |
| 10 | 7, 8, 9 | fvmpt 7016 |
. . . . 5
⊢ ((𝑦 + 𝑧) ∈ ℕ0 → ((𝑥 ∈ ℕ0
↦ (𝐴↑𝑥))‘(𝑦 + 𝑧)) = (𝐴↑(𝑦 + 𝑧))) |
| 11 | 6, 10 | syl 17 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℕ0
∧ 𝑧 ∈
ℕ0)) → ((𝑥 ∈ ℕ0 ↦ (𝐴↑𝑥))‘(𝑦 + 𝑧)) = (𝐴↑(𝑦 + 𝑧))) |
| 12 | | oveq2 7439 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (𝐴↑𝑥) = (𝐴↑𝑦)) |
| 13 | | ovex 7464 |
. . . . . . 7
⊢ (𝐴↑𝑦) ∈ V |
| 14 | 12, 8, 13 | fvmpt 7016 |
. . . . . 6
⊢ (𝑦 ∈ ℕ0
→ ((𝑥 ∈
ℕ0 ↦ (𝐴↑𝑥))‘𝑦) = (𝐴↑𝑦)) |
| 15 | | oveq2 7439 |
. . . . . . 7
⊢ (𝑥 = 𝑧 → (𝐴↑𝑥) = (𝐴↑𝑧)) |
| 16 | | ovex 7464 |
. . . . . . 7
⊢ (𝐴↑𝑧) ∈ V |
| 17 | 15, 8, 16 | fvmpt 7016 |
. . . . . 6
⊢ (𝑧 ∈ ℕ0
→ ((𝑥 ∈
ℕ0 ↦ (𝐴↑𝑥))‘𝑧) = (𝐴↑𝑧)) |
| 18 | 14, 17 | oveqan12d 7450 |
. . . . 5
⊢ ((𝑦 ∈ ℕ0
∧ 𝑧 ∈
ℕ0) → (((𝑥 ∈ ℕ0 ↦ (𝐴↑𝑥))‘𝑦) · ((𝑥 ∈ ℕ0 ↦ (𝐴↑𝑥))‘𝑧)) = ((𝐴↑𝑦) · (𝐴↑𝑧))) |
| 19 | 18 | adantl 481 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℕ0
∧ 𝑧 ∈
ℕ0)) → (((𝑥 ∈ ℕ0 ↦ (𝐴↑𝑥))‘𝑦) · ((𝑥 ∈ ℕ0 ↦ (𝐴↑𝑥))‘𝑧)) = ((𝐴↑𝑦) · (𝐴↑𝑧))) |
| 20 | 4, 11, 19 | 3eqtr4d 2787 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℕ0
∧ 𝑧 ∈
ℕ0)) → ((𝑥 ∈ ℕ0 ↦ (𝐴↑𝑥))‘(𝑦 + 𝑧)) = (((𝑥 ∈ ℕ0 ↦ (𝐴↑𝑥))‘𝑦) · ((𝑥 ∈ ℕ0 ↦ (𝐴↑𝑥))‘𝑧))) |
| 21 | 20 | ralrimivva 3202 |
. 2
⊢ (𝐴 ∈ ℂ →
∀𝑦 ∈
ℕ0 ∀𝑧 ∈ ℕ0 ((𝑥 ∈ ℕ0
↦ (𝐴↑𝑥))‘(𝑦 + 𝑧)) = (((𝑥 ∈ ℕ0 ↦ (𝐴↑𝑥))‘𝑦) · ((𝑥 ∈ ℕ0 ↦ (𝐴↑𝑥))‘𝑧))) |
| 22 | | 0nn0 12541 |
. . . 4
⊢ 0 ∈
ℕ0 |
| 23 | | oveq2 7439 |
. . . . 5
⊢ (𝑥 = 0 → (𝐴↑𝑥) = (𝐴↑0)) |
| 24 | | ovex 7464 |
. . . . 5
⊢ (𝐴↑0) ∈
V |
| 25 | 23, 8, 24 | fvmpt 7016 |
. . . 4
⊢ (0 ∈
ℕ0 → ((𝑥 ∈ ℕ0 ↦ (𝐴↑𝑥))‘0) = (𝐴↑0)) |
| 26 | 22, 25 | ax-mp 5 |
. . 3
⊢ ((𝑥 ∈ ℕ0
↦ (𝐴↑𝑥))‘0) = (𝐴↑0) |
| 27 | | exp0 14106 |
. . 3
⊢ (𝐴 ∈ ℂ → (𝐴↑0) = 1) |
| 28 | 26, 27 | eqtrid 2789 |
. 2
⊢ (𝐴 ∈ ℂ → ((𝑥 ∈ ℕ0
↦ (𝐴↑𝑥))‘0) =
1) |
| 29 | | nn0subm 21440 |
. . . . 5
⊢
ℕ0 ∈
(SubMnd‘ℂfld) |
| 30 | | expmhm.1 |
. . . . . 6
⊢ 𝑁 = (ℂfld
↾s ℕ0) |
| 31 | 30 | submmnd 18826 |
. . . . 5
⊢
(ℕ0 ∈ (SubMnd‘ℂfld) →
𝑁 ∈
Mnd) |
| 32 | 29, 31 | ax-mp 5 |
. . . 4
⊢ 𝑁 ∈ Mnd |
| 33 | | cnring 21403 |
. . . . 5
⊢
ℂfld ∈ Ring |
| 34 | | expmhm.2 |
. . . . . 6
⊢ 𝑀 =
(mulGrp‘ℂfld) |
| 35 | 34 | ringmgp 20236 |
. . . . 5
⊢
(ℂfld ∈ Ring → 𝑀 ∈ Mnd) |
| 36 | 33, 35 | ax-mp 5 |
. . . 4
⊢ 𝑀 ∈ Mnd |
| 37 | 32, 36 | pm3.2i 470 |
. . 3
⊢ (𝑁 ∈ Mnd ∧ 𝑀 ∈ Mnd) |
| 38 | 30 | submbas 18827 |
. . . . 5
⊢
(ℕ0 ∈ (SubMnd‘ℂfld) →
ℕ0 = (Base‘𝑁)) |
| 39 | 29, 38 | ax-mp 5 |
. . . 4
⊢
ℕ0 = (Base‘𝑁) |
| 40 | | cnfldbas 21368 |
. . . . 5
⊢ ℂ =
(Base‘ℂfld) |
| 41 | 34, 40 | mgpbas 20142 |
. . . 4
⊢ ℂ =
(Base‘𝑀) |
| 42 | | cnfldadd 21370 |
. . . . . 6
⊢ + =
(+g‘ℂfld) |
| 43 | 30, 42 | ressplusg 17334 |
. . . . 5
⊢
(ℕ0 ∈ (SubMnd‘ℂfld) →
+ = (+g‘𝑁)) |
| 44 | 29, 43 | ax-mp 5 |
. . . 4
⊢ + =
(+g‘𝑁) |
| 45 | | cnfldmul 21372 |
. . . . 5
⊢ ·
= (.r‘ℂfld) |
| 46 | 34, 45 | mgpplusg 20141 |
. . . 4
⊢ ·
= (+g‘𝑀) |
| 47 | | cnfld0 21405 |
. . . . . 6
⊢ 0 =
(0g‘ℂfld) |
| 48 | 30, 47 | subm0 18828 |
. . . . 5
⊢
(ℕ0 ∈ (SubMnd‘ℂfld) →
0 = (0g‘𝑁)) |
| 49 | 29, 48 | ax-mp 5 |
. . . 4
⊢ 0 =
(0g‘𝑁) |
| 50 | | cnfld1 21406 |
. . . . 5
⊢ 1 =
(1r‘ℂfld) |
| 51 | 34, 50 | ringidval 20180 |
. . . 4
⊢ 1 =
(0g‘𝑀) |
| 52 | 39, 41, 44, 46, 49, 51 | ismhm 18798 |
. . 3
⊢ ((𝑥 ∈ ℕ0
↦ (𝐴↑𝑥)) ∈ (𝑁 MndHom 𝑀) ↔ ((𝑁 ∈ Mnd ∧ 𝑀 ∈ Mnd) ∧ ((𝑥 ∈ ℕ0 ↦ (𝐴↑𝑥)):ℕ0⟶ℂ ∧
∀𝑦 ∈
ℕ0 ∀𝑧 ∈ ℕ0 ((𝑥 ∈ ℕ0
↦ (𝐴↑𝑥))‘(𝑦 + 𝑧)) = (((𝑥 ∈ ℕ0 ↦ (𝐴↑𝑥))‘𝑦) · ((𝑥 ∈ ℕ0 ↦ (𝐴↑𝑥))‘𝑧)) ∧ ((𝑥 ∈ ℕ0 ↦ (𝐴↑𝑥))‘0) = 1))) |
| 53 | 37, 52 | mpbiran 709 |
. 2
⊢ ((𝑥 ∈ ℕ0
↦ (𝐴↑𝑥)) ∈ (𝑁 MndHom 𝑀) ↔ ((𝑥 ∈ ℕ0 ↦ (𝐴↑𝑥)):ℕ0⟶ℂ ∧
∀𝑦 ∈
ℕ0 ∀𝑧 ∈ ℕ0 ((𝑥 ∈ ℕ0
↦ (𝐴↑𝑥))‘(𝑦 + 𝑧)) = (((𝑥 ∈ ℕ0 ↦ (𝐴↑𝑥))‘𝑦) · ((𝑥 ∈ ℕ0 ↦ (𝐴↑𝑥))‘𝑧)) ∧ ((𝑥 ∈ ℕ0 ↦ (𝐴↑𝑥))‘0) = 1)) |
| 54 | 2, 21, 28, 53 | syl3anbrc 1344 |
1
⊢ (𝐴 ∈ ℂ → (𝑥 ∈ ℕ0
↦ (𝐴↑𝑥)) ∈ (𝑁 MndHom 𝑀)) |