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.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
	mhphf4.s	⊢ ( 𝜑 → 𝑆 ∈ CRing )
	mhphf4.l	⊢ ( 𝜑 → 𝐿 ∈ 𝐾 )
	mhphf4.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
	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.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
10		mhphf4.s	⊢ ( 𝜑 → 𝑆 ∈ CRing )
11		mhphf4.l	⊢ ( 𝜑 → 𝐿 ∈ 𝐾 )
12		mhphf4.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
13		mhphf4.p	⊢ ( 𝜑 → 𝑋 ∈ ( 𝐻 ‘ 𝑁 ) )
14		mhphf4.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑀 )
15	1 3	evlval	⊢ 𝑄 = ( ( 𝐼 evalSub 𝑆 ) ‘ 𝐾 )
16		eqid	⊢ ( 𝐼 mHomP ( 𝑆 ↾s 𝐾 ) ) = ( 𝐼 mHomP ( 𝑆 ↾s 𝐾 ) )
17		eqid	⊢ ( 𝑆 ↾s 𝐾 ) = ( 𝑆 ↾s 𝐾 )
18	10	crngringd	⊢ ( 𝜑 → 𝑆 ∈ Ring )
19	3	subrgid	⊢ ( 𝑆 ∈ Ring → 𝐾 ∈ ( SubRing ‘ 𝑆 ) )
20	18 19	syl	⊢ ( 𝜑 → 𝐾 ∈ ( SubRing ‘ 𝑆 ) )
21	3	ressid	⊢ ( 𝑆 ∈ CRing → ( 𝑆 ↾s 𝐾 ) = 𝑆 )
22	10 21	syl	⊢ ( 𝜑 → ( 𝑆 ↾s 𝐾 ) = 𝑆 )
23	22	eqcomd	⊢ ( 𝜑 → 𝑆 = ( 𝑆 ↾s 𝐾 ) )
24	23	oveq2d	⊢ ( 𝜑 → ( 𝐼 mHomP 𝑆 ) = ( 𝐼 mHomP ( 𝑆 ↾s 𝐾 ) ) )
25	2 24	eqtrid	⊢ ( 𝜑 → 𝐻 = ( 𝐼 mHomP ( 𝑆 ↾s 𝐾 ) ) )
26	25	fveq1d	⊢ ( 𝜑 → ( 𝐻 ‘ 𝑁 ) = ( ( 𝐼 mHomP ( 𝑆 ↾s 𝐾 ) ) ‘ 𝑁 ) )
27	13 26	eleqtrd	⊢ ( 𝜑 → 𝑋 ∈ ( ( 𝐼 mHomP ( 𝑆 ↾s 𝐾 ) ) ‘ 𝑁 ) )
28	15 16 17 3 4 5 6 7 8 9 10 20 11 12 27 14	mhphf3	⊢ ( 𝜑 → ( ( 𝑄 ‘ 𝑋 ) ‘ ( 𝐿 ∙ 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑋 ) ‘ 𝐴 ) ) )