deg1mul3

Description: Degree of multiplication of a polynomial on the left by a nonzero-dividing scalar. (Contributed by Stefan O'Rear, 29-Mar-2015) (Proof shortened by AV, 25-Jul-2019)

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

Proof

Step	Hyp	Ref	Expression
1		deg1mul3.d	$⊢ D = \deg_{1} (R)$
2		deg1mul3.p	$⊢ P = {Poly}_{1} (R)$
3		deg1mul3.e	$⊢ E = RLReg (R)$
4		deg1mul3.b	$⊢ B = {Base}_{P}$
5		deg1mul3.t	$⊢ \underset{˙}{\cdot} = \cdot_{P}$
6		deg1mul3.a	$⊢ A = algSc (P)$
7		eqid	$⊢ {Base}_{R} = {Base}_{R}$
8	3 7	rrgss	$⊢ E \subseteq {Base}_{R}$
9	8	sseli	$⊢ F \in E \to F \in {Base}_{R}$
10		eqid	$⊢ \cdot_{R} = \cdot_{R}$
11	2 4 7 6 5 10	coe1sclmul	$⊢ (R \in Ring \land F \in {Base}_{R} \land G \in B) \to {coe}_{1} (A (F) \underset{˙}{\cdot} G) = (ℕ_{0} \times \{F\}) {\cdot_{R}}_{f} {coe}_{1} (G)$
12	9 11	syl3an2	$⊢ (R \in Ring \land F \in E \land G \in B) \to {coe}_{1} (A (F) \underset{˙}{\cdot} G) = (ℕ_{0} \times \{F\}) {\cdot_{R}}_{f} {coe}_{1} (G)$
13	12	oveq1d	$⊢ (R \in Ring \land F \in E \land G \in B) \to {coe}_{1} (A (F) \underset{˙}{\cdot} G) supp 0_{R} = ((ℕ_{0} \times \{F\}) {\cdot_{R}}_{f} {coe}_{1} (G)) supp 0_{R}$
14		eqid	$⊢ 0_{R} = 0_{R}$
15		nn0ex	$⊢ ℕ_{0} \in V$
16	15	a1i	$⊢ (R \in Ring \land F \in E \land G \in B) \to ℕ_{0} \in V$
17		simp1	$⊢ (R \in Ring \land F \in E \land G \in B) \to R \in Ring$
18		simp2	$⊢ (R \in Ring \land F \in E \land G \in B) \to F \in E$
19		eqid	$⊢ {coe}_{1} (G) = {coe}_{1} (G)$
20	19 4 2 7	coe1f	$⊢ G \in B \to {coe}_{1} (G) : ℕ_{0} ⟶ {Base}_{R}$
21	20	3ad2ant3	$⊢ (R \in Ring \land F \in E \land G \in B) \to {coe}_{1} (G) : ℕ_{0} ⟶ {Base}_{R}$
22	3 7 10 14 16 17 18 21	rrgsupp	$⊢ (R \in Ring \land F \in E \land G \in B) \to ((ℕ_{0} \times \{F\}) {\cdot_{R}}_{f} {coe}_{1} (G)) supp 0_{R} = {coe}_{1} (G) supp 0_{R}$
23	13 22	eqtrd	$⊢ (R \in Ring \land F \in E \land G \in B) \to {coe}_{1} (A (F) \underset{˙}{\cdot} G) supp 0_{R} = {coe}_{1} (G) supp 0_{R}$
24	23	supeq1d	$⊢ (R \in Ring \land F \in E \land G \in B) \to sup ({coe}_{1} (A (F) \underset{˙}{\cdot} G) supp 0_{R} ℝ^{} <) = sup ({coe}_{1} (G) supp 0_{R} ℝ^{} <)$
25	2	ply1ring	$⊢ R \in Ring \to P \in Ring$
26	25	3ad2ant1	$⊢ (R \in Ring \land F \in E \land G \in B) \to P \in Ring$
27	2 6 7 4	ply1sclf	$⊢ R \in Ring \to A : {Base}_{R} ⟶ B$
28	27	3ad2ant1	$⊢ (R \in Ring \land F \in E \land G \in B) \to A : {Base}_{R} ⟶ B$
29	9	3ad2ant2	$⊢ (R \in Ring \land F \in E \land G \in B) \to F \in {Base}_{R}$
30	28 29	ffvelrnd	$⊢ (R \in Ring \land F \in E \land G \in B) \to A (F) \in B$
31		simp3	$⊢ (R \in Ring \land F \in E \land G \in B) \to G \in B$
32	4 5	ringcl	$⊢ (P \in Ring \land A (F) \in B \land G \in B) \to A (F) \underset{˙}{\cdot} G \in B$
33	26 30 31 32	syl3anc	$⊢ (R \in Ring \land F \in E \land G \in B) \to A (F) \underset{˙}{\cdot} G \in B$
34		eqid	$⊢ {coe}_{1} (A (F) \underset{˙}{\cdot} G) = {coe}_{1} (A (F) \underset{˙}{\cdot} G)$
35	1 2 4 14 34	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} ℝ^{*} <)$
36	33 35	syl	$⊢ (R \in Ring \land F \in E \land G \in B) \to D (A (F) \underset{˙}{\cdot} G) = sup ({coe}_{1} (A (F) \underset{˙}{\cdot} G) supp 0_{R} ℝ^{*} <)$
37	1 2 4 14 19	deg1val	$⊢ G \in B \to D (G) = sup ({coe}_{1} (G) supp 0_{R} ℝ^{*} <)$
38	37	3ad2ant3	$⊢ (R \in Ring \land F \in E \land G \in B) \to D (G) = sup ({coe}_{1} (G) supp 0_{R} ℝ^{*} <)$
39	24 36 38	3eqtr4d	$⊢ (R \in Ring \land F \in E \land G \in B) \to D (A (F) \underset{˙}{\cdot} G) = D (G)$

Metamath Proof Explorer

Theorem deg1mul3

Proof