Step | Hyp | Ref
| Expression |
1 | | expcl 13539 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℕ0)
→ (𝐴↑𝑥) ∈
ℂ) |
2 | 1 | fmpttd 6889 |
. 2
⊢ (𝐴 ∈ ℂ → (𝑥 ∈ ℕ0
↦ (𝐴↑𝑥)):ℕ0⟶ℂ) |
3 | | expadd 13563 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℕ0
∧ 𝑧 ∈
ℕ0) → (𝐴↑(𝑦 + 𝑧)) = ((𝐴↑𝑦) · (𝐴↑𝑧))) |
4 | 3 | 3expb 1121 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℕ0
∧ 𝑧 ∈
ℕ0)) → (𝐴↑(𝑦 + 𝑧)) = ((𝐴↑𝑦) · (𝐴↑𝑧))) |
5 | | nn0addcl 12011 |
. . . . . 6
⊢ ((𝑦 ∈ ℕ0
∧ 𝑧 ∈
ℕ0) → (𝑦 + 𝑧) ∈
ℕ0) |
6 | 5 | adantl 485 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℕ0
∧ 𝑧 ∈
ℕ0)) → (𝑦 + 𝑧) ∈
ℕ0) |
7 | | oveq2 7178 |
. . . . . 6
⊢ (𝑥 = (𝑦 + 𝑧) → (𝐴↑𝑥) = (𝐴↑(𝑦 + 𝑧))) |
8 | | eqid 2738 |
. . . . . 6
⊢ (𝑥 ∈ ℕ0
↦ (𝐴↑𝑥)) = (𝑥 ∈ ℕ0 ↦ (𝐴↑𝑥)) |
9 | | ovex 7203 |
. . . . . 6
⊢ (𝐴↑(𝑦 + 𝑧)) ∈ V |
10 | 7, 8, 9 | fvmpt 6775 |
. . . . 5
⊢ ((𝑦 + 𝑧) ∈ ℕ0 → ((𝑥 ∈ ℕ0
↦ (𝐴↑𝑥))‘(𝑦 + 𝑧)) = (𝐴↑(𝑦 + 𝑧))) |
11 | 6, 10 | syl 17 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℕ0
∧ 𝑧 ∈
ℕ0)) → ((𝑥 ∈ ℕ0 ↦ (𝐴↑𝑥))‘(𝑦 + 𝑧)) = (𝐴↑(𝑦 + 𝑧))) |
12 | | oveq2 7178 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (𝐴↑𝑥) = (𝐴↑𝑦)) |
13 | | ovex 7203 |
. . . . . . 7
⊢ (𝐴↑𝑦) ∈ V |
14 | 12, 8, 13 | fvmpt 6775 |
. . . . . 6
⊢ (𝑦 ∈ ℕ0
→ ((𝑥 ∈
ℕ0 ↦ (𝐴↑𝑥))‘𝑦) = (𝐴↑𝑦)) |
15 | | oveq2 7178 |
. . . . . . 7
⊢ (𝑥 = 𝑧 → (𝐴↑𝑥) = (𝐴↑𝑧)) |
16 | | ovex 7203 |
. . . . . . 7
⊢ (𝐴↑𝑧) ∈ V |
17 | 15, 8, 16 | fvmpt 6775 |
. . . . . 6
⊢ (𝑧 ∈ ℕ0
→ ((𝑥 ∈
ℕ0 ↦ (𝐴↑𝑥))‘𝑧) = (𝐴↑𝑧)) |
18 | 14, 17 | oveqan12d 7189 |
. . . . 5
⊢ ((𝑦 ∈ ℕ0
∧ 𝑧 ∈
ℕ0) → (((𝑥 ∈ ℕ0 ↦ (𝐴↑𝑥))‘𝑦) · ((𝑥 ∈ ℕ0 ↦ (𝐴↑𝑥))‘𝑧)) = ((𝐴↑𝑦) · (𝐴↑𝑧))) |
19 | 18 | adantl 485 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℕ0
∧ 𝑧 ∈
ℕ0)) → (((𝑥 ∈ ℕ0 ↦ (𝐴↑𝑥))‘𝑦) · ((𝑥 ∈ ℕ0 ↦ (𝐴↑𝑥))‘𝑧)) = ((𝐴↑𝑦) · (𝐴↑𝑧))) |
20 | 4, 11, 19 | 3eqtr4d 2783 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℕ0
∧ 𝑧 ∈
ℕ0)) → ((𝑥 ∈ ℕ0 ↦ (𝐴↑𝑥))‘(𝑦 + 𝑧)) = (((𝑥 ∈ ℕ0 ↦ (𝐴↑𝑥))‘𝑦) · ((𝑥 ∈ ℕ0 ↦ (𝐴↑𝑥))‘𝑧))) |
21 | 20 | ralrimivva 3103 |
. 2
⊢ (𝐴 ∈ ℂ →
∀𝑦 ∈
ℕ0 ∀𝑧 ∈ ℕ0 ((𝑥 ∈ ℕ0
↦ (𝐴↑𝑥))‘(𝑦 + 𝑧)) = (((𝑥 ∈ ℕ0 ↦ (𝐴↑𝑥))‘𝑦) · ((𝑥 ∈ ℕ0 ↦ (𝐴↑𝑥))‘𝑧))) |
22 | | 0nn0 11991 |
. . . 4
⊢ 0 ∈
ℕ0 |
23 | | oveq2 7178 |
. . . . 5
⊢ (𝑥 = 0 → (𝐴↑𝑥) = (𝐴↑0)) |
24 | | ovex 7203 |
. . . . 5
⊢ (𝐴↑0) ∈
V |
25 | 23, 8, 24 | fvmpt 6775 |
. . . 4
⊢ (0 ∈
ℕ0 → ((𝑥 ∈ ℕ0 ↦ (𝐴↑𝑥))‘0) = (𝐴↑0)) |
26 | 22, 25 | ax-mp 5 |
. . 3
⊢ ((𝑥 ∈ ℕ0
↦ (𝐴↑𝑥))‘0) = (𝐴↑0) |
27 | | exp0 13525 |
. . 3
⊢ (𝐴 ∈ ℂ → (𝐴↑0) = 1) |
28 | 26, 27 | syl5eq 2785 |
. 2
⊢ (𝐴 ∈ ℂ → ((𝑥 ∈ ℕ0
↦ (𝐴↑𝑥))‘0) =
1) |
29 | | nn0subm 20272 |
. . . . 5
⊢
ℕ0 ∈
(SubMnd‘ℂfld) |
30 | | expmhm.1 |
. . . . . 6
⊢ 𝑁 = (ℂfld
↾s ℕ0) |
31 | 30 | submmnd 18094 |
. . . . 5
⊢
(ℕ0 ∈ (SubMnd‘ℂfld) →
𝑁 ∈
Mnd) |
32 | 29, 31 | ax-mp 5 |
. . . 4
⊢ 𝑁 ∈ Mnd |
33 | | cnring 20239 |
. . . . 5
⊢
ℂfld ∈ Ring |
34 | | expmhm.2 |
. . . . . 6
⊢ 𝑀 =
(mulGrp‘ℂfld) |
35 | 34 | ringmgp 19422 |
. . . . 5
⊢
(ℂfld ∈ Ring → 𝑀 ∈ Mnd) |
36 | 33, 35 | ax-mp 5 |
. . . 4
⊢ 𝑀 ∈ Mnd |
37 | 32, 36 | pm3.2i 474 |
. . 3
⊢ (𝑁 ∈ Mnd ∧ 𝑀 ∈ Mnd) |
38 | 30 | submbas 18095 |
. . . . 5
⊢
(ℕ0 ∈ (SubMnd‘ℂfld) →
ℕ0 = (Base‘𝑁)) |
39 | 29, 38 | ax-mp 5 |
. . . 4
⊢
ℕ0 = (Base‘𝑁) |
40 | | cnfldbas 20221 |
. . . . 5
⊢ ℂ =
(Base‘ℂfld) |
41 | 34, 40 | mgpbas 19364 |
. . . 4
⊢ ℂ =
(Base‘𝑀) |
42 | | cnfldadd 20222 |
. . . . . 6
⊢ + =
(+g‘ℂfld) |
43 | 30, 42 | ressplusg 16715 |
. . . . 5
⊢
(ℕ0 ∈ (SubMnd‘ℂfld) →
+ = (+g‘𝑁)) |
44 | 29, 43 | ax-mp 5 |
. . . 4
⊢ + =
(+g‘𝑁) |
45 | | cnfldmul 20223 |
. . . . 5
⊢ ·
= (.r‘ℂfld) |
46 | 34, 45 | mgpplusg 19362 |
. . . 4
⊢ ·
= (+g‘𝑀) |
47 | | cnfld0 20241 |
. . . . . 6
⊢ 0 =
(0g‘ℂfld) |
48 | 30, 47 | subm0 18096 |
. . . . 5
⊢
(ℕ0 ∈ (SubMnd‘ℂfld) →
0 = (0g‘𝑁)) |
49 | 29, 48 | ax-mp 5 |
. . . 4
⊢ 0 =
(0g‘𝑁) |
50 | | cnfld1 20242 |
. . . . 5
⊢ 1 =
(1r‘ℂfld) |
51 | 34, 50 | ringidval 19372 |
. . . 4
⊢ 1 =
(0g‘𝑀) |
52 | 39, 41, 44, 46, 49, 51 | ismhm 18074 |
. . 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 𝑀)) |