Theorem deg1mul

Description: Degree of multiplication of two nonzero polynomials in a domain. (Contributed by metakunt, 6-May-2025)

	Ref	Expression
Hypotheses	deg1mul.1	⊢ 𝐷 = ( deg1 ‘ 𝑅 )
	deg1mul.2	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	deg1mul.3	⊢ 𝐵 = ( Base ‘ 𝑃 )
	deg1mul.4	⊢ · = ( .r ‘ 𝑃 )
	deg1mul.5	⊢ 0 = ( 0g ‘ 𝑃 )
	deg1mul.6	⊢ ( 𝜑 → 𝑅 ∈ Domn )
	deg1mul.7	⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
	deg1mul.8	⊢ ( 𝜑 → 𝐹 ≠ 0 )
	deg1mul.9	⊢ ( 𝜑 → 𝐺 ∈ 𝐵 )
	deg1mul.10	⊢ ( 𝜑 → 𝐺 ≠ 0 )
Assertion	deg1mul	⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝐹 · 𝐺 ) ) = ( ( 𝐷 ‘ 𝐹 ) + ( 𝐷 ‘ 𝐺 ) ) )

Proof

Step	Hyp	Ref	Expression
1		deg1mul.1	⊢ 𝐷 = ( deg1 ‘ 𝑅 )
2		deg1mul.2	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
3		deg1mul.3	⊢ 𝐵 = ( Base ‘ 𝑃 )
4		deg1mul.4	⊢ · = ( .r ‘ 𝑃 )
5		deg1mul.5	⊢ 0 = ( 0g ‘ 𝑃 )
6		deg1mul.6	⊢ ( 𝜑 → 𝑅 ∈ Domn )
7		deg1mul.7	⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
8		deg1mul.8	⊢ ( 𝜑 → 𝐹 ≠ 0 )
9		deg1mul.9	⊢ ( 𝜑 → 𝐺 ∈ 𝐵 )
10		deg1mul.10	⊢ ( 𝜑 → 𝐺 ≠ 0 )
11		eqid	⊢ ( RLReg ‘ 𝑅 ) = ( RLReg ‘ 𝑅 )
12		domnring	⊢ ( 𝑅 ∈ Domn → 𝑅 ∈ Ring )
13	6 12	syl	⊢ ( 𝜑 → 𝑅 ∈ Ring )
14	1 2 5 3	deg1nn0cl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 0 ) → ( 𝐷 ‘ 𝐹 ) ∈ ℕ0 )
15	13 7 8 14	syl3anc	⊢ ( 𝜑 → ( 𝐷 ‘ 𝐹 ) ∈ ℕ0 )
16		eqid	⊢ ( coe1 ‘ 𝐹 ) = ( coe1 ‘ 𝐹 )
17		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
18	16 3 2 17	coe1fvalcl	⊢ ( ( 𝐹 ∈ 𝐵 ∧ ( 𝐷 ‘ 𝐹 ) ∈ ℕ0 ) → ( ( coe1 ‘ 𝐹 ) ‘ ( 𝐷 ‘ 𝐹 ) ) ∈ ( Base ‘ 𝑅 ) )
19	7 15 18	syl2anc	⊢ ( 𝜑 → ( ( coe1 ‘ 𝐹 ) ‘ ( 𝐷 ‘ 𝐹 ) ) ∈ ( Base ‘ 𝑅 ) )
20		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
21	1 2 5 3 20 16	deg1ldg	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 0 ) → ( ( coe1 ‘ 𝐹 ) ‘ ( 𝐷 ‘ 𝐹 ) ) ≠ ( 0g ‘ 𝑅 ) )
22	13 7 8 21	syl3anc	⊢ ( 𝜑 → ( ( coe1 ‘ 𝐹 ) ‘ ( 𝐷 ‘ 𝐹 ) ) ≠ ( 0g ‘ 𝑅 ) )
23	17 11 20	domnrrg	⊢ ( ( 𝑅 ∈ Domn ∧ ( ( coe1 ‘ 𝐹 ) ‘ ( 𝐷 ‘ 𝐹 ) ) ∈ ( Base ‘ 𝑅 ) ∧ ( ( coe1 ‘ 𝐹 ) ‘ ( 𝐷 ‘ 𝐹 ) ) ≠ ( 0g ‘ 𝑅 ) ) → ( ( coe1 ‘ 𝐹 ) ‘ ( 𝐷 ‘ 𝐹 ) ) ∈ ( RLReg ‘ 𝑅 ) )
24	6 19 22 23	syl3anc	⊢ ( 𝜑 → ( ( coe1 ‘ 𝐹 ) ‘ ( 𝐷 ‘ 𝐹 ) ) ∈ ( RLReg ‘ 𝑅 ) )
25	1 2 11 3 4 5 13 7 8 24 9 10	deg1mul2	⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝐹 · 𝐺 ) ) = ( ( 𝐷 ‘ 𝐹 ) + ( 𝐷 ‘ 𝐺 ) ) )