This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑋 ) ‘ 𝐴 ) ) )