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 = ( ( I evalSub S ) ` R )
	mhphf2.h	|- H = ( I mHomP U )
	mhphf2.u	|- U = ( S |`s R )
	mhphf2.k	|- K = ( Base ` S )
	mhphf2.b	|- .xb = ( .s ` ( ( ringLMod ` S ) ^s I ) )
	mhphf2.m	|- .x. = ( .r ` S )
	mhphf2.e	|- .^ = ( .g ` ( mulGrp ` S ) )
	mhphf2.i	|- ( ph -> I e. V )
	mhphf2.s	|- ( ph -> S e. CRing )
	mhphf2.r	|- ( ph -> R e. ( SubRing ` S ) )
	mhphf2.l	|- ( ph -> L e. R )
	mhphf2.n	|- ( ph -> N e. NN0 )
	mhphf2.x	|- ( ph -> X e. ( H ` N ) )
	mhphf2.a	|- ( ph -> A e. ( K ^m I ) )
Assertion	mhphf2	|- ( ph -> ( ( Q ` X ) ` ( L .xb A ) ) = ( ( N .^ L ) .x. ( ( Q ` X ) ` A ) ) )

Proof

Step	Hyp	Ref	Expression
1		mhphf2.q	|- Q = ( ( I evalSub S ) ` R )
2		mhphf2.h	|- H = ( I mHomP U )
3		mhphf2.u	|- U = ( S |`s R )
4		mhphf2.k	|- K = ( Base ` S )
5		mhphf2.b	|- .xb = ( .s ` ( ( ringLMod ` S ) ^s I ) )
6		mhphf2.m	|- .x. = ( .r ` S )
7		mhphf2.e	|- .^ = ( .g ` ( mulGrp ` S ) )
8		mhphf2.i	|- ( ph -> I e. V )
9		mhphf2.s	|- ( ph -> S e. CRing )
10		mhphf2.r	|- ( ph -> R e. ( SubRing ` S ) )
11		mhphf2.l	|- ( ph -> L e. R )
12		mhphf2.n	|- ( ph -> N e. NN0 )
13		mhphf2.x	|- ( ph -> X e. ( H ` N ) )
14		mhphf2.a	|- ( ph -> A e. ( K ^m I ) )
15		eqid	|- ( ( ringLMod ` S ) ^s I ) = ( ( ringLMod ` S ) ^s I )
16		eqid	|- ( Base ` ( ( ringLMod ` S ) ^s I ) ) = ( Base ` ( ( ringLMod ` S ) ^s I ) )
17		rlmvsca	|- ( .r ` S ) = ( .s ` ( ringLMod ` S ) )
18		eqid	|- ( Scalar ` ( ringLMod ` S ) ) = ( Scalar ` ( ringLMod ` S ) )
19		eqid	|- ( Base ` ( Scalar ` ( ringLMod ` S ) ) ) = ( Base ` ( Scalar ` ( ringLMod ` S ) ) )
20		fvexd	|- ( ph -> ( ringLMod ` S ) e. _V )
21	4	subrgss	|- ( R e. ( SubRing ` S ) -> R C_ K )
22	10 21	syl	|- ( ph -> R C_ K )
23	22 11	sseldd	|- ( ph -> L e. K )
24		rlmsca	|- ( S e. CRing -> S = ( Scalar ` ( ringLMod ` S ) ) )
25	9 24	syl	|- ( ph -> S = ( Scalar ` ( ringLMod ` S ) ) )
26	25	fveq2d	|- ( ph -> ( Base ` S ) = ( Base ` ( Scalar ` ( ringLMod ` S ) ) ) )
27	4 26	syl5eq	|- ( ph -> K = ( Base ` ( Scalar ` ( ringLMod ` S ) ) ) )
28	23 27	eleqtrd	|- ( ph -> L e. ( Base ` ( Scalar ` ( ringLMod ` S ) ) ) )
29	4	oveq1i	|- ( K ^m I ) = ( ( Base ` S ) ^m I )
30	14 29	eleqtrdi	|- ( ph -> A e. ( ( Base ` S ) ^m I ) )
31		rlmbas	|- ( Base ` S ) = ( Base ` ( ringLMod ` S ) )
32	15 31	pwsbas	|- ( ( ( ringLMod ` S ) e. _V /\ I e. V ) -> ( ( Base ` S ) ^m I ) = ( Base ` ( ( ringLMod ` S ) ^s I ) ) )
33	20 8 32	syl2anc	|- ( ph -> ( ( Base ` S ) ^m I ) = ( Base ` ( ( ringLMod ` S ) ^s I ) ) )
34	30 33	eleqtrd	|- ( ph -> A e. ( Base ` ( ( ringLMod ` S ) ^s I ) ) )
35	15 16 17 5 18 19 20 8 28 34	pwsvscafval	|- ( ph -> ( L .xb A ) = ( ( I X. { L } ) oF ( .r ` S ) A ) )
36	6	eqcomi	|- ( .r ` S ) = .x.
37		ofeq	|- ( ( .r ` S ) = .x. -> oF ( .r ` S ) = oF .x. )
38	36 37	mp1i	|- ( ph -> oF ( .r ` S ) = oF .x. )
39	38	oveqd	|- ( ph -> ( ( I X. { L } ) oF ( .r ` S ) A ) = ( ( I X. { L } ) oF .x. A ) )
40	35 39	eqtrd	|- ( ph -> ( L .xb A ) = ( ( I X. { L } ) oF .x. A ) )
41	40	fveq2d	|- ( ph -> ( ( Q ` X ) ` ( L .xb A ) ) = ( ( Q ` X ) ` ( ( I X. { L } ) oF .x. A ) ) )
42	1 2 3 4 6 7 8 9 10 11 12 13 14	mhphf	|- ( ph -> ( ( Q ` X ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` X ) ` A ) ) )
43	41 42	eqtrd	|- ( ph -> ( ( Q ` X ) ` ( L .xb A ) ) = ( ( N .^ L ) .x. ( ( Q ` X ) ` A ) ) )