Theorem mhppwdeg

Description: Degree of a homogeneous polynomial raised to a power. General version of deg1pw . (Contributed by SN, 26-Jul-2024) Remove closure hypotheses. (Revised by SN, 4-Sep-2025)

	Ref	Expression
Hypotheses	mhppwdeg.h	$$⊢H=I\mathrm{mHomP}R$$
	mhppwdeg.p	$$⊢P=I\mathrm{mPoly}R$$
	mhppwdeg.t	$$⊢T={\mathrm{mulGrp}}_P$$
	mhppwdeg.e	$$⊢\underset{\dot{}}{\times }={\cdot }_T$$
	mhppwdeg.r	$$⊢\phi \to R\in \mathrm{Ring}$$
	mhppwdeg.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
	mhppwdeg.x	$$⊢\phi \to X\in H\left(M\right)$$
Assertion	mhppwdeg	$$⊢\phi \to N\underset{\dot{}}{\times }X\in H\left(\mathrm{<mi\; mathcolor="\#808">M</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right)$$

Proof

Step	Hyp	Ref	Expression
1		mhppwdeg.h	$$⊢H=I\mathrm{mHomP}R$$
2		mhppwdeg.p	$$⊢P=I\mathrm{mPoly}R$$
3		mhppwdeg.t	$$⊢T={\mathrm{mulGrp}}_P$$
4		mhppwdeg.e	$$⊢\underset{\dot{}}{\times }={\cdot }_T$$
5		mhppwdeg.r	$$⊢\phi \to R\in \mathrm{Ring}$$
6		mhppwdeg.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
7		mhppwdeg.x	$$⊢\phi \to X\in H\left(M\right)$$
8		oveq1	$$⊢x=0\to x\underset{\dot{}}{\times }X=0\underset{\dot{}}{\times }X$$
9		oveq2	$$⊢x=0\to Mx=\mathrm{<mi\; mathcolor="\#808">M</mi>}\cdot 0$$
10	9	fveq2d	$$⊢x=0\to H\left(Mx\right)=H\left(\mathrm{<mi\; mathcolor="\#808">M</mi>}\cdot 0\right)$$
11	8 10	eleq12d	$$⊢x=0\to \left(x\underset{\dot{}}{\times }X\in H\left(Mx\right)\leftrightarrow 0\underset{\dot{}}{\times }X\in H\left(\mathrm{<mi\; mathcolor="\#808">M</mi>}\cdot 0\right)\right)$$
12		oveq1	$$⊢x=y\to x\underset{\dot{}}{\times }X=y\underset{\dot{}}{\times }X$$
13		oveq2	$$⊢x=y\to Mx=My$$
14	13	fveq2d	$$⊢x=y\to H\left(Mx\right)=H\left(My\right)$$
15	12 14	eleq12d	$$⊢x=y\to \left(x\underset{\dot{}}{\times }X\in H\left(Mx\right)\leftrightarrow y\underset{\dot{}}{\times }X\in H\left(My\right)\right)$$
16		oveq1	$$⊢x=y+1\to x\underset{\dot{}}{\times }X=\left(y+1\right)\underset{\dot{}}{\times }X$$
17		oveq2	$$⊢x=y+1\to Mx=M\left(y+1\right)$$
18	17	fveq2d	$$⊢x=y+1\to H\left(Mx\right)=H\left(M\left(y+1\right)\right)$$
19	16 18	eleq12d	$$⊢x=y+1\to \left(x\underset{\dot{}}{\times }X\in H\left(Mx\right)\leftrightarrow \left(y+1\right)\underset{\dot{}}{\times }X\in H\left(M\left(y+1\right)\right)\right)$$
20		oveq1	$$⊢x=N\to x\underset{\dot{}}{\times }X=N\underset{\dot{}}{\times }X$$
21		oveq2	$$⊢x=N\to Mx=\mathrm{<mi\; mathcolor="\#808">M</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$
22	21	fveq2d	$$⊢x=N\to H\left(Mx\right)=H\left(\mathrm{<mi\; mathcolor="\#808">M</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right)$$
23	20 22	eleq12d	$$⊢x=N\to \left(x\underset{\dot{}}{\times }X\in H\left(Mx\right)\leftrightarrow N\underset{\dot{}}{\times }X\in H\left(\mathrm{<mi\; mathcolor="\#808">M</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right)\right)$$
24		reldmmhp	$$⊢\mathrm{Rel}\mathrm{dom}\mathrm{mHomP}$$
25	24 1 7	elfvov1	$$⊢\phi \to I\in \mathrm{V}$$
26	2 25 5	mplsca	$$⊢\phi \to R=\mathrm{Scalar}\left(P\right)$$
27	26	fveq2d	$$⊢\phi \to 1_R=1_{\mathrm{Scalar}\left(P\right)}$$
28	27	fveq2d	$$⊢\phi \to \mathrm{algSc}\left(P\right)\left(1_R\right)=\mathrm{algSc}\left(P\right)\left(1_{\mathrm{Scalar}\left(P\right)}\right)$$
29		eqid	$$⊢\mathrm{algSc}\left(P\right)=\mathrm{algSc}\left(P\right)$$
30		eqid	$$⊢\mathrm{Scalar}\left(P\right)=\mathrm{Scalar}\left(P\right)$$
31	2 25 5	mpllmodd	$$⊢\phi \to P\in \mathrm{LMod}$$
32	2 25 5	mplringd	$$⊢\phi \to P\in \mathrm{Ring}$$
33	29 30 31 32	ascl1	$$⊢\phi \to \mathrm{algSc}\left(P\right)\left(1_{\mathrm{Scalar}\left(P\right)}\right)=1_P$$
34	28 33	eqtrd	$$⊢\phi \to \mathrm{algSc}\left(P\right)\left(1_R\right)=1_P$$
35		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
36		eqid	$$⊢1_R=1_R$$
37	35 36	ringidcl	$$⊢R\in \mathrm{Ring}\to 1_R\in {\mathrm{Base}}_R$$
38	5 37	syl	$$⊢\phi \to 1_R\in {\mathrm{Base}}_R$$
39	1 2 29 35 25 5 38	mhpsclcl	$$⊢\phi \to \mathrm{algSc}\left(P\right)\left(1_R\right)\in H\left(0\right)$$
40	34 39	eqeltrrd	$$⊢\phi \to 1_P\in H\left(0\right)$$
41		eqid	$$⊢{\mathrm{Base}}_P={\mathrm{Base}}_P$$
42	1 2 41 7	mhpmpl	$$⊢\phi \to X\in {\mathrm{Base}}_P$$
43	3 41	mgpbas	$$⊢{\mathrm{Base}}_P={\mathrm{Base}}_T$$
44		eqid	$$⊢1_P=1_P$$
45	3 44	ringidval	$$⊢1_P=0_T$$
46	43 45 4	mulg0	$$⊢X\in {\mathrm{Base}}_P\to 0\underset{\dot{}}{\times }X=1_P$$
47	42 46	syl	$$⊢\phi \to 0\underset{\dot{}}{\times }X=1_P$$
48	1 7	mhprcl	$$⊢\phi \to M\in {\mathbb{N}}_0$$
49	48	nn0cnd	$$⊢\phi \to M\in ℂ$$
50	49	mul01d	$$⊢\phi \to \mathrm{<mi\; mathcolor="\#808">M</mi>}\cdot 0=0$$
51	50	fveq2d	$$⊢\phi \to H\left(\mathrm{<mi\; mathcolor="\#808">M</mi>}\cdot 0\right)=H\left(0\right)$$
52	40 47 51	3eltr4d	$$⊢\phi \to 0\underset{\dot{}}{\times }X\in H\left(\mathrm{<mi\; mathcolor="\#808">M</mi>}\cdot 0\right)$$
53		eqid	$$⊢{\cdot }_P={\cdot }_P$$
54	5	ad2antrr	$$⊢\left(\left(\phi \wedge y\in {\mathbb{N}}_0\right)\wedge y\underset{\dot{}}{\times }X\in H\left(My\right)\right)\to R\in \mathrm{Ring}$$
55		simpr	$$⊢\left(\left(\phi \wedge y\in {\mathbb{N}}_0\right)\wedge y\underset{\dot{}}{\times }X\in H\left(My\right)\right)\to y\underset{\dot{}}{\times }X\in H\left(My\right)$$
56	7	ad2antrr	$$⊢\left(\left(\phi \wedge y\in {\mathbb{N}}_0\right)\wedge y\underset{\dot{}}{\times }X\in H\left(My\right)\right)\to X\in H\left(M\right)$$
57	1 2 53 54 55 56	mhpmulcl	$$⊢\left(\left(\phi \wedge y\in {\mathbb{N}}_0\right)\wedge y\underset{\dot{}}{\times }X\in H\left(My\right)\right)\to \left(y\underset{\dot{}}{\times }X\right){\cdot }_{P}X\in H\left(My+M\right)$$
58	3	ringmgp	$$⊢P\in \mathrm{Ring}\to T\in \mathrm{Mnd}$$
59	32 58	syl	$$⊢\phi \to T\in \mathrm{Mnd}$$
60	59	ad2antrr	$$⊢\left(\left(\phi \wedge y\in {\mathbb{N}}_0\right)\wedge y\underset{\dot{}}{\times }X\in H\left(My\right)\right)\to T\in \mathrm{Mnd}$$
61		simplr	$$⊢\left(\left(\phi \wedge y\in {\mathbb{N}}_0\right)\wedge y\underset{\dot{}}{\times }X\in H\left(My\right)\right)\to y\in {\mathbb{N}}_0$$
62	42	ad2antrr	$$⊢\left(\left(\phi \wedge y\in {\mathbb{N}}_0\right)\wedge y\underset{\dot{}}{\times }X\in H\left(My\right)\right)\to X\in {\mathrm{Base}}_P$$
63	3 53	mgpplusg	$$⊢{\cdot }_P={+}_T$$
64	43 4 63	mulgnn0p1	$$⊢\left(T\in \mathrm{Mnd}\wedge y\in {\mathbb{N}}_0\wedge X\in {\mathrm{Base}}_P\right)\to \left(y+1\right)\underset{\dot{}}{\times }X=\left(y\underset{\dot{}}{\times }X\right){\cdot }_{P}X$$
65	60 61 62 64	syl3anc	$$⊢\left(\left(\phi \wedge y\in {\mathbb{N}}_0\right)\wedge y\underset{\dot{}}{\times }X\in H\left(My\right)\right)\to \left(y+1\right)\underset{\dot{}}{\times }X=\left(y\underset{\dot{}}{\times }X\right){\cdot }_{P}X$$
66	49	ad2antrr	$$⊢\left(\left(\phi \wedge y\in {\mathbb{N}}_0\right)\wedge y\underset{\dot{}}{\times }X\in H\left(My\right)\right)\to M\in ℂ$$
67	61	nn0cnd	$$⊢\left(\left(\phi \wedge y\in {\mathbb{N}}_0\right)\wedge y\underset{\dot{}}{\times }X\in H\left(My\right)\right)\to y\in ℂ$$
68		1cnd	$$⊢\left(\left(\phi \wedge y\in {\mathbb{N}}_0\right)\wedge y\underset{\dot{}}{\times }X\in H\left(My\right)\right)\to 1\in ℂ$$
69	66 67 68	adddid	$$⊢\left(\left(\phi \wedge y\in {\mathbb{N}}_0\right)\wedge y\underset{\dot{}}{\times }X\in H\left(My\right)\right)\to M\left(y+1\right)=My+\mathrm{<mi\; mathcolor="\#808">M</mi>}\cdot 1$$
70	66	mulridd	$$⊢\left(\left(\phi \wedge y\in {\mathbb{N}}_0\right)\wedge y\underset{\dot{}}{\times }X\in H\left(My\right)\right)\to \mathrm{<mi\; mathcolor="\#808">M</mi>}\cdot 1=M$$
71	70	oveq2d	$$⊢\left(\left(\phi \wedge y\in {\mathbb{N}}_0\right)\wedge y\underset{\dot{}}{\times }X\in H\left(My\right)\right)\to My+\mathrm{<mi\; mathcolor="\#808">M</mi>}\cdot 1=My+M$$
72	69 71	eqtrd	$$⊢\left(\left(\phi \wedge y\in {\mathbb{N}}_0\right)\wedge y\underset{\dot{}}{\times }X\in H\left(My\right)\right)\to M\left(y+1\right)=My+M$$
73	72	fveq2d	$$⊢\left(\left(\phi \wedge y\in {\mathbb{N}}_0\right)\wedge y\underset{\dot{}}{\times }X\in H\left(My\right)\right)\to H\left(M\left(y+1\right)\right)=H\left(My+M\right)$$
74	57 65 73	3eltr4d	$$⊢\left(\left(\phi \wedge y\in {\mathbb{N}}_0\right)\wedge y\underset{\dot{}}{\times }X\in H\left(My\right)\right)\to \left(y+1\right)\underset{\dot{}}{\times }X\in H\left(M\left(y+1\right)\right)$$
75	11 15 19 23 52 74	nn0indd	$$⊢\left(\phi \wedge N\in {\mathbb{N}}_0\right)\to N\underset{\dot{}}{\times }X\in H\left(\mathrm{<mi\; mathcolor="\#808">M</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right)$$
76	6 75	mpdan	$$⊢\phi \to N\underset{\dot{}}{\times }X\in H\left(\mathrm{<mi\; mathcolor="\#808">M</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right)$$