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	$$⊢Q=I\mathrm{eval}S$$
	mhphf4.h	$$⊢H=I\mathrm{mHomP}S$$
	mhphf4.k	$$⊢K={\mathrm{Base}}_S$$
	mhphf4.f	$$⊢F=S\mathrm{freeLMod}I$$
	mhphf4.m	$$⊢M={\mathrm{Base}}_F$$
	mhphf4.b	$$⊢\underset{\dot{}}{\bullet }={\cdot }_F$$
	mhphf4.x	$$⊢\underset{\dot{}}{·}={\cdot }_S$$
	mhphf4.e	$$⊢\underset{\dot{}}{\times }={\cdot }_{{\mathrm{mulGrp}}_S}$$
	mhphf4.i	$$⊢\phi \to I\in V$$
	mhphf4.s	$$⊢\phi \to S\in \mathrm{CRing}$$
	mhphf4.l	$$⊢\phi \to L\in K$$
	mhphf4.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
	mhphf4.p	$$⊢\phi \to X\in H\left(N\right)$$
	mhphf4.a	$$⊢\phi \to A\in M$$
Assertion	mhphf4	$$⊢\phi \to Q\left(X\right)\left(L\underset{\dot{}}{\bullet }A\right)=\left(N\underset{\dot{}}{\times }L\right)\underset{\dot{}}{·}Q\left(X\right)\left(A\right)$$

Proof

Step	Hyp	Ref	Expression
1		mhphf4.q	$$⊢Q=I\mathrm{eval}S$$
2		mhphf4.h	$$⊢H=I\mathrm{mHomP}S$$
3		mhphf4.k	$$⊢K={\mathrm{Base}}_S$$
4		mhphf4.f	$$⊢F=S\mathrm{freeLMod}I$$
5		mhphf4.m	$$⊢M={\mathrm{Base}}_F$$
6		mhphf4.b	$$⊢\underset{\dot{}}{\bullet }={\cdot }_F$$
7		mhphf4.x	$$⊢\underset{\dot{}}{·}={\cdot }_S$$
8		mhphf4.e	$$⊢\underset{\dot{}}{\times }={\cdot }_{{\mathrm{mulGrp}}_S}$$
9		mhphf4.i	$$⊢\phi \to I\in V$$
10		mhphf4.s	$$⊢\phi \to S\in \mathrm{CRing}$$
11		mhphf4.l	$$⊢\phi \to L\in K$$
12		mhphf4.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
13		mhphf4.p	$$⊢\phi \to X\in H\left(N\right)$$
14		mhphf4.a	$$⊢\phi \to A\in M$$
15	1 3	evlval	$$⊢Q=\left(I\mathrm{evalSub}S\right)\left(K\right)$$
16		eqid	$$⊢I\mathrm{mHomP}\left(S{\upharpoonright }_{𝑠}K\right)=I\mathrm{mHomP}\left(S{\upharpoonright }_{𝑠}K\right)$$
17		eqid	$$⊢S{\upharpoonright }_{𝑠}K=S{\upharpoonright }_{𝑠}K$$
18	10	crngringd	$$⊢\phi \to S\in \mathrm{Ring}$$
19	3	subrgid	$$⊢S\in \mathrm{Ring}\to K\in \mathrm{SubRing}\left(S\right)$$
20	18 19	syl	$$⊢\phi \to K\in \mathrm{SubRing}\left(S\right)$$
21	3	ressid	$$⊢S\in \mathrm{CRing}\to S{\upharpoonright }_{𝑠}K=S$$
22	10 21	syl	$$⊢\phi \to S{\upharpoonright }_{𝑠}K=S$$
23	22	eqcomd	$$⊢\phi \to S=S{\upharpoonright }_{𝑠}K$$
24	23	oveq2d	$$⊢\phi \to I\mathrm{mHomP}S=I\mathrm{mHomP}\left(S{\upharpoonright }_{𝑠}K\right)$$
25	2 24	eqtrid	$$⊢\phi \to H=I\mathrm{mHomP}\left(S{\upharpoonright }_{𝑠}K\right)$$
26	25	fveq1d	$$⊢\phi \to H\left(N\right)=\left(I\mathrm{mHomP}\left(S{\upharpoonright }_{𝑠}K\right)\right)\left(N\right)$$
27	13 26	eleqtrd	$$⊢\phi \to X\in \left(I\mathrm{mHomP}\left(S{\upharpoonright }_{𝑠}K\right)\right)\left(N\right)$$
28	15 16 17 3 4 5 6 7 8 9 10 20 11 12 27 14	mhphf3	$$⊢\phi \to Q\left(X\right)\left(L\underset{\dot{}}{\bullet }A\right)=\left(N\underset{\dot{}}{\times }L\right)\underset{\dot{}}{·}Q\left(X\right)\left(A\right)$$