| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | nn0subm 21440 | . . . 4
⊢
ℕ0 ∈
(SubMnd‘ℂfld) | 
| 2 |  | eqid 2737 | . . . . 5
⊢
(ℂfld ↾s ℕ0) =
(ℂfld ↾s
ℕ0) | 
| 3 | 2 | submbas 18827 | . . . 4
⊢
(ℕ0 ∈ (SubMnd‘ℂfld) →
ℕ0 = (Base‘(ℂfld ↾s
ℕ0))) | 
| 4 | 1, 3 | ax-mp 5 | . . 3
⊢
ℕ0 = (Base‘(ℂfld
↾s ℕ0)) | 
| 5 |  | cnfld0 21405 | . . . . 5
⊢ 0 =
(0g‘ℂfld) | 
| 6 | 2, 5 | subm0 18828 | . . . 4
⊢
(ℕ0 ∈ (SubMnd‘ℂfld) →
0 = (0g‘(ℂfld ↾s
ℕ0))) | 
| 7 | 1, 6 | ax-mp 5 | . . 3
⊢ 0 =
(0g‘(ℂfld ↾s
ℕ0)) | 
| 8 |  | cnring 21403 | . . . . . 6
⊢
ℂfld ∈ Ring | 
| 9 |  | ringcmn 20279 | . . . . . 6
⊢
(ℂfld ∈ Ring → ℂfld ∈
CMnd) | 
| 10 | 8, 9 | ax-mp 5 | . . . . 5
⊢
ℂfld ∈ CMnd | 
| 11 | 2 | submcmn 19856 | . . . . 5
⊢
((ℂfld ∈ CMnd ∧ ℕ0 ∈
(SubMnd‘ℂfld)) → (ℂfld
↾s ℕ0) ∈ CMnd) | 
| 12 | 10, 1, 11 | mp2an 692 | . . . 4
⊢
(ℂfld ↾s ℕ0) ∈
CMnd | 
| 13 | 12 | a1i 11 | . . 3
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐻) → (ℂfld
↾s ℕ0) ∈ CMnd) | 
| 14 |  | mhphflem.g | . . . 4
⊢ (𝜑 → 𝐺 ∈ Mnd) | 
| 15 | 14 | adantr 480 | . . 3
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐻) → 𝐺 ∈ Mnd) | 
| 16 |  | mhphflem.i | . . . 4
⊢ (𝜑 → 𝐼 ∈ 𝑉) | 
| 17 | 16 | adantr 480 | . . 3
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐻) → 𝐼 ∈ 𝑉) | 
| 18 |  | mhphflem.k | . . . 4
⊢ 𝐵 = (Base‘𝐺) | 
| 19 |  | cnfldadd 21370 | . . . . . 6
⊢  + =
(+g‘ℂfld) | 
| 20 | 2, 19 | ressplusg 17334 | . . . . 5
⊢
(ℕ0 ∈ (SubMnd‘ℂfld) →
+ = (+g‘(ℂfld ↾s
ℕ0))) | 
| 21 | 1, 20 | ax-mp 5 | . . . 4
⊢  + =
(+g‘(ℂfld ↾s
ℕ0)) | 
| 22 |  | eqid 2737 | . . . 4
⊢
(+g‘𝐺) = (+g‘𝐺) | 
| 23 |  | eqid 2737 | . . . 4
⊢
(0g‘𝐺) = (0g‘𝐺) | 
| 24 | 2 | submmnd 18826 | . . . . 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 726 | . . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐻) ∧ 𝑛 ∈ ℕ0) → 𝐺 ∈ Mnd) | 
| 28 |  | simpr 484 | . . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐻) ∧ 𝑛 ∈ ℕ0) → 𝑛 ∈
ℕ0) | 
| 29 |  | mhphflem.l | . . . . . . 7
⊢ (𝜑 → 𝐿 ∈ 𝐵) | 
| 30 | 29 | ad2antrr 726 | . . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐻) ∧ 𝑛 ∈ ℕ0) → 𝐿 ∈ 𝐵) | 
| 31 | 18, 26, 27, 28, 30 | mulgnn0cld 19113 | . . . . 5
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐻) ∧ 𝑛 ∈ ℕ0) → (𝑛 · 𝐿) ∈ 𝐵) | 
| 32 | 31 | fmpttd 7135 | . . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐻) → (𝑛 ∈ ℕ0 ↦ (𝑛 · 𝐿)):ℕ0⟶𝐵) | 
| 33 | 14 | ad2antrr 726 | . . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐻) ∧ (𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0))
→ 𝐺 ∈
Mnd) | 
| 34 |  | simprl 771 | . . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐻) ∧ (𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0))
→ 𝑥 ∈
ℕ0) | 
| 35 |  | simprr 773 | . . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐻) ∧ (𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0))
→ 𝑦 ∈
ℕ0) | 
| 36 | 29 | ad2antrr 726 | . . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐻) ∧ (𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0))
→ 𝐿 ∈ 𝐵) | 
| 37 | 18, 26, 22 | mulgnn0dir 19122 | . . . . . 6
⊢ ((𝐺 ∈ Mnd ∧ (𝑥 ∈ ℕ0
∧ 𝑦 ∈
ℕ0 ∧ 𝐿
∈ 𝐵)) → ((𝑥 + 𝑦) · 𝐿) = ((𝑥 · 𝐿)(+g‘𝐺)(𝑦 · 𝐿))) | 
| 38 | 33, 34, 35, 36, 37 | syl13anc 1374 | . . . . 5
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐻) ∧ (𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0))
→ ((𝑥 + 𝑦) · 𝐿) = ((𝑥 · 𝐿)(+g‘𝐺)(𝑦 · 𝐿))) | 
| 39 |  | eqid 2737 | . . . . . 6
⊢ (𝑛 ∈ ℕ0
↦ (𝑛 · 𝐿)) = (𝑛 ∈ ℕ0 ↦ (𝑛 · 𝐿)) | 
| 40 |  | oveq1 7438 | . . . . . 6
⊢ (𝑛 = (𝑥 + 𝑦) → (𝑛 · 𝐿) = ((𝑥 + 𝑦) · 𝐿)) | 
| 41 |  | nn0addcl 12561 | . . . . . . 7
⊢ ((𝑥 ∈ ℕ0
∧ 𝑦 ∈
ℕ0) → (𝑥 + 𝑦) ∈
ℕ0) | 
| 42 | 41 | adantl 481 | . . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐻) ∧ (𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0))
→ (𝑥 + 𝑦) ∈
ℕ0) | 
| 43 |  | ovexd 7466 | . . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐻) ∧ (𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0))
→ ((𝑥 + 𝑦) · 𝐿) ∈ V) | 
| 44 | 39, 40, 42, 43 | fvmptd3 7039 | . . . . 5
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐻) ∧ (𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0))
→ ((𝑛 ∈
ℕ0 ↦ (𝑛 · 𝐿))‘(𝑥 + 𝑦)) = ((𝑥 + 𝑦) · 𝐿)) | 
| 45 |  | oveq1 7438 | . . . . . . 7
⊢ (𝑛 = 𝑥 → (𝑛 · 𝐿) = (𝑥 · 𝐿)) | 
| 46 |  | ovexd 7466 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐻) ∧ (𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0))
→ (𝑥 · 𝐿) ∈ V) | 
| 47 | 39, 45, 34, 46 | fvmptd3 7039 | . . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐻) ∧ (𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0))
→ ((𝑛 ∈
ℕ0 ↦ (𝑛 · 𝐿))‘𝑥) = (𝑥 · 𝐿)) | 
| 48 |  | oveq1 7438 | . . . . . . 7
⊢ (𝑛 = 𝑦 → (𝑛 · 𝐿) = (𝑦 · 𝐿)) | 
| 49 |  | ovexd 7466 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐻) ∧ (𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0))
→ (𝑦 · 𝐿) ∈ V) | 
| 50 | 39, 48, 35, 49 | fvmptd3 7039 | . . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐻) ∧ (𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0))
→ ((𝑛 ∈
ℕ0 ↦ (𝑛 · 𝐿))‘𝑦) = (𝑦 · 𝐿)) | 
| 51 | 47, 50 | oveq12d 7449 | . . . . 5
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐻) ∧ (𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0))
→ (((𝑛 ∈
ℕ0 ↦ (𝑛 · 𝐿))‘𝑥)(+g‘𝐺)((𝑛 ∈ ℕ0 ↦ (𝑛 · 𝐿))‘𝑦)) = ((𝑥 · 𝐿)(+g‘𝐺)(𝑦 · 𝐿))) | 
| 52 | 38, 44, 51 | 3eqtr4d 2787 | . . . 4
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐻) ∧ (𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0))
→ ((𝑛 ∈
ℕ0 ↦ (𝑛 · 𝐿))‘(𝑥 + 𝑦)) = (((𝑛 ∈ ℕ0 ↦ (𝑛 · 𝐿))‘𝑥)(+g‘𝐺)((𝑛 ∈ ℕ0 ↦ (𝑛 · 𝐿))‘𝑦))) | 
| 53 |  | oveq1 7438 | . . . . . 6
⊢ (𝑛 = 0 → (𝑛 · 𝐿) = (0 · 𝐿)) | 
| 54 |  | 0nn0 12541 | . . . . . . 7
⊢ 0 ∈
ℕ0 | 
| 55 | 54 | a1i 11 | . . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐻) → 0 ∈
ℕ0) | 
| 56 |  | ovexd 7466 | . . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐻) → (0 · 𝐿) ∈ V) | 
| 57 | 39, 53, 55, 56 | fvmptd3 7039 | . . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐻) → ((𝑛 ∈ ℕ0 ↦ (𝑛 · 𝐿))‘0) = (0 · 𝐿)) | 
| 58 | 29 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐻) → 𝐿 ∈ 𝐵) | 
| 59 | 18, 23, 26 | mulg0 19092 | . . . . . 6
⊢ (𝐿 ∈ 𝐵 → (0 · 𝐿) = (0g‘𝐺)) | 
| 60 | 58, 59 | syl 17 | . . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐻) → (0 · 𝐿) = (0g‘𝐺)) | 
| 61 | 57, 60 | eqtrd 2777 | . . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐻) → ((𝑛 ∈ ℕ0 ↦ (𝑛 · 𝐿))‘0) = (0g‘𝐺)) | 
| 62 | 4, 18, 21, 22, 7, 23, 25, 15, 32, 52, 61 | ismhmd 18799 | . . 3
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐻) → (𝑛 ∈ ℕ0 ↦ (𝑛 · 𝐿)) ∈ ((ℂfld
↾s ℕ0) MndHom 𝐺)) | 
| 63 |  | elrabi 3687 | . . . . . . 7
⊢ (𝑎 ∈ {𝑔 ∈ 𝐷 ∣ ((ℂfld
↾s ℕ0) Σg 𝑔) = 𝑁} → 𝑎 ∈ 𝐷) | 
| 64 |  | mhphflem.h | . . . . . . 7
⊢ 𝐻 = {𝑔 ∈ 𝐷 ∣ ((ℂfld
↾s ℕ0) Σg 𝑔) = 𝑁} | 
| 65 | 63, 64 | eleq2s 2859 | . . . . . 6
⊢ (𝑎 ∈ 𝐻 → 𝑎 ∈ 𝐷) | 
| 66 | 65 | adantl 481 | . . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐻) → 𝑎 ∈ 𝐷) | 
| 67 |  | mhphflem.d | . . . . . 6
⊢ 𝐷 = {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} | 
| 68 | 67 | psrbagf 21938 | . . . . 5
⊢ (𝑎 ∈ 𝐷 → 𝑎:𝐼⟶ℕ0) | 
| 69 | 66, 68 | syl 17 | . . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐻) → 𝑎:𝐼⟶ℕ0) | 
| 70 | 69 | ffvelcdmda 7104 | . . 3
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐻) ∧ 𝑣 ∈ 𝐼) → (𝑎‘𝑣) ∈
ℕ0) | 
| 71 | 69 | feqmptd 6977 | . . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐻) → 𝑎 = (𝑣 ∈ 𝐼 ↦ (𝑎‘𝑣))) | 
| 72 | 67 | psrbagfsupp 21939 | . . . . 5
⊢ (𝑎 ∈ 𝐷 → 𝑎 finSupp 0) | 
| 73 | 66, 72 | syl 17 | . . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐻) → 𝑎 finSupp 0) | 
| 74 | 71, 73 | eqbrtrrd 5167 | . . 3
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐻) → (𝑣 ∈ 𝐼 ↦ (𝑎‘𝑣)) finSupp 0) | 
| 75 |  | oveq1 7438 | . . 3
⊢ (𝑛 = (𝑎‘𝑣) → (𝑛 · 𝐿) = ((𝑎‘𝑣) · 𝐿)) | 
| 76 |  | oveq1 7438 | . . 3
⊢ (𝑛 = ((ℂfld
↾s ℕ0) Σg (𝑣 ∈ 𝐼 ↦ (𝑎‘𝑣))) → (𝑛 · 𝐿) = (((ℂfld
↾s ℕ0) Σg (𝑣 ∈ 𝐼 ↦ (𝑎‘𝑣))) · 𝐿)) | 
| 77 | 4, 7, 13, 15, 17, 62, 70, 74, 75, 76 | gsummhm2 19957 | . 2
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐻) → (𝐺 Σg (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) · 𝐿))) = (((ℂfld
↾s ℕ0) Σg (𝑣 ∈ 𝐼 ↦ (𝑎‘𝑣))) · 𝐿)) | 
| 78 | 71 | oveq2d 7447 | . . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐻) → ((ℂfld
↾s ℕ0) Σg 𝑎) = ((ℂfld
↾s ℕ0) Σg (𝑣 ∈ 𝐼 ↦ (𝑎‘𝑣)))) | 
| 79 |  | oveq2 7439 | . . . . . . . 8
⊢ (𝑔 = 𝑎 → ((ℂfld
↾s ℕ0) Σg 𝑔) = ((ℂfld
↾s ℕ0) Σg 𝑎)) | 
| 80 | 79 | eqeq1d 2739 | . . . . . . 7
⊢ (𝑔 = 𝑎 → (((ℂfld
↾s ℕ0) Σg 𝑔) = 𝑁 ↔ ((ℂfld
↾s ℕ0) Σg 𝑎) = 𝑁)) | 
| 81 | 80, 64 | elrab2 3695 | . . . . . 6
⊢ (𝑎 ∈ 𝐻 ↔ (𝑎 ∈ 𝐷 ∧ ((ℂfld
↾s ℕ0) Σg 𝑎) = 𝑁)) | 
| 82 | 81 | simprbi 496 | . . . . 5
⊢ (𝑎 ∈ 𝐻 → ((ℂfld
↾s ℕ0) Σg 𝑎) = 𝑁) | 
| 83 | 82 | adantl 481 | . . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐻) → ((ℂfld
↾s ℕ0) Σg 𝑎) = 𝑁) | 
| 84 | 78, 83 | eqtr3d 2779 | . . 3
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐻) → ((ℂfld
↾s ℕ0) Σg (𝑣 ∈ 𝐼 ↦ (𝑎‘𝑣))) = 𝑁) | 
| 85 | 84 | oveq1d 7446 | . 2
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐻) → (((ℂfld
↾s ℕ0) Σg (𝑣 ∈ 𝐼 ↦ (𝑎‘𝑣))) · 𝐿) = (𝑁 · 𝐿)) | 
| 86 | 77, 85 | eqtrd 2777 | 1
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐻) → (𝐺 Σg (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) · 𝐿))) = (𝑁 · 𝐿)) |