deg1mul3le

Description: Degree of multiplication of a polynomial on the left by a scalar. (Contributed by Stefan O'Rear, 1-Apr-2015)

	Ref	Expression
Hypotheses	deg1mul3le.d	$⊢ D = \deg_{1} (R)$
	deg1mul3le.p	$⊢ P = {Poly}_{1} (R)$
	deg1mul3le.k	$⊢ K = {Base}_{R}$
	deg1mul3le.b	$⊢ B = {Base}_{P}$
	deg1mul3le.t	$⊢ \underset{˙}{\cdot} = \cdot_{P}$
	deg1mul3le.a	$⊢ A = algSc (P)$
Assertion	deg1mul3le	$⊢ (R \in Ring \land F \in K \land G \in B) \to D (A (F) \underset{˙}{\cdot} G) \leq D (G)$

Proof

Step	Hyp	Ref	Expression
1		deg1mul3le.d	$⊢ D = \deg_{1} (R)$
2		deg1mul3le.p	$⊢ P = {Poly}_{1} (R)$
3		deg1mul3le.k	$⊢ K = {Base}_{R}$
4		deg1mul3le.b	$⊢ B = {Base}_{P}$
5		deg1mul3le.t	$⊢ \underset{˙}{\cdot} = \cdot_{P}$
6		deg1mul3le.a	$⊢ A = algSc (P)$
7	2	ply1ring	$⊢ R \in Ring \to P \in Ring$
8	7	3ad2ant1	$⊢ (R \in Ring \land F \in K \land G \in B) \to P \in Ring$
9	2 6 3 4	ply1sclf	$⊢ R \in Ring \to A : K ⟶ B$
10	9	3ad2ant1	$⊢ (R \in Ring \land F \in K \land G \in B) \to A : K ⟶ B$
11		simp2	$⊢ (R \in Ring \land F \in K \land G \in B) \to F \in K$
12	10 11	ffvelrnd	$⊢ (R \in Ring \land F \in K \land G \in B) \to A (F) \in B$
13		simp3	$⊢ (R \in Ring \land F \in K \land G \in B) \to G \in B$
14	4 5	ringcl	$⊢ (P \in Ring \land A (F) \in B \land G \in B) \to A (F) \underset{˙}{\cdot} G \in B$
15	8 12 13 14	syl3anc	$⊢ (R \in Ring \land F \in K \land G \in B) \to A (F) \underset{˙}{\cdot} G \in B$
16		eqid	$⊢ {coe}_{1} (A (F) \underset{˙}{\cdot} G) = {coe}_{1} (A (F) \underset{˙}{\cdot} G)$
17	16 4 2 3	coe1f	$⊢ A (F) \underset{˙}{\cdot} G \in B \to {coe}_{1} (A (F) \underset{˙}{\cdot} G) : ℕ_{0} ⟶ K$
18	15 17	syl	$⊢ (R \in Ring \land F \in K \land G \in B) \to {coe}_{1} (A (F) \underset{˙}{\cdot} G) : ℕ_{0} ⟶ K$
19		eldifi	$⊢ a \in (ℕ_{0} ∖ {supp}_{0_{R}} ({coe}_{1} (G))) \to a \in ℕ_{0}$
20		simpl1	$⊢ ((R \in Ring \land F \in K \land G \in B) \land a \in ℕ_{0}) \to R \in Ring$
21		simpl2	$⊢ ((R \in Ring \land F \in K \land G \in B) \land a \in ℕ_{0}) \to F \in K$
22		simpl3	$⊢ ((R \in Ring \land F \in K \land G \in B) \land a \in ℕ_{0}) \to G \in B$
23		simpr	$⊢ ((R \in Ring \land F \in K \land G \in B) \land a \in ℕ_{0}) \to a \in ℕ_{0}$
24		eqid	$⊢ \cdot_{R} = \cdot_{R}$
25	2 4 3 6 5 24	coe1sclmulfv	$⊢ (R \in Ring \land (F \in K \land G \in B) \land a \in ℕ_{0}) \to {coe}_{1} (A (F) \underset{˙}{\cdot} G) (a) = F \cdot_{R} {coe}_{1} (G) (a)$
26	20 21 22 23 25	syl121anc	$⊢ ((R \in Ring \land F \in K \land G \in B) \land a \in ℕ_{0}) \to {coe}_{1} (A (F) \underset{˙}{\cdot} G) (a) = F \cdot_{R} {coe}_{1} (G) (a)$
27	19 26	sylan2	$⊢ ((R \in Ring \land F \in K \land G \in B) \land a \in (ℕ_{0} ∖ {supp}_{0_{R}} ({coe}_{1} (G)))) \to {coe}_{1} (A (F) \underset{˙}{\cdot} G) (a) = F \cdot_{R} {coe}_{1} (G) (a)$
28		eqid	$⊢ {coe}_{1} (G) = {coe}_{1} (G)$
29	28 4 2 3	coe1f	$⊢ G \in B \to {coe}_{1} (G) : ℕ_{0} ⟶ K$
30	29	3ad2ant3	$⊢ (R \in Ring \land F \in K \land G \in B) \to {coe}_{1} (G) : ℕ_{0} ⟶ K$
31		ssidd	$⊢ (R \in Ring \land F \in K \land G \in B) \to {coe}_{1} (G) supp 0_{R} \subseteq {coe}_{1} (G) supp 0_{R}$
32		nn0ex	$⊢ ℕ_{0} \in V$
33	32	a1i	$⊢ (R \in Ring \land F \in K \land G \in B) \to ℕ_{0} \in V$
34		fvexd	$⊢ (R \in Ring \land F \in K \land G \in B) \to 0_{R} \in V$
35	30 31 33 34	suppssr	$⊢ ((R \in Ring \land F \in K \land G \in B) \land a \in (ℕ_{0} ∖ {supp}_{0_{R}} ({coe}_{1} (G)))) \to {coe}_{1} (G) (a) = 0_{R}$
36	35	oveq2d	$⊢ ((R \in Ring \land F \in K \land G \in B) \land a \in (ℕ_{0} ∖ {supp}_{0_{R}} ({coe}_{1} (G)))) \to F \cdot_{R} {coe}_{1} (G) (a) = F \cdot_{R} 0_{R}$
37		eqid	$⊢ 0_{R} = 0_{R}$
38	3 24 37	ringrz	$⊢ (R \in Ring \land F \in K) \to F \cdot_{R} 0_{R} = 0_{R}$
39	38	3adant3	$⊢ (R \in Ring \land F \in K \land G \in B) \to F \cdot_{R} 0_{R} = 0_{R}$
40	39	adantr	$⊢ ((R \in Ring \land F \in K \land G \in B) \land a \in (ℕ_{0} ∖ {supp}_{0_{R}} ({coe}_{1} (G)))) \to F \cdot_{R} 0_{R} = 0_{R}$
41	27 36 40	3eqtrd	$⊢ ((R \in Ring \land F \in K \land G \in B) \land a \in (ℕ_{0} ∖ {supp}_{0_{R}} ({coe}_{1} (G)))) \to {coe}_{1} (A (F) \underset{˙}{\cdot} G) (a) = 0_{R}$
42	18 41	suppss	$⊢ (R \in Ring \land F \in K \land G \in B) \to {coe}_{1} (A (F) \underset{˙}{\cdot} G) supp 0_{R} \subseteq {coe}_{1} (G) supp 0_{R}$
43		suppssdm	$⊢ {coe}_{1} (G) supp 0_{R} \subseteq dom {coe}_{1} (G)$
44	43 30	fssdm	$⊢ (R \in Ring \land F \in K \land G \in B) \to {coe}_{1} (G) supp 0_{R} \subseteq ℕ_{0}$
45		nn0ssre	$⊢ ℕ_{0} \subseteq ℝ$
46		ressxr	$⊢ ℝ \subseteq ℝ^{*}$
47	45 46	sstri	$⊢ ℕ_{0} \subseteq ℝ^{*}$
48	44 47	sstrdi	$⊢ (R \in Ring \land F \in K \land G \in B) \to {coe}_{1} (G) supp 0_{R} \subseteq ℝ^{*}$
49		supxrss	$⊢ ({coe}_{1} (A (F) \underset{˙}{\cdot} G) supp 0_{R} \subseteq {coe}_{1} (G) supp 0_{R} \land {coe}_{1} (G) supp 0_{R} \subseteq ℝ^{}) \to sup ({coe}_{1} (A (F) \underset{˙}{\cdot} G) supp 0_{R} ℝ^{} <) \leq sup ({coe}_{1} (G) supp 0_{R} ℝ^{*} <)$
50	42 48 49	syl2anc	$⊢ (R \in Ring \land F \in K \land G \in B) \to sup ({coe}_{1} (A (F) \underset{˙}{\cdot} G) supp 0_{R} ℝ^{} <) \leq sup ({coe}_{1} (G) supp 0_{R} ℝ^{} <)$
51	1 2 4 37 16	deg1val	$⊢ A (F) \underset{˙}{\cdot} G \in B \to D (A (F) \underset{˙}{\cdot} G) = sup ({coe}_{1} (A (F) \underset{˙}{\cdot} G) supp 0_{R} ℝ^{*} <)$
52	15 51	syl	$⊢ (R \in Ring \land F \in K \land G \in B) \to D (A (F) \underset{˙}{\cdot} G) = sup ({coe}_{1} (A (F) \underset{˙}{\cdot} G) supp 0_{R} ℝ^{*} <)$
53	1 2 4 37 28	deg1val	$⊢ G \in B \to D (G) = sup ({coe}_{1} (G) supp 0_{R} ℝ^{*} <)$
54	53	3ad2ant3	$⊢ (R \in Ring \land F \in K \land G \in B) \to D (G) = sup ({coe}_{1} (G) supp 0_{R} ℝ^{*} <)$
55	50 52 54	3brtr4d	$⊢ (R \in Ring \land F \in K \land G \in B) \to D (A (F) \underset{˙}{\cdot} G) \leq D (G)$

Metamath Proof Explorer

Theorem deg1mul3le

Proof