Theorem coe1mul4

Description: Value of the "leading" coefficient of a product of two nonzero polynomials. This will fail to actually be the leading coefficient only if it is zero (requiring the basic ring to contain zero divisors). (Contributed by Stefan O'Rear, 25-Mar-2015)

	Ref	Expression
Hypotheses	coe1mul3.s	⊢ 𝑌 = ( Poly1 ‘ 𝑅 )
	coe1mul3.t	⊢ ∙ = ( .r ‘ 𝑌 )
	coe1mul3.u	⊢ · = ( .r ‘ 𝑅 )
	coe1mul3.b	⊢ 𝐵 = ( Base ‘ 𝑌 )
	coe1mul3.d	⊢ 𝐷 = ( deg1 ‘ 𝑅 )
	coe1mul4.z	⊢ 0 = ( 0g ‘ 𝑌 )
	coe1mul4.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
	coe1mul4.f1	⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
	coe1mul4.f2	⊢ ( 𝜑 → 𝐹 ≠ 0 )
	coe1mul4.g1	⊢ ( 𝜑 → 𝐺 ∈ 𝐵 )
	coe1mul4.g2	⊢ ( 𝜑 → 𝐺 ≠ 0 )
Assertion	coe1mul4	⊢ ( 𝜑 → ( ( coe1 ‘ ( 𝐹 ∙ 𝐺 ) ) ‘ ( ( 𝐷 ‘ 𝐹 ) + ( 𝐷 ‘ 𝐺 ) ) ) = ( ( ( coe1 ‘ 𝐹 ) ‘ ( 𝐷 ‘ 𝐹 ) ) · ( ( coe1 ‘ 𝐺 ) ‘ ( 𝐷 ‘ 𝐺 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		coe1mul3.s	⊢ 𝑌 = ( Poly1 ‘ 𝑅 )
2		coe1mul3.t	⊢ ∙ = ( .r ‘ 𝑌 )
3		coe1mul3.u	⊢ · = ( .r ‘ 𝑅 )
4		coe1mul3.b	⊢ 𝐵 = ( Base ‘ 𝑌 )
5		coe1mul3.d	⊢ 𝐷 = ( deg1 ‘ 𝑅 )
6		coe1mul4.z	⊢ 0 = ( 0g ‘ 𝑌 )
7		coe1mul4.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
8		coe1mul4.f1	⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
9		coe1mul4.f2	⊢ ( 𝜑 → 𝐹 ≠ 0 )
10		coe1mul4.g1	⊢ ( 𝜑 → 𝐺 ∈ 𝐵 )
11		coe1mul4.g2	⊢ ( 𝜑 → 𝐺 ≠ 0 )
12	5 1 6 4	deg1nn0cl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 0 ) → ( 𝐷 ‘ 𝐹 ) ∈ ℕ0 )
13	7 8 9 12	syl3anc	⊢ ( 𝜑 → ( 𝐷 ‘ 𝐹 ) ∈ ℕ0 )
14	13	nn0red	⊢ ( 𝜑 → ( 𝐷 ‘ 𝐹 ) ∈ ℝ )
15	14	leidd	⊢ ( 𝜑 → ( 𝐷 ‘ 𝐹 ) ≤ ( 𝐷 ‘ 𝐹 ) )
16	5 1 6 4	deg1nn0cl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐺 ∈ 𝐵 ∧ 𝐺 ≠ 0 ) → ( 𝐷 ‘ 𝐺 ) ∈ ℕ0 )
17	7 10 11 16	syl3anc	⊢ ( 𝜑 → ( 𝐷 ‘ 𝐺 ) ∈ ℕ0 )
18	17	nn0red	⊢ ( 𝜑 → ( 𝐷 ‘ 𝐺 ) ∈ ℝ )
19	18	leidd	⊢ ( 𝜑 → ( 𝐷 ‘ 𝐺 ) ≤ ( 𝐷 ‘ 𝐺 ) )
20	1 2 3 4 5 7 8 13 15 10 17 19	coe1mul3	⊢ ( 𝜑 → ( ( coe1 ‘ ( 𝐹 ∙ 𝐺 ) ) ‘ ( ( 𝐷 ‘ 𝐹 ) + ( 𝐷 ‘ 𝐺 ) ) ) = ( ( ( coe1 ‘ 𝐹 ) ‘ ( 𝐷 ‘ 𝐹 ) ) · ( ( coe1 ‘ 𝐺 ) ‘ ( 𝐷 ‘ 𝐺 ) ) ) )