deg1pwle

Description: Limiting degree of a variable power. (Contributed by Stefan O'Rear, 1-Apr-2015)

	Ref	Expression
Hypotheses	deg1pw.d	$⊢ D = \deg_{1} (R)$
	deg1pw.p	$⊢ P = {Poly}_{1} (R)$
	deg1pw.x	$⊢ X = {var}_{1} (R)$
	deg1pw.n	$⊢ N = {mulGrp}_{P}$
	deg1pw.e	$⊢ \underset{˙}{\times} = \cdot_{N}$
Assertion	deg1pwle	$⊢ (R \in Ring \land F \in ℕ_{0}) \to D (F \underset{˙}{\times} X) \leq F$

Proof

Step	Hyp	Ref	Expression
1		deg1pw.d	$⊢ D = \deg_{1} (R)$
2		deg1pw.p	$⊢ P = {Poly}_{1} (R)$
3		deg1pw.x	$⊢ X = {var}_{1} (R)$
4		deg1pw.n	$⊢ N = {mulGrp}_{P}$
5		deg1pw.e	$⊢ \underset{˙}{\times} = \cdot_{N}$
6	2	ply1lmod	$⊢ R \in Ring \to P \in LMod$
7		eqid	$⊢ {Base}_{P} = {Base}_{P}$
8	2 3 4 5 7	ply1moncl	$⊢ (R \in Ring \land F \in ℕ_{0}) \to F \underset{˙}{\times} X \in {Base}_{P}$
9		eqid	$⊢ Scalar (P) = Scalar (P)$
10		eqid	$⊢ \cdot_{P} = \cdot_{P}$
11		eqid	$⊢ 1_{Scalar (P)} = 1_{Scalar (P)}$
12	7 9 10 11	lmodvs1	$⊢ (P \in LMod \land F \underset{˙}{\times} X \in {Base}_{P}) \to 1_{Scalar (P)} \cdot_{P} (F \underset{˙}{\times} X) = F \underset{˙}{\times} X$
13	6 8 12	syl2an2r	$⊢ (R \in Ring \land F \in ℕ_{0}) \to 1_{Scalar (P)} \cdot_{P} (F \underset{˙}{\times} X) = F \underset{˙}{\times} X$
14	13	fveq2d	$⊢ (R \in Ring \land F \in ℕ_{0}) \to D (1_{Scalar (P)} \cdot_{P} (F \underset{˙}{\times} X)) = D (F \underset{˙}{\times} X)$
15		simpl	$⊢ (R \in Ring \land F \in ℕ_{0}) \to R \in Ring$
16	2	ply1sca	$⊢ R \in Ring \to R = Scalar (P)$
17	16	fveq2d	$⊢ R \in Ring \to 1_{R} = 1_{Scalar (P)}$
18		eqid	$⊢ {Base}_{R} = {Base}_{R}$
19		eqid	$⊢ 1_{R} = 1_{R}$
20	18 19	ringidcl	$⊢ R \in Ring \to 1_{R} \in {Base}_{R}$
21	17 20	eqeltrrd	$⊢ R \in Ring \to 1_{Scalar (P)} \in {Base}_{R}$
22	21	adantr	$⊢ (R \in Ring \land F \in ℕ_{0}) \to 1_{Scalar (P)} \in {Base}_{R}$
23		simpr	$⊢ (R \in Ring \land F \in ℕ_{0}) \to F \in ℕ_{0}$
24	1 18 2 3 10 4 5	deg1tmle	$⊢ (R \in Ring \land 1_{Scalar (P)} \in {Base}_{R} \land F \in ℕ_{0}) \to D (1_{Scalar (P)} \cdot_{P} (F \underset{˙}{\times} X)) \leq F$
25	15 22 23 24	syl3anc	$⊢ (R \in Ring \land F \in ℕ_{0}) \to D (1_{Scalar (P)} \cdot_{P} (F \underset{˙}{\times} X)) \leq F$
26	14 25	eqbrtrrd	$⊢ (R \in Ring \land F \in ℕ_{0}) \to D (F \underset{˙}{\times} X) \leq F$

Metamath Proof Explorer

Theorem deg1pwle

Proof