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