Metamath Proof Explorer


Theorem mhphf3

Description: A homogeneous polynomial defines a homogeneous function; this is mhphf2 with the finite support restriction ( frlmpws , frlmbas ) on the assignments A from variables to values. See comment of mhphf2 . (Contributed by SN, 23-Nov-2024)

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

Proof

Step Hyp Ref Expression
1 mhphf3.q 𝑄 = ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 )
2 mhphf3.h 𝐻 = ( 𝐼 mHomP 𝑈 )
3 mhphf3.u 𝑈 = ( 𝑆s 𝑅 )
4 mhphf3.k 𝐾 = ( Base ‘ 𝑆 )
5 mhphf3.f 𝐹 = ( 𝑆 freeLMod 𝐼 )
6 mhphf3.m 𝑀 = ( Base ‘ 𝐹 )
7 mhphf3.b = ( ·𝑠𝐹 )
8 mhphf3.x · = ( .r𝑆 )
9 mhphf3.e = ( .g ‘ ( mulGrp ‘ 𝑆 ) )
10 mhphf3.s ( 𝜑𝑆 ∈ CRing )
11 mhphf3.r ( 𝜑𝑅 ∈ ( SubRing ‘ 𝑆 ) )
12 mhphf3.l ( 𝜑𝐿𝑅 )
13 mhphf3.p ( 𝜑𝑋 ∈ ( 𝐻𝑁 ) )
14 mhphf3.a ( 𝜑𝐴𝑀 )
15 reldmmhp Rel dom mHomP
16 15 2 13 elfvov1 ( 𝜑𝐼 ∈ V )
17 4 subrgss ( 𝑅 ∈ ( SubRing ‘ 𝑆 ) → 𝑅𝐾 )
18 11 17 syl ( 𝜑𝑅𝐾 )
19 18 12 sseldd ( 𝜑𝐿𝐾 )
20 5 6 4 16 19 14 7 8 frlmvscafval ( 𝜑 → ( 𝐿 𝐴 ) = ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) )
21 20 fveq2d ( 𝜑 → ( ( 𝑄𝑋 ) ‘ ( 𝐿 𝐴 ) ) = ( ( 𝑄𝑋 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) )
22 5 4 6 frlmbasmap ( ( 𝐼 ∈ V ∧ 𝐴𝑀 ) → 𝐴 ∈ ( 𝐾m 𝐼 ) )
23 16 14 22 syl2anc ( 𝜑𝐴 ∈ ( 𝐾m 𝐼 ) )
24 1 2 3 4 8 9 10 11 12 13 23 mhphf ( 𝜑 → ( ( 𝑄𝑋 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 𝐿 ) · ( ( 𝑄𝑋 ) ‘ 𝐴 ) ) )
25 21 24 eqtrd ( 𝜑 → ( ( 𝑄𝑋 ) ‘ ( 𝐿 𝐴 ) ) = ( ( 𝑁 𝐿 ) · ( ( 𝑄𝑋 ) ‘ 𝐴 ) ) )