Step | Hyp | Ref
| Expression |
1 | | expcl 13450 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℕ0)
→ (𝐴↑𝑥) ∈
ℂ) |
2 | 1 | fmpttd 6882 |
. 2
⊢ (𝐴 ∈ ℂ → (𝑥 ∈ ℕ0
↦ (𝐴↑𝑥)):ℕ0⟶ℂ) |
3 | | expadd 13474 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℕ0
∧ 𝑧 ∈
ℕ0) → (𝐴↑(𝑦 + 𝑧)) = ((𝐴↑𝑦) · (𝐴↑𝑧))) |
4 | 3 | 3expb 1116 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℕ0
∧ 𝑧 ∈
ℕ0)) → (𝐴↑(𝑦 + 𝑧)) = ((𝐴↑𝑦) · (𝐴↑𝑧))) |
5 | | nn0addcl 11935 |
. . . . . 6
⊢ ((𝑦 ∈ ℕ0
∧ 𝑧 ∈
ℕ0) → (𝑦 + 𝑧) ∈
ℕ0) |
6 | 5 | adantl 484 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℕ0
∧ 𝑧 ∈
ℕ0)) → (𝑦 + 𝑧) ∈
ℕ0) |
7 | | oveq2 7167 |
. . . . . 6
⊢ (𝑥 = (𝑦 + 𝑧) → (𝐴↑𝑥) = (𝐴↑(𝑦 + 𝑧))) |
8 | | eqid 2824 |
. . . . . 6
⊢ (𝑥 ∈ ℕ0
↦ (𝐴↑𝑥)) = (𝑥 ∈ ℕ0 ↦ (𝐴↑𝑥)) |
9 | | ovex 7192 |
. . . . . 6
⊢ (𝐴↑(𝑦 + 𝑧)) ∈ V |
10 | 7, 8, 9 | fvmpt 6771 |
. . . . 5
⊢ ((𝑦 + 𝑧) ∈ ℕ0 → ((𝑥 ∈ ℕ0
↦ (𝐴↑𝑥))‘(𝑦 + 𝑧)) = (𝐴↑(𝑦 + 𝑧))) |
11 | 6, 10 | syl 17 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℕ0
∧ 𝑧 ∈
ℕ0)) → ((𝑥 ∈ ℕ0 ↦ (𝐴↑𝑥))‘(𝑦 + 𝑧)) = (𝐴↑(𝑦 + 𝑧))) |
12 | | oveq2 7167 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (𝐴↑𝑥) = (𝐴↑𝑦)) |
13 | | ovex 7192 |
. . . . . . 7
⊢ (𝐴↑𝑦) ∈ V |
14 | 12, 8, 13 | fvmpt 6771 |
. . . . . 6
⊢ (𝑦 ∈ ℕ0
→ ((𝑥 ∈
ℕ0 ↦ (𝐴↑𝑥))‘𝑦) = (𝐴↑𝑦)) |
15 | | oveq2 7167 |
. . . . . . 7
⊢ (𝑥 = 𝑧 → (𝐴↑𝑥) = (𝐴↑𝑧)) |
16 | | ovex 7192 |
. . . . . . 7
⊢ (𝐴↑𝑧) ∈ V |
17 | 15, 8, 16 | fvmpt 6771 |
. . . . . 6
⊢ (𝑧 ∈ ℕ0
→ ((𝑥 ∈
ℕ0 ↦ (𝐴↑𝑥))‘𝑧) = (𝐴↑𝑧)) |
18 | 14, 17 | oveqan12d 7178 |
. . . . 5
⊢ ((𝑦 ∈ ℕ0
∧ 𝑧 ∈
ℕ0) → (((𝑥 ∈ ℕ0 ↦ (𝐴↑𝑥))‘𝑦) · ((𝑥 ∈ ℕ0 ↦ (𝐴↑𝑥))‘𝑧)) = ((𝐴↑𝑦) · (𝐴↑𝑧))) |
19 | 18 | adantl 484 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℕ0
∧ 𝑧 ∈
ℕ0)) → (((𝑥 ∈ ℕ0 ↦ (𝐴↑𝑥))‘𝑦) · ((𝑥 ∈ ℕ0 ↦ (𝐴↑𝑥))‘𝑧)) = ((𝐴↑𝑦) · (𝐴↑𝑧))) |
20 | 4, 11, 19 | 3eqtr4d 2869 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℕ0
∧ 𝑧 ∈
ℕ0)) → ((𝑥 ∈ ℕ0 ↦ (𝐴↑𝑥))‘(𝑦 + 𝑧)) = (((𝑥 ∈ ℕ0 ↦ (𝐴↑𝑥))‘𝑦) · ((𝑥 ∈ ℕ0 ↦ (𝐴↑𝑥))‘𝑧))) |
21 | 20 | ralrimivva 3194 |
. 2
⊢ (𝐴 ∈ ℂ →
∀𝑦 ∈
ℕ0 ∀𝑧 ∈ ℕ0 ((𝑥 ∈ ℕ0
↦ (𝐴↑𝑥))‘(𝑦 + 𝑧)) = (((𝑥 ∈ ℕ0 ↦ (𝐴↑𝑥))‘𝑦) · ((𝑥 ∈ ℕ0 ↦ (𝐴↑𝑥))‘𝑧))) |
22 | | 0nn0 11915 |
. . . 4
⊢ 0 ∈
ℕ0 |
23 | | oveq2 7167 |
. . . . 5
⊢ (𝑥 = 0 → (𝐴↑𝑥) = (𝐴↑0)) |
24 | | ovex 7192 |
. . . . 5
⊢ (𝐴↑0) ∈
V |
25 | 23, 8, 24 | fvmpt 6771 |
. . . 4
⊢ (0 ∈
ℕ0 → ((𝑥 ∈ ℕ0 ↦ (𝐴↑𝑥))‘0) = (𝐴↑0)) |
26 | 22, 25 | ax-mp 5 |
. . 3
⊢ ((𝑥 ∈ ℕ0
↦ (𝐴↑𝑥))‘0) = (𝐴↑0) |
27 | | exp0 13436 |
. . 3
⊢ (𝐴 ∈ ℂ → (𝐴↑0) = 1) |
28 | 26, 27 | syl5eq 2871 |
. 2
⊢ (𝐴 ∈ ℂ → ((𝑥 ∈ ℕ0
↦ (𝐴↑𝑥))‘0) =
1) |
29 | | nn0subm 20603 |
. . . . 5
⊢
ℕ0 ∈
(SubMnd‘ℂfld) |
30 | | expmhm.1 |
. . . . . 6
⊢ 𝑁 = (ℂfld
↾s ℕ0) |
31 | 30 | submmnd 17981 |
. . . . 5
⊢
(ℕ0 ∈ (SubMnd‘ℂfld) →
𝑁 ∈
Mnd) |
32 | 29, 31 | ax-mp 5 |
. . . 4
⊢ 𝑁 ∈ Mnd |
33 | | cnring 20570 |
. . . . 5
⊢
ℂfld ∈ Ring |
34 | | expmhm.2 |
. . . . . 6
⊢ 𝑀 =
(mulGrp‘ℂfld) |
35 | 34 | ringmgp 19306 |
. . . . 5
⊢
(ℂfld ∈ Ring → 𝑀 ∈ Mnd) |
36 | 33, 35 | ax-mp 5 |
. . . 4
⊢ 𝑀 ∈ Mnd |
37 | 32, 36 | pm3.2i 473 |
. . 3
⊢ (𝑁 ∈ Mnd ∧ 𝑀 ∈ Mnd) |
38 | 30 | submbas 17982 |
. . . . 5
⊢
(ℕ0 ∈ (SubMnd‘ℂfld) →
ℕ0 = (Base‘𝑁)) |
39 | 29, 38 | ax-mp 5 |
. . . 4
⊢
ℕ0 = (Base‘𝑁) |
40 | | cnfldbas 20552 |
. . . . 5
⊢ ℂ =
(Base‘ℂfld) |
41 | 34, 40 | mgpbas 19248 |
. . . 4
⊢ ℂ =
(Base‘𝑀) |
42 | | cnfldadd 20553 |
. . . . . 6
⊢ + =
(+g‘ℂfld) |
43 | 30, 42 | ressplusg 16615 |
. . . . 5
⊢
(ℕ0 ∈ (SubMnd‘ℂfld) →
+ = (+g‘𝑁)) |
44 | 29, 43 | ax-mp 5 |
. . . 4
⊢ + =
(+g‘𝑁) |
45 | | cnfldmul 20554 |
. . . . 5
⊢ ·
= (.r‘ℂfld) |
46 | 34, 45 | mgpplusg 19246 |
. . . 4
⊢ ·
= (+g‘𝑀) |
47 | | cnfld0 20572 |
. . . . . 6
⊢ 0 =
(0g‘ℂfld) |
48 | 30, 47 | subm0 17983 |
. . . . 5
⊢
(ℕ0 ∈ (SubMnd‘ℂfld) →
0 = (0g‘𝑁)) |
49 | 29, 48 | ax-mp 5 |
. . . 4
⊢ 0 =
(0g‘𝑁) |
50 | | cnfld1 20573 |
. . . . 5
⊢ 1 =
(1r‘ℂfld) |
51 | 34, 50 | ringidval 19256 |
. . . 4
⊢ 1 =
(0g‘𝑀) |
52 | 39, 41, 44, 46, 49, 51 | ismhm 17961 |
. . 3
⊢ ((𝑥 ∈ ℕ0
↦ (𝐴↑𝑥)) ∈ (𝑁 MndHom 𝑀) ↔ ((𝑁 ∈ Mnd ∧ 𝑀 ∈ Mnd) ∧ ((𝑥 ∈ ℕ0 ↦ (𝐴↑𝑥)):ℕ0⟶ℂ ∧
∀𝑦 ∈
ℕ0 ∀𝑧 ∈ ℕ0 ((𝑥 ∈ ℕ0
↦ (𝐴↑𝑥))‘(𝑦 + 𝑧)) = (((𝑥 ∈ ℕ0 ↦ (𝐴↑𝑥))‘𝑦) · ((𝑥 ∈ ℕ0 ↦ (𝐴↑𝑥))‘𝑧)) ∧ ((𝑥 ∈ ℕ0 ↦ (𝐴↑𝑥))‘0) = 1))) |
53 | 37, 52 | mpbiran 707 |
. 2
⊢ ((𝑥 ∈ ℕ0
↦ (𝐴↑𝑥)) ∈ (𝑁 MndHom 𝑀) ↔ ((𝑥 ∈ ℕ0 ↦ (𝐴↑𝑥)):ℕ0⟶ℂ ∧
∀𝑦 ∈
ℕ0 ∀𝑧 ∈ ℕ0 ((𝑥 ∈ ℕ0
↦ (𝐴↑𝑥))‘(𝑦 + 𝑧)) = (((𝑥 ∈ ℕ0 ↦ (𝐴↑𝑥))‘𝑦) · ((𝑥 ∈ ℕ0 ↦ (𝐴↑𝑥))‘𝑧)) ∧ ((𝑥 ∈ ℕ0 ↦ (𝐴↑𝑥))‘0) = 1)) |
54 | 2, 21, 28, 53 | syl3anbrc 1339 |
1
⊢ (𝐴 ∈ ℂ → (𝑥 ∈ ℕ0
↦ (𝐴↑𝑥)) ∈ (𝑁 MndHom 𝑀)) |