deg1tm

Description: Exact degree of a polynomial term. (Contributed by Stefan O'Rear, 27-Mar-2015)

	Ref	Expression
Hypotheses	deg1tm.d	$⊢ D = \deg_{1} (R)$
	deg1tm.k	$⊢ K = {Base}_{R}$
	deg1tm.p	$⊢ P = {Poly}_{1} (R)$
	deg1tm.x	$⊢ X = {var}_{1} (R)$
	deg1tm.m	$⊢ \underset{˙}{\cdot} = \cdot_{P}$
	deg1tm.n	$⊢ N = {mulGrp}_{P}$
	deg1tm.e	$⊢ \underset{˙}{\times} = \cdot_{N}$
	deg1tm.z	$⊢ \underset{˙}{0} = 0_{R}$
Assertion	deg1tm	$⊢ (R \in Ring \land (C \in K \land C \neq \underset{˙}{0}) \land F \in ℕ_{0}) \to D (C \underset{˙}{\cdot} (F \underset{˙}{\times} X)) = F$

Proof

Step	Hyp	Ref	Expression
1		deg1tm.d	$⊢ D = \deg_{1} (R)$
2		deg1tm.k	$⊢ K = {Base}_{R}$
3		deg1tm.p	$⊢ P = {Poly}_{1} (R)$
4		deg1tm.x	$⊢ X = {var}_{1} (R)$
5		deg1tm.m	$⊢ \underset{˙}{\cdot} = \cdot_{P}$
6		deg1tm.n	$⊢ N = {mulGrp}_{P}$
7		deg1tm.e	$⊢ \underset{˙}{\times} = \cdot_{N}$
8		deg1tm.z	$⊢ \underset{˙}{0} = 0_{R}$
9		eqid	$⊢ {Base}_{P} = {Base}_{P}$
10	2 3 4 5 6 7 9	ply1tmcl	$⊢ (R \in Ring \land C \in K \land F \in ℕ_{0}) \to C \underset{˙}{\cdot} (F \underset{˙}{\times} X) \in {Base}_{P}$
11	10	3adant2r	$⊢ (R \in Ring \land (C \in K \land C \neq \underset{˙}{0}) \land F \in ℕ_{0}) \to C \underset{˙}{\cdot} (F \underset{˙}{\times} X) \in {Base}_{P}$
12	1 3 9	deg1xrcl	$⊢ C \underset{˙}{\cdot} (F \underset{˙}{\times} X) \in {Base}_{P} \to D (C \underset{˙}{\cdot} (F \underset{˙}{\times} X)) \in ℝ^{*}$
13	11 12	syl	$⊢ (R \in Ring \land (C \in K \land C \neq \underset{˙}{0}) \land F \in ℕ_{0}) \to D (C \underset{˙}{\cdot} (F \underset{˙}{\times} X)) \in ℝ^{*}$
14		simp3	$⊢ (R \in Ring \land (C \in K \land C \neq \underset{˙}{0}) \land F \in ℕ_{0}) \to F \in ℕ_{0}$
15	14	nn0red	$⊢ (R \in Ring \land (C \in K \land C \neq \underset{˙}{0}) \land F \in ℕ_{0}) \to F \in ℝ$
16	15	rexrd	$⊢ (R \in Ring \land (C \in K \land C \neq \underset{˙}{0}) \land F \in ℕ_{0}) \to F \in ℝ^{*}$
17	1 2 3 4 5 6 7	deg1tmle	$⊢ (R \in Ring \land C \in K \land F \in ℕ_{0}) \to D (C \underset{˙}{\cdot} (F \underset{˙}{\times} X)) \leq F$
18	17	3adant2r	$⊢ (R \in Ring \land (C \in K \land C \neq \underset{˙}{0}) \land F \in ℕ_{0}) \to D (C \underset{˙}{\cdot} (F \underset{˙}{\times} X)) \leq F$
19	8 2 3 4 5 6 7	coe1tmfv1	$⊢ (R \in Ring \land C \in K \land F \in ℕ_{0}) \to {coe}_{1} (C \underset{˙}{\cdot} (F \underset{˙}{\times} X)) (F) = C$
20	19	3adant2r	$⊢ (R \in Ring \land (C \in K \land C \neq \underset{˙}{0}) \land F \in ℕ_{0}) \to {coe}_{1} (C \underset{˙}{\cdot} (F \underset{˙}{\times} X)) (F) = C$
21		simp2r	$⊢ (R \in Ring \land (C \in K \land C \neq \underset{˙}{0}) \land F \in ℕ_{0}) \to C \neq \underset{˙}{0}$
22	20 21	eqnetrd	$⊢ (R \in Ring \land (C \in K \land C \neq \underset{˙}{0}) \land F \in ℕ_{0}) \to {coe}_{1} (C \underset{˙}{\cdot} (F \underset{˙}{\times} X)) (F) \neq \underset{˙}{0}$
23		eqid	$⊢ {coe}_{1} (C \underset{˙}{\cdot} (F \underset{˙}{\times} X)) = {coe}_{1} (C \underset{˙}{\cdot} (F \underset{˙}{\times} X))$
24	1 3 9 8 23	deg1ge	$⊢ (C \underset{˙}{\cdot} (F \underset{˙}{\times} X) \in {Base}_{P} \land F \in ℕ_{0} \land {coe}_{1} (C \underset{˙}{\cdot} (F \underset{˙}{\times} X)) (F) \neq \underset{˙}{0}) \to F \leq D (C \underset{˙}{\cdot} (F \underset{˙}{\times} X))$
25	11 14 22 24	syl3anc	$⊢ (R \in Ring \land (C \in K \land C \neq \underset{˙}{0}) \land F \in ℕ_{0}) \to F \leq D (C \underset{˙}{\cdot} (F \underset{˙}{\times} X))$
26	13 16 18 25	xrletrid	$⊢ (R \in Ring \land (C \in K \land C \neq \underset{˙}{0}) \land F \in ℕ_{0}) \to D (C \underset{˙}{\cdot} (F \underset{˙}{\times} X)) = F$

Metamath Proof Explorer

Theorem deg1tm

Proof