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

Metamath Proof Explorer

Theorem mdegpropd

Description: Property deduction for polynomial degree. (Contributed by Stefan O'Rear, 28-Mar-2015) (Proof shortened by AV, 27-Jul-2019)

Ref Expression
Hypotheses mdegpropd.b1 ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝑅 ) )
mdegpropd.b2 ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝑆 ) )
mdegpropd.p ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) )
Assertion mdegpropd ( 𝜑 → ( 𝐼 mDeg 𝑅 ) = ( 𝐼 mDeg 𝑆 ) )

Proof

Step Hyp Ref Expression
1 mdegpropd.b1 ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝑅 ) )
2 mdegpropd.b2 ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝑆 ) )
3 mdegpropd.p ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) )
4 1 2 3 mplbaspropd ⊢ ( 𝜑 → ( Base ‘ ( 𝐼 mPoly 𝑅 ) ) = ( Base ‘ ( 𝐼 mPoly 𝑆 ) ) )
5 1 2 3 grpidpropd ⊢ ( 𝜑 → ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑆 ) )
6 5 oveq2d ⊢ ( 𝜑 → ( 𝑐 supp ( 0g ‘ 𝑅 ) ) = ( 𝑐 supp ( 0g ‘ 𝑆 ) ) )
7 6 imaeq2d ⊢ ( 𝜑 → ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) “ ( 𝑐 supp ( 0g ‘ 𝑅 ) ) ) = ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) “ ( 𝑐 supp ( 0g ‘ 𝑆 ) ) ) )
8 7 supeq1d ⊢ ( 𝜑 → sup ( ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) “ ( 𝑐 supp ( 0g ‘ 𝑅 ) ) ) , ℝ* , < ) = sup ( ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) “ ( 𝑐 supp ( 0g ‘ 𝑆 ) ) ) , ℝ* , < ) )
9 4 8 mpteq12dv ⊢ ( 𝜑 → ( 𝑐 ∈ ( Base ‘ ( 𝐼 mPoly 𝑅 ) ) ↦ sup ( ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) “ ( 𝑐 supp ( 0g ‘ 𝑅 ) ) ) , ℝ* , < ) ) = ( 𝑐 ∈ ( Base ‘ ( 𝐼 mPoly 𝑆 ) ) ↦ sup ( ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) “ ( 𝑐 supp ( 0g ‘ 𝑆 ) ) ) , ℝ* , < ) ) )
10 eqid ⊢ ( 𝐼 mDeg 𝑅 ) = ( 𝐼 mDeg 𝑅 )
11 eqid ⊢ ( 𝐼 mPoly 𝑅 ) = ( 𝐼 mPoly 𝑅 )
12 eqid ⊢ ( Base ‘ ( 𝐼 mPoly 𝑅 ) ) = ( Base ‘ ( 𝐼 mPoly 𝑅 ) )
13 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
14 eqid ⊢ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } = { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin }
15 eqid ⊢ ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) = ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) )
16 10 11 12 13 14 15 mdegfval ⊢ ( 𝐼 mDeg 𝑅 ) = ( 𝑐 ∈ ( Base ‘ ( 𝐼 mPoly 𝑅 ) ) ↦ sup ( ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) “ ( 𝑐 supp ( 0g ‘ 𝑅 ) ) ) , ℝ* , < ) )
17 eqid ⊢ ( 𝐼 mDeg 𝑆 ) = ( 𝐼 mDeg 𝑆 )
18 eqid ⊢ ( 𝐼 mPoly 𝑆 ) = ( 𝐼 mPoly 𝑆 )
19 eqid ⊢ ( Base ‘ ( 𝐼 mPoly 𝑆 ) ) = ( Base ‘ ( 𝐼 mPoly 𝑆 ) )
20 eqid ⊢ ( 0g ‘ 𝑆 ) = ( 0g ‘ 𝑆 )
21 17 18 19 20 14 15 mdegfval ⊢ ( 𝐼 mDeg 𝑆 ) = ( 𝑐 ∈ ( Base ‘ ( 𝐼 mPoly 𝑆 ) ) ↦ sup ( ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) “ ( 𝑐 supp ( 0g ‘ 𝑆 ) ) ) , ℝ* , < ) )
22 9 16 21 3eqtr4g ⊢ ( 𝜑 → ( 𝐼 mDeg 𝑅 ) = ( 𝐼 mDeg 𝑆 ) )