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

Proof

Step	Hyp	Ref	Expression
1		mhphf4.q	\|- Q = ( I eval S )
2		mhphf4.h	\|- H = ( I mHomP S )
3		mhphf4.k	\|- K = ( Base ` S )
4		mhphf4.f	\|- F = ( S freeLMod I )
5		mhphf4.m	\|- M = ( Base ` F )
6		mhphf4.b	\|- .xb = ( .s ` F )
7		mhphf4.x	\|- .x. = ( .r ` S )
8		mhphf4.e	\|- .^ = ( .g ` ( mulGrp ` S ) )
9		mhphf4.i	\|- ( ph -> I e. V )
10		mhphf4.s	\|- ( ph -> S e. CRing )
11		mhphf4.l	\|- ( ph -> L e. K )
12		mhphf4.n	\|- ( ph -> N e. NN0 )
13		mhphf4.p	\|- ( ph -> X e. ( H ` N ) )
14		mhphf4.a	\|- ( ph -> A e. M )
15	1 3	evlval	\|- Q = ( ( I evalSub S ) ` K )
16		eqid	\|- ( I mHomP ( S \|`s K ) ) = ( I mHomP ( S \|`s K ) )
17		eqid	\|- ( S \|`s K ) = ( S \|`s K )
18	10	crngringd	\|- ( ph -> S e. Ring )
19	3	subrgid	\|- ( S e. Ring -> K e. ( SubRing ` S ) )
20	18 19	syl	\|- ( ph -> K e. ( SubRing ` S ) )
21	3	ressid	\|- ( S e. CRing -> ( S \|`s K ) = S )
22	10 21	syl	\|- ( ph -> ( S \|`s K ) = S )
23	22	eqcomd	\|- ( ph -> S = ( S \|`s K ) )
24	23	oveq2d	\|- ( ph -> ( I mHomP S ) = ( I mHomP ( S \|`s K ) ) )
25	2 24	eqtrid	\|- ( ph -> H = ( I mHomP ( S \|`s K ) ) )
26	25	fveq1d	\|- ( ph -> ( H ` N ) = ( ( I mHomP ( S \|`s K ) ) ` N ) )
27	13 26	eleqtrd	\|- ( ph -> X e. ( ( I mHomP ( S \|`s K ) ) ` N ) )
28	15 16 17 3 4 5 6 7 8 9 10 20 11 12 27 14	mhphf3	\|- ( ph -> ( ( Q ` X ) ` ( L .xb A ) ) = ( ( N .^ L ) .x. ( ( Q ` X ) ` A ) ) )

Metamath Proof Explorer

Theorem mhphf4

Proof