Theorem mhppwdeg

Description: Degree of a homogeneous polynomial raised to a power. General version of deg1pw . (Contributed by SN, 26-Jul-2024) Remove sethood hypothesis. (Revised by SN, 18-May-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.m	$$⊢\phi \to M\in {\mathbb{N}}_0$$
	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.m	$$⊢\phi \to M\in {\mathbb{N}}_0$$
7		mhppwdeg.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
8		mhppwdeg.x	$$⊢\phi \to X\in H\left(M\right)$$
9		oveq1	$$⊢x=0\to x\underset{\dot{}}{\times }X=0\underset{\dot{}}{\times }X$$
10		oveq2	$$⊢x=0\to Mx=\mathrm{<mi\; mathcolor="\#808">M</mi>}\cdot 0$$
11	10	fveq2d	$$⊢x=0\to H\left(Mx\right)=H\left(\mathrm{<mi\; mathcolor="\#808">M</mi>}\cdot 0\right)$$
12	9 11	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)$$
13		oveq1	$$⊢x=y\to x\underset{\dot{}}{\times }X=y\underset{\dot{}}{\times }X$$
14		oveq2	$$⊢x=y\to Mx=My$$
15	14	fveq2d	$$⊢x=y\to H\left(Mx\right)=H\left(My\right)$$
16	13 15	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)$$
17		oveq1	$$⊢x=y+1\to x\underset{\dot{}}{\times }X=\left(y+1\right)\underset{\dot{}}{\times }X$$
18		oveq2	$$⊢x=y+1\to Mx=M\left(y+1\right)$$
19	18	fveq2d	$$⊢x=y+1\to H\left(Mx\right)=H\left(M\left(y+1\right)\right)$$
20	17 19	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)$$
21		oveq1	$$⊢x=N\to x\underset{\dot{}}{\times }X=N\underset{\dot{}}{\times }X$$
22		oveq2	$$⊢x=N\to Mx=\mathrm{<mi\; mathcolor="\#808">M</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$
23	22	fveq2d	$$⊢x=N\to H\left(Mx\right)=H\left(\mathrm{<mi\; mathcolor="\#808">M</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right)$$
24	21 23	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)$$
25		reldmmhp	$$⊢\mathrm{Rel}\mathrm{dom}\mathrm{mHomP}$$
26	25 1 8	elfvov1	$$⊢\phi \to I\in \mathrm{V}$$
27	2 26 5	mplsca	$$⊢\phi \to R=\mathrm{Scalar}\left(P\right)$$
28	27	fveq2d	$$⊢\phi \to 1_R=1_{\mathrm{Scalar}\left(P\right)}$$
29	28	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)$$
30		eqid	$$⊢\mathrm{algSc}\left(P\right)=\mathrm{algSc}\left(P\right)$$
31		eqid	$$⊢\mathrm{Scalar}\left(P\right)=\mathrm{Scalar}\left(P\right)$$
32	2	mpllmod	$$⊢\left(I\in \mathrm{V}\wedge R\in \mathrm{Ring}\right)\to P\in \mathrm{LMod}$$
33	26 5 32	syl2anc	$$⊢\phi \to P\in \mathrm{LMod}$$
34	2	mplring	$$⊢\left(I\in \mathrm{V}\wedge R\in \mathrm{Ring}\right)\to P\in \mathrm{Ring}$$
35	26 5 34	syl2anc	$$⊢\phi \to P\in \mathrm{Ring}$$
36	30 31 33 35	ascl1	$$⊢\phi \to \mathrm{algSc}\left(P\right)\left(1_{\mathrm{Scalar}\left(P\right)}\right)=1_P$$
37	29 36	eqtrd	$$⊢\phi \to \mathrm{algSc}\left(P\right)\left(1_R\right)=1_P$$
38		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
39		eqid	$$⊢1_R=1_R$$
40	38 39	ringidcl	$$⊢R\in \mathrm{Ring}\to 1_R\in {\mathrm{Base}}_R$$
41	5 40	syl	$$⊢\phi \to 1_R\in {\mathrm{Base}}_R$$
42	1 2 30 38 26 5 41	mhpsclcl	$$⊢\phi \to \mathrm{algSc}\left(P\right)\left(1_R\right)\in H\left(0\right)$$
43	37 42	eqeltrrd	$$⊢\phi \to 1_P\in H\left(0\right)$$
44		eqid	$$⊢{\mathrm{Base}}_P={\mathrm{Base}}_P$$
45	1 2 44 26 5 6 8	mhpmpl	$$⊢\phi \to X\in {\mathrm{Base}}_P$$
46	3 44	mgpbas	$$⊢{\mathrm{Base}}_P={\mathrm{Base}}_T$$
47		eqid	$$⊢1_P=1_P$$
48	3 47	ringidval	$$⊢1_P=0_T$$
49	46 48 4	mulg0	$$⊢X\in {\mathrm{Base}}_P\to 0\underset{\dot{}}{\times }X=1_P$$
50	45 49	syl	$$⊢\phi \to 0\underset{\dot{}}{\times }X=1_P$$
51	6	nn0cnd	$$⊢\phi \to M\in ℂ$$
52	51	mul01d	$$⊢\phi \to \mathrm{<mi\; mathcolor="\#808">M</mi>}\cdot 0=0$$
53	52	fveq2d	$$⊢\phi \to H\left(\mathrm{<mi\; mathcolor="\#808">M</mi>}\cdot 0\right)=H\left(0\right)$$
54	43 50 53	3eltr4d	$$⊢\phi \to 0\underset{\dot{}}{\times }X\in H\left(\mathrm{<mi\; mathcolor="\#808">M</mi>}\cdot 0\right)$$
55		eqid	$$⊢{\cdot }_P={\cdot }_P$$
56	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}$$
57	6	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 {\mathbb{N}}_0$$
58		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$$
59	57 58	nn0mulcld	$$⊢\left(\left(\phi \wedge y\in {\mathbb{N}}_0\right)\wedge y\underset{\dot{}}{\times }X\in H\left(My\right)\right)\to My\in {\mathbb{N}}_0$$
60		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)$$
61	8	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)$$
62	1 2 55 56 59 57 60 61	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)$$
63	3	ringmgp	$$⊢P\in \mathrm{Ring}\to T\in \mathrm{Mnd}$$
64	35 63	syl	$$⊢\phi \to T\in \mathrm{Mnd}$$
65	64	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}$$
66	45	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$$
67	3 55	mgpplusg	$$⊢{\cdot }_P={+}_T$$
68	46 4 67	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$$
69	65 58 66 68	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$$
70	51	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 ℂ$$
71	58	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 ℂ$$
72		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 ℂ$$
73	70 71 72	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$$
74	70	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$$
75	74	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$$
76	73 75	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$$
77	76	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)$$
78	62 69 77	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)$$
79	12 16 20 24 54 78	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)$$
80	7 79	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)$$