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	⊢ ( 𝜑 → ( ( 𝑄 ‘ 𝑋 ) ‘ ( 𝐿 ∙ 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑋 ) ‘ 𝐴 ) ) )

Metamath Proof Explorer

Theorem mhphf4

Proof