Theorem deg1mul3

Description: Degree of multiplication of a polynomial on the left by a nonzero-dividing scalar. (Contributed by Stefan O'Rear, 29-Mar-2015) (Proof shortened by AV, 25-Jul-2019)

	Ref	Expression
Hypotheses	deg1mul3.d	⊢ 𝐷 = ( deg1 ‘ 𝑅 )
	deg1mul3.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	deg1mul3.e	⊢ 𝐸 = ( RLReg ‘ 𝑅 )
	deg1mul3.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
	deg1mul3.t	⊢ · = ( .r ‘ 𝑃 )
	deg1mul3.a	⊢ 𝐴 = ( algSc ‘ 𝑃 )
Assertion	deg1mul3	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐸 ∧ 𝐺 ∈ 𝐵 ) → ( 𝐷 ‘ ( ( 𝐴 ‘ 𝐹 ) · 𝐺 ) ) = ( 𝐷 ‘ 𝐺 ) )

Proof

Step	Hyp	Ref	Expression
1		deg1mul3.d	⊢ 𝐷 = ( deg1 ‘ 𝑅 )
2		deg1mul3.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
3		deg1mul3.e	⊢ 𝐸 = ( RLReg ‘ 𝑅 )
4		deg1mul3.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
5		deg1mul3.t	⊢ · = ( .r ‘ 𝑃 )
6		deg1mul3.a	⊢ 𝐴 = ( algSc ‘ 𝑃 )
7		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
8	3 7	rrgss	⊢ 𝐸 ⊆ ( Base ‘ 𝑅 )
9	8	sseli	⊢ ( 𝐹 ∈ 𝐸 → 𝐹 ∈ ( Base ‘ 𝑅 ) )
10		eqid	⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
11	2 4 7 6 5 10	coe1sclmul	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ ( Base ‘ 𝑅 ) ∧ 𝐺 ∈ 𝐵 ) → ( coe1 ‘ ( ( 𝐴 ‘ 𝐹 ) · 𝐺 ) ) = ( ( ℕ0 × { 𝐹 } ) ∘f ( .r ‘ 𝑅 ) ( coe1 ‘ 𝐺 ) ) )
12	9 11	syl3an2	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐸 ∧ 𝐺 ∈ 𝐵 ) → ( coe1 ‘ ( ( 𝐴 ‘ 𝐹 ) · 𝐺 ) ) = ( ( ℕ0 × { 𝐹 } ) ∘f ( .r ‘ 𝑅 ) ( coe1 ‘ 𝐺 ) ) )
13	12	oveq1d	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐸 ∧ 𝐺 ∈ 𝐵 ) → ( ( coe1 ‘ ( ( 𝐴 ‘ 𝐹 ) · 𝐺 ) ) supp ( 0g ‘ 𝑅 ) ) = ( ( ( ℕ0 × { 𝐹 } ) ∘f ( .r ‘ 𝑅 ) ( coe1 ‘ 𝐺 ) ) supp ( 0g ‘ 𝑅 ) ) )
14		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
15		nn0ex	⊢ ℕ0 ∈ V
16	15	a1i	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐸 ∧ 𝐺 ∈ 𝐵 ) → ℕ0 ∈ V )
17		simp1	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐸 ∧ 𝐺 ∈ 𝐵 ) → 𝑅 ∈ Ring )
18		simp2	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐸 ∧ 𝐺 ∈ 𝐵 ) → 𝐹 ∈ 𝐸 )
19		eqid	⊢ ( coe1 ‘ 𝐺 ) = ( coe1 ‘ 𝐺 )
20	19 4 2 7	coe1f	⊢ ( 𝐺 ∈ 𝐵 → ( coe1 ‘ 𝐺 ) : ℕ0 ⟶ ( Base ‘ 𝑅 ) )
21	20	3ad2ant3	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐸 ∧ 𝐺 ∈ 𝐵 ) → ( coe1 ‘ 𝐺 ) : ℕ0 ⟶ ( Base ‘ 𝑅 ) )
22	3 7 10 14 16 17 18 21	rrgsupp	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐸 ∧ 𝐺 ∈ 𝐵 ) → ( ( ( ℕ0 × { 𝐹 } ) ∘f ( .r ‘ 𝑅 ) ( coe1 ‘ 𝐺 ) ) supp ( 0g ‘ 𝑅 ) ) = ( ( coe1 ‘ 𝐺 ) supp ( 0g ‘ 𝑅 ) ) )
23	13 22	eqtrd	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐸 ∧ 𝐺 ∈ 𝐵 ) → ( ( coe1 ‘ ( ( 𝐴 ‘ 𝐹 ) · 𝐺 ) ) supp ( 0g ‘ 𝑅 ) ) = ( ( coe1 ‘ 𝐺 ) supp ( 0g ‘ 𝑅 ) ) )
24	23	supeq1d	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐸 ∧ 𝐺 ∈ 𝐵 ) → sup ( ( ( coe1 ‘ ( ( 𝐴 ‘ 𝐹 ) · 𝐺 ) ) supp ( 0g ‘ 𝑅 ) ) , ℝ* , < ) = sup ( ( ( coe1 ‘ 𝐺 ) supp ( 0g ‘ 𝑅 ) ) , ℝ* , < ) )
25	2	ply1ring	⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
26	25	3ad2ant1	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐸 ∧ 𝐺 ∈ 𝐵 ) → 𝑃 ∈ Ring )
27	2 6 7 4	ply1sclf	⊢ ( 𝑅 ∈ Ring → 𝐴 : ( Base ‘ 𝑅 ) ⟶ 𝐵 )
28	27	3ad2ant1	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐸 ∧ 𝐺 ∈ 𝐵 ) → 𝐴 : ( Base ‘ 𝑅 ) ⟶ 𝐵 )
29	9	3ad2ant2	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐸 ∧ 𝐺 ∈ 𝐵 ) → 𝐹 ∈ ( Base ‘ 𝑅 ) )
30	28 29	ffvelrnd	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐸 ∧ 𝐺 ∈ 𝐵 ) → ( 𝐴 ‘ 𝐹 ) ∈ 𝐵 )
31		simp3	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐸 ∧ 𝐺 ∈ 𝐵 ) → 𝐺 ∈ 𝐵 )
32	4 5	ringcl	⊢ ( ( 𝑃 ∈ Ring ∧ ( 𝐴 ‘ 𝐹 ) ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( ( 𝐴 ‘ 𝐹 ) · 𝐺 ) ∈ 𝐵 )
33	26 30 31 32	syl3anc	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐸 ∧ 𝐺 ∈ 𝐵 ) → ( ( 𝐴 ‘ 𝐹 ) · 𝐺 ) ∈ 𝐵 )
34		eqid	⊢ ( coe1 ‘ ( ( 𝐴 ‘ 𝐹 ) · 𝐺 ) ) = ( coe1 ‘ ( ( 𝐴 ‘ 𝐹 ) · 𝐺 ) )
35	1 2 4 14 34	deg1val	⊢ ( ( ( 𝐴 ‘ 𝐹 ) · 𝐺 ) ∈ 𝐵 → ( 𝐷 ‘ ( ( 𝐴 ‘ 𝐹 ) · 𝐺 ) ) = sup ( ( ( coe1 ‘ ( ( 𝐴 ‘ 𝐹 ) · 𝐺 ) ) supp ( 0g ‘ 𝑅 ) ) , ℝ* , < ) )
36	33 35	syl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐸 ∧ 𝐺 ∈ 𝐵 ) → ( 𝐷 ‘ ( ( 𝐴 ‘ 𝐹 ) · 𝐺 ) ) = sup ( ( ( coe1 ‘ ( ( 𝐴 ‘ 𝐹 ) · 𝐺 ) ) supp ( 0g ‘ 𝑅 ) ) , ℝ* , < ) )
37	1 2 4 14 19	deg1val	⊢ ( 𝐺 ∈ 𝐵 → ( 𝐷 ‘ 𝐺 ) = sup ( ( ( coe1 ‘ 𝐺 ) supp ( 0g ‘ 𝑅 ) ) , ℝ* , < ) )
38	37	3ad2ant3	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐸 ∧ 𝐺 ∈ 𝐵 ) → ( 𝐷 ‘ 𝐺 ) = sup ( ( ( coe1 ‘ 𝐺 ) supp ( 0g ‘ 𝑅 ) ) , ℝ* , < ) )
39	24 36 38	3eqtr4d	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐸 ∧ 𝐺 ∈ 𝐵 ) → ( 𝐷 ‘ ( ( 𝐴 ‘ 𝐹 ) · 𝐺 ) ) = ( 𝐷 ‘ 𝐺 ) )