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