Theorem mhphf2

Description: A homogeneous polynomial defines a homogeneous function; this is mhphf with simpler notation in the conclusion in exchange for a complex definition of .xb , which is based on frlmvscafval but without the finite support restriction ( frlmpws , frlmbas ) on the assignments A from variables to values.

TODO?: Polynomials ( df-mpl ) are defined to have a finite amount of terms (of finite degree). As such, any assignment may be replaced by an assignment with finite support (as only a finite amount of variables matter in a given polynomial, even if the set of variables is infinite). So the finite support restriction can be assumed without loss of generality. (Contributed by SN, 11-Nov-2024)

	Ref	Expression
Hypotheses	mhphf2.q	$$⊢Q=\left(I\mathrm{evalSub}S\right)\left(R\right)$$
	mhphf2.h	$$⊢H=I\mathrm{mHomP}U$$
	mhphf2.u	$$⊢U=S{\upharpoonright }_{𝑠}R$$
	mhphf2.k	$$⊢K={\mathrm{Base}}_S$$
	mhphf2.b	$$⊢\underset{\dot{}}{\bullet }={\cdot }_{\left(\mathrm{ringLMod}\left(S\right){\uparrow }_{𝑠}I\right)}$$
	mhphf2.m	$$⊢\underset{\dot{}}{·}={\cdot }_S$$
	mhphf2.e	$$⊢\underset{\dot{}}{\times }={\cdot }_{{\mathrm{mulGrp}}_S}$$
	mhphf2.s	$$⊢\phi \to S\in \mathrm{CRing}$$
	mhphf2.r	$$⊢\phi \to R\in \mathrm{SubRing}\left(S\right)$$
	mhphf2.l	$$⊢\phi \to L\in R$$
	mhphf2.x	$$⊢\phi \to X\in H\left(N\right)$$
	mhphf2.a	$$⊢\phi \to A\in \left(K^I\right)$$
Assertion	mhphf2	$$⊢\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		mhphf2.q	$$⊢Q=\left(I\mathrm{evalSub}S\right)\left(R\right)$$
2		mhphf2.h	$$⊢H=I\mathrm{mHomP}U$$
3		mhphf2.u	$$⊢U=S{\upharpoonright }_{𝑠}R$$
4		mhphf2.k	$$⊢K={\mathrm{Base}}_S$$
5		mhphf2.b	$$⊢\underset{\dot{}}{\bullet }={\cdot }_{\left(\mathrm{ringLMod}\left(S\right){\uparrow }_{𝑠}I\right)}$$
6		mhphf2.m	$$⊢\underset{\dot{}}{·}={\cdot }_S$$
7		mhphf2.e	$$⊢\underset{\dot{}}{\times }={\cdot }_{{\mathrm{mulGrp}}_S}$$
8		mhphf2.s	$$⊢\phi \to S\in \mathrm{CRing}$$
9		mhphf2.r	$$⊢\phi \to R\in \mathrm{SubRing}\left(S\right)$$
10		mhphf2.l	$$⊢\phi \to L\in R$$
11		mhphf2.x	$$⊢\phi \to X\in H\left(N\right)$$
12		mhphf2.a	$$⊢\phi \to A\in \left(K^I\right)$$
13		eqid	$$⊢\mathrm{ringLMod}\left(S\right){\uparrow }_{𝑠}I=\mathrm{ringLMod}\left(S\right){\uparrow }_{𝑠}I$$
14		eqid	$$⊢{\mathrm{Base}}_{\left(\mathrm{ringLMod}\left(S\right){\uparrow }_{𝑠}I\right)}={\mathrm{Base}}_{\left(\mathrm{ringLMod}\left(S\right){\uparrow }_{𝑠}I\right)}$$
15		rlmvsca	$$⊢{\cdot }_S={\cdot }_{\mathrm{ringLMod}\left(S\right)}$$
16		eqid	$$⊢\mathrm{Scalar}\left(\mathrm{ringLMod}\left(S\right)\right)=\mathrm{Scalar}\left(\mathrm{ringLMod}\left(S\right)\right)$$
17		eqid	$$⊢{\mathrm{Base}}_{\mathrm{Scalar}\left(\mathrm{ringLMod}\left(S\right)\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(\mathrm{ringLMod}\left(S\right)\right)}$$
18		fvexd	$$⊢\phi \to \mathrm{ringLMod}\left(S\right)\in \mathrm{V}$$
19		reldmmhp	$$⊢\mathrm{Rel}\mathrm{dom}\mathrm{mHomP}$$
20	19 2 11	elfvov1	$$⊢\phi \to I\in \mathrm{V}$$
21	4	subrgss	$$⊢R\in \mathrm{SubRing}\left(S\right)\to R\subseteq K$$
22	9 21	syl	$$⊢\phi \to R\subseteq K$$
23	22 10	sseldd	$$⊢\phi \to L\in K$$
24		rlmsca	$$⊢S\in \mathrm{CRing}\to S=\mathrm{Scalar}\left(\mathrm{ringLMod}\left(S\right)\right)$$
25	8 24	syl	$$⊢\phi \to S=\mathrm{Scalar}\left(\mathrm{ringLMod}\left(S\right)\right)$$
26	25	fveq2d	$$⊢\phi \to {\mathrm{Base}}_S={\mathrm{Base}}_{\mathrm{Scalar}\left(\mathrm{ringLMod}\left(S\right)\right)}$$
27	4 26	eqtrid	$$⊢\phi \to K={\mathrm{Base}}_{\mathrm{Scalar}\left(\mathrm{ringLMod}\left(S\right)\right)}$$
28	23 27	eleqtrd	$$⊢\phi \to L\in {\mathrm{Base}}_{\mathrm{Scalar}\left(\mathrm{ringLMod}\left(S\right)\right)}$$
29	4	oveq1i	$$⊢K^I={{\mathrm{Base}}_S}^I$$
30	12 29	eleqtrdi	$$⊢\phi \to A\in \left({{\mathrm{Base}}_S}^I\right)$$
31		rlmbas	$$⊢{\mathrm{Base}}_S={\mathrm{Base}}_{\mathrm{ringLMod}\left(S\right)}$$
32	13 31	pwsbas	$$⊢\left(\mathrm{ringLMod}\left(S\right)\in \mathrm{V}\wedge I\in \mathrm{V}\right)\to {{\mathrm{Base}}_S}^I={\mathrm{Base}}_{\left(\mathrm{ringLMod}\left(S\right){\uparrow }_{𝑠}I\right)}$$
33	18 20 32	syl2anc	$$⊢\phi \to {{\mathrm{Base}}_S}^I={\mathrm{Base}}_{\left(\mathrm{ringLMod}\left(S\right){\uparrow }_{𝑠}I\right)}$$
34	30 33	eleqtrd	$$⊢\phi \to A\in {\mathrm{Base}}_{\left(\mathrm{ringLMod}\left(S\right){\uparrow }_{𝑠}I\right)}$$
35	13 14 15 5 16 17 18 20 28 34	pwsvscafval	$$⊢\phi \to L\underset{\dot{}}{\bullet }A=\left(I\times \left\{L\right\}\right){{\cdot }_S}_{f}A$$
36	6	eqcomi	$$⊢{\cdot }_S=\underset{\dot{}}{·}$$
37		ofeq	$$⊢{\cdot }_S=\underset{\dot{}}{·}\to {\circ }_f{\cdot }_S={\circ }_f\underset{\dot{}}{·}$$
38	36 37	mp1i	$$⊢\phi \to {\circ }_f{\cdot }_S={\circ }_f\underset{\dot{}}{·}$$
39	38	oveqd	$$⊢\phi \to \left(I\times \left\{L\right\}\right){{\cdot }_S}_{f}A=\left(I\times \left\{L\right\}\right){\underset{\dot{}}{·}}_{f}A$$
40	35 39	eqtrd	$$⊢\phi \to L\underset{\dot{}}{\bullet }A=\left(I\times \left\{L\right\}\right){\underset{\dot{}}{·}}_{f}A$$
41	40	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)$$
42	1 2 3 4 6 7 8 9 10 11 12	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)$$
43	41 42	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)$$