Theorem 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	⊢ 𝐷 = ( deg1 ‘ 𝑅 )
	deg1mul3le.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	deg1mul3le.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
	deg1mul3le.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
	deg1mul3le.t	⊢ · = ( .r ‘ 𝑃 )
	deg1mul3le.a	⊢ 𝐴 = ( algSc ‘ 𝑃 )
Assertion	deg1mul3le	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵 ) → ( 𝐷 ‘ ( ( 𝐴 ‘ 𝐹 ) · 𝐺 ) ) ≤ ( 𝐷 ‘ 𝐺 ) )

Proof

Step	Hyp	Ref	Expression
1		deg1mul3le.d	⊢ 𝐷 = ( deg1 ‘ 𝑅 )
2		deg1mul3le.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
3		deg1mul3le.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
4		deg1mul3le.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
5		deg1mul3le.t	⊢ · = ( .r ‘ 𝑃 )
6		deg1mul3le.a	⊢ 𝐴 = ( algSc ‘ 𝑃 )
7	2	ply1ring	⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
8	7	3ad2ant1	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵 ) → 𝑃 ∈ Ring )
9	2 6 3 4	ply1sclf	⊢ ( 𝑅 ∈ Ring → 𝐴 : 𝐾 ⟶ 𝐵 )
10	9	3ad2ant1	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵 ) → 𝐴 : 𝐾 ⟶ 𝐵 )
11		simp2	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵 ) → 𝐹 ∈ 𝐾 )
12	10 11	ffvelrnd	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵 ) → ( 𝐴 ‘ 𝐹 ) ∈ 𝐵 )
13		simp3	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵 ) → 𝐺 ∈ 𝐵 )
14	4 5	ringcl	⊢ ( ( 𝑃 ∈ Ring ∧ ( 𝐴 ‘ 𝐹 ) ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( ( 𝐴 ‘ 𝐹 ) · 𝐺 ) ∈ 𝐵 )
15	8 12 13 14	syl3anc	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵 ) → ( ( 𝐴 ‘ 𝐹 ) · 𝐺 ) ∈ 𝐵 )
16		eqid	⊢ ( coe1 ‘ ( ( 𝐴 ‘ 𝐹 ) · 𝐺 ) ) = ( coe1 ‘ ( ( 𝐴 ‘ 𝐹 ) · 𝐺 ) )
17	16 4 2 3	coe1f	⊢ ( ( ( 𝐴 ‘ 𝐹 ) · 𝐺 ) ∈ 𝐵 → ( coe1 ‘ ( ( 𝐴 ‘ 𝐹 ) · 𝐺 ) ) : ℕ0 ⟶ 𝐾 )
18	15 17	syl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵 ) → ( coe1 ‘ ( ( 𝐴 ‘ 𝐹 ) · 𝐺 ) ) : ℕ0 ⟶ 𝐾 )
19		eldifi	⊢ ( 𝑎 ∈ ( ℕ0 ∖ ( ( coe1 ‘ 𝐺 ) supp ( 0g ‘ 𝑅 ) ) ) → 𝑎 ∈ ℕ0 )
20		simpl1	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑎 ∈ ℕ0 ) → 𝑅 ∈ Ring )
21		simpl2	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑎 ∈ ℕ0 ) → 𝐹 ∈ 𝐾 )
22		simpl3	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑎 ∈ ℕ0 ) → 𝐺 ∈ 𝐵 )
23		simpr	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑎 ∈ ℕ0 ) → 𝑎 ∈ ℕ0 )
24		eqid	⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
25	2 4 3 6 5 24	coe1sclmulfv	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑎 ∈ ℕ0 ) → ( ( coe1 ‘ ( ( 𝐴 ‘ 𝐹 ) · 𝐺 ) ) ‘ 𝑎 ) = ( 𝐹 ( .r ‘ 𝑅 ) ( ( coe1 ‘ 𝐺 ) ‘ 𝑎 ) ) )
26	20 21 22 23 25	syl121anc	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑎 ∈ ℕ0 ) → ( ( coe1 ‘ ( ( 𝐴 ‘ 𝐹 ) · 𝐺 ) ) ‘ 𝑎 ) = ( 𝐹 ( .r ‘ 𝑅 ) ( ( coe1 ‘ 𝐺 ) ‘ 𝑎 ) ) )
27	19 26	sylan2	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑎 ∈ ( ℕ0 ∖ ( ( coe1 ‘ 𝐺 ) supp ( 0g ‘ 𝑅 ) ) ) ) → ( ( coe1 ‘ ( ( 𝐴 ‘ 𝐹 ) · 𝐺 ) ) ‘ 𝑎 ) = ( 𝐹 ( .r ‘ 𝑅 ) ( ( coe1 ‘ 𝐺 ) ‘ 𝑎 ) ) )
28		eqid	⊢ ( coe1 ‘ 𝐺 ) = ( coe1 ‘ 𝐺 )
29	28 4 2 3	coe1f	⊢ ( 𝐺 ∈ 𝐵 → ( coe1 ‘ 𝐺 ) : ℕ0 ⟶ 𝐾 )
30	29	3ad2ant3	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵 ) → ( coe1 ‘ 𝐺 ) : ℕ0 ⟶ 𝐾 )
31		ssidd	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵 ) → ( ( coe1 ‘ 𝐺 ) supp ( 0g ‘ 𝑅 ) ) ⊆ ( ( coe1 ‘ 𝐺 ) supp ( 0g ‘ 𝑅 ) ) )
32		nn0ex	⊢ ℕ0 ∈ V
33	32	a1i	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵 ) → ℕ0 ∈ V )
34		fvexd	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵 ) → ( 0g ‘ 𝑅 ) ∈ V )
35	30 31 33 34	suppssr	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑎 ∈ ( ℕ0 ∖ ( ( coe1 ‘ 𝐺 ) supp ( 0g ‘ 𝑅 ) ) ) ) → ( ( coe1 ‘ 𝐺 ) ‘ 𝑎 ) = ( 0g ‘ 𝑅 ) )
36	35	oveq2d	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑎 ∈ ( ℕ0 ∖ ( ( coe1 ‘ 𝐺 ) supp ( 0g ‘ 𝑅 ) ) ) ) → ( 𝐹 ( .r ‘ 𝑅 ) ( ( coe1 ‘ 𝐺 ) ‘ 𝑎 ) ) = ( 𝐹 ( .r ‘ 𝑅 ) ( 0g ‘ 𝑅 ) ) )
37		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
38	3 24 37	ringrz	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ) → ( 𝐹 ( .r ‘ 𝑅 ) ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) )
39	38	3adant3	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵 ) → ( 𝐹 ( .r ‘ 𝑅 ) ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) )
40	39	adantr	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑎 ∈ ( ℕ0 ∖ ( ( coe1 ‘ 𝐺 ) supp ( 0g ‘ 𝑅 ) ) ) ) → ( 𝐹 ( .r ‘ 𝑅 ) ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) )
41	27 36 40	3eqtrd	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑎 ∈ ( ℕ0 ∖ ( ( coe1 ‘ 𝐺 ) supp ( 0g ‘ 𝑅 ) ) ) ) → ( ( coe1 ‘ ( ( 𝐴 ‘ 𝐹 ) · 𝐺 ) ) ‘ 𝑎 ) = ( 0g ‘ 𝑅 ) )
42	18 41	suppss	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵 ) → ( ( coe1 ‘ ( ( 𝐴 ‘ 𝐹 ) · 𝐺 ) ) supp ( 0g ‘ 𝑅 ) ) ⊆ ( ( coe1 ‘ 𝐺 ) supp ( 0g ‘ 𝑅 ) ) )
43		suppssdm	⊢ ( ( coe1 ‘ 𝐺 ) supp ( 0g ‘ 𝑅 ) ) ⊆ dom ( coe1 ‘ 𝐺 )
44	43 30	fssdm	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵 ) → ( ( coe1 ‘ 𝐺 ) supp ( 0g ‘ 𝑅 ) ) ⊆ ℕ0 )
45		nn0ssre	⊢ ℕ0 ⊆ ℝ
46		ressxr	⊢ ℝ ⊆ ℝ*
47	45 46	sstri	⊢ ℕ0 ⊆ ℝ*
48	44 47	sstrdi	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵 ) → ( ( coe1 ‘ 𝐺 ) supp ( 0g ‘ 𝑅 ) ) ⊆ ℝ* )
49		supxrss	⊢ ( ( ( ( coe1 ‘ ( ( 𝐴 ‘ 𝐹 ) · 𝐺 ) ) supp ( 0g ‘ 𝑅 ) ) ⊆ ( ( coe1 ‘ 𝐺 ) supp ( 0g ‘ 𝑅 ) ) ∧ ( ( coe1 ‘ 𝐺 ) supp ( 0g ‘ 𝑅 ) ) ⊆ ℝ* ) → sup ( ( ( coe1 ‘ ( ( 𝐴 ‘ 𝐹 ) · 𝐺 ) ) supp ( 0g ‘ 𝑅 ) ) , ℝ* , < ) ≤ sup ( ( ( coe1 ‘ 𝐺 ) supp ( 0g ‘ 𝑅 ) ) , ℝ* , < ) )
50	42 48 49	syl2anc	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵 ) → sup ( ( ( coe1 ‘ ( ( 𝐴 ‘ 𝐹 ) · 𝐺 ) ) supp ( 0g ‘ 𝑅 ) ) , ℝ* , < ) ≤ sup ( ( ( coe1 ‘ 𝐺 ) supp ( 0g ‘ 𝑅 ) ) , ℝ* , < ) )
51	1 2 4 37 16	deg1val	⊢ ( ( ( 𝐴 ‘ 𝐹 ) · 𝐺 ) ∈ 𝐵 → ( 𝐷 ‘ ( ( 𝐴 ‘ 𝐹 ) · 𝐺 ) ) = sup ( ( ( coe1 ‘ ( ( 𝐴 ‘ 𝐹 ) · 𝐺 ) ) supp ( 0g ‘ 𝑅 ) ) , ℝ* , < ) )
52	15 51	syl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵 ) → ( 𝐷 ‘ ( ( 𝐴 ‘ 𝐹 ) · 𝐺 ) ) = sup ( ( ( coe1 ‘ ( ( 𝐴 ‘ 𝐹 ) · 𝐺 ) ) supp ( 0g ‘ 𝑅 ) ) , ℝ* , < ) )
53	1 2 4 37 28	deg1val	⊢ ( 𝐺 ∈ 𝐵 → ( 𝐷 ‘ 𝐺 ) = sup ( ( ( coe1 ‘ 𝐺 ) supp ( 0g ‘ 𝑅 ) ) , ℝ* , < ) )
54	53	3ad2ant3	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵 ) → ( 𝐷 ‘ 𝐺 ) = sup ( ( ( coe1 ‘ 𝐺 ) supp ( 0g ‘ 𝑅 ) ) , ℝ* , < ) )
55	50 52 54	3brtr4d	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵 ) → ( 𝐷 ‘ ( ( 𝐴 ‘ 𝐹 ) · 𝐺 ) ) ≤ ( 𝐷 ‘ 𝐺 ) )