Step | Hyp | Ref
| Expression |
1 | | expcl 13800 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℕ0)
→ (𝐴↑𝑥) ∈
ℂ) |
2 | 1 | fmpttd 6989 |
. 2
⊢ (𝐴 ∈ ℂ → (𝑥 ∈ ℕ0
↦ (𝐴↑𝑥)):ℕ0⟶ℂ) |
3 | | expadd 13825 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℕ0
∧ 𝑧 ∈
ℕ0) → (𝐴↑(𝑦 + 𝑧)) = ((𝐴↑𝑦) · (𝐴↑𝑧))) |
4 | 3 | 3expb 1119 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℕ0
∧ 𝑧 ∈
ℕ0)) → (𝐴↑(𝑦 + 𝑧)) = ((𝐴↑𝑦) · (𝐴↑𝑧))) |
5 | | nn0addcl 12268 |
. . . . . 6
⊢ ((𝑦 ∈ ℕ0
∧ 𝑧 ∈
ℕ0) → (𝑦 + 𝑧) ∈
ℕ0) |
6 | 5 | adantl 482 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℕ0
∧ 𝑧 ∈
ℕ0)) → (𝑦 + 𝑧) ∈
ℕ0) |
7 | | oveq2 7283 |
. . . . . 6
⊢ (𝑥 = (𝑦 + 𝑧) → (𝐴↑𝑥) = (𝐴↑(𝑦 + 𝑧))) |
8 | | eqid 2738 |
. . . . . 6
⊢ (𝑥 ∈ ℕ0
↦ (𝐴↑𝑥)) = (𝑥 ∈ ℕ0 ↦ (𝐴↑𝑥)) |
9 | | ovex 7308 |
. . . . . 6
⊢ (𝐴↑(𝑦 + 𝑧)) ∈ V |
10 | 7, 8, 9 | fvmpt 6875 |
. . . . 5
⊢ ((𝑦 + 𝑧) ∈ ℕ0 → ((𝑥 ∈ ℕ0
↦ (𝐴↑𝑥))‘(𝑦 + 𝑧)) = (𝐴↑(𝑦 + 𝑧))) |
11 | 6, 10 | syl 17 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℕ0
∧ 𝑧 ∈
ℕ0)) → ((𝑥 ∈ ℕ0 ↦ (𝐴↑𝑥))‘(𝑦 + 𝑧)) = (𝐴↑(𝑦 + 𝑧))) |
12 | | oveq2 7283 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (𝐴↑𝑥) = (𝐴↑𝑦)) |
13 | | ovex 7308 |
. . . . . . 7
⊢ (𝐴↑𝑦) ∈ V |
14 | 12, 8, 13 | fvmpt 6875 |
. . . . . 6
⊢ (𝑦 ∈ ℕ0
→ ((𝑥 ∈
ℕ0 ↦ (𝐴↑𝑥))‘𝑦) = (𝐴↑𝑦)) |
15 | | oveq2 7283 |
. . . . . . 7
⊢ (𝑥 = 𝑧 → (𝐴↑𝑥) = (𝐴↑𝑧)) |
16 | | ovex 7308 |
. . . . . . 7
⊢ (𝐴↑𝑧) ∈ V |
17 | 15, 8, 16 | fvmpt 6875 |
. . . . . 6
⊢ (𝑧 ∈ ℕ0
→ ((𝑥 ∈
ℕ0 ↦ (𝐴↑𝑥))‘𝑧) = (𝐴↑𝑧)) |
18 | 14, 17 | oveqan12d 7294 |
. . . . 5
⊢ ((𝑦 ∈ ℕ0
∧ 𝑧 ∈
ℕ0) → (((𝑥 ∈ ℕ0 ↦ (𝐴↑𝑥))‘𝑦) · ((𝑥 ∈ ℕ0 ↦ (𝐴↑𝑥))‘𝑧)) = ((𝐴↑𝑦) · (𝐴↑𝑧))) |
19 | 18 | adantl 482 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℕ0
∧ 𝑧 ∈
ℕ0)) → (((𝑥 ∈ ℕ0 ↦ (𝐴↑𝑥))‘𝑦) · ((𝑥 ∈ ℕ0 ↦ (𝐴↑𝑥))‘𝑧)) = ((𝐴↑𝑦) · (𝐴↑𝑧))) |
20 | 4, 11, 19 | 3eqtr4d 2788 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℕ0
∧ 𝑧 ∈
ℕ0)) → ((𝑥 ∈ ℕ0 ↦ (𝐴↑𝑥))‘(𝑦 + 𝑧)) = (((𝑥 ∈ ℕ0 ↦ (𝐴↑𝑥))‘𝑦) · ((𝑥 ∈ ℕ0 ↦ (𝐴↑𝑥))‘𝑧))) |
21 | 20 | ralrimivva 3123 |
. 2
⊢ (𝐴 ∈ ℂ →
∀𝑦 ∈
ℕ0 ∀𝑧 ∈ ℕ0 ((𝑥 ∈ ℕ0
↦ (𝐴↑𝑥))‘(𝑦 + 𝑧)) = (((𝑥 ∈ ℕ0 ↦ (𝐴↑𝑥))‘𝑦) · ((𝑥 ∈ ℕ0 ↦ (𝐴↑𝑥))‘𝑧))) |
22 | | 0nn0 12248 |
. . . 4
⊢ 0 ∈
ℕ0 |
23 | | oveq2 7283 |
. . . . 5
⊢ (𝑥 = 0 → (𝐴↑𝑥) = (𝐴↑0)) |
24 | | ovex 7308 |
. . . . 5
⊢ (𝐴↑0) ∈
V |
25 | 23, 8, 24 | fvmpt 6875 |
. . . 4
⊢ (0 ∈
ℕ0 → ((𝑥 ∈ ℕ0 ↦ (𝐴↑𝑥))‘0) = (𝐴↑0)) |
26 | 22, 25 | ax-mp 5 |
. . 3
⊢ ((𝑥 ∈ ℕ0
↦ (𝐴↑𝑥))‘0) = (𝐴↑0) |
27 | | exp0 13786 |
. . 3
⊢ (𝐴 ∈ ℂ → (𝐴↑0) = 1) |
28 | 26, 27 | eqtrid 2790 |
. 2
⊢ (𝐴 ∈ ℂ → ((𝑥 ∈ ℕ0
↦ (𝐴↑𝑥))‘0) =
1) |
29 | | nn0subm 20653 |
. . . . 5
⊢
ℕ0 ∈
(SubMnd‘ℂfld) |
30 | | expmhm.1 |
. . . . . 6
⊢ 𝑁 = (ℂfld
↾s ℕ0) |
31 | 30 | submmnd 18452 |
. . . . 5
⊢
(ℕ0 ∈ (SubMnd‘ℂfld) →
𝑁 ∈
Mnd) |
32 | 29, 31 | ax-mp 5 |
. . . 4
⊢ 𝑁 ∈ Mnd |
33 | | cnring 20620 |
. . . . 5
⊢
ℂfld ∈ Ring |
34 | | expmhm.2 |
. . . . . 6
⊢ 𝑀 =
(mulGrp‘ℂfld) |
35 | 34 | ringmgp 19789 |
. . . . 5
⊢
(ℂfld ∈ Ring → 𝑀 ∈ Mnd) |
36 | 33, 35 | ax-mp 5 |
. . . 4
⊢ 𝑀 ∈ Mnd |
37 | 32, 36 | pm3.2i 471 |
. . 3
⊢ (𝑁 ∈ Mnd ∧ 𝑀 ∈ Mnd) |
38 | 30 | submbas 18453 |
. . . . 5
⊢
(ℕ0 ∈ (SubMnd‘ℂfld) →
ℕ0 = (Base‘𝑁)) |
39 | 29, 38 | ax-mp 5 |
. . . 4
⊢
ℕ0 = (Base‘𝑁) |
40 | | cnfldbas 20601 |
. . . . 5
⊢ ℂ =
(Base‘ℂfld) |
41 | 34, 40 | mgpbas 19726 |
. . . 4
⊢ ℂ =
(Base‘𝑀) |
42 | | cnfldadd 20602 |
. . . . . 6
⊢ + =
(+g‘ℂfld) |
43 | 30, 42 | ressplusg 17000 |
. . . . 5
⊢
(ℕ0 ∈ (SubMnd‘ℂfld) →
+ = (+g‘𝑁)) |
44 | 29, 43 | ax-mp 5 |
. . . 4
⊢ + =
(+g‘𝑁) |
45 | | cnfldmul 20603 |
. . . . 5
⊢ ·
= (.r‘ℂfld) |
46 | 34, 45 | mgpplusg 19724 |
. . . 4
⊢ ·
= (+g‘𝑀) |
47 | | cnfld0 20622 |
. . . . . 6
⊢ 0 =
(0g‘ℂfld) |
48 | 30, 47 | subm0 18454 |
. . . . 5
⊢
(ℕ0 ∈ (SubMnd‘ℂfld) →
0 = (0g‘𝑁)) |
49 | 29, 48 | ax-mp 5 |
. . . 4
⊢ 0 =
(0g‘𝑁) |
50 | | cnfld1 20623 |
. . . . 5
⊢ 1 =
(1r‘ℂfld) |
51 | 34, 50 | ringidval 19739 |
. . . 4
⊢ 1 =
(0g‘𝑀) |
52 | 39, 41, 44, 46, 49, 51 | ismhm 18432 |
. . 3
⊢ ((𝑥 ∈ ℕ0
↦ (𝐴↑𝑥)) ∈ (𝑁 MndHom 𝑀) ↔ ((𝑁 ∈ Mnd ∧ 𝑀 ∈ Mnd) ∧ ((𝑥 ∈ ℕ0 ↦ (𝐴↑𝑥)):ℕ0⟶ℂ ∧
∀𝑦 ∈
ℕ0 ∀𝑧 ∈ ℕ0 ((𝑥 ∈ ℕ0
↦ (𝐴↑𝑥))‘(𝑦 + 𝑧)) = (((𝑥 ∈ ℕ0 ↦ (𝐴↑𝑥))‘𝑦) · ((𝑥 ∈ ℕ0 ↦ (𝐴↑𝑥))‘𝑧)) ∧ ((𝑥 ∈ ℕ0 ↦ (𝐴↑𝑥))‘0) = 1))) |
53 | 37, 52 | mpbiran 706 |
. 2
⊢ ((𝑥 ∈ ℕ0
↦ (𝐴↑𝑥)) ∈ (𝑁 MndHom 𝑀) ↔ ((𝑥 ∈ ℕ0 ↦ (𝐴↑𝑥)):ℕ0⟶ℂ ∧
∀𝑦 ∈
ℕ0 ∀𝑧 ∈ ℕ0 ((𝑥 ∈ ℕ0
↦ (𝐴↑𝑥))‘(𝑦 + 𝑧)) = (((𝑥 ∈ ℕ0 ↦ (𝐴↑𝑥))‘𝑦) · ((𝑥 ∈ ℕ0 ↦ (𝐴↑𝑥))‘𝑧)) ∧ ((𝑥 ∈ ℕ0 ↦ (𝐴↑𝑥))‘0) = 1)) |
54 | 2, 21, 28, 53 | syl3anbrc 1342 |
1
⊢ (𝐴 ∈ ℂ → (𝑥 ∈ ℕ0
↦ (𝐴↑𝑥)) ∈ (𝑁 MndHom 𝑀)) |