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	⊢ 𝐻 = ( 𝐼 mHomP 𝑅 )
	mhppwdeg.p	⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
	mhppwdeg.t	⊢ 𝑇 = ( mulGrp ‘ 𝑃 )
	mhppwdeg.e	⊢ ↑ = ( .g ‘ 𝑇 )
	mhppwdeg.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
	mhppwdeg.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
	mhppwdeg.x	⊢ ( 𝜑 → 𝑋 ∈ ( 𝐻 ‘ 𝑀 ) )
Assertion	mhppwdeg	⊢ ( 𝜑 → ( 𝑁 ↑ 𝑋 ) ∈ ( 𝐻 ‘ ( 𝑀 · 𝑁 ) ) )

Proof

Step	Hyp	Ref	Expression
1		mhppwdeg.h	⊢ 𝐻 = ( 𝐼 mHomP 𝑅 )
2		mhppwdeg.p	⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
3		mhppwdeg.t	⊢ 𝑇 = ( mulGrp ‘ 𝑃 )
4		mhppwdeg.e	⊢ ↑ = ( .g ‘ 𝑇 )
5		mhppwdeg.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
6		mhppwdeg.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
7		mhppwdeg.x	⊢ ( 𝜑 → 𝑋 ∈ ( 𝐻 ‘ 𝑀 ) )
8		oveq1	⊢ ( 𝑥 = 0 → ( 𝑥 ↑ 𝑋 ) = ( 0 ↑ 𝑋 ) )
9		oveq2	⊢ ( 𝑥 = 0 → ( 𝑀 · 𝑥 ) = ( 𝑀 · 0 ) )
10	9	fveq2d	⊢ ( 𝑥 = 0 → ( 𝐻 ‘ ( 𝑀 · 𝑥 ) ) = ( 𝐻 ‘ ( 𝑀 · 0 ) ) )
11	8 10	eleq12d	⊢ ( 𝑥 = 0 → ( ( 𝑥 ↑ 𝑋 ) ∈ ( 𝐻 ‘ ( 𝑀 · 𝑥 ) ) ↔ ( 0 ↑ 𝑋 ) ∈ ( 𝐻 ‘ ( 𝑀 · 0 ) ) ) )
12		oveq1	⊢ ( 𝑥 = 𝑦 → ( 𝑥 ↑ 𝑋 ) = ( 𝑦 ↑ 𝑋 ) )
13		oveq2	⊢ ( 𝑥 = 𝑦 → ( 𝑀 · 𝑥 ) = ( 𝑀 · 𝑦 ) )
14	13	fveq2d	⊢ ( 𝑥 = 𝑦 → ( 𝐻 ‘ ( 𝑀 · 𝑥 ) ) = ( 𝐻 ‘ ( 𝑀 · 𝑦 ) ) )
15	12 14	eleq12d	⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ↑ 𝑋 ) ∈ ( 𝐻 ‘ ( 𝑀 · 𝑥 ) ) ↔ ( 𝑦 ↑ 𝑋 ) ∈ ( 𝐻 ‘ ( 𝑀 · 𝑦 ) ) ) )
16		oveq1	⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( 𝑥 ↑ 𝑋 ) = ( ( 𝑦 + 1 ) ↑ 𝑋 ) )
17		oveq2	⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( 𝑀 · 𝑥 ) = ( 𝑀 · ( 𝑦 + 1 ) ) )
18	17	fveq2d	⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( 𝐻 ‘ ( 𝑀 · 𝑥 ) ) = ( 𝐻 ‘ ( 𝑀 · ( 𝑦 + 1 ) ) ) )
19	16 18	eleq12d	⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( ( 𝑥 ↑ 𝑋 ) ∈ ( 𝐻 ‘ ( 𝑀 · 𝑥 ) ) ↔ ( ( 𝑦 + 1 ) ↑ 𝑋 ) ∈ ( 𝐻 ‘ ( 𝑀 · ( 𝑦 + 1 ) ) ) ) )
20		oveq1	⊢ ( 𝑥 = 𝑁 → ( 𝑥 ↑ 𝑋 ) = ( 𝑁 ↑ 𝑋 ) )
21		oveq2	⊢ ( 𝑥 = 𝑁 → ( 𝑀 · 𝑥 ) = ( 𝑀 · 𝑁 ) )
22	21	fveq2d	⊢ ( 𝑥 = 𝑁 → ( 𝐻 ‘ ( 𝑀 · 𝑥 ) ) = ( 𝐻 ‘ ( 𝑀 · 𝑁 ) ) )
23	20 22	eleq12d	⊢ ( 𝑥 = 𝑁 → ( ( 𝑥 ↑ 𝑋 ) ∈ ( 𝐻 ‘ ( 𝑀 · 𝑥 ) ) ↔ ( 𝑁 ↑ 𝑋 ) ∈ ( 𝐻 ‘ ( 𝑀 · 𝑁 ) ) ) )
24		reldmmhp	⊢ Rel dom mHomP
25	24 1 7	elfvov1	⊢ ( 𝜑 → 𝐼 ∈ V )
26	2 25 5	mplsca	⊢ ( 𝜑 → 𝑅 = ( Scalar ‘ 𝑃 ) )
27	26	fveq2d	⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) = ( 1r ‘ ( Scalar ‘ 𝑃 ) ) )
28	27	fveq2d	⊢ ( 𝜑 → ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑅 ) ) = ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ ( Scalar ‘ 𝑃 ) ) ) )
29		eqid	⊢ ( algSc ‘ 𝑃 ) = ( algSc ‘ 𝑃 )
30		eqid	⊢ ( Scalar ‘ 𝑃 ) = ( Scalar ‘ 𝑃 )
31	2 25 5	mpllmodd	⊢ ( 𝜑 → 𝑃 ∈ LMod )
32	2 25 5	mplringd	⊢ ( 𝜑 → 𝑃 ∈ Ring )
33	29 30 31 32	ascl1	⊢ ( 𝜑 → ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ ( Scalar ‘ 𝑃 ) ) ) = ( 1r ‘ 𝑃 ) )
34	28 33	eqtrd	⊢ ( 𝜑 → ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑅 ) ) = ( 1r ‘ 𝑃 ) )
35		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
36		eqid	⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
37	35 36	ringidcl	⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
38	5 37	syl	⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
39	1 2 29 35 25 5 38	mhpsclcl	⊢ ( 𝜑 → ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑅 ) ) ∈ ( 𝐻 ‘ 0 ) )
40	34 39	eqeltrrd	⊢ ( 𝜑 → ( 1r ‘ 𝑃 ) ∈ ( 𝐻 ‘ 0 ) )
41		eqid	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
42	1 2 41 7	mhpmpl	⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝑃 ) )
43	3 41	mgpbas	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑇 )
44		eqid	⊢ ( 1r ‘ 𝑃 ) = ( 1r ‘ 𝑃 )
45	3 44	ringidval	⊢ ( 1r ‘ 𝑃 ) = ( 0g ‘ 𝑇 )
46	43 45 4	mulg0	⊢ ( 𝑋 ∈ ( Base ‘ 𝑃 ) → ( 0 ↑ 𝑋 ) = ( 1r ‘ 𝑃 ) )
47	42 46	syl	⊢ ( 𝜑 → ( 0 ↑ 𝑋 ) = ( 1r ‘ 𝑃 ) )
48	1 7	mhprcl	⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
49	48	nn0cnd	⊢ ( 𝜑 → 𝑀 ∈ ℂ )
50	49	mul01d	⊢ ( 𝜑 → ( 𝑀 · 0 ) = 0 )
51	50	fveq2d	⊢ ( 𝜑 → ( 𝐻 ‘ ( 𝑀 · 0 ) ) = ( 𝐻 ‘ 0 ) )
52	40 47 51	3eltr4d	⊢ ( 𝜑 → ( 0 ↑ 𝑋 ) ∈ ( 𝐻 ‘ ( 𝑀 · 0 ) ) )
53		eqid	⊢ ( .r ‘ 𝑃 ) = ( .r ‘ 𝑃 )
54	5	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ0 ) ∧ ( 𝑦 ↑ 𝑋 ) ∈ ( 𝐻 ‘ ( 𝑀 · 𝑦 ) ) ) → 𝑅 ∈ Ring )
55		simpr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ0 ) ∧ ( 𝑦 ↑ 𝑋 ) ∈ ( 𝐻 ‘ ( 𝑀 · 𝑦 ) ) ) → ( 𝑦 ↑ 𝑋 ) ∈ ( 𝐻 ‘ ( 𝑀 · 𝑦 ) ) )
56	7	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ0 ) ∧ ( 𝑦 ↑ 𝑋 ) ∈ ( 𝐻 ‘ ( 𝑀 · 𝑦 ) ) ) → 𝑋 ∈ ( 𝐻 ‘ 𝑀 ) )
57	1 2 53 54 55 56	mhpmulcl	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ0 ) ∧ ( 𝑦 ↑ 𝑋 ) ∈ ( 𝐻 ‘ ( 𝑀 · 𝑦 ) ) ) → ( ( 𝑦 ↑ 𝑋 ) ( .r ‘ 𝑃 ) 𝑋 ) ∈ ( 𝐻 ‘ ( ( 𝑀 · 𝑦 ) + 𝑀 ) ) )
58	3	ringmgp	⊢ ( 𝑃 ∈ Ring → 𝑇 ∈ Mnd )
59	32 58	syl	⊢ ( 𝜑 → 𝑇 ∈ Mnd )
60	59	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ0 ) ∧ ( 𝑦 ↑ 𝑋 ) ∈ ( 𝐻 ‘ ( 𝑀 · 𝑦 ) ) ) → 𝑇 ∈ Mnd )
61		simplr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ0 ) ∧ ( 𝑦 ↑ 𝑋 ) ∈ ( 𝐻 ‘ ( 𝑀 · 𝑦 ) ) ) → 𝑦 ∈ ℕ0 )
62	42	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ0 ) ∧ ( 𝑦 ↑ 𝑋 ) ∈ ( 𝐻 ‘ ( 𝑀 · 𝑦 ) ) ) → 𝑋 ∈ ( Base ‘ 𝑃 ) )
63	3 53	mgpplusg	⊢ ( .r ‘ 𝑃 ) = ( +g ‘ 𝑇 )
64	43 4 63	mulgnn0p1	⊢ ( ( 𝑇 ∈ Mnd ∧ 𝑦 ∈ ℕ0 ∧ 𝑋 ∈ ( Base ‘ 𝑃 ) ) → ( ( 𝑦 + 1 ) ↑ 𝑋 ) = ( ( 𝑦 ↑ 𝑋 ) ( .r ‘ 𝑃 ) 𝑋 ) )
65	60 61 62 64	syl3anc	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ0 ) ∧ ( 𝑦 ↑ 𝑋 ) ∈ ( 𝐻 ‘ ( 𝑀 · 𝑦 ) ) ) → ( ( 𝑦 + 1 ) ↑ 𝑋 ) = ( ( 𝑦 ↑ 𝑋 ) ( .r ‘ 𝑃 ) 𝑋 ) )
66	49	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ0 ) ∧ ( 𝑦 ↑ 𝑋 ) ∈ ( 𝐻 ‘ ( 𝑀 · 𝑦 ) ) ) → 𝑀 ∈ ℂ )
67	61	nn0cnd	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ0 ) ∧ ( 𝑦 ↑ 𝑋 ) ∈ ( 𝐻 ‘ ( 𝑀 · 𝑦 ) ) ) → 𝑦 ∈ ℂ )
68		1cnd	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ0 ) ∧ ( 𝑦 ↑ 𝑋 ) ∈ ( 𝐻 ‘ ( 𝑀 · 𝑦 ) ) ) → 1 ∈ ℂ )
69	66 67 68	adddid	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ0 ) ∧ ( 𝑦 ↑ 𝑋 ) ∈ ( 𝐻 ‘ ( 𝑀 · 𝑦 ) ) ) → ( 𝑀 · ( 𝑦 + 1 ) ) = ( ( 𝑀 · 𝑦 ) + ( 𝑀 · 1 ) ) )
70	66	mulridd	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ0 ) ∧ ( 𝑦 ↑ 𝑋 ) ∈ ( 𝐻 ‘ ( 𝑀 · 𝑦 ) ) ) → ( 𝑀 · 1 ) = 𝑀 )
71	70	oveq2d	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ0 ) ∧ ( 𝑦 ↑ 𝑋 ) ∈ ( 𝐻 ‘ ( 𝑀 · 𝑦 ) ) ) → ( ( 𝑀 · 𝑦 ) + ( 𝑀 · 1 ) ) = ( ( 𝑀 · 𝑦 ) + 𝑀 ) )
72	69 71	eqtrd	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ0 ) ∧ ( 𝑦 ↑ 𝑋 ) ∈ ( 𝐻 ‘ ( 𝑀 · 𝑦 ) ) ) → ( 𝑀 · ( 𝑦 + 1 ) ) = ( ( 𝑀 · 𝑦 ) + 𝑀 ) )
73	72	fveq2d	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ0 ) ∧ ( 𝑦 ↑ 𝑋 ) ∈ ( 𝐻 ‘ ( 𝑀 · 𝑦 ) ) ) → ( 𝐻 ‘ ( 𝑀 · ( 𝑦 + 1 ) ) ) = ( 𝐻 ‘ ( ( 𝑀 · 𝑦 ) + 𝑀 ) ) )
74	57 65 73	3eltr4d	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ0 ) ∧ ( 𝑦 ↑ 𝑋 ) ∈ ( 𝐻 ‘ ( 𝑀 · 𝑦 ) ) ) → ( ( 𝑦 + 1 ) ↑ 𝑋 ) ∈ ( 𝐻 ‘ ( 𝑀 · ( 𝑦 + 1 ) ) ) )
75	11 15 19 23 52 74	nn0indd	⊢ ( ( 𝜑 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑁 ↑ 𝑋 ) ∈ ( 𝐻 ‘ ( 𝑀 · 𝑁 ) ) )
76	6 75	mpdan	⊢ ( 𝜑 → ( 𝑁 ↑ 𝑋 ) ∈ ( 𝐻 ‘ ( 𝑀 · 𝑁 ) ) )