Step | Hyp | Ref
| Expression |
1 | | nn0subm 20852 |
. . . 4
⊢
ℕ0 ∈
(SubMnd‘ℂfld) |
2 | | eqid 2736 |
. . . . 5
⊢
(ℂfld ↾s ℕ0) =
(ℂfld ↾s
ℕ0) |
3 | 2 | submbas 18625 |
. . . 4
⊢
(ℕ0 ∈ (SubMnd‘ℂfld) →
ℕ0 = (Base‘(ℂfld ↾s
ℕ0))) |
4 | 1, 3 | ax-mp 5 |
. . 3
⊢
ℕ0 = (Base‘(ℂfld
↾s ℕ0)) |
5 | | cnfld0 20821 |
. . . . 5
⊢ 0 =
(0g‘ℂfld) |
6 | 2, 5 | subm0 18626 |
. . . 4
⊢
(ℕ0 ∈ (SubMnd‘ℂfld) →
0 = (0g‘(ℂfld ↾s
ℕ0))) |
7 | 1, 6 | ax-mp 5 |
. . 3
⊢ 0 =
(0g‘(ℂfld ↾s
ℕ0)) |
8 | | cnring 20819 |
. . . . . 6
⊢
ℂfld ∈ Ring |
9 | | ringcmn 20003 |
. . . . . 6
⊢
(ℂfld ∈ Ring → ℂfld ∈
CMnd) |
10 | 8, 9 | ax-mp 5 |
. . . . 5
⊢
ℂfld ∈ CMnd |
11 | 2 | submcmn 19616 |
. . . . 5
⊢
((ℂfld ∈ CMnd ∧ ℕ0 ∈
(SubMnd‘ℂfld)) → (ℂfld
↾s ℕ0) ∈ CMnd) |
12 | 10, 1, 11 | mp2an 690 |
. . . 4
⊢
(ℂfld ↾s ℕ0) ∈
CMnd |
13 | 12 | a1i 11 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐻) → (ℂfld
↾s ℕ0) ∈ CMnd) |
14 | | mhphflem.g |
. . . 4
⊢ (𝜑 → 𝐺 ∈ Mnd) |
15 | 14 | adantr 481 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐻) → 𝐺 ∈ Mnd) |
16 | | mhphflem.i |
. . . 4
⊢ (𝜑 → 𝐼 ∈ 𝑉) |
17 | 16 | adantr 481 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐻) → 𝐼 ∈ 𝑉) |
18 | | mhphflem.k |
. . . 4
⊢ 𝐵 = (Base‘𝐺) |
19 | | cnfldadd 20801 |
. . . . . 6
⊢ + =
(+g‘ℂfld) |
20 | 2, 19 | ressplusg 17171 |
. . . . 5
⊢
(ℕ0 ∈ (SubMnd‘ℂfld) →
+ = (+g‘(ℂfld ↾s
ℕ0))) |
21 | 1, 20 | ax-mp 5 |
. . . 4
⊢ + =
(+g‘(ℂfld ↾s
ℕ0)) |
22 | | eqid 2736 |
. . . 4
⊢
(+g‘𝐺) = (+g‘𝐺) |
23 | | eqid 2736 |
. . . 4
⊢
(0g‘𝐺) = (0g‘𝐺) |
24 | 2 | submmnd 18624 |
. . . . 5
⊢
(ℕ0 ∈ (SubMnd‘ℂfld) →
(ℂfld ↾s ℕ0) ∈
Mnd) |
25 | 1, 24 | mp1i 13 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐻) → (ℂfld
↾s ℕ0) ∈ Mnd) |
26 | | mhphflem.e |
. . . . . 6
⊢ · =
(.g‘𝐺) |
27 | 14 | ad2antrr 724 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐻) ∧ 𝑛 ∈ ℕ0) → 𝐺 ∈ Mnd) |
28 | | simpr 485 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐻) ∧ 𝑛 ∈ ℕ0) → 𝑛 ∈
ℕ0) |
29 | | mhphflem.l |
. . . . . . 7
⊢ (𝜑 → 𝐿 ∈ 𝐵) |
30 | 29 | ad2antrr 724 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐻) ∧ 𝑛 ∈ ℕ0) → 𝐿 ∈ 𝐵) |
31 | 18, 26, 27, 28, 30 | mulgnn0cld 18897 |
. . . . 5
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐻) ∧ 𝑛 ∈ ℕ0) → (𝑛 · 𝐿) ∈ 𝐵) |
32 | 31 | fmpttd 7063 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐻) → (𝑛 ∈ ℕ0 ↦ (𝑛 · 𝐿)):ℕ0⟶𝐵) |
33 | 14 | ad2antrr 724 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐻) ∧ (𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0))
→ 𝐺 ∈
Mnd) |
34 | | simprl 769 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐻) ∧ (𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0))
→ 𝑥 ∈
ℕ0) |
35 | | simprr 771 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐻) ∧ (𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0))
→ 𝑦 ∈
ℕ0) |
36 | 29 | ad2antrr 724 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐻) ∧ (𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0))
→ 𝐿 ∈ 𝐵) |
37 | 18, 26, 22 | mulgnn0dir 18906 |
. . . . . 6
⊢ ((𝐺 ∈ Mnd ∧ (𝑥 ∈ ℕ0
∧ 𝑦 ∈
ℕ0 ∧ 𝐿
∈ 𝐵)) → ((𝑥 + 𝑦) · 𝐿) = ((𝑥 · 𝐿)(+g‘𝐺)(𝑦 · 𝐿))) |
38 | 33, 34, 35, 36, 37 | syl13anc 1372 |
. . . . 5
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐻) ∧ (𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0))
→ ((𝑥 + 𝑦) · 𝐿) = ((𝑥 · 𝐿)(+g‘𝐺)(𝑦 · 𝐿))) |
39 | | eqid 2736 |
. . . . . 6
⊢ (𝑛 ∈ ℕ0
↦ (𝑛 · 𝐿)) = (𝑛 ∈ ℕ0 ↦ (𝑛 · 𝐿)) |
40 | | oveq1 7364 |
. . . . . 6
⊢ (𝑛 = (𝑥 + 𝑦) → (𝑛 · 𝐿) = ((𝑥 + 𝑦) · 𝐿)) |
41 | | nn0addcl 12448 |
. . . . . . 7
⊢ ((𝑥 ∈ ℕ0
∧ 𝑦 ∈
ℕ0) → (𝑥 + 𝑦) ∈
ℕ0) |
42 | 41 | adantl 482 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐻) ∧ (𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0))
→ (𝑥 + 𝑦) ∈
ℕ0) |
43 | | ovexd 7392 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐻) ∧ (𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0))
→ ((𝑥 + 𝑦) · 𝐿) ∈ V) |
44 | 39, 40, 42, 43 | fvmptd3 6971 |
. . . . 5
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐻) ∧ (𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0))
→ ((𝑛 ∈
ℕ0 ↦ (𝑛 · 𝐿))‘(𝑥 + 𝑦)) = ((𝑥 + 𝑦) · 𝐿)) |
45 | | oveq1 7364 |
. . . . . . 7
⊢ (𝑛 = 𝑥 → (𝑛 · 𝐿) = (𝑥 · 𝐿)) |
46 | | ovexd 7392 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐻) ∧ (𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0))
→ (𝑥 · 𝐿) ∈ V) |
47 | 39, 45, 34, 46 | fvmptd3 6971 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐻) ∧ (𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0))
→ ((𝑛 ∈
ℕ0 ↦ (𝑛 · 𝐿))‘𝑥) = (𝑥 · 𝐿)) |
48 | | oveq1 7364 |
. . . . . . 7
⊢ (𝑛 = 𝑦 → (𝑛 · 𝐿) = (𝑦 · 𝐿)) |
49 | | ovexd 7392 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐻) ∧ (𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0))
→ (𝑦 · 𝐿) ∈ V) |
50 | 39, 48, 35, 49 | fvmptd3 6971 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐻) ∧ (𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0))
→ ((𝑛 ∈
ℕ0 ↦ (𝑛 · 𝐿))‘𝑦) = (𝑦 · 𝐿)) |
51 | 47, 50 | oveq12d 7375 |
. . . . 5
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐻) ∧ (𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0))
→ (((𝑛 ∈
ℕ0 ↦ (𝑛 · 𝐿))‘𝑥)(+g‘𝐺)((𝑛 ∈ ℕ0 ↦ (𝑛 · 𝐿))‘𝑦)) = ((𝑥 · 𝐿)(+g‘𝐺)(𝑦 · 𝐿))) |
52 | 38, 44, 51 | 3eqtr4d 2786 |
. . . 4
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐻) ∧ (𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0))
→ ((𝑛 ∈
ℕ0 ↦ (𝑛 · 𝐿))‘(𝑥 + 𝑦)) = (((𝑛 ∈ ℕ0 ↦ (𝑛 · 𝐿))‘𝑥)(+g‘𝐺)((𝑛 ∈ ℕ0 ↦ (𝑛 · 𝐿))‘𝑦))) |
53 | | oveq1 7364 |
. . . . . 6
⊢ (𝑛 = 0 → (𝑛 · 𝐿) = (0 · 𝐿)) |
54 | | 0nn0 12428 |
. . . . . . 7
⊢ 0 ∈
ℕ0 |
55 | 54 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐻) → 0 ∈
ℕ0) |
56 | | ovexd 7392 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐻) → (0 · 𝐿) ∈ V) |
57 | 39, 53, 55, 56 | fvmptd3 6971 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐻) → ((𝑛 ∈ ℕ0 ↦ (𝑛 · 𝐿))‘0) = (0 · 𝐿)) |
58 | 29 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐻) → 𝐿 ∈ 𝐵) |
59 | 18, 23, 26 | mulg0 18879 |
. . . . . 6
⊢ (𝐿 ∈ 𝐵 → (0 · 𝐿) = (0g‘𝐺)) |
60 | 58, 59 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐻) → (0 · 𝐿) = (0g‘𝐺)) |
61 | 57, 60 | eqtrd 2776 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐻) → ((𝑛 ∈ ℕ0 ↦ (𝑛 · 𝐿))‘0) = (0g‘𝐺)) |
62 | 4, 18, 21, 22, 7, 23, 25, 15, 32, 52, 61 | ismhmd 18604 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐻) → (𝑛 ∈ ℕ0 ↦ (𝑛 · 𝐿)) ∈ ((ℂfld
↾s ℕ0) MndHom 𝐺)) |
63 | | elrabi 3639 |
. . . . . . 7
⊢ (𝑎 ∈ {𝑔 ∈ 𝐷 ∣ ((ℂfld
↾s ℕ0) Σg 𝑔) = 𝑁} → 𝑎 ∈ 𝐷) |
64 | | mhphflem.h |
. . . . . . 7
⊢ 𝐻 = {𝑔 ∈ 𝐷 ∣ ((ℂfld
↾s ℕ0) Σg 𝑔) = 𝑁} |
65 | 63, 64 | eleq2s 2856 |
. . . . . 6
⊢ (𝑎 ∈ 𝐻 → 𝑎 ∈ 𝐷) |
66 | 65 | adantl 482 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐻) → 𝑎 ∈ 𝐷) |
67 | | mhphflem.d |
. . . . . 6
⊢ 𝐷 = {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} |
68 | 67 | psrbagf 21320 |
. . . . 5
⊢ (𝑎 ∈ 𝐷 → 𝑎:𝐼⟶ℕ0) |
69 | 66, 68 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐻) → 𝑎:𝐼⟶ℕ0) |
70 | 69 | ffvelcdmda 7035 |
. . 3
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐻) ∧ 𝑣 ∈ 𝐼) → (𝑎‘𝑣) ∈
ℕ0) |
71 | 69 | feqmptd 6910 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐻) → 𝑎 = (𝑣 ∈ 𝐼 ↦ (𝑎‘𝑣))) |
72 | 67 | psrbagfsupp 21322 |
. . . . 5
⊢ (𝑎 ∈ 𝐷 → 𝑎 finSupp 0) |
73 | 66, 72 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐻) → 𝑎 finSupp 0) |
74 | 71, 73 | eqbrtrrd 5129 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐻) → (𝑣 ∈ 𝐼 ↦ (𝑎‘𝑣)) finSupp 0) |
75 | | oveq1 7364 |
. . 3
⊢ (𝑛 = (𝑎‘𝑣) → (𝑛 · 𝐿) = ((𝑎‘𝑣) · 𝐿)) |
76 | | oveq1 7364 |
. . 3
⊢ (𝑛 = ((ℂfld
↾s ℕ0) Σg (𝑣 ∈ 𝐼 ↦ (𝑎‘𝑣))) → (𝑛 · 𝐿) = (((ℂfld
↾s ℕ0) Σg (𝑣 ∈ 𝐼 ↦ (𝑎‘𝑣))) · 𝐿)) |
77 | 4, 7, 13, 15, 17, 62, 70, 74, 75, 76 | gsummhm2 19716 |
. 2
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐻) → (𝐺 Σg (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) · 𝐿))) = (((ℂfld
↾s ℕ0) Σg (𝑣 ∈ 𝐼 ↦ (𝑎‘𝑣))) · 𝐿)) |
78 | 71 | oveq2d 7373 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐻) → ((ℂfld
↾s ℕ0) Σg 𝑎) = ((ℂfld
↾s ℕ0) Σg (𝑣 ∈ 𝐼 ↦ (𝑎‘𝑣)))) |
79 | | oveq2 7365 |
. . . . . . . 8
⊢ (𝑔 = 𝑎 → ((ℂfld
↾s ℕ0) Σg 𝑔) = ((ℂfld
↾s ℕ0) Σg 𝑎)) |
80 | 79 | eqeq1d 2738 |
. . . . . . 7
⊢ (𝑔 = 𝑎 → (((ℂfld
↾s ℕ0) Σg 𝑔) = 𝑁 ↔ ((ℂfld
↾s ℕ0) Σg 𝑎) = 𝑁)) |
81 | 80, 64 | elrab2 3648 |
. . . . . 6
⊢ (𝑎 ∈ 𝐻 ↔ (𝑎 ∈ 𝐷 ∧ ((ℂfld
↾s ℕ0) Σg 𝑎) = 𝑁)) |
82 | 81 | simprbi 497 |
. . . . 5
⊢ (𝑎 ∈ 𝐻 → ((ℂfld
↾s ℕ0) Σg 𝑎) = 𝑁) |
83 | 82 | adantl 482 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐻) → ((ℂfld
↾s ℕ0) Σg 𝑎) = 𝑁) |
84 | 78, 83 | eqtr3d 2778 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐻) → ((ℂfld
↾s ℕ0) Σg (𝑣 ∈ 𝐼 ↦ (𝑎‘𝑣))) = 𝑁) |
85 | 84 | oveq1d 7372 |
. 2
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐻) → (((ℂfld
↾s ℕ0) Σg (𝑣 ∈ 𝐼 ↦ (𝑎‘𝑣))) · 𝐿) = (𝑁 · 𝐿)) |
86 | 77, 85 | eqtrd 2776 |
1
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐻) → (𝐺 Σg (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) · 𝐿))) = (𝑁 · 𝐿)) |