Theorem mhphf 41634

Description: A homogeneous polynomial defines a homogeneous function. Equivalently, an algebraic form is a homogeneous function. (An algebraic form is the function corresponding to a homogeneous polynomial, which in this case is the (𝑄‘𝑋) which corresponds to 𝑋). (Contributed by SN, 28-Jul-2024.) (Proof shortened by SN, 8-Mar-2025.)

Hypotheses

Ref	Expression
mhphf.q	⊢ 𝑄 = ((𝐼 evalSub 𝑆)‘𝑅)
mhphf.h	⊢ 𝐻 = (𝐼 mHomP 𝑈)
mhphf.u	⊢ 𝑈 = (𝑆 ↾s 𝑅)
mhphf.k	⊢ 𝐾 = (Base‘𝑆)
mhphf.m	⊢ · = (.r‘𝑆)
mhphf.e	⊢ ↑ = (.g‘(mulGrp‘𝑆))
mhphf.i	⊢ (𝜑 → 𝐼 ∈ 𝑉)
mhphf.s	⊢ (𝜑 → 𝑆 ∈ CRing)
mhphf.r	⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆))
mhphf.l	⊢ (𝜑 → 𝐿 ∈ 𝑅)
mhphf.n	⊢ (𝜑 → 𝑁 ∈ ℕ0)
mhphf.x	⊢ (𝜑 → 𝑋 ∈ (𝐻‘𝑁))
mhphf.a	⊢ (𝜑 → 𝐴 ∈ (𝐾 ↑m 𝐼))

Assertion

Ref	Expression
mhphf	⊢ (𝜑 → ((𝑄‘𝑋)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑋)‘𝐴)))

Proof of Theorem mhphf

Dummy variables 𝑏 𝑖 𝑘 𝑗 𝑔 ℎ are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		mhphf.i	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐼 ∈ 𝑉)
2	1	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁}) → 𝐼 ∈ 𝑉)
3		mhphf.l	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐿 ∈ 𝑅)
4	3	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁}) → 𝐿 ∈ 𝑅)
5		mhphf.a	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐴 ∈ (𝐾 ↑m 𝐼))
6		elmapi 8849	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ∈ (𝐾 ↑m 𝐼) → 𝐴:𝐼⟶𝐾)
7	5, 6	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐴:𝐼⟶𝐾)
8	7	ffnd 6718	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐴 Fn 𝐼)
9	8	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁}) → 𝐴 Fn 𝐼)
10		eqidd 2732	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁}) ∧ 𝑖 ∈ 𝐼) → (𝐴‘𝑖) = (𝐴‘𝑖))
11	2, 4, 9, 10	ofc1 7700	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁}) ∧ 𝑖 ∈ 𝐼) → (((𝐼 × {𝐿}) ∘f · 𝐴)‘𝑖) = (𝐿 · (𝐴‘𝑖)))
12	11	oveq2d 7428	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁}) ∧ 𝑖 ∈ 𝐼) → ((𝑏‘𝑖) ↑ (((𝐼 × {𝐿}) ∘f · 𝐴)‘𝑖)) = ((𝑏‘𝑖) ↑ (𝐿 · (𝐴‘𝑖))))
13		mhphf.s	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑆 ∈ CRing)
14		eqid 2731	. . . . . . . . . . . . . . 15 ⊢ (mulGrp‘𝑆) = (mulGrp‘𝑆)
15	14	crngmgp 20142	. . . . . . . . . . . . . 14 ⊢ (𝑆 ∈ CRing → (mulGrp‘𝑆) ∈ CMnd)
16	13, 15	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → (mulGrp‘𝑆) ∈ CMnd)
17	16	ad2antrr 723	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁}) ∧ 𝑖 ∈ 𝐼) → (mulGrp‘𝑆) ∈ CMnd)
18		elrabi 3677	. . . . . . . . . . . . . . 15 ⊢ (𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} → 𝑏 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin})
19		eqid 2731	. . . . . . . . . . . . . . . 16 ⊢ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}
20	19	psrbagf 21781	. . . . . . . . . . . . . . 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 7086	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁}) ∧ 𝑖 ∈ 𝐼) → (𝑏‘𝑖) ∈ ℕ0)
24		mhphf.r	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆))
25		mhphf.k	. . . . . . . . . . . . . . . 16 ⊢ 𝐾 = (Base‘𝑆)
26	25	subrgss 20470	. . . . . . . . . . . . . . 15 ⊢ (𝑅 ∈ (SubRing‘𝑆) → 𝑅 ⊆ 𝐾)
27	24, 26	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑅 ⊆ 𝐾)
28	27, 3	sseldd 3983	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐿 ∈ 𝐾)
29	28	ad2antrr 723	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁}) ∧ 𝑖 ∈ 𝐼) → 𝐿 ∈ 𝐾)
30	7	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁}) → 𝐴:𝐼⟶𝐾)
31	30	ffvelcdmda 7086	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁}) ∧ 𝑖 ∈ 𝐼) → (𝐴‘𝑖) ∈ 𝐾)
32	14, 25	mgpbas 20041	. . . . . . . . . . . . 13 ⊢ 𝐾 = (Base‘(mulGrp‘𝑆))
33		mhphf.e	. . . . . . . . . . . . 13 ⊢ ↑ = (.g‘(mulGrp‘𝑆))
34		mhphf.m	. . . . . . . . . . . . . 14 ⊢ · = (.r‘𝑆)
35	14, 34	mgpplusg 20039	. . . . . . . . . . . . 13 ⊢ · = (+g‘(mulGrp‘𝑆))
36	32, 33, 35	mulgnn0di 19741	. . . . . . . . . . . 12 ⊢ (((mulGrp‘𝑆) ∈ CMnd ∧ ((𝑏‘𝑖) ∈ ℕ0 ∧ 𝐿 ∈ 𝐾 ∧ (𝐴‘𝑖) ∈ 𝐾)) → ((𝑏‘𝑖) ↑ (𝐿 · (𝐴‘𝑖))) = (((𝑏‘𝑖) ↑ 𝐿) · ((𝑏‘𝑖) ↑ (𝐴‘𝑖))))
37	17, 23, 29, 31, 36	syl13anc 1371	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁}) ∧ 𝑖 ∈ 𝐼) → ((𝑏‘𝑖) ↑ (𝐿 · (𝐴‘𝑖))) = (((𝑏‘𝑖) ↑ 𝐿) · ((𝑏‘𝑖) ↑ (𝐴‘𝑖))))
38	12, 37	eqtrd 2771	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁}) ∧ 𝑖 ∈ 𝐼) → ((𝑏‘𝑖) ↑ (((𝐼 × {𝐿}) ∘f · 𝐴)‘𝑖)) = (((𝑏‘𝑖) ↑ 𝐿) · ((𝑏‘𝑖) ↑ (𝐴‘𝑖))))
39	38	mpteq2dva 5248	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁}) → (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (((𝐼 × {𝐿}) ∘f · 𝐴)‘𝑖))) = (𝑖 ∈ 𝐼 ↦ (((𝑏‘𝑖) ↑ 𝐿) · ((𝑏‘𝑖) ↑ (𝐴‘𝑖)))))
40	39	oveq2d 7428	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁}) → ((mulGrp‘𝑆) Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (((𝐼 × {𝐿}) ∘f · 𝐴)‘𝑖)))) = ((mulGrp‘𝑆) Σg (𝑖 ∈ 𝐼 ↦ (((𝑏‘𝑖) ↑ 𝐿) · ((𝑏‘𝑖) ↑ (𝐴‘𝑖))))))
41		eqid 2731	. . . . . . . . . 10 ⊢ (1r‘𝑆) = (1r‘𝑆)
42	14, 41	ringidval 20084	. . . . . . . . 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 20147	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑆 ∈ Ring)
46	14	ringmgp 20140	. . . . . . . . . . . 12 ⊢ (𝑆 ∈ Ring → (mulGrp‘𝑆) ∈ Mnd)
47	45, 46	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (mulGrp‘𝑆) ∈ Mnd)
48	47	ad2antrr 723	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁}) ∧ 𝑖 ∈ 𝐼) → (mulGrp‘𝑆) ∈ Mnd)
49	32, 33, 48, 23, 29	mulgnn0cld 19018	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁}) ∧ 𝑖 ∈ 𝐼) → ((𝑏‘𝑖) ↑ 𝐿) ∈ 𝐾)
50	32, 33, 48, 23, 31	mulgnn0cld 19018	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁}) ∧ 𝑖 ∈ 𝐼) → ((𝑏‘𝑖) ↑ (𝐴‘𝑖)) ∈ 𝐾)
51		eqidd 2732	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁}) → (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ 𝐿)) = (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ 𝐿)))
52		eqidd 2732	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁}) → (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝐴‘𝑖))) = (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝐴‘𝑖))))
53	1	mptexd 7228	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ 𝐿)) ∈ V)
54	53	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁}) → (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ 𝐿)) ∈ V)
55		fvexd 6906	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁}) → (1r‘𝑆) ∈ V)
56		funmpt 6586	. . . . . . . . . . 11 ⊢ Fun (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ 𝐿))
57	56	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁}) → Fun (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ 𝐿)))
58	19	psrbagfsupp 21783	. . . . . . . . . . . 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 6960	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁}) → 𝑏 = (𝑖 ∈ 𝐼 ↦ (𝑏‘𝑖)))
62	61	oveq1d 7427	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁}) → (𝑏 supp 0) = ((𝑖 ∈ 𝐼 ↦ (𝑏‘𝑖)) supp 0))
63	62	eqimsscd 4039	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁}) → ((𝑖 ∈ 𝐼 ↦ (𝑏‘𝑖)) supp 0) ⊆ (𝑏 supp 0))
64	32, 42, 33	mulg0 19000	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ 𝐾 → (0 ↑ 𝑘) = (1r‘𝑆))
65	64	adantl 481	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁}) ∧ 𝑘 ∈ 𝐾) → (0 ↑ 𝑘) = (1r‘𝑆))
66		0zd 12577	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁}) → 0 ∈ ℤ)
67	63, 65, 23, 29, 66	suppssov1 8188	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁}) → ((𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ 𝐿)) supp (1r‘𝑆)) ⊆ (𝑏 supp 0))
68	54, 55, 57, 60, 67	fsuppsssuppgd 41533	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁}) → (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ 𝐿)) finSupp (1r‘𝑆))
69	1	mptexd 7228	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝐴‘𝑖))) ∈ V)
70	69	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁}) → (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝐴‘𝑖))) ∈ V)
71		funmpt 6586	. . . . . . . . . . 11 ⊢ Fun (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝐴‘𝑖)))
72	71	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁}) → Fun (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝐴‘𝑖))))
73	63, 65, 23, 31, 66	suppssov1 8188	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁}) → ((𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝐴‘𝑖))) supp (1r‘𝑆)) ⊆ (𝑏 supp 0))
74	70, 55, 72, 60, 73	fsuppsssuppgd 41533	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁}) → (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝐴‘𝑖))) finSupp (1r‘𝑆))
75	32, 42, 35, 44, 2, 49, 50, 51, 52, 68, 74	gsummptfsadd 19840	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁}) → ((mulGrp‘𝑆) Σg (𝑖 ∈ 𝐼 ↦ (((𝑏‘𝑖) ↑ 𝐿) · ((𝑏‘𝑖) ↑ (𝐴‘𝑖))))) = (((mulGrp‘𝑆) Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ 𝐿))) · ((mulGrp‘𝑆) Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝐴‘𝑖))))))
76		eqid 2731	. . . . . . . . . 10 ⊢ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} = {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁}
77		mhphf.n	. . . . . . . . . 10 ⊢ (𝜑 → 𝑁 ∈ ℕ0)
78	19, 76, 32, 33, 1, 47, 28, 77	mhphflem 41633	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁}) → ((mulGrp‘𝑆) Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ 𝐿))) = (𝑁 ↑ 𝐿))
79	78	oveq1d 7427	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁}) → (((mulGrp‘𝑆) Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ 𝐿))) · ((mulGrp‘𝑆) Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝐴‘𝑖))))) = ((𝑁 ↑ 𝐿) · ((mulGrp‘𝑆) Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝐴‘𝑖))))))
80	40, 75, 79	3eqtrd 2775	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁}) → ((mulGrp‘𝑆) Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (((𝐼 × {𝐿}) ∘f · 𝐴)‘𝑖)))) = ((𝑁 ↑ 𝐿) · ((mulGrp‘𝑆) Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝐴‘𝑖))))))
81	80	oveq2d 7428	. . . . . 6 ⊢ ((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁}) → ((𝑋‘𝑏) · ((mulGrp‘𝑆) Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (((𝐼 × {𝐿}) ∘f · 𝐴)‘𝑖))))) = ((𝑋‘𝑏) · ((𝑁 ↑ 𝐿) · ((mulGrp‘𝑆) Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝐴‘𝑖)))))))
82		eqid 2731	. . . . . . . . . . 11 ⊢ (𝐼 mPoly 𝑈) = (𝐼 mPoly 𝑈)
83		eqid 2731	. . . . . . . . . . 11 ⊢ (Base‘𝑈) = (Base‘𝑈)
84		eqid 2731	. . . . . . . . . . 11 ⊢ (Base‘(𝐼 mPoly 𝑈)) = (Base‘(𝐼 mPoly 𝑈))
85		mhphf.h	. . . . . . . . . . . 12 ⊢ 𝐻 = (𝐼 mHomP 𝑈)
86		mhphf.u	. . . . . . . . . . . . . 14 ⊢ 𝑈 = (𝑆 ↾s 𝑅)
87	86	ovexi 7446	. . . . . . . . . . . . 13 ⊢ 𝑈 ∈ V
88	87	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑈 ∈ V)
89		mhphf.x	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑋 ∈ (𝐻‘𝑁))
90	85, 82, 84, 1, 88, 77, 89	mhpmpl 21996	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑋 ∈ (Base‘(𝐼 mPoly 𝑈)))
91	82, 83, 84, 19, 90	mplelf 21868	. . . . . . . . . 10 ⊢ (𝜑 → 𝑋:{ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}⟶(Base‘𝑈))
92	86	subrgbas 20479	. . . . . . . . . . . 12 ⊢ (𝑅 ∈ (SubRing‘𝑆) → 𝑅 = (Base‘𝑈))
93	92, 26	eqsstrrd 4021	. . . . . . . . . . 11 ⊢ (𝑅 ∈ (SubRing‘𝑆) → (Base‘𝑈) ⊆ 𝐾)
94	24, 93	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (Base‘𝑈) ⊆ 𝐾)
95	91, 94	fssd 6735	. . . . . . . . 9 ⊢ (𝜑 → 𝑋:{ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}⟶𝐾)
96	95	ffvelcdmda 7086	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}) → (𝑋‘𝑏) ∈ 𝐾)
97	18, 96	sylan2 592	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁}) → (𝑋‘𝑏) ∈ 𝐾)
98	32, 33, 47, 77, 28	mulgnn0cld 19018	. . . . . . . 8 ⊢ (𝜑 → (𝑁 ↑ 𝐿) ∈ 𝐾)
99	98	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁}) → (𝑁 ↑ 𝐿) ∈ 𝐾)
100	1	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}) → 𝐼 ∈ 𝑉)
101	13	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}) → 𝑆 ∈ CRing)
102	5	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}) → 𝐴 ∈ (𝐾 ↑m 𝐼))
103		simpr 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}) → 𝑏 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin})
104	19, 25, 14, 33, 100, 101, 102, 103	evlsvvvallem 41598	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}) → ((mulGrp‘𝑆) Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝐴‘𝑖)))) ∈ 𝐾)
105	18, 104	sylan2 592	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁}) → ((mulGrp‘𝑆) Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝐴‘𝑖)))) ∈ 𝐾)
106	25, 34, 43, 97, 99, 105	crng12d 41555	. . . . . 6 ⊢ ((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁}) → ((𝑋‘𝑏) · ((𝑁 ↑ 𝐿) · ((mulGrp‘𝑆) Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝐴‘𝑖)))))) = ((𝑁 ↑ 𝐿) · ((𝑋‘𝑏) · ((mulGrp‘𝑆) Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝐴‘𝑖)))))))
107	81, 106	eqtrd 2771	. . . . 5 ⊢ ((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁}) → ((𝑋‘𝑏) · ((mulGrp‘𝑆) Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (((𝐼 × {𝐿}) ∘f · 𝐴)‘𝑖))))) = ((𝑁 ↑ 𝐿) · ((𝑋‘𝑏) · ((mulGrp‘𝑆) Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝐴‘𝑖)))))))
108	107	mpteq2dva 5248	. . . 4 ⊢ (𝜑 → (𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ↦ ((𝑋‘𝑏) · ((mulGrp‘𝑆) Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (((𝐼 × {𝐿}) ∘f · 𝐴)‘𝑖)))))) = (𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ↦ ((𝑁 ↑ 𝐿) · ((𝑋‘𝑏) · ((mulGrp‘𝑆) Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝐴‘𝑖))))))))
109	108	oveq2d 7428	. . 3 ⊢ (𝜑 → (𝑆 Σg (𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ↦ ((𝑋‘𝑏) · ((mulGrp‘𝑆) Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (((𝐼 × {𝐿}) ∘f · 𝐴)‘𝑖))))))) = (𝑆 Σg (𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ↦ ((𝑁 ↑ 𝐿) · ((𝑋‘𝑏) · ((mulGrp‘𝑆) Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝐴‘𝑖)))))))))
110		eqid 2731	. . . 4 ⊢ (0g‘𝑆) = (0g‘𝑆)
111		ovex 7445	. . . . . . 7 ⊢ (ℕ0 ↑m 𝐼) ∈ V
112	111	rabex 5332	. . . . . 6 ⊢ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∈ V
113	112	rabex 5332	. . . . 5 ⊢ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∈ V
114	113	a1i 11	. . . 4 ⊢ (𝜑 → {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ∈ V)
115	45	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}) → 𝑆 ∈ Ring)
116	25, 34, 115, 96, 104	ringcld 20158	. . . . 5 ⊢ ((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}) → ((𝑋‘𝑏) · ((mulGrp‘𝑆) Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝐴‘𝑖))))) ∈ 𝐾)
117	18, 116	sylan2 592	. . . 4 ⊢ ((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁}) → ((𝑋‘𝑏) · ((mulGrp‘𝑆) Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝐴‘𝑖))))) ∈ 𝐾)
118		ssrab2 4077	. . . . . 6 ⊢ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ⊆ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}
119		mptss 6042	. . . . . 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 (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝐴‘𝑖)))))))
120	118, 119	mp1i 13	. . . . 5 ⊢ (𝜑 → (𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ↦ ((𝑋‘𝑏) · ((mulGrp‘𝑆) Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝐴‘𝑖)))))) ⊆ (𝑏 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ ((𝑋‘𝑏) · ((mulGrp‘𝑆) Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝐴‘𝑖)))))))
121	19, 82, 86, 84, 25, 14, 33, 34, 1, 13, 24, 90, 5	evlsvvvallem2 41599	. . . . 5 ⊢ (𝜑 → (𝑏 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ ((𝑋‘𝑏) · ((mulGrp‘𝑆) Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝐴‘𝑖)))))) finSupp (0g‘𝑆))
122	120, 121	fsuppss 41534	. . . 4 ⊢ (𝜑 → (𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ↦ ((𝑋‘𝑏) · ((mulGrp‘𝑆) Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝐴‘𝑖)))))) finSupp (0g‘𝑆))
123	25, 110, 34, 45, 114, 98, 117, 122	gsummulc2 20212	. . 3 ⊢ (𝜑 → (𝑆 Σg (𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ↦ ((𝑁 ↑ 𝐿) · ((𝑋‘𝑏) · ((mulGrp‘𝑆) Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝐴‘𝑖)))))))) = ((𝑁 ↑ 𝐿) · (𝑆 Σg (𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ↦ ((𝑋‘𝑏) · ((mulGrp‘𝑆) Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝐴‘𝑖)))))))))
124	109, 123	eqtrd 2771	. 2 ⊢ (𝜑 → (𝑆 Σg (𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ↦ ((𝑋‘𝑏) · ((mulGrp‘𝑆) Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (((𝐼 × {𝐿}) ∘f · 𝐴)‘𝑖))))))) = ((𝑁 ↑ 𝐿) · (𝑆 Σg (𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ↦ ((𝑋‘𝑏) · ((mulGrp‘𝑆) Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝐴‘𝑖)))))))))
125		mhphf.q	. . 3 ⊢ 𝑄 = ((𝐼 evalSub 𝑆)‘𝑅)
126	25	fvexi 6905	. . . . 5 ⊢ 𝐾 ∈ V
127	126	a1i 11	. . . 4 ⊢ (𝜑 → 𝐾 ∈ V)
128	25, 34	ringcl 20151	. . . . . . 7 ⊢ ((𝑆 ∈ Ring ∧ 𝑗 ∈ 𝐾 ∧ 𝑘 ∈ 𝐾) → (𝑗 · 𝑘) ∈ 𝐾)
129	45, 128	syl3an1 1162	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐾 ∧ 𝑘 ∈ 𝐾) → (𝑗 · 𝑘) ∈ 𝐾)
130	129	3expb 1119	. . . . 5 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝐾 ∧ 𝑘 ∈ 𝐾)) → (𝑗 · 𝑘) ∈ 𝐾)
131		fconst6g 6780	. . . . . 6 ⊢ (𝐿 ∈ 𝐾 → (𝐼 × {𝐿}):𝐼⟶𝐾)
132	28, 131	syl 17	. . . . 5 ⊢ (𝜑 → (𝐼 × {𝐿}):𝐼⟶𝐾)
133		inidm 4218	. . . . 5 ⊢ (𝐼 ∩ 𝐼) = 𝐼
134	130, 132, 7, 1, 1, 133	off 7692	. . . 4 ⊢ (𝜑 → ((𝐼 × {𝐿}) ∘f · 𝐴):𝐼⟶𝐾)
135	127, 1, 134	elmapdd 8841	. . 3 ⊢ (𝜑 → ((𝐼 × {𝐿}) ∘f · 𝐴) ∈ (𝐾 ↑m 𝐼))
136	125, 85, 86, 19, 76, 25, 14, 33, 34, 1, 13, 24, 77, 89, 135	evlsmhpvvval 41632	. 2 ⊢ (𝜑 → ((𝑄‘𝑋)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = (𝑆 Σg (𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ↦ ((𝑋‘𝑏) · ((mulGrp‘𝑆) Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (((𝐼 × {𝐿}) ∘f · 𝐴)‘𝑖))))))))
137	125, 85, 86, 19, 76, 25, 14, 33, 34, 1, 13, 24, 77, 89, 5	evlsmhpvvval 41632	. . 3 ⊢ (𝜑 → ((𝑄‘𝑋)‘𝐴) = (𝑆 Σg (𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ↦ ((𝑋‘𝑏) · ((mulGrp‘𝑆) Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝐴‘𝑖))))))))
138	137	oveq2d 7428	. 2 ⊢ (𝜑 → ((𝑁 ↑ 𝐿) · ((𝑄‘𝑋)‘𝐴)) = ((𝑁 ↑ 𝐿) · (𝑆 Σg (𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} ↦ ((𝑋‘𝑏) · ((mulGrp‘𝑆) Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝐴‘𝑖)))))))))
139	124, 136, 138	3eqtr4d 2781	1 ⊢ (𝜑 → ((𝑄‘𝑋)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑋)‘𝐴)))

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2105  {crab 3431  Vcvv 3473   ⊆ wss 3948  {csn 4628   class class class wbr 5148   ↦ cmpt 5231   × cxp 5674  ^◡ccnv 5675   “ cima 5679  Fun wfun 6537   Fn wfn 6538  ⟶wf 6539  ‘cfv 6543  (class class class)co 7412   ∘_f cof 7672   supp csupp 8151   ↑_m cmap 8826  Fincfn 8945   finSupp cfsupp 9367  0cc0 11116  ℕcn 12219  ℕ₀cn0 12479  ℤcz 12565  Basecbs 17151   ↾_s cress 17180  ._rcmulr 17205  0_gc0g 17392   Σ_g cgsu 17393  Mndcmnd 18665  ._gcmg 18993  CMndccmn 19696  mulGrpcmgp 20035  1_rcur 20082  Ringcrg 20134  CRingccrg 20135  SubRingcsubrg 20465  ℂ_fldccnfld 21233   mPoly cmpl 21769   evalSub ces 21944   mHomP cmhp 21983

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7729  ax-cnex 11172  ax-resscn 11173  ax-1cn 11174  ax-icn 11175  ax-addcl 11176  ax-addrcl 11177  ax-mulcl 11178  ax-mulrcl 11179  ax-mulcom 11180  ax-addass 11181  ax-mulass 11182  ax-distr 11183  ax-i2m1 11184  ax-1ne0 11185  ax-1rid 11186  ax-rnegex 11187  ax-rrecex 11188  ax-cnre 11189  ax-pre-lttri 11190  ax-pre-lttrn 11191  ax-pre-ltadd 11192  ax-pre-mulgt0 11193  ax-addf 11195  ax-mulf 11196

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-rmo 3375  df-reu 3376  df-rab 3432  df-v 3475  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-tp 4633  df-op 4635  df-uni 4909  df-int 4951  df-iun 4999  df-iin 5000  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-se 5632  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-isom 6552  df-riota 7368  df-ov 7415  df-oprab 7416  df-mpo 7417  df-of 7674  df-ofr 7675  df-om 7860  df-1st 7979  df-2nd 7980  df-supp 8152  df-frecs 8272  df-wrecs 8303  df-recs 8377  df-rdg 8416  df-1o 8472  df-er 8709  df-map 8828  df-pm 8829  df-ixp 8898  df-en 8946  df-dom 8947  df-sdom 8948  df-fin 8949  df-fsupp 9368  df-sup 9443  df-oi 9511  df-card 9940  df-pnf 11257  df-mnf 11258  df-xr 11259  df-ltxr 11260  df-le 11261  df-sub 11453  df-neg 11454  df-nn 12220  df-2 12282  df-3 12283  df-4 12284  df-5 12285  df-6 12286  df-7 12287  df-8 12288  df-9 12289  df-n0 12480  df-z 12566  df-dec 12685  df-uz 12830  df-fz 13492  df-fzo 13635  df-seq 13974  df-hash 14298  df-struct 17087  df-sets 17104  df-slot 17122  df-ndx 17134  df-base 17152  df-ress 17181  df-plusg 17217  df-mulr 17218  df-starv 17219  df-sca 17220  df-vsca 17221  df-ip 17222  df-tset 17223  df-ple 17224  df-ds 17226  df-unif 17227  df-hom 17228  df-cco 17229  df-0g 17394  df-gsum 17395  df-prds 17400  df-pws 17402  df-mre 17537  df-mrc 17538  df-acs 17540  df-mgm 18571  df-sgrp 18650  df-mnd 18666  df-mhm 18711  df-submnd 18712  df-grp 18864  df-minusg 18865  df-sbg 18866  df-mulg 18994  df-subg 19046  df-ghm 19135  df-cntz 19229  df-cmn 19698  df-abl 19699  df-mgp 20036  df-rng 20054  df-ur 20083  df-srg 20088  df-ring 20136  df-cring 20137  df-rhm 20370  df-subrng 20442  df-subrg 20467  df-lmod 20704  df-lss 20775  df-lsp 20815  df-cnfld 21234  df-assa 21718  df-asp 21719  df-ascl 21720  df-psr 21772  df-mvr 21773  df-mpl 21774  df-evls 21946  df-mhp 21990

This theorem is referenced by:  mhphf2  41635  mhphf3  41636