Theorem mdegmulle2

Description: The multivariate degree of a product of polynomials is at most the sum of the degrees of the polynomials. (Contributed by Stefan O'Rear, 26-Mar-2015)

	Ref	Expression
Hypotheses	mdegaddle.y	⊢ 𝑌 = ( 𝐼 mPoly 𝑅 )
	mdegaddle.d	⊢ 𝐷 = ( 𝐼 mDeg 𝑅 )
	mdegaddle.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
	mdegaddle.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
	mdegmulle2.b	⊢ 𝐵 = ( Base ‘ 𝑌 )
	mdegmulle2.t	⊢ · = ( .r ‘ 𝑌 )
	mdegmulle2.f	⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
	mdegmulle2.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐵 )
	mdegmulle2.j1	⊢ ( 𝜑 → 𝐽 ∈ ℕ0 )
	mdegmulle2.k1	⊢ ( 𝜑 → 𝐾 ∈ ℕ0 )
	mdegmulle2.j2	⊢ ( 𝜑 → ( 𝐷 ‘ 𝐹 ) ≤ 𝐽 )
	mdegmulle2.k2	⊢ ( 𝜑 → ( 𝐷 ‘ 𝐺 ) ≤ 𝐾 )
Assertion	mdegmulle2	⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝐹 · 𝐺 ) ) ≤ ( 𝐽 + 𝐾 ) )

Proof

Step	Hyp	Ref	Expression
1		mdegaddle.y	⊢ 𝑌 = ( 𝐼 mPoly 𝑅 )
2		mdegaddle.d	⊢ 𝐷 = ( 𝐼 mDeg 𝑅 )
3		mdegaddle.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
4		mdegaddle.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
5		mdegmulle2.b	⊢ 𝐵 = ( Base ‘ 𝑌 )
6		mdegmulle2.t	⊢ · = ( .r ‘ 𝑌 )
7		mdegmulle2.f	⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
8		mdegmulle2.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐵 )
9		mdegmulle2.j1	⊢ ( 𝜑 → 𝐽 ∈ ℕ0 )
10		mdegmulle2.k1	⊢ ( 𝜑 → 𝐾 ∈ ℕ0 )
11		mdegmulle2.j2	⊢ ( 𝜑 → ( 𝐷 ‘ 𝐹 ) ≤ 𝐽 )
12		mdegmulle2.k2	⊢ ( 𝜑 → ( 𝐷 ‘ 𝐺 ) ≤ 𝐾 )
13		eqid	⊢ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } = { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin }
14		eqid	⊢ ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) = ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) )
15	1 2 3 4 5 6 7 8 9 10 11 12 13 14	mdegmullem	⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝐹 · 𝐺 ) ) ≤ ( 𝐽 + 𝐾 ) )