Theorem mhphf

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 ( QX ) which corresponds to X ). (Contributed by SN, 28-Jul-2024) (Proof shortened by SN, 8-Mar-2025)

	Ref	Expression
Hypotheses	mhphf.q	⊢ 𝑄 = ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 )
	mhphf.h	⊢ 𝐻 = ( 𝐼 mHomP 𝑈 )
	mhphf.u	⊢ 𝑈 = ( 𝑆 ↾s 𝑅 )
	mhphf.k	⊢ 𝐾 = ( Base ‘ 𝑆 )
	mhphf.m	⊢ · = ( .r ‘ 𝑆 )
	mhphf.e	⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑆 ) )
	mhphf.s	⊢ ( 𝜑 → 𝑆 ∈ CRing )
	mhphf.r	⊢ ( 𝜑 → 𝑅 ∈ ( SubRing ‘ 𝑆 ) )
	mhphf.l	⊢ ( 𝜑 → 𝐿 ∈ 𝑅 )
	mhphf.x	⊢ ( 𝜑 → 𝑋 ∈ ( 𝐻 ‘ 𝑁 ) )
	mhphf.a	⊢ ( 𝜑 → 𝐴 ∈ ( 𝐾 ↑m 𝐼 ) )
Assertion	mhphf	⊢ ( 𝜑 → ( ( 𝑄 ‘ 𝑋 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑋 ) ‘ 𝐴 ) ) )

Proof

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