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	$⊢ \underset{˙}{∙} = \cdot_{F}$
	mhphf4.x	$⊢ \underset{˙}{\cdot} = \cdot_{S}$
	mhphf4.e	$⊢ \underset{˙}{\times} = \cdot_{{mulGrp}_{S}}$
	mhphf4.s	$⊢ φ \to S \in CRing$
	mhphf4.l	$⊢ φ \to L \in K$
	mhphf4.p	$⊢ φ \to X \in H (N)$
	mhphf4.a	$⊢ φ \to A \in M$
Assertion	mhphf4	$⊢ φ \to Q (X) (L \underset{˙}{∙} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} 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	$⊢ \underset{˙}{∙} = \cdot_{F}$
7		mhphf4.x	$⊢ \underset{˙}{\cdot} = \cdot_{S}$
8		mhphf4.e	$⊢ \underset{˙}{\times} = \cdot_{{mulGrp}_{S}}$
9		mhphf4.s	$⊢ φ \to S \in CRing$
10		mhphf4.l	$⊢ φ \to L \in K$
11		mhphf4.p	$⊢ φ \to X \in H (N)$
12		mhphf4.a	$⊢ φ \to A \in M$
13	1 3	evlval	$⊢ Q = (I evalSub S) (K)$
14		eqid	$⊢ I mHomP (S ↾_{𝑠} K) = I mHomP (S ↾_{𝑠} K)$
15		eqid	$⊢ S ↾_{𝑠} K = S ↾_{𝑠} K$
16	9	crngringd	$⊢ φ \to S \in Ring$
17	3	subrgid	$⊢ S \in Ring \to K \in SubRing (S)$
18	16 17	syl	$⊢ φ \to K \in SubRing (S)$
19	3	ressid	$⊢ S \in CRing \to S ↾_{𝑠} K = S$
20	9 19	syl	$⊢ φ \to S ↾_{𝑠} K = S$
21	20	eqcomd	$⊢ φ \to S = S ↾_{𝑠} K$
22	21	oveq2d	$⊢ φ \to I mHomP S = I mHomP (S ↾_{𝑠} K)$
23	2 22	eqtrid	$⊢ φ \to H = I mHomP (S ↾_{𝑠} K)$
24	23	fveq1d	$⊢ φ \to H (N) = (I mHomP (S ↾_{𝑠} K)) (N)$
25	11 24	eleqtrd	$⊢ φ \to X \in (I mHomP (S ↾_{𝑠} K)) (N)$
26	13 14 15 3 4 5 6 7 8 9 18 10 25 12	mhphf3	$⊢ φ \to Q (X) (L \underset{˙}{∙} A) = (N \underset{˙}{\times} L) \underset{˙}{\cdot} Q (X) (A)$

Metamath Proof Explorer

Theorem mhphf4

Proof