Metamath Proof Explorer


Theorem mhphf2

Description: A homogeneous polynomial defines a homogeneous function; this is mhphf with simpler notation in the conclusion in exchange for a complex definition of .xb , which is based on frlmvscafval but without the finite support restriction ( frlmpws , frlmbas ) on the assignments A from variables to values.

TODO?: Polynomials ( df-mpl ) are defined to have a finite amount of terms (of finite degree). As such, any assignment may be replaced by an assignment with finite support (as only a finite amount of variables matter in a given polynomial, even if the set of variables is infinite). So the finite support restriction can be assumed without loss of generality. (Contributed by SN, 11-Nov-2024)

Ref Expression
Hypotheses mhphf2.q 𝑄 = ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 )
mhphf2.h 𝐻 = ( 𝐼 mHomP 𝑈 )
mhphf2.u 𝑈 = ( 𝑆s 𝑅 )
mhphf2.k 𝐾 = ( Base ‘ 𝑆 )
mhphf2.b = ( ·𝑠 ‘ ( ( ringLMod ‘ 𝑆 ) ↑s 𝐼 ) )
mhphf2.m · = ( .r𝑆 )
mhphf2.e = ( .g ‘ ( mulGrp ‘ 𝑆 ) )
mhphf2.s ( 𝜑𝑆 ∈ CRing )
mhphf2.r ( 𝜑𝑅 ∈ ( SubRing ‘ 𝑆 ) )
mhphf2.l ( 𝜑𝐿𝑅 )
mhphf2.x ( 𝜑𝑋 ∈ ( 𝐻𝑁 ) )
mhphf2.a ( 𝜑𝐴 ∈ ( 𝐾m 𝐼 ) )
Assertion mhphf2 ( 𝜑 → ( ( 𝑄𝑋 ) ‘ ( 𝐿 𝐴 ) ) = ( ( 𝑁 𝐿 ) · ( ( 𝑄𝑋 ) ‘ 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 mhphf2.q 𝑄 = ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 )
2 mhphf2.h 𝐻 = ( 𝐼 mHomP 𝑈 )
3 mhphf2.u 𝑈 = ( 𝑆s 𝑅 )
4 mhphf2.k 𝐾 = ( Base ‘ 𝑆 )
5 mhphf2.b = ( ·𝑠 ‘ ( ( ringLMod ‘ 𝑆 ) ↑s 𝐼 ) )
6 mhphf2.m · = ( .r𝑆 )
7 mhphf2.e = ( .g ‘ ( mulGrp ‘ 𝑆 ) )
8 mhphf2.s ( 𝜑𝑆 ∈ CRing )
9 mhphf2.r ( 𝜑𝑅 ∈ ( SubRing ‘ 𝑆 ) )
10 mhphf2.l ( 𝜑𝐿𝑅 )
11 mhphf2.x ( 𝜑𝑋 ∈ ( 𝐻𝑁 ) )
12 mhphf2.a ( 𝜑𝐴 ∈ ( 𝐾m 𝐼 ) )
13 eqid ( ( ringLMod ‘ 𝑆 ) ↑s 𝐼 ) = ( ( ringLMod ‘ 𝑆 ) ↑s 𝐼 )
14 eqid ( Base ‘ ( ( ringLMod ‘ 𝑆 ) ↑s 𝐼 ) ) = ( Base ‘ ( ( ringLMod ‘ 𝑆 ) ↑s 𝐼 ) )
15 rlmvsca ( .r𝑆 ) = ( ·𝑠 ‘ ( ringLMod ‘ 𝑆 ) )
16 eqid ( Scalar ‘ ( ringLMod ‘ 𝑆 ) ) = ( Scalar ‘ ( ringLMod ‘ 𝑆 ) )
17 eqid ( Base ‘ ( Scalar ‘ ( ringLMod ‘ 𝑆 ) ) ) = ( Base ‘ ( Scalar ‘ ( ringLMod ‘ 𝑆 ) ) )
18 fvexd ( 𝜑 → ( ringLMod ‘ 𝑆 ) ∈ V )
19 reldmmhp Rel dom mHomP
20 19 2 11 elfvov1 ( 𝜑𝐼 ∈ V )
21 4 subrgss ( 𝑅 ∈ ( SubRing ‘ 𝑆 ) → 𝑅𝐾 )
22 9 21 syl ( 𝜑𝑅𝐾 )
23 22 10 sseldd ( 𝜑𝐿𝐾 )
24 rlmsca ( 𝑆 ∈ CRing → 𝑆 = ( Scalar ‘ ( ringLMod ‘ 𝑆 ) ) )
25 8 24 syl ( 𝜑𝑆 = ( Scalar ‘ ( ringLMod ‘ 𝑆 ) ) )
26 25 fveq2d ( 𝜑 → ( Base ‘ 𝑆 ) = ( Base ‘ ( Scalar ‘ ( ringLMod ‘ 𝑆 ) ) ) )
27 4 26 eqtrid ( 𝜑𝐾 = ( Base ‘ ( Scalar ‘ ( ringLMod ‘ 𝑆 ) ) ) )
28 23 27 eleqtrd ( 𝜑𝐿 ∈ ( Base ‘ ( Scalar ‘ ( ringLMod ‘ 𝑆 ) ) ) )
29 4 oveq1i ( 𝐾m 𝐼 ) = ( ( Base ‘ 𝑆 ) ↑m 𝐼 )
30 12 29 eleqtrdi ( 𝜑𝐴 ∈ ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) )
31 rlmbas ( Base ‘ 𝑆 ) = ( Base ‘ ( ringLMod ‘ 𝑆 ) )
32 13 31 pwsbas ( ( ( ringLMod ‘ 𝑆 ) ∈ V ∧ 𝐼 ∈ V ) → ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) = ( Base ‘ ( ( ringLMod ‘ 𝑆 ) ↑s 𝐼 ) ) )
33 18 20 32 syl2anc ( 𝜑 → ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) = ( Base ‘ ( ( ringLMod ‘ 𝑆 ) ↑s 𝐼 ) ) )
34 30 33 eleqtrd ( 𝜑𝐴 ∈ ( Base ‘ ( ( ringLMod ‘ 𝑆 ) ↑s 𝐼 ) ) )
35 13 14 15 5 16 17 18 20 28 34 pwsvscafval ( 𝜑 → ( 𝐿 𝐴 ) = ( ( 𝐼 × { 𝐿 } ) ∘f ( .r𝑆 ) 𝐴 ) )
36 6 eqcomi ( .r𝑆 ) = ·
37 ofeq ( ( .r𝑆 ) = · → ∘f ( .r𝑆 ) = ∘f · )
38 36 37 mp1i ( 𝜑 → ∘f ( .r𝑆 ) = ∘f · )
39 38 oveqd ( 𝜑 → ( ( 𝐼 × { 𝐿 } ) ∘f ( .r𝑆 ) 𝐴 ) = ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) )
40 35 39 eqtrd ( 𝜑 → ( 𝐿 𝐴 ) = ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) )
41 40 fveq2d ( 𝜑 → ( ( 𝑄𝑋 ) ‘ ( 𝐿 𝐴 ) ) = ( ( 𝑄𝑋 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) )
42 1 2 3 4 6 7 8 9 10 11 12 mhphf ( 𝜑 → ( ( 𝑄𝑋 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 𝐿 ) · ( ( 𝑄𝑋 ) ‘ 𝐴 ) ) )
43 41 42 eqtrd ( 𝜑 → ( ( 𝑄𝑋 ) ‘ ( 𝐿 𝐴 ) ) = ( ( 𝑁 𝐿 ) · ( ( 𝑄𝑋 ) ‘ 𝐴 ) ) )