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 mHomP R$
	mhppwdeg.p	$⊢ P = I mPoly R$
	mhppwdeg.t	$⊢ T = {mulGrp}_{P}$
	mhppwdeg.e	$⊢ \underset{˙}{\times} = \cdot_{T}$
	mhppwdeg.r	$⊢ φ \to R \in Ring$
	mhppwdeg.m	$⊢ φ \to M \in ℕ_{0}$
	mhppwdeg.n	$⊢ φ \to N \in ℕ_{0}$
	mhppwdeg.x	$⊢ φ \to X \in H (M)$
Assertion	mhppwdeg	$⊢ φ \to N \underset{˙}{\times} X \in H (M \cdot 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	$⊢ \underset{˙}{\times} = \cdot_{T}$
5		mhppwdeg.r	$⊢ φ \to R \in Ring$
6		mhppwdeg.m	$⊢ φ \to M \in ℕ_{0}$
7		mhppwdeg.n	$⊢ φ \to N \in ℕ_{0}$
8		mhppwdeg.x	$⊢ φ \to X \in H (M)$
9		oveq1	$⊢ x = 0 \to x \underset{˙}{\times} X = 0 \underset{˙}{\times} X$
10		oveq2	$⊢ x = 0 \to M x = M \cdot 0$
11	10	fveq2d	$⊢ x = 0 \to H (M x) = H (M \cdot 0)$
12	9 11	eleq12d	$⊢ x = 0 \to (x \underset{˙}{\times} X \in H (M x) \leftrightarrow 0 \underset{˙}{\times} X \in H (M \cdot 0))$
13		oveq1	$⊢ x = y \to x \underset{˙}{\times} X = y \underset{˙}{\times} X$
14		oveq2	$⊢ x = y \to M x = M y$
15	14	fveq2d	$⊢ x = y \to H (M x) = H (M y)$
16	13 15	eleq12d	$⊢ x = y \to (x \underset{˙}{\times} X \in H (M x) \leftrightarrow y \underset{˙}{\times} X \in H (M y))$
17		oveq1	$⊢ x = y + 1 \to x \underset{˙}{\times} X = (y + 1) \underset{˙}{\times} X$
18		oveq2	$⊢ x = y + 1 \to M x = M (y + 1)$
19	18	fveq2d	$⊢ x = y + 1 \to H (M x) = H (M (y + 1))$
20	17 19	eleq12d	$⊢ x = y + 1 \to (x \underset{˙}{\times} X \in H (M x) \leftrightarrow (y + 1) \underset{˙}{\times} X \in H (M (y + 1)))$
21		oveq1	$⊢ x = N \to x \underset{˙}{\times} X = N \underset{˙}{\times} X$
22		oveq2	$⊢ x = N \to M x = M \cdot N$
23	22	fveq2d	$⊢ x = N \to H (M x) = H (M \cdot N)$
24	21 23	eleq12d	$⊢ x = N \to (x \underset{˙}{\times} X \in H (M x) \leftrightarrow N \underset{˙}{\times} X \in H (M \cdot N))$
25		reldmmhp	$⊢ Rel dom mHomP$
26	25 1 8	elfvov1	$⊢ φ \to I \in V$
27	2 26 5	mplsca	$⊢ φ \to R = Scalar (P)$
28	27	fveq2d	$⊢ φ \to 1_{R} = 1_{Scalar (P)}$
29	28	fveq2d	$⊢ φ \to algSc (P) (1_{R}) = algSc (P) (1_{Scalar (P)})$
30		eqid	$⊢ algSc (P) = algSc (P)$
31		eqid	$⊢ Scalar (P) = Scalar (P)$
32	2 26 5	mpllmodd	$⊢ φ \to P \in LMod$
33	2 26 5	mplringd	$⊢ φ \to P \in Ring$
34	30 31 32 33	ascl1	$⊢ φ \to algSc (P) (1_{Scalar (P)}) = 1_{P}$
35	29 34	eqtrd	$⊢ φ \to algSc (P) (1_{R}) = 1_{P}$
36		eqid	$⊢ {Base}_{R} = {Base}_{R}$
37		eqid	$⊢ 1_{R} = 1_{R}$
38	36 37	ringidcl	$⊢ R \in Ring \to 1_{R} \in {Base}_{R}$
39	5 38	syl	$⊢ φ \to 1_{R} \in {Base}_{R}$
40	1 2 30 36 26 5 39	mhpsclcl	$⊢ φ \to algSc (P) (1_{R}) \in H (0)$
41	35 40	eqeltrrd	$⊢ φ \to 1_{P} \in H (0)$
42		eqid	$⊢ {Base}_{P} = {Base}_{P}$
43	1 2 42 26 5 6 8	mhpmpl	$⊢ φ \to X \in {Base}_{P}$
44	3 42	mgpbas	$⊢ {Base}_{P} = {Base}_{T}$
45		eqid	$⊢ 1_{P} = 1_{P}$
46	3 45	ringidval	$⊢ 1_{P} = 0_{T}$
47	44 46 4	mulg0	$⊢ X \in {Base}_{P} \to 0 \underset{˙}{\times} X = 1_{P}$
48	43 47	syl	$⊢ φ \to 0 \underset{˙}{\times} X = 1_{P}$
49	6	nn0cnd	$⊢ φ \to M \in ℂ$
50	49	mul01d	$⊢ φ \to M \cdot 0 = 0$
51	50	fveq2d	$⊢ φ \to H (M \cdot 0) = H (0)$
52	41 48 51	3eltr4d	$⊢ φ \to 0 \underset{˙}{\times} X \in H (M \cdot 0)$
53		eqid	$⊢ \cdot_{P} = \cdot_{P}$
54	5	ad2antrr	$⊢ ((φ \land y \in ℕ_{0}) \land y \underset{˙}{\times} X \in H (M y)) \to R \in Ring$
55	6	ad2antrr	$⊢ ((φ \land y \in ℕ_{0}) \land y \underset{˙}{\times} X \in H (M y)) \to M \in ℕ_{0}$
56		simplr	$⊢ ((φ \land y \in ℕ_{0}) \land y \underset{˙}{\times} X \in H (M y)) \to y \in ℕ_{0}$
57	55 56	nn0mulcld	$⊢ ((φ \land y \in ℕ_{0}) \land y \underset{˙}{\times} X \in H (M y)) \to M y \in ℕ_{0}$
58		simpr	$⊢ ((φ \land y \in ℕ_{0}) \land y \underset{˙}{\times} X \in H (M y)) \to y \underset{˙}{\times} X \in H (M y)$
59	8	ad2antrr	$⊢ ((φ \land y \in ℕ_{0}) \land y \underset{˙}{\times} X \in H (M y)) \to X \in H (M)$
60	1 2 53 54 57 55 58 59	mhpmulcl	$⊢ ((φ \land y \in ℕ_{0}) \land y \underset{˙}{\times} X \in H (M y)) \to (y \underset{˙}{\times} X) \cdot_{P} X \in H (M y + M)$
61	3	ringmgp	$⊢ P \in Ring \to T \in Mnd$
62	33 61	syl	$⊢ φ \to T \in Mnd$
63	62	ad2antrr	$⊢ ((φ \land y \in ℕ_{0}) \land y \underset{˙}{\times} X \in H (M y)) \to T \in Mnd$
64	43	ad2antrr	$⊢ ((φ \land y \in ℕ_{0}) \land y \underset{˙}{\times} X \in H (M y)) \to X \in {Base}_{P}$
65	3 53	mgpplusg	$⊢ \cdot_{P} = +_{T}$
66	44 4 65	mulgnn0p1	$⊢ (T \in Mnd \land y \in ℕ_{0} \land X \in {Base}_{P}) \to (y + 1) \underset{˙}{\times} X = (y \underset{˙}{\times} X) \cdot_{P} X$
67	63 56 64 66	syl3anc	$⊢ ((φ \land y \in ℕ_{0}) \land y \underset{˙}{\times} X \in H (M y)) \to (y + 1) \underset{˙}{\times} X = (y \underset{˙}{\times} X) \cdot_{P} X$
68	49	ad2antrr	$⊢ ((φ \land y \in ℕ_{0}) \land y \underset{˙}{\times} X \in H (M y)) \to M \in ℂ$
69	56	nn0cnd	$⊢ ((φ \land y \in ℕ_{0}) \land y \underset{˙}{\times} X \in H (M y)) \to y \in ℂ$
70		1cnd	$⊢ ((φ \land y \in ℕ_{0}) \land y \underset{˙}{\times} X \in H (M y)) \to 1 \in ℂ$
71	68 69 70	adddid	$⊢ ((φ \land y \in ℕ_{0}) \land y \underset{˙}{\times} X \in H (M y)) \to M (y + 1) = M y + M \cdot 1$
72	68	mulridd	$⊢ ((φ \land y \in ℕ_{0}) \land y \underset{˙}{\times} X \in H (M y)) \to M \cdot 1 = M$
73	72	oveq2d	$⊢ ((φ \land y \in ℕ_{0}) \land y \underset{˙}{\times} X \in H (M y)) \to M y + M \cdot 1 = M y + M$
74	71 73	eqtrd	$⊢ ((φ \land y \in ℕ_{0}) \land y \underset{˙}{\times} X \in H (M y)) \to M (y + 1) = M y + M$
75	74	fveq2d	$⊢ ((φ \land y \in ℕ_{0}) \land y \underset{˙}{\times} X \in H (M y)) \to H (M (y + 1)) = H (M y + M)$
76	60 67 75	3eltr4d	$⊢ ((φ \land y \in ℕ_{0}) \land y \underset{˙}{\times} X \in H (M y)) \to (y + 1) \underset{˙}{\times} X \in H (M (y + 1))$
77	12 16 20 24 52 76	nn0indd	$⊢ (φ \land N \in ℕ_{0}) \to N \underset{˙}{\times} X \in H (M \cdot N)$
78	7 77	mpdan	$⊢ φ \to N \underset{˙}{\times} X \in H (M \cdot N)$

Metamath Proof Explorer

Theorem mhppwdeg

Proof