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 mHomP R )
	mhppwdeg.p	\|- P = ( I mPoly R )
	mhppwdeg.t	\|- T = ( mulGrp ` P )
	mhppwdeg.e	\|- .^ = ( .g ` T )
	mhppwdeg.r	\|- ( ph -> R e. Ring )
	mhppwdeg.n	\|- ( ph -> N e. NN0 )
	mhppwdeg.x	\|- ( ph -> X e. ( H ` M ) )
Assertion	mhppwdeg	\|- ( ph -> ( N .^ X ) e. ( H ` ( M x. N ) ) )

Proof

Step	Hyp	Ref	Expression
1		mhppwdeg.h	\|- H = ( I mHomP R )
2		mhppwdeg.p	\|- P = ( I mPoly R )
3		mhppwdeg.t	\|- T = ( mulGrp ` P )
4		mhppwdeg.e	\|- .^ = ( .g ` T )
5		mhppwdeg.r	\|- ( ph -> R e. Ring )
6		mhppwdeg.n	\|- ( ph -> N e. NN0 )
7		mhppwdeg.x	\|- ( ph -> X e. ( H ` M ) )
8		oveq1	\|- ( x = 0 -> ( x .^ X ) = ( 0 .^ X ) )
9		oveq2	\|- ( x = 0 -> ( M x. x ) = ( M x. 0 ) )
10	9	fveq2d	\|- ( x = 0 -> ( H ` ( M x. x ) ) = ( H ` ( M x. 0 ) ) )
11	8 10	eleq12d	\|- ( x = 0 -> ( ( x .^ X ) e. ( H ` ( M x. x ) ) <-> ( 0 .^ X ) e. ( H ` ( M x. 0 ) ) ) )
12		oveq1	\|- ( x = y -> ( x .^ X ) = ( y .^ X ) )
13		oveq2	\|- ( x = y -> ( M x. x ) = ( M x. y ) )
14	13	fveq2d	\|- ( x = y -> ( H ` ( M x. x ) ) = ( H ` ( M x. y ) ) )
15	12 14	eleq12d	\|- ( x = y -> ( ( x .^ X ) e. ( H ` ( M x. x ) ) <-> ( y .^ X ) e. ( H ` ( M x. y ) ) ) )
16		oveq1	\|- ( x = ( y + 1 ) -> ( x .^ X ) = ( ( y + 1 ) .^ X ) )
17		oveq2	\|- ( x = ( y + 1 ) -> ( M x. x ) = ( M x. ( y + 1 ) ) )
18	17	fveq2d	\|- ( x = ( y + 1 ) -> ( H ` ( M x. x ) ) = ( H ` ( M x. ( y + 1 ) ) ) )
19	16 18	eleq12d	\|- ( x = ( y + 1 ) -> ( ( x .^ X ) e. ( H ` ( M x. x ) ) <-> ( ( y + 1 ) .^ X ) e. ( H ` ( M x. ( y + 1 ) ) ) ) )
20		oveq1	\|- ( x = N -> ( x .^ X ) = ( N .^ X ) )
21		oveq2	\|- ( x = N -> ( M x. x ) = ( M x. N ) )
22	21	fveq2d	\|- ( x = N -> ( H ` ( M x. x ) ) = ( H ` ( M x. N ) ) )
23	20 22	eleq12d	\|- ( x = N -> ( ( x .^ X ) e. ( H ` ( M x. x ) ) <-> ( N .^ X ) e. ( H ` ( M x. N ) ) ) )
24		reldmmhp	\|- Rel dom mHomP
25	24 1 7	elfvov1	\|- ( ph -> I e. _V )
26	2 25 5	mplsca	\|- ( ph -> R = ( Scalar ` P ) )
27	26	fveq2d	\|- ( ph -> ( 1r ` R ) = ( 1r ` ( Scalar ` P ) ) )
28	27	fveq2d	\|- ( ph -> ( ( algSc ` P ) ` ( 1r ` R ) ) = ( ( algSc ` P ) ` ( 1r ` ( Scalar ` P ) ) ) )
29		eqid	\|- ( algSc ` P ) = ( algSc ` P )
30		eqid	\|- ( Scalar ` P ) = ( Scalar ` P )
31	2 25 5	mpllmodd	\|- ( ph -> P e. LMod )
32	2 25 5	mplringd	\|- ( ph -> P e. Ring )
33	29 30 31 32	ascl1	\|- ( ph -> ( ( algSc ` P ) ` ( 1r ` ( Scalar ` P ) ) ) = ( 1r ` P ) )
34	28 33	eqtrd	\|- ( ph -> ( ( algSc ` P ) ` ( 1r ` R ) ) = ( 1r ` P ) )
35		eqid	\|- ( Base ` R ) = ( Base ` R )
36		eqid	\|- ( 1r ` R ) = ( 1r ` R )
37	35 36	ringidcl	\|- ( R e. Ring -> ( 1r ` R ) e. ( Base ` R ) )
38	5 37	syl	\|- ( ph -> ( 1r ` R ) e. ( Base ` R ) )
39	1 2 29 35 25 5 38	mhpsclcl	\|- ( ph -> ( ( algSc ` P ) ` ( 1r ` R ) ) e. ( H ` 0 ) )
40	34 39	eqeltrrd	\|- ( ph -> ( 1r ` P ) e. ( H ` 0 ) )
41		eqid	\|- ( Base ` P ) = ( Base ` P )
42	1 2 41 7	mhpmpl	\|- ( ph -> X e. ( Base ` P ) )
43	3 41	mgpbas	\|- ( Base ` P ) = ( Base ` T )
44		eqid	\|- ( 1r ` P ) = ( 1r ` P )
45	3 44	ringidval	\|- ( 1r ` P ) = ( 0g ` T )
46	43 45 4	mulg0	\|- ( X e. ( Base ` P ) -> ( 0 .^ X ) = ( 1r ` P ) )
47	42 46	syl	\|- ( ph -> ( 0 .^ X ) = ( 1r ` P ) )
48	1 7	mhprcl	\|- ( ph -> M e. NN0 )
49	48	nn0cnd	\|- ( ph -> M e. CC )
50	49	mul01d	\|- ( ph -> ( M x. 0 ) = 0 )
51	50	fveq2d	\|- ( ph -> ( H ` ( M x. 0 ) ) = ( H ` 0 ) )
52	40 47 51	3eltr4d	\|- ( ph -> ( 0 .^ X ) e. ( H ` ( M x. 0 ) ) )
53		eqid	\|- ( .r ` P ) = ( .r ` P )
54	5	ad2antrr	\|- ( ( ( ph /\ y e. NN0 ) /\ ( y .^ X ) e. ( H ` ( M x. y ) ) ) -> R e. Ring )
55		simpr	\|- ( ( ( ph /\ y e. NN0 ) /\ ( y .^ X ) e. ( H ` ( M x. y ) ) ) -> ( y .^ X ) e. ( H ` ( M x. y ) ) )
56	7	ad2antrr	\|- ( ( ( ph /\ y e. NN0 ) /\ ( y .^ X ) e. ( H ` ( M x. y ) ) ) -> X e. ( H ` M ) )
57	1 2 53 54 55 56	mhpmulcl	\|- ( ( ( ph /\ y e. NN0 ) /\ ( y .^ X ) e. ( H ` ( M x. y ) ) ) -> ( ( y .^ X ) ( .r ` P ) X ) e. ( H ` ( ( M x. y ) + M ) ) )
58	3	ringmgp	\|- ( P e. Ring -> T e. Mnd )
59	32 58	syl	\|- ( ph -> T e. Mnd )
60	59	ad2antrr	\|- ( ( ( ph /\ y e. NN0 ) /\ ( y .^ X ) e. ( H ` ( M x. y ) ) ) -> T e. Mnd )
61		simplr	\|- ( ( ( ph /\ y e. NN0 ) /\ ( y .^ X ) e. ( H ` ( M x. y ) ) ) -> y e. NN0 )
62	42	ad2antrr	\|- ( ( ( ph /\ y e. NN0 ) /\ ( y .^ X ) e. ( H ` ( M x. y ) ) ) -> X e. ( Base ` P ) )
63	3 53	mgpplusg	\|- ( .r ` P ) = ( +g ` T )
64	43 4 63	mulgnn0p1	\|- ( ( T e. Mnd /\ y e. NN0 /\ X e. ( Base ` P ) ) -> ( ( y + 1 ) .^ X ) = ( ( y .^ X ) ( .r ` P ) X ) )
65	60 61 62 64	syl3anc	\|- ( ( ( ph /\ y e. NN0 ) /\ ( y .^ X ) e. ( H ` ( M x. y ) ) ) -> ( ( y + 1 ) .^ X ) = ( ( y .^ X ) ( .r ` P ) X ) )
66	49	ad2antrr	\|- ( ( ( ph /\ y e. NN0 ) /\ ( y .^ X ) e. ( H ` ( M x. y ) ) ) -> M e. CC )
67	61	nn0cnd	\|- ( ( ( ph /\ y e. NN0 ) /\ ( y .^ X ) e. ( H ` ( M x. y ) ) ) -> y e. CC )
68		1cnd	\|- ( ( ( ph /\ y e. NN0 ) /\ ( y .^ X ) e. ( H ` ( M x. y ) ) ) -> 1 e. CC )
69	66 67 68	adddid	\|- ( ( ( ph /\ y e. NN0 ) /\ ( y .^ X ) e. ( H ` ( M x. y ) ) ) -> ( M x. ( y + 1 ) ) = ( ( M x. y ) + ( M x. 1 ) ) )
70	66	mulridd	\|- ( ( ( ph /\ y e. NN0 ) /\ ( y .^ X ) e. ( H ` ( M x. y ) ) ) -> ( M x. 1 ) = M )
71	70	oveq2d	\|- ( ( ( ph /\ y e. NN0 ) /\ ( y .^ X ) e. ( H ` ( M x. y ) ) ) -> ( ( M x. y ) + ( M x. 1 ) ) = ( ( M x. y ) + M ) )
72	69 71	eqtrd	\|- ( ( ( ph /\ y e. NN0 ) /\ ( y .^ X ) e. ( H ` ( M x. y ) ) ) -> ( M x. ( y + 1 ) ) = ( ( M x. y ) + M ) )
73	72	fveq2d	\|- ( ( ( ph /\ y e. NN0 ) /\ ( y .^ X ) e. ( H ` ( M x. y ) ) ) -> ( H ` ( M x. ( y + 1 ) ) ) = ( H ` ( ( M x. y ) + M ) ) )
74	57 65 73	3eltr4d	\|- ( ( ( ph /\ y e. NN0 ) /\ ( y .^ X ) e. ( H ` ( M x. y ) ) ) -> ( ( y + 1 ) .^ X ) e. ( H ` ( M x. ( y + 1 ) ) ) )
75	11 15 19 23 52 74	nn0indd	\|- ( ( ph /\ N e. NN0 ) -> ( N .^ X ) e. ( H ` ( M x. N ) ) )
76	6 75	mpdan	\|- ( ph -> ( N .^ X ) e. ( H ` ( M x. N ) ) )

Metamath Proof Explorer

Theorem mhppwdeg

Proof