| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | mhphf.a | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐴 ∈ (𝐾 ↑m 𝐼)) | 
| 2 |  | elmapi 8890 | . . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ (𝐾 ↑m 𝐼) → 𝐴:𝐼⟶𝐾) | 
| 3 | 1, 2 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐴:𝐼⟶𝐾) | 
| 4 | 3 | ffnd 6736 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐴 Fn 𝐼) | 
| 5 | 1, 4 | fndmexd 7927 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐼 ∈ V) | 
| 6 | 5 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) → 𝐼 ∈ V) | 
| 7 |  | mhphf.l | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐿 ∈ 𝑅) | 
| 8 | 7 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) → 𝐿 ∈ 𝑅) | 
| 9 | 4 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) → 𝐴 Fn 𝐼) | 
| 10 |  | eqidd 2737 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) ∧ 𝑖 ∈ 𝐼) → (𝐴‘𝑖) = (𝐴‘𝑖)) | 
| 11 | 6, 8, 9, 10 | ofc1 7726 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) ∧ 𝑖 ∈ 𝐼) → (((𝐼 × {𝐿}) ∘f · 𝐴)‘𝑖) = (𝐿 · (𝐴‘𝑖))) | 
| 12 | 11 | oveq2d 7448 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) ∧ 𝑖 ∈ 𝐼) → ((𝑏‘𝑖) ↑ (((𝐼 × {𝐿}) ∘f · 𝐴)‘𝑖)) = ((𝑏‘𝑖) ↑ (𝐿 · (𝐴‘𝑖)))) | 
| 13 |  | mhphf.s | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑆 ∈ CRing) | 
| 14 |  | eqid 2736 | . . . . . . . . . . . . . . 15
⊢
(mulGrp‘𝑆) =
(mulGrp‘𝑆) | 
| 15 | 14 | crngmgp 20239 | . . . . . . . . . . . . . 14
⊢ (𝑆 ∈ CRing →
(mulGrp‘𝑆) ∈
CMnd) | 
| 16 | 13, 15 | syl 17 | . . . . . . . . . . . . 13
⊢ (𝜑 → (mulGrp‘𝑆) ∈ CMnd) | 
| 17 | 16 | ad2antrr 726 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) ∧ 𝑖 ∈ 𝐼) → (mulGrp‘𝑆) ∈ CMnd) | 
| 18 |  | elrabi 3686 | . . . . . . . . . . . . . . 15
⊢ (𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} → 𝑏 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈
Fin}) | 
| 19 |  | eqid 2736 | . . . . . . . . . . . . . . . 16
⊢ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} = {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} | 
| 20 | 19 | psrbagf 21939 | . . . . . . . . . . . . . . 15
⊢ (𝑏 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} → 𝑏:𝐼⟶ℕ0) | 
| 21 | 18, 20 | syl 17 | . . . . . . . . . . . . . 14
⊢ (𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} → 𝑏:𝐼⟶ℕ0) | 
| 22 | 21 | adantl 481 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) → 𝑏:𝐼⟶ℕ0) | 
| 23 | 22 | ffvelcdmda 7103 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) ∧ 𝑖 ∈ 𝐼) → (𝑏‘𝑖) ∈
ℕ0) | 
| 24 |  | mhphf.r | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆)) | 
| 25 |  | mhphf.k | . . . . . . . . . . . . . . . 16
⊢ 𝐾 = (Base‘𝑆) | 
| 26 | 25 | subrgss 20573 | . . . . . . . . . . . . . . 15
⊢ (𝑅 ∈ (SubRing‘𝑆) → 𝑅 ⊆ 𝐾) | 
| 27 | 24, 26 | syl 17 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑅 ⊆ 𝐾) | 
| 28 | 27, 7 | sseldd 3983 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝐿 ∈ 𝐾) | 
| 29 | 28 | ad2antrr 726 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) ∧ 𝑖 ∈ 𝐼) → 𝐿 ∈ 𝐾) | 
| 30 | 3 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) → 𝐴:𝐼⟶𝐾) | 
| 31 | 30 | ffvelcdmda 7103 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) ∧ 𝑖 ∈ 𝐼) → (𝐴‘𝑖) ∈ 𝐾) | 
| 32 | 14, 25 | mgpbas 20143 | . . . . . . . . . . . . 13
⊢ 𝐾 =
(Base‘(mulGrp‘𝑆)) | 
| 33 |  | mhphf.e | . . . . . . . . . . . . 13
⊢  ↑ =
(.g‘(mulGrp‘𝑆)) | 
| 34 |  | mhphf.m | . . . . . . . . . . . . . 14
⊢  · =
(.r‘𝑆) | 
| 35 | 14, 34 | mgpplusg 20142 | . . . . . . . . . . . . 13
⊢  · =
(+g‘(mulGrp‘𝑆)) | 
| 36 | 32, 33, 35 | mulgnn0di 19844 | . . . . . . . . . . . 12
⊢
(((mulGrp‘𝑆)
∈ CMnd ∧ ((𝑏‘𝑖) ∈ ℕ0 ∧ 𝐿 ∈ 𝐾 ∧ (𝐴‘𝑖) ∈ 𝐾)) → ((𝑏‘𝑖) ↑ (𝐿 · (𝐴‘𝑖))) = (((𝑏‘𝑖) ↑ 𝐿) · ((𝑏‘𝑖) ↑ (𝐴‘𝑖)))) | 
| 37 | 17, 23, 29, 31, 36 | syl13anc 1373 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) ∧ 𝑖 ∈ 𝐼) → ((𝑏‘𝑖) ↑ (𝐿 · (𝐴‘𝑖))) = (((𝑏‘𝑖) ↑ 𝐿) · ((𝑏‘𝑖) ↑ (𝐴‘𝑖)))) | 
| 38 | 12, 37 | eqtrd 2776 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) ∧ 𝑖 ∈ 𝐼) → ((𝑏‘𝑖) ↑ (((𝐼 × {𝐿}) ∘f · 𝐴)‘𝑖)) = (((𝑏‘𝑖) ↑ 𝐿) · ((𝑏‘𝑖) ↑ (𝐴‘𝑖)))) | 
| 39 | 38 | mpteq2dva 5241 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) → (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (((𝐼 × {𝐿}) ∘f · 𝐴)‘𝑖))) = (𝑖 ∈ 𝐼 ↦ (((𝑏‘𝑖) ↑ 𝐿) · ((𝑏‘𝑖) ↑ (𝐴‘𝑖))))) | 
| 40 | 39 | oveq2d 7448 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) → ((mulGrp‘𝑆) Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (((𝐼 × {𝐿}) ∘f · 𝐴)‘𝑖)))) = ((mulGrp‘𝑆) Σg (𝑖 ∈ 𝐼 ↦ (((𝑏‘𝑖) ↑ 𝐿) · ((𝑏‘𝑖) ↑ (𝐴‘𝑖)))))) | 
| 41 |  | eqid 2736 | . . . . . . . . . 10
⊢
(1r‘𝑆) = (1r‘𝑆) | 
| 42 | 14, 41 | ringidval 20181 | . . . . . . . . 9
⊢
(1r‘𝑆) = (0g‘(mulGrp‘𝑆)) | 
| 43 | 13 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) → 𝑆 ∈ CRing) | 
| 44 | 43, 15 | syl 17 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) → (mulGrp‘𝑆) ∈ CMnd) | 
| 45 | 13 | crngringd 20244 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝑆 ∈ Ring) | 
| 46 | 14 | ringmgp 20237 | . . . . . . . . . . . 12
⊢ (𝑆 ∈ Ring →
(mulGrp‘𝑆) ∈
Mnd) | 
| 47 | 45, 46 | syl 17 | . . . . . . . . . . 11
⊢ (𝜑 → (mulGrp‘𝑆) ∈ Mnd) | 
| 48 | 47 | ad2antrr 726 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) ∧ 𝑖 ∈ 𝐼) → (mulGrp‘𝑆) ∈ Mnd) | 
| 49 | 32, 33, 48, 23, 29 | mulgnn0cld 19114 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) ∧ 𝑖 ∈ 𝐼) → ((𝑏‘𝑖) ↑ 𝐿) ∈ 𝐾) | 
| 50 | 32, 33, 48, 23, 31 | mulgnn0cld 19114 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) ∧ 𝑖 ∈ 𝐼) → ((𝑏‘𝑖) ↑ (𝐴‘𝑖)) ∈ 𝐾) | 
| 51 |  | eqidd 2737 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) → (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ 𝐿)) = (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ 𝐿))) | 
| 52 |  | eqidd 2737 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) → (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝐴‘𝑖))) = (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝐴‘𝑖)))) | 
| 53 | 5 | mptexd 7245 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ 𝐿)) ∈ V) | 
| 54 | 53 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) → (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ 𝐿)) ∈ V) | 
| 55 |  | fvexd 6920 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) → (1r‘𝑆) ∈ V) | 
| 56 |  | funmpt 6603 | . . . . . . . . . . 11
⊢ Fun
(𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ 𝐿)) | 
| 57 | 56 | a1i 11 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) → Fun (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ 𝐿))) | 
| 58 | 19 | psrbagfsupp 21940 | . . . . . . . . . . . 12
⊢ (𝑏 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} → 𝑏 finSupp 0) | 
| 59 | 18, 58 | syl 17 | . . . . . . . . . . 11
⊢ (𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} → 𝑏 finSupp 0) | 
| 60 | 59 | adantl 481 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) → 𝑏 finSupp 0) | 
| 61 | 22 | feqmptd 6976 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) → 𝑏 = (𝑖 ∈ 𝐼 ↦ (𝑏‘𝑖))) | 
| 62 | 61 | oveq1d 7447 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) → (𝑏 supp 0) = ((𝑖 ∈ 𝐼 ↦ (𝑏‘𝑖)) supp 0)) | 
| 63 | 62 | eqimsscd 4040 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) → ((𝑖 ∈ 𝐼 ↦ (𝑏‘𝑖)) supp 0) ⊆ (𝑏 supp 0)) | 
| 64 | 32, 42, 33 | mulg0 19093 | . . . . . . . . . . . 12
⊢ (𝑘 ∈ 𝐾 → (0 ↑ 𝑘) = (1r‘𝑆)) | 
| 65 | 64 | adantl 481 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) ∧ 𝑘 ∈ 𝐾) → (0 ↑ 𝑘) = (1r‘𝑆)) | 
| 66 |  | 0zd 12627 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) → 0 ∈ ℤ) | 
| 67 | 63, 65, 23, 29, 66 | suppssov1 8223 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) → ((𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ 𝐿)) supp (1r‘𝑆)) ⊆ (𝑏 supp 0)) | 
| 68 | 54, 55, 57, 60, 67 | fsuppsssuppgd 9423 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) → (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ 𝐿)) finSupp (1r‘𝑆)) | 
| 69 | 5 | mptexd 7245 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝐴‘𝑖))) ∈ V) | 
| 70 | 69 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) → (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝐴‘𝑖))) ∈ V) | 
| 71 |  | funmpt 6603 | . . . . . . . . . . 11
⊢ Fun
(𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝐴‘𝑖))) | 
| 72 | 71 | a1i 11 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) → Fun (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝐴‘𝑖)))) | 
| 73 | 63, 65, 23, 31, 66 | suppssov1 8223 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) → ((𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝐴‘𝑖))) supp (1r‘𝑆)) ⊆ (𝑏 supp 0)) | 
| 74 | 70, 55, 72, 60, 73 | fsuppsssuppgd 9423 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) → (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝐴‘𝑖))) finSupp (1r‘𝑆)) | 
| 75 | 32, 42, 35, 44, 6, 49, 50, 51, 52, 68, 74 | gsummptfsadd 19943 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) → ((mulGrp‘𝑆) Σg (𝑖 ∈ 𝐼 ↦ (((𝑏‘𝑖) ↑ 𝐿) · ((𝑏‘𝑖) ↑ (𝐴‘𝑖))))) = (((mulGrp‘𝑆) Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ 𝐿))) ·
((mulGrp‘𝑆)
Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝐴‘𝑖)))))) | 
| 76 |  | eqid 2736 | . . . . . . . . . 10
⊢ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} = {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} | 
| 77 |  | mhphf.h | . . . . . . . . . . 11
⊢ 𝐻 = (𝐼 mHomP 𝑈) | 
| 78 |  | mhphf.x | . . . . . . . . . . 11
⊢ (𝜑 → 𝑋 ∈ (𝐻‘𝑁)) | 
| 79 | 77, 78 | mhprcl 22148 | . . . . . . . . . 10
⊢ (𝜑 → 𝑁 ∈
ℕ0) | 
| 80 | 19, 76, 32, 33, 5, 47, 28, 79 | mhphflem 42611 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) → ((mulGrp‘𝑆) Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ 𝐿))) = (𝑁 ↑ 𝐿)) | 
| 81 | 80 | oveq1d 7447 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) → (((mulGrp‘𝑆) Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ 𝐿))) ·
((mulGrp‘𝑆)
Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝐴‘𝑖))))) = ((𝑁 ↑ 𝐿) ·
((mulGrp‘𝑆)
Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝐴‘𝑖)))))) | 
| 82 | 40, 75, 81 | 3eqtrd 2780 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) → ((mulGrp‘𝑆) Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (((𝐼 × {𝐿}) ∘f · 𝐴)‘𝑖)))) = ((𝑁 ↑ 𝐿) ·
((mulGrp‘𝑆)
Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝐴‘𝑖)))))) | 
| 83 | 82 | oveq2d 7448 | . . . . . 6
⊢ ((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) → ((𝑋‘𝑏) ·
((mulGrp‘𝑆)
Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (((𝐼 × {𝐿}) ∘f · 𝐴)‘𝑖))))) = ((𝑋‘𝑏) · ((𝑁 ↑ 𝐿) ·
((mulGrp‘𝑆)
Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝐴‘𝑖))))))) | 
| 84 |  | eqid 2736 | . . . . . . . . . . 11
⊢ (𝐼 mPoly 𝑈) = (𝐼 mPoly 𝑈) | 
| 85 |  | eqid 2736 | . . . . . . . . . . 11
⊢
(Base‘𝑈) =
(Base‘𝑈) | 
| 86 |  | eqid 2736 | . . . . . . . . . . 11
⊢
(Base‘(𝐼 mPoly
𝑈)) = (Base‘(𝐼 mPoly 𝑈)) | 
| 87 | 77, 84, 86, 78 | mhpmpl 22149 | . . . . . . . . . . 11
⊢ (𝜑 → 𝑋 ∈ (Base‘(𝐼 mPoly 𝑈))) | 
| 88 | 84, 85, 86, 19, 87 | mplelf 22019 | . . . . . . . . . 10
⊢ (𝜑 → 𝑋:{ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈
Fin}⟶(Base‘𝑈)) | 
| 89 |  | mhphf.u | . . . . . . . . . . . . 13
⊢ 𝑈 = (𝑆 ↾s 𝑅) | 
| 90 | 89 | subrgbas 20582 | . . . . . . . . . . . 12
⊢ (𝑅 ∈ (SubRing‘𝑆) → 𝑅 = (Base‘𝑈)) | 
| 91 | 90, 26 | eqsstrrd 4018 | . . . . . . . . . . 11
⊢ (𝑅 ∈ (SubRing‘𝑆) → (Base‘𝑈) ⊆ 𝐾) | 
| 92 | 24, 91 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 → (Base‘𝑈) ⊆ 𝐾) | 
| 93 | 88, 92 | fssd 6752 | . . . . . . . . 9
⊢ (𝜑 → 𝑋:{ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}⟶𝐾) | 
| 94 | 93 | ffvelcdmda 7103 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → (𝑋‘𝑏) ∈ 𝐾) | 
| 95 | 18, 94 | sylan2 593 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) → (𝑋‘𝑏) ∈ 𝐾) | 
| 96 | 32, 33, 47, 79, 28 | mulgnn0cld 19114 | . . . . . . . 8
⊢ (𝜑 → (𝑁 ↑ 𝐿) ∈ 𝐾) | 
| 97 | 96 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) → (𝑁 ↑ 𝐿) ∈ 𝐾) | 
| 98 | 5 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → 𝐼 ∈ V) | 
| 99 | 13 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → 𝑆 ∈ CRing) | 
| 100 | 1 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → 𝐴 ∈ (𝐾 ↑m 𝐼)) | 
| 101 |  | simpr 484 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → 𝑏 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈
Fin}) | 
| 102 | 19, 25, 14, 33, 98, 99, 100, 101 | evlsvvvallem 42576 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) →
((mulGrp‘𝑆)
Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝐴‘𝑖)))) ∈ 𝐾) | 
| 103 | 18, 102 | sylan2 593 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) → ((mulGrp‘𝑆) Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝐴‘𝑖)))) ∈ 𝐾) | 
| 104 | 25, 34, 43, 95, 97, 103 | crng12d 20256 | . . . . . 6
⊢ ((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) → ((𝑋‘𝑏) · ((𝑁 ↑ 𝐿) ·
((mulGrp‘𝑆)
Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝐴‘𝑖)))))) = ((𝑁 ↑ 𝐿) · ((𝑋‘𝑏) ·
((mulGrp‘𝑆)
Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝐴‘𝑖))))))) | 
| 105 | 83, 104 | eqtrd 2776 | . . . . 5
⊢ ((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) → ((𝑋‘𝑏) ·
((mulGrp‘𝑆)
Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (((𝐼 × {𝐿}) ∘f · 𝐴)‘𝑖))))) = ((𝑁 ↑ 𝐿) · ((𝑋‘𝑏) ·
((mulGrp‘𝑆)
Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝐴‘𝑖))))))) | 
| 106 | 105 | mpteq2dva 5241 | . . . 4
⊢ (𝜑 → (𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ↦ ((𝑋‘𝑏) ·
((mulGrp‘𝑆)
Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (((𝐼 × {𝐿}) ∘f · 𝐴)‘𝑖)))))) = (𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ↦ ((𝑁 ↑ 𝐿) · ((𝑋‘𝑏) ·
((mulGrp‘𝑆)
Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝐴‘𝑖)))))))) | 
| 107 | 106 | oveq2d 7448 | . . 3
⊢ (𝜑 → (𝑆 Σg (𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ↦ ((𝑋‘𝑏) ·
((mulGrp‘𝑆)
Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (((𝐼 × {𝐿}) ∘f · 𝐴)‘𝑖))))))) = (𝑆 Σg (𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ↦ ((𝑁 ↑ 𝐿) · ((𝑋‘𝑏) ·
((mulGrp‘𝑆)
Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝐴‘𝑖))))))))) | 
| 108 |  | eqid 2736 | . . . 4
⊢
(0g‘𝑆) = (0g‘𝑆) | 
| 109 |  | ovex 7465 | . . . . . . 7
⊢
(ℕ0 ↑m 𝐼) ∈ V | 
| 110 | 109 | rabex 5338 | . . . . . 6
⊢ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∈
V | 
| 111 | 110 | rabex 5338 | . . . . 5
⊢ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ∈ V | 
| 112 | 111 | a1i 11 | . . . 4
⊢ (𝜑 → {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ∈ V) | 
| 113 | 45 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → 𝑆 ∈ Ring) | 
| 114 | 25, 34, 113, 94, 102 | ringcld 20258 | . . . . 5
⊢ ((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → ((𝑋‘𝑏) ·
((mulGrp‘𝑆)
Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝐴‘𝑖))))) ∈ 𝐾) | 
| 115 | 18, 114 | sylan2 593 | . . . 4
⊢ ((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) → ((𝑋‘𝑏) ·
((mulGrp‘𝑆)
Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝐴‘𝑖))))) ∈ 𝐾) | 
| 116 |  | ssrab2 4079 | . . . . . 6
⊢ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ⊆ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} | 
| 117 |  | mptss 6059 | . . . . . 6
⊢ ({𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ⊆ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} → (𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ↦ ((𝑋‘𝑏) ·
((mulGrp‘𝑆)
Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝐴‘𝑖)))))) ⊆ (𝑏 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ ((𝑋‘𝑏) ·
((mulGrp‘𝑆)
Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝐴‘𝑖))))))) | 
| 118 | 116, 117 | mp1i 13 | . . . . 5
⊢ (𝜑 → (𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ↦ ((𝑋‘𝑏) ·
((mulGrp‘𝑆)
Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝐴‘𝑖)))))) ⊆ (𝑏 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ ((𝑋‘𝑏) ·
((mulGrp‘𝑆)
Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝐴‘𝑖))))))) | 
| 119 | 19, 84, 89, 86, 25, 14, 33, 34, 5, 13, 24, 87, 1 | evlsvvvallem2 42577 | . . . . 5
⊢ (𝜑 → (𝑏 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ ((𝑋‘𝑏) ·
((mulGrp‘𝑆)
Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝐴‘𝑖)))))) finSupp (0g‘𝑆)) | 
| 120 | 118, 119 | fsuppss 9424 | . . . 4
⊢ (𝜑 → (𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ↦ ((𝑋‘𝑏) ·
((mulGrp‘𝑆)
Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝐴‘𝑖)))))) finSupp (0g‘𝑆)) | 
| 121 | 25, 108, 34, 45, 112, 96, 115, 120 | gsummulc2 20315 | . . 3
⊢ (𝜑 → (𝑆 Σg (𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ↦ ((𝑁 ↑ 𝐿) · ((𝑋‘𝑏) ·
((mulGrp‘𝑆)
Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝐴‘𝑖)))))))) = ((𝑁 ↑ 𝐿) · (𝑆 Σg (𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ↦ ((𝑋‘𝑏) ·
((mulGrp‘𝑆)
Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝐴‘𝑖))))))))) | 
| 122 | 107, 121 | eqtrd 2776 | . 2
⊢ (𝜑 → (𝑆 Σg (𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ↦ ((𝑋‘𝑏) ·
((mulGrp‘𝑆)
Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (((𝐼 × {𝐿}) ∘f · 𝐴)‘𝑖))))))) = ((𝑁 ↑ 𝐿) · (𝑆 Σg (𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ↦ ((𝑋‘𝑏) ·
((mulGrp‘𝑆)
Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝐴‘𝑖))))))))) | 
| 123 |  | mhphf.q | . . 3
⊢ 𝑄 = ((𝐼 evalSub 𝑆)‘𝑅) | 
| 124 | 25 | fvexi 6919 | . . . . 5
⊢ 𝐾 ∈ V | 
| 125 | 124 | a1i 11 | . . . 4
⊢ (𝜑 → 𝐾 ∈ V) | 
| 126 | 25, 34 | ringcl 20248 | . . . . . . 7
⊢ ((𝑆 ∈ Ring ∧ 𝑗 ∈ 𝐾 ∧ 𝑘 ∈ 𝐾) → (𝑗 · 𝑘) ∈ 𝐾) | 
| 127 | 45, 126 | syl3an1 1163 | . . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐾 ∧ 𝑘 ∈ 𝐾) → (𝑗 · 𝑘) ∈ 𝐾) | 
| 128 | 127 | 3expb 1120 | . . . . 5
⊢ ((𝜑 ∧ (𝑗 ∈ 𝐾 ∧ 𝑘 ∈ 𝐾)) → (𝑗 · 𝑘) ∈ 𝐾) | 
| 129 |  | fconst6g 6796 | . . . . . 6
⊢ (𝐿 ∈ 𝐾 → (𝐼 × {𝐿}):𝐼⟶𝐾) | 
| 130 | 28, 129 | syl 17 | . . . . 5
⊢ (𝜑 → (𝐼 × {𝐿}):𝐼⟶𝐾) | 
| 131 |  | inidm 4226 | . . . . 5
⊢ (𝐼 ∩ 𝐼) = 𝐼 | 
| 132 | 128, 130,
3, 5, 5, 131 | off 7716 | . . . 4
⊢ (𝜑 → ((𝐼 × {𝐿}) ∘f · 𝐴):𝐼⟶𝐾) | 
| 133 | 125, 5, 132 | elmapdd 8882 | . . 3
⊢ (𝜑 → ((𝐼 × {𝐿}) ∘f · 𝐴) ∈ (𝐾 ↑m 𝐼)) | 
| 134 | 123, 77, 89, 19, 76, 25, 14, 33, 34, 13, 24, 78, 133 | evlsmhpvvval 42610 | . 2
⊢ (𝜑 → ((𝑄‘𝑋)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = (𝑆 Σg (𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ↦ ((𝑋‘𝑏) ·
((mulGrp‘𝑆)
Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (((𝐼 × {𝐿}) ∘f · 𝐴)‘𝑖)))))))) | 
| 135 | 123, 77, 89, 19, 76, 25, 14, 33, 34, 13, 24, 78, 1 | evlsmhpvvval 42610 | . . 3
⊢ (𝜑 → ((𝑄‘𝑋)‘𝐴) = (𝑆 Σg (𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ↦ ((𝑋‘𝑏) ·
((mulGrp‘𝑆)
Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝐴‘𝑖)))))))) | 
| 136 | 135 | oveq2d 7448 | . 2
⊢ (𝜑 → ((𝑁 ↑ 𝐿) · ((𝑄‘𝑋)‘𝐴)) = ((𝑁 ↑ 𝐿) · (𝑆 Σg (𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ↦ ((𝑋‘𝑏) ·
((mulGrp‘𝑆)
Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝐴‘𝑖))))))))) | 
| 137 | 122, 134,
136 | 3eqtr4d 2786 | 1
⊢ (𝜑 → ((𝑄‘𝑋)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑋)‘𝐴))) |