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