Theorem mhppwdeg

Description: Degree of a homogeneous polynomial raised to a power. General version of deg1pw . (Contributed by SN, 26-Jul-2024)

	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.i	$$⊢\phi \to I\in V$$
	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.i	$$⊢\phi \to I\in V$$
6		mhppwdeg.r	$$⊢\phi \to R\in \mathrm{Ring}$$
7		mhppwdeg.m	$$⊢\phi \to M\in {\mathbb{N}}_0$$
8		mhppwdeg.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
9		mhppwdeg.x	$$⊢\phi \to X\in H\left(M\right)$$
10		oveq1	$$⊢x=0\to x\underset{\dot{}}{\times }X=0\underset{\dot{}}{\times }X$$
11		oveq2	$$⊢x=0\to Mx=\mathrm{<mi\; mathcolor="\#808">M</mi>}\cdot 0$$
12	11	fveq2d	$$⊢x=0\to H\left(Mx\right)=H\left(\mathrm{<mi\; mathcolor="\#808">M</mi>}\cdot 0\right)$$
13	10 12	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)$$
14		oveq1	$$⊢x=y\to x\underset{\dot{}}{\times }X=y\underset{\dot{}}{\times }X$$
15		oveq2	$$⊢x=y\to Mx=My$$
16	15	fveq2d	$$⊢x=y\to H\left(Mx\right)=H\left(My\right)$$
17	14 16	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)$$
18		oveq1	$$⊢x=y+1\to x\underset{\dot{}}{\times }X=\left(y+1\right)\underset{\dot{}}{\times }X$$
19		oveq2	$$⊢x=y+1\to Mx=M\left(y+1\right)$$
20	19	fveq2d	$$⊢x=y+1\to H\left(Mx\right)=H\left(M\left(y+1\right)\right)$$
21	18 20	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)$$
22		oveq1	$$⊢x=N\to x\underset{\dot{}}{\times }X=N\underset{\dot{}}{\times }X$$
23		oveq2	$$⊢x=N\to Mx=\mathrm{<mi\; mathcolor="\#808">M</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$
24	23	fveq2d	$$⊢x=N\to H\left(Mx\right)=H\left(\mathrm{<mi\; mathcolor="\#808">M</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right)$$
25	22 24	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)$$
26	2 5 6	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	mpllmod	$$⊢\left(I\in V\wedge R\in \mathrm{Ring}\right)\to P\in \mathrm{LMod}$$
32	5 6 31	syl2anc	$$⊢\phi \to P\in \mathrm{LMod}$$
33	2	mplring	$$⊢\left(I\in V\wedge R\in \mathrm{Ring}\right)\to P\in \mathrm{Ring}$$
34	5 6 33	syl2anc	$$⊢\phi \to P\in \mathrm{Ring}$$
35	29 30 32 34	ascl1	$$⊢\phi \to \mathrm{algSc}\left(P\right)\left(1_{\mathrm{Scalar}\left(P\right)}\right)=1_P$$
36	28 35	eqtrd	$$⊢\phi \to \mathrm{algSc}\left(P\right)\left(1_R\right)=1_P$$
37		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
38		eqid	$$⊢1_R=1_R$$
39	37 38	ringidcl	$$⊢R\in \mathrm{Ring}\to 1_R\in {\mathrm{Base}}_R$$
40	6 39	syl	$$⊢\phi \to 1_R\in {\mathrm{Base}}_R$$
41	1 2 29 37 5 6 40	mhpsclcl	$$⊢\phi \to \mathrm{algSc}\left(P\right)\left(1_R\right)\in H\left(0\right)$$
42	36 41	eqeltrrd	$$⊢\phi \to 1_P\in H\left(0\right)$$
43		eqid	$$⊢{\mathrm{Base}}_P={\mathrm{Base}}_P$$
44	1 2 43 5 6 7 9	mhpmpl	$$⊢\phi \to X\in {\mathrm{Base}}_P$$
45	3 43	mgpbas	$$⊢{\mathrm{Base}}_P={\mathrm{Base}}_T$$
46		eqid	$$⊢1_P=1_P$$
47	3 46	ringidval	$$⊢1_P=0_T$$
48	45 47 4	mulg0	$$⊢X\in {\mathrm{Base}}_P\to 0\underset{\dot{}}{\times }X=1_P$$
49	44 48	syl	$$⊢\phi \to 0\underset{\dot{}}{\times }X=1_P$$
50	7	nn0cnd	$$⊢\phi \to M\in ℂ$$
51	50	mul01d	$$⊢\phi \to \mathrm{<mi\; mathcolor="\#808">M</mi>}\cdot 0=0$$
52	51	fveq2d	$$⊢\phi \to H\left(\mathrm{<mi\; mathcolor="\#808">M</mi>}\cdot 0\right)=H\left(0\right)$$
53	42 49 52	3eltr4d	$$⊢\phi \to 0\underset{\dot{}}{\times }X\in H\left(\mathrm{<mi\; mathcolor="\#808">M</mi>}\cdot 0\right)$$
54		eqid	$$⊢{\cdot }_P={\cdot }_P$$
55	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 I\in V$$
56	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 R\in \mathrm{Ring}$$
57	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 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	9	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 54 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	34 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	44	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 54	mgpplusg	$$⊢{\cdot }_P={+}_T$$
68	45 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	50	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	mulid1d	$$⊢\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	13 17 21 25 53 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	8 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)$$