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.s	\|- ( ph -> S e. CRing )
	mhphf4.l	\|- ( ph -> L e. K )
	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.s	\|- ( ph -> S e. CRing )
10		mhphf4.l	\|- ( ph -> L e. K )
11		mhphf4.p	\|- ( ph -> X e. ( H ` N ) )
12		mhphf4.a	\|- ( ph -> A e. M )
13	1 3	evlval	\|- Q = ( ( I evalSub S ) ` K )
14		eqid	\|- ( I mHomP ( S \|`s K ) ) = ( I mHomP ( S \|`s K ) )
15		eqid	\|- ( S \|`s K ) = ( S \|`s K )
16	9	crngringd	\|- ( ph -> S e. Ring )
17	3	subrgid	\|- ( S e. Ring -> K e. ( SubRing ` S ) )
18	16 17	syl	\|- ( ph -> K e. ( SubRing ` S ) )
19	3	ressid	\|- ( S e. CRing -> ( S \|`s K ) = S )
20	9 19	syl	\|- ( ph -> ( S \|`s K ) = S )
21	20	eqcomd	\|- ( ph -> S = ( S \|`s K ) )
22	21	oveq2d	\|- ( ph -> ( I mHomP S ) = ( I mHomP ( S \|`s K ) ) )
23	2 22	eqtrid	\|- ( ph -> H = ( I mHomP ( S \|`s K ) ) )
24	23	fveq1d	\|- ( ph -> ( H ` N ) = ( ( I mHomP ( S \|`s K ) ) ` N ) )
25	11 24	eleqtrd	\|- ( ph -> X e. ( ( I mHomP ( S \|`s K ) ) ` N ) )
26	13 14 15 3 4 5 6 7 8 9 18 10 25 12	mhphf3	\|- ( ph -> ( ( Q ` X ) ` ( L .xb A ) ) = ( ( N .^ L ) .x. ( ( Q ` X ) ` A ) ) )

Metamath Proof Explorer

Theorem mhphf4

Proof