This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ffvelcdmd ⊢ ( ( 𝑅 ∈ 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 ∧ 𝐹 ∈ 𝐸 ∧ 𝐺 ∈ 𝐵 ) → ( 𝐷 ‘ ( ( 𝐴 ‘ 𝐹 ) · 𝐺 ) ) = ( 𝐷 ‘ 𝐺 ) )