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.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
	mhphf3.s	⊢ ( 𝜑 → 𝑆 ∈ CRing )
	mhphf3.r	⊢ ( 𝜑 → 𝑅 ∈ ( SubRing ‘ 𝑆 ) )
	mhphf3.l	⊢ ( 𝜑 → 𝐿 ∈ 𝑅 )
	mhphf3.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
	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.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
11		mhphf3.s	⊢ ( 𝜑 → 𝑆 ∈ CRing )
12		mhphf3.r	⊢ ( 𝜑 → 𝑅 ∈ ( SubRing ‘ 𝑆 ) )
13		mhphf3.l	⊢ ( 𝜑 → 𝐿 ∈ 𝑅 )
14		mhphf3.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
15		mhphf3.p	⊢ ( 𝜑 → 𝑋 ∈ ( 𝐻 ‘ 𝑁 ) )
16		mhphf3.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑀 )
17	4	subrgss	⊢ ( 𝑅 ∈ ( SubRing ‘ 𝑆 ) → 𝑅 ⊆ 𝐾 )
18	12 17	syl	⊢ ( 𝜑 → 𝑅 ⊆ 𝐾 )
19	18 13	sseldd	⊢ ( 𝜑 → 𝐿 ∈ 𝐾 )
20	5 6 4 10 19 16 7 8	frlmvscafval	⊢ ( 𝜑 → ( 𝐿 ∙ 𝐴 ) = ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) )
21	20	fveq2d	⊢ ( 𝜑 → ( ( 𝑄 ‘ 𝑋 ) ‘ ( 𝐿 ∙ 𝐴 ) ) = ( ( 𝑄 ‘ 𝑋 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) )
22	5 4 6	frlmbasmap	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ 𝑀 ) → 𝐴 ∈ ( 𝐾 ↑m 𝐼 ) )
23	10 16 22	syl2anc	⊢ ( 𝜑 → 𝐴 ∈ ( 𝐾 ↑m 𝐼 ) )
24	1 2 3 4 8 9 10 11 12 13 14 15 23	mhphf	⊢ ( 𝜑 → ( ( 𝑄 ‘ 𝑋 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑋 ) ‘ 𝐴 ) ) )
25	21 24	eqtrd	⊢ ( 𝜑 → ( ( 𝑄 ‘ 𝑋 ) ‘ ( 𝐿 ∙ 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑋 ) ‘ 𝐴 ) ) )