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 𝑆 ) )