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.s	$$⊢\phi \to S\in \mathrm{CRing}$$
	mhphf4.l	$$⊢\phi \to L\in K$$
	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.s	$$⊢\phi \to S\in \mathrm{CRing}$$
10		mhphf4.l	$$⊢\phi \to L\in K$$
11		mhphf4.p	$$⊢\phi \to X\in H\left(N\right)$$
12		mhphf4.a	$$⊢\phi \to A\in M$$
13	1 3	evlval	$$⊢Q=\left(I\mathrm{evalSub}S\right)\left(K\right)$$
14		eqid	$$⊢I\mathrm{mHomP}\left(S{\upharpoonright }_{𝑠}K\right)=I\mathrm{mHomP}\left(S{\upharpoonright }_{𝑠}K\right)$$
15		eqid	$$⊢S{\upharpoonright }_{𝑠}K=S{\upharpoonright }_{𝑠}K$$
16	9	crngringd	$$⊢\phi \to S\in \mathrm{Ring}$$
17	3	subrgid	$$⊢S\in \mathrm{Ring}\to K\in \mathrm{SubRing}\left(S\right)$$
18	16 17	syl	$$⊢\phi \to K\in \mathrm{SubRing}\left(S\right)$$
19	3	ressid	$$⊢S\in \mathrm{CRing}\to S{\upharpoonright }_{𝑠}K=S$$
20	9 19	syl	$$⊢\phi \to S{\upharpoonright }_{𝑠}K=S$$
21	20	eqcomd	$$⊢\phi \to S=S{\upharpoonright }_{𝑠}K$$
22	21	oveq2d	$$⊢\phi \to I\mathrm{mHomP}S=I\mathrm{mHomP}\left(S{\upharpoonright }_{𝑠}K\right)$$
23	2 22	eqtrid	$$⊢\phi \to H=I\mathrm{mHomP}\left(S{\upharpoonright }_{𝑠}K\right)$$
24	23	fveq1d	$$⊢\phi \to H\left(N\right)=\left(I\mathrm{mHomP}\left(S{\upharpoonright }_{𝑠}K\right)\right)\left(N\right)$$
25	11 24	eleqtrd	$$⊢\phi \to X\in \left(I\mathrm{mHomP}\left(S{\upharpoonright }_{𝑠}K\right)\right)\left(N\right)$$
26	13 14 15 3 4 5 6 7 8 9 18 10 25 12	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)$$