Theorem deg1mul2

Description: Degree of multiplication of two nonzero polynomials when the first leads with a nonzero-divisor coefficient. (Contributed by Stefan O'Rear, 26-Mar-2015)

	Ref	Expression
Hypotheses	deg1mul2.d	⊢ 𝐷 = ( deg1 ‘ 𝑅 )
	deg1mul2.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	deg1mul2.e	⊢ 𝐸 = ( RLReg ‘ 𝑅 )
	deg1mul2.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
	deg1mul2.t	⊢ · = ( .r ‘ 𝑃 )
	deg1mul2.z	⊢ 0 = ( 0g ‘ 𝑃 )
	deg1mul2.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
	deg1mul2.fb	⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
	deg1mul2.fz	⊢ ( 𝜑 → 𝐹 ≠ 0 )
	deg1mul2.fc	⊢ ( 𝜑 → ( ( coe1 ‘ 𝐹 ) ‘ ( 𝐷 ‘ 𝐹 ) ) ∈ 𝐸 )
	deg1mul2.gb	⊢ ( 𝜑 → 𝐺 ∈ 𝐵 )
	deg1mul2.gz	⊢ ( 𝜑 → 𝐺 ≠ 0 )
Assertion	deg1mul2	⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝐹 · 𝐺 ) ) = ( ( 𝐷 ‘ 𝐹 ) + ( 𝐷 ‘ 𝐺 ) ) )

Proof

Step	Hyp	Ref	Expression
1		deg1mul2.d	⊢ 𝐷 = ( deg1 ‘ 𝑅 )
2		deg1mul2.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
3		deg1mul2.e	⊢ 𝐸 = ( RLReg ‘ 𝑅 )
4		deg1mul2.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
5		deg1mul2.t	⊢ · = ( .r ‘ 𝑃 )
6		deg1mul2.z	⊢ 0 = ( 0g ‘ 𝑃 )
7		deg1mul2.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
8		deg1mul2.fb	⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
9		deg1mul2.fz	⊢ ( 𝜑 → 𝐹 ≠ 0 )
10		deg1mul2.fc	⊢ ( 𝜑 → ( ( coe1 ‘ 𝐹 ) ‘ ( 𝐷 ‘ 𝐹 ) ) ∈ 𝐸 )
11		deg1mul2.gb	⊢ ( 𝜑 → 𝐺 ∈ 𝐵 )
12		deg1mul2.gz	⊢ ( 𝜑 → 𝐺 ≠ 0 )
13	2	ply1ring	⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
14	7 13	syl	⊢ ( 𝜑 → 𝑃 ∈ Ring )
15	4 5	ringcl	⊢ ( ( 𝑃 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( 𝐹 · 𝐺 ) ∈ 𝐵 )
16	14 8 11 15	syl3anc	⊢ ( 𝜑 → ( 𝐹 · 𝐺 ) ∈ 𝐵 )
17	1 2 4	deg1xrcl	⊢ ( ( 𝐹 · 𝐺 ) ∈ 𝐵 → ( 𝐷 ‘ ( 𝐹 · 𝐺 ) ) ∈ ℝ* )
18	16 17	syl	⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝐹 · 𝐺 ) ) ∈ ℝ* )
19	1 2 6 4	deg1nn0cl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 0 ) → ( 𝐷 ‘ 𝐹 ) ∈ ℕ0 )
20	7 8 9 19	syl3anc	⊢ ( 𝜑 → ( 𝐷 ‘ 𝐹 ) ∈ ℕ0 )
21	1 2 6 4	deg1nn0cl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐺 ∈ 𝐵 ∧ 𝐺 ≠ 0 ) → ( 𝐷 ‘ 𝐺 ) ∈ ℕ0 )
22	7 11 12 21	syl3anc	⊢ ( 𝜑 → ( 𝐷 ‘ 𝐺 ) ∈ ℕ0 )
23	20 22	nn0addcld	⊢ ( 𝜑 → ( ( 𝐷 ‘ 𝐹 ) + ( 𝐷 ‘ 𝐺 ) ) ∈ ℕ0 )
24	23	nn0red	⊢ ( 𝜑 → ( ( 𝐷 ‘ 𝐹 ) + ( 𝐷 ‘ 𝐺 ) ) ∈ ℝ )
25	24	rexrd	⊢ ( 𝜑 → ( ( 𝐷 ‘ 𝐹 ) + ( 𝐷 ‘ 𝐺 ) ) ∈ ℝ* )
26	20	nn0red	⊢ ( 𝜑 → ( 𝐷 ‘ 𝐹 ) ∈ ℝ )
27	26	leidd	⊢ ( 𝜑 → ( 𝐷 ‘ 𝐹 ) ≤ ( 𝐷 ‘ 𝐹 ) )
28	22	nn0red	⊢ ( 𝜑 → ( 𝐷 ‘ 𝐺 ) ∈ ℝ )
29	28	leidd	⊢ ( 𝜑 → ( 𝐷 ‘ 𝐺 ) ≤ ( 𝐷 ‘ 𝐺 ) )
30	2 1 7 4 5 8 11 20 22 27 29	deg1mulle2	⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝐹 · 𝐺 ) ) ≤ ( ( 𝐷 ‘ 𝐹 ) + ( 𝐷 ‘ 𝐺 ) ) )
31		eqid	⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
32	2 5 31 4 1 6 7 8 9 11 12	coe1mul4	⊢ ( 𝜑 → ( ( coe1 ‘ ( 𝐹 · 𝐺 ) ) ‘ ( ( 𝐷 ‘ 𝐹 ) + ( 𝐷 ‘ 𝐺 ) ) ) = ( ( ( coe1 ‘ 𝐹 ) ‘ ( 𝐷 ‘ 𝐹 ) ) ( .r ‘ 𝑅 ) ( ( coe1 ‘ 𝐺 ) ‘ ( 𝐷 ‘ 𝐺 ) ) ) )
33		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
34		eqid	⊢ ( coe1 ‘ 𝐺 ) = ( coe1 ‘ 𝐺 )
35	1 2 6 4 33 34	deg1ldg	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐺 ∈ 𝐵 ∧ 𝐺 ≠ 0 ) → ( ( coe1 ‘ 𝐺 ) ‘ ( 𝐷 ‘ 𝐺 ) ) ≠ ( 0g ‘ 𝑅 ) )
36	7 11 12 35	syl3anc	⊢ ( 𝜑 → ( ( coe1 ‘ 𝐺 ) ‘ ( 𝐷 ‘ 𝐺 ) ) ≠ ( 0g ‘ 𝑅 ) )
37		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
38	34 4 2 37	coe1f	⊢ ( 𝐺 ∈ 𝐵 → ( coe1 ‘ 𝐺 ) : ℕ0 ⟶ ( Base ‘ 𝑅 ) )
39	11 38	syl	⊢ ( 𝜑 → ( coe1 ‘ 𝐺 ) : ℕ0 ⟶ ( Base ‘ 𝑅 ) )
40	39 22	ffvelcdmd	⊢ ( 𝜑 → ( ( coe1 ‘ 𝐺 ) ‘ ( 𝐷 ‘ 𝐺 ) ) ∈ ( Base ‘ 𝑅 ) )
41	3 37 31 33	rrgeq0i	⊢ ( ( ( ( coe1 ‘ 𝐹 ) ‘ ( 𝐷 ‘ 𝐹 ) ) ∈ 𝐸 ∧ ( ( coe1 ‘ 𝐺 ) ‘ ( 𝐷 ‘ 𝐺 ) ) ∈ ( Base ‘ 𝑅 ) ) → ( ( ( ( coe1 ‘ 𝐹 ) ‘ ( 𝐷 ‘ 𝐹 ) ) ( .r ‘ 𝑅 ) ( ( coe1 ‘ 𝐺 ) ‘ ( 𝐷 ‘ 𝐺 ) ) ) = ( 0g ‘ 𝑅 ) → ( ( coe1 ‘ 𝐺 ) ‘ ( 𝐷 ‘ 𝐺 ) ) = ( 0g ‘ 𝑅 ) ) )
42	10 40 41	syl2anc	⊢ ( 𝜑 → ( ( ( ( coe1 ‘ 𝐹 ) ‘ ( 𝐷 ‘ 𝐹 ) ) ( .r ‘ 𝑅 ) ( ( coe1 ‘ 𝐺 ) ‘ ( 𝐷 ‘ 𝐺 ) ) ) = ( 0g ‘ 𝑅 ) → ( ( coe1 ‘ 𝐺 ) ‘ ( 𝐷 ‘ 𝐺 ) ) = ( 0g ‘ 𝑅 ) ) )
43	42	necon3d	⊢ ( 𝜑 → ( ( ( coe1 ‘ 𝐺 ) ‘ ( 𝐷 ‘ 𝐺 ) ) ≠ ( 0g ‘ 𝑅 ) → ( ( ( coe1 ‘ 𝐹 ) ‘ ( 𝐷 ‘ 𝐹 ) ) ( .r ‘ 𝑅 ) ( ( coe1 ‘ 𝐺 ) ‘ ( 𝐷 ‘ 𝐺 ) ) ) ≠ ( 0g ‘ 𝑅 ) ) )
44	36 43	mpd	⊢ ( 𝜑 → ( ( ( coe1 ‘ 𝐹 ) ‘ ( 𝐷 ‘ 𝐹 ) ) ( .r ‘ 𝑅 ) ( ( coe1 ‘ 𝐺 ) ‘ ( 𝐷 ‘ 𝐺 ) ) ) ≠ ( 0g ‘ 𝑅 ) )
45	32 44	eqnetrd	⊢ ( 𝜑 → ( ( coe1 ‘ ( 𝐹 · 𝐺 ) ) ‘ ( ( 𝐷 ‘ 𝐹 ) + ( 𝐷 ‘ 𝐺 ) ) ) ≠ ( 0g ‘ 𝑅 ) )
46		eqid	⊢ ( coe1 ‘ ( 𝐹 · 𝐺 ) ) = ( coe1 ‘ ( 𝐹 · 𝐺 ) )
47	1 2 4 33 46	deg1ge	⊢ ( ( ( 𝐹 · 𝐺 ) ∈ 𝐵 ∧ ( ( 𝐷 ‘ 𝐹 ) + ( 𝐷 ‘ 𝐺 ) ) ∈ ℕ0 ∧ ( ( coe1 ‘ ( 𝐹 · 𝐺 ) ) ‘ ( ( 𝐷 ‘ 𝐹 ) + ( 𝐷 ‘ 𝐺 ) ) ) ≠ ( 0g ‘ 𝑅 ) ) → ( ( 𝐷 ‘ 𝐹 ) + ( 𝐷 ‘ 𝐺 ) ) ≤ ( 𝐷 ‘ ( 𝐹 · 𝐺 ) ) )
48	16 23 45 47	syl3anc	⊢ ( 𝜑 → ( ( 𝐷 ‘ 𝐹 ) + ( 𝐷 ‘ 𝐺 ) ) ≤ ( 𝐷 ‘ ( 𝐹 · 𝐺 ) ) )
49	18 25 30 48	xrletrid	⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝐹 · 𝐺 ) ) = ( ( 𝐷 ‘ 𝐹 ) + ( 𝐷 ‘ 𝐺 ) ) )