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

Proof

Step	Hyp	Ref	Expression
1		mhphf3.q	\|- Q = ( ( I evalSub S ) ` R )
2		mhphf3.h	\|- H = ( I mHomP U )
3		mhphf3.u	\|- U = ( S \|`s R )
4		mhphf3.k	\|- K = ( Base ` S )
5		mhphf3.f	\|- F = ( S freeLMod I )
6		mhphf3.m	\|- M = ( Base ` F )
7		mhphf3.b	\|- .xb = ( .s ` F )
8		mhphf3.x	\|- .x. = ( .r ` S )
9		mhphf3.e	\|- .^ = ( .g ` ( mulGrp ` S ) )
10		mhphf3.i	\|- ( ph -> I e. V )
11		mhphf3.s	\|- ( ph -> S e. CRing )
12		mhphf3.r	\|- ( ph -> R e. ( SubRing ` S ) )
13		mhphf3.l	\|- ( ph -> L e. R )
14		mhphf3.n	\|- ( ph -> N e. NN0 )
15		mhphf3.p	\|- ( ph -> X e. ( H ` N ) )
16		mhphf3.a	\|- ( ph -> A e. M )
17	4	subrgss	\|- ( R e. ( SubRing ` S ) -> R C_ K )
18	12 17	syl	\|- ( ph -> R C_ K )
19	18 13	sseldd	\|- ( ph -> L e. K )
20	5 6 4 10 19 16 7 8	frlmvscafval	\|- ( ph -> ( L .xb A ) = ( ( I X. { L } ) oF .x. A ) )
21	20	fveq2d	\|- ( ph -> ( ( Q ` X ) ` ( L .xb A ) ) = ( ( Q ` X ) ` ( ( I X. { L } ) oF .x. A ) ) )
22	5 4 6	frlmbasmap	\|- ( ( I e. V /\ A e. M ) -> A e. ( K ^m I ) )
23	10 16 22	syl2anc	\|- ( ph -> A e. ( K ^m I ) )
24	1 2 3 4 8 9 10 11 12 13 14 15 23	mhphf	\|- ( ph -> ( ( Q ` X ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` X ) ` A ) ) )
25	21 24	eqtrd	\|- ( ph -> ( ( Q ` X ) ` ( L .xb A ) ) = ( ( N .^ L ) .x. ( ( Q ` X ) ` A ) ) )

Metamath Proof Explorer

Theorem mhphf3

Proof