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	$$⊢Q=\left(I\mathrm{evalSub}S\right)\left(R\right)$$
	mhphf3.h	$$⊢H=I\mathrm{mHomP}U$$
	mhphf3.u	$$⊢U=S{\upharpoonright }_{𝑠}R$$
	mhphf3.k	$$⊢K={\mathrm{Base}}_S$$
	mhphf3.f	$$⊢F=S\mathrm{freeLMod}I$$
	mhphf3.m	$$⊢M={\mathrm{Base}}_F$$
	mhphf3.b	$$⊢\underset{\dot{}}{\bullet }={\cdot }_F$$
	mhphf3.x	$$⊢\underset{\dot{}}{·}={\cdot }_S$$
	mhphf3.e	$$⊢\underset{\dot{}}{\times }={\cdot }_{{\mathrm{mulGrp}}_S}$$
	mhphf3.s	$$⊢\phi \to S\in \mathrm{CRing}$$
	mhphf3.r	$$⊢\phi \to R\in \mathrm{SubRing}\left(S\right)$$
	mhphf3.l	$$⊢\phi \to L\in R$$
	mhphf3.p	$$⊢\phi \to X\in H\left(N\right)$$
	mhphf3.a	$$⊢\phi \to A\in M$$
Assertion	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)$$

Proof

Step	Hyp	Ref	Expression
1		mhphf3.q	$$⊢Q=\left(I\mathrm{evalSub}S\right)\left(R\right)$$
2		mhphf3.h	$$⊢H=I\mathrm{mHomP}U$$
3		mhphf3.u	$$⊢U=S{\upharpoonright }_{𝑠}R$$
4		mhphf3.k	$$⊢K={\mathrm{Base}}_S$$
5		mhphf3.f	$$⊢F=S\mathrm{freeLMod}I$$
6		mhphf3.m	$$⊢M={\mathrm{Base}}_F$$
7		mhphf3.b	$$⊢\underset{\dot{}}{\bullet }={\cdot }_F$$
8		mhphf3.x	$$⊢\underset{\dot{}}{·}={\cdot }_S$$
9		mhphf3.e	$$⊢\underset{\dot{}}{\times }={\cdot }_{{\mathrm{mulGrp}}_S}$$
10		mhphf3.s	$$⊢\phi \to S\in \mathrm{CRing}$$
11		mhphf3.r	$$⊢\phi \to R\in \mathrm{SubRing}\left(S\right)$$
12		mhphf3.l	$$⊢\phi \to L\in R$$
13		mhphf3.p	$$⊢\phi \to X\in H\left(N\right)$$
14		mhphf3.a	$$⊢\phi \to A\in M$$
15		reldmmhp	$$⊢\mathrm{Rel}\mathrm{dom}\mathrm{mHomP}$$
16	15 2 13	elfvov1	$$⊢\phi \to I\in \mathrm{V}$$
17	4	subrgss	$$⊢R\in \mathrm{SubRing}\left(S\right)\to R\subseteq K$$
18	11 17	syl	$$⊢\phi \to R\subseteq K$$
19	18 12	sseldd	$$⊢\phi \to L\in K$$
20	5 6 4 16 19 14 7 8	frlmvscafval	$$⊢\phi \to L\underset{\dot{}}{\bullet }A=\left(I\times \left\{L\right\}\right){\underset{\dot{}}{·}}_{f}A$$
21	20	fveq2d	$$⊢\phi \to Q\left(X\right)\left(L\underset{\dot{}}{\bullet }A\right)=Q\left(X\right)\left(\left(I\times \left\{L\right\}\right){\underset{\dot{}}{·}}_{f}A\right)$$
22	5 4 6	frlmbasmap	$$⊢\left(I\in \mathrm{V}\wedge A\in M\right)\to A\in \left(K^I\right)$$
23	16 14 22	syl2anc	$$⊢\phi \to A\in \left(K^I\right)$$
24	1 2 3 4 8 9 10 11 12 13 23	mhphf	$$⊢\phi \to Q\left(X\right)\left(\left(I\times \left\{L\right\}\right){\underset{\dot{}}{·}}_{f}A\right)=\left(N\underset{\dot{}}{\times }L\right)\underset{\dot{}}{·}Q\left(X\right)\left(A\right)$$
25	21 24	eqtrd	$$⊢\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)$$