Metamath Proof Explorer


Theorem mhphf4

Description: A homogeneous polynomial defines a homogeneous function; this is mhphf3 with evalSub collapsed to eval . (Contributed by SN, 23-Nov-2024)

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

Proof

Step Hyp Ref Expression
1 mhphf4.q 𝑄 = ( 𝐼 eval 𝑆 )
2 mhphf4.h 𝐻 = ( 𝐼 mHomP 𝑆 )
3 mhphf4.k 𝐾 = ( Base ‘ 𝑆 )
4 mhphf4.f 𝐹 = ( 𝑆 freeLMod 𝐼 )
5 mhphf4.m 𝑀 = ( Base ‘ 𝐹 )
6 mhphf4.b = ( ·𝑠𝐹 )
7 mhphf4.x · = ( .r𝑆 )
8 mhphf4.e = ( .g ‘ ( mulGrp ‘ 𝑆 ) )
9 mhphf4.s ( 𝜑𝑆 ∈ CRing )
10 mhphf4.l ( 𝜑𝐿𝐾 )
11 mhphf4.p ( 𝜑𝑋 ∈ ( 𝐻𝑁 ) )
12 mhphf4.a ( 𝜑𝐴𝑀 )
13 1 3 evlval 𝑄 = ( ( 𝐼 evalSub 𝑆 ) ‘ 𝐾 )
14 eqid ( 𝐼 mHomP ( 𝑆s 𝐾 ) ) = ( 𝐼 mHomP ( 𝑆s 𝐾 ) )
15 eqid ( 𝑆s 𝐾 ) = ( 𝑆s 𝐾 )
16 9 crngringd ( 𝜑𝑆 ∈ Ring )
17 3 subrgid ( 𝑆 ∈ Ring → 𝐾 ∈ ( SubRing ‘ 𝑆 ) )
18 16 17 syl ( 𝜑𝐾 ∈ ( SubRing ‘ 𝑆 ) )
19 3 ressid ( 𝑆 ∈ CRing → ( 𝑆s 𝐾 ) = 𝑆 )
20 9 19 syl ( 𝜑 → ( 𝑆s 𝐾 ) = 𝑆 )
21 20 eqcomd ( 𝜑𝑆 = ( 𝑆s 𝐾 ) )
22 21 oveq2d ( 𝜑 → ( 𝐼 mHomP 𝑆 ) = ( 𝐼 mHomP ( 𝑆s 𝐾 ) ) )
23 2 22 eqtrid ( 𝜑𝐻 = ( 𝐼 mHomP ( 𝑆s 𝐾 ) ) )
24 23 fveq1d ( 𝜑 → ( 𝐻𝑁 ) = ( ( 𝐼 mHomP ( 𝑆s 𝐾 ) ) ‘ 𝑁 ) )
25 11 24 eleqtrd ( 𝜑𝑋 ∈ ( ( 𝐼 mHomP ( 𝑆s 𝐾 ) ) ‘ 𝑁 ) )
26 13 14 15 3 4 5 6 7 8 9 18 10 25 12 mhphf3 ( 𝜑 → ( ( 𝑄𝑋 ) ‘ ( 𝐿 𝐴 ) ) = ( ( 𝑁 𝐿 ) · ( ( 𝑄𝑋 ) ‘ 𝐴 ) ) )