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

Metamath Proof Explorer

Theorem deg1val

Description: Value of the univariate degree as a supremum. (Contributed by Stefan O'Rear, 29-Mar-2015) (Revised by AV, 25-Jul-2019)

Ref Expression
Hypotheses deg1leb.d ⊢ 𝐷 = ( deg1 ‘ 𝑅 )
deg1leb.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
deg1leb.b ⊢ 𝐵 = ( Base ‘ 𝑃 )
deg1leb.y ⊢ 0 = ( 0g ‘ 𝑅 )
deg1leb.a ⊢ 𝐴 = ( coe1 ‘ 𝐹 )
Assertion deg1val ( 𝐹 ∈ 𝐵 → ( 𝐷 ‘ 𝐹 ) = sup ( ( 𝐴 supp 0 ) , ℝ* , < ) )

Proof

Step Hyp Ref Expression
1 deg1leb.d ⊢ 𝐷 = ( deg1 ‘ 𝑅 )
2 deg1leb.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
3 deg1leb.b ⊢ 𝐵 = ( Base ‘ 𝑃 )
4 deg1leb.y ⊢ 0 = ( 0g ‘ 𝑅 )
5 deg1leb.a ⊢ 𝐴 = ( coe1 ‘ 𝐹 )
6 1 deg1fval ⊢ 𝐷 = ( 1o mDeg 𝑅 )
7 eqid ⊢ ( 1o mPoly 𝑅 ) = ( 1o mPoly 𝑅 )
8 2 3 ply1bas ⊢ 𝐵 = ( Base ‘ ( 1o mPoly 𝑅 ) )
9 psr1baslem ⊢ ( ℕ0 ↑m 1o ) = { 𝑦 ∈ ( ℕ0 ↑m 1o ) ∣ ( ◡ 𝑦 “ ℕ ) ∈ Fin }
10 tdeglem2 ⊢ ( 𝑥 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑥 ‘ ∅ ) ) = ( 𝑥 ∈ ( ℕ0 ↑m 1o ) ↦ ( ℂfld Σg 𝑥 ) )
11 6 7 8 4 9 10 mdegval ⊢ ( 𝐹 ∈ 𝐵 → ( 𝐷 ‘ 𝐹 ) = sup ( ( ( 𝑥 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑥 ‘ ∅ ) ) “ ( 𝐹 supp 0 ) ) , ℝ* , < ) )
12 4 fvexi ⊢ 0 ∈ V
13 suppimacnv ⊢ ( ( 𝐹 ∈ 𝐵 ∧ 0 ∈ V ) → ( 𝐹 supp 0 ) = ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) )
14 12 13 mpan2 ⊢ ( 𝐹 ∈ 𝐵 → ( 𝐹 supp 0 ) = ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) )
15 14 imaeq2d ⊢ ( 𝐹 ∈ 𝐵 → ( ( 𝑥 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑥 ‘ ∅ ) ) “ ( 𝐹 supp 0 ) ) = ( ( 𝑥 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑥 ‘ ∅ ) ) “ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) )
16 imaco ⊢ ( ( ( 𝑥 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑥 ‘ ∅ ) ) ∘ ◡ 𝐹 ) “ ( V ∖ { 0 } ) ) = ( ( 𝑥 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑥 ‘ ∅ ) ) “ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) )
17 15 16 eqtr4di ⊢ ( 𝐹 ∈ 𝐵 → ( ( 𝑥 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑥 ‘ ∅ ) ) “ ( 𝐹 supp 0 ) ) = ( ( ( 𝑥 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑥 ‘ ∅ ) ) ∘ ◡ 𝐹 ) “ ( V ∖ { 0 } ) ) )
18 df1o2 ⊢ 1o = { ∅ }
19 nn0ex ⊢ ℕ0 ∈ V
20 0ex ⊢ ∅ ∈ V
21 eqid ⊢ ( 𝑥 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑥 ‘ ∅ ) ) = ( 𝑥 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑥 ‘ ∅ ) )
22 18 19 20 21 mapsncnv ⊢ ◡ ( 𝑥 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑥 ‘ ∅ ) ) = ( 𝑦 ∈ ℕ0 ↦ ( 1o × { 𝑦 } ) )
23 5 3 2 22 coe1fval2 ⊢ ( 𝐹 ∈ 𝐵 → 𝐴 = ( 𝐹 ∘ ◡ ( 𝑥 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑥 ‘ ∅ ) ) ) )
24 23 cnveqd ⊢ ( 𝐹 ∈ 𝐵 → ◡ 𝐴 = ◡ ( 𝐹 ∘ ◡ ( 𝑥 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑥 ‘ ∅ ) ) ) )
25 cnvco ⊢ ◡ ( 𝐹 ∘ ◡ ( 𝑥 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑥 ‘ ∅ ) ) ) = ( ◡ ◡ ( 𝑥 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑥 ‘ ∅ ) ) ∘ ◡ 𝐹 )
26 cocnvcnv1 ⊢ ( ◡ ◡ ( 𝑥 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑥 ‘ ∅ ) ) ∘ ◡ 𝐹 ) = ( ( 𝑥 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑥 ‘ ∅ ) ) ∘ ◡ 𝐹 )
27 25 26 eqtri ⊢ ◡ ( 𝐹 ∘ ◡ ( 𝑥 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑥 ‘ ∅ ) ) ) = ( ( 𝑥 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑥 ‘ ∅ ) ) ∘ ◡ 𝐹 )
28 24 27 eqtr2di ⊢ ( 𝐹 ∈ 𝐵 → ( ( 𝑥 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑥 ‘ ∅ ) ) ∘ ◡ 𝐹 ) = ◡ 𝐴 )
29 28 imaeq1d ⊢ ( 𝐹 ∈ 𝐵 → ( ( ( 𝑥 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑥 ‘ ∅ ) ) ∘ ◡ 𝐹 ) “ ( V ∖ { 0 } ) ) = ( ◡ 𝐴 “ ( V ∖ { 0 } ) ) )
30 17 29 eqtrd ⊢ ( 𝐹 ∈ 𝐵 → ( ( 𝑥 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑥 ‘ ∅ ) ) “ ( 𝐹 supp 0 ) ) = ( ◡ 𝐴 “ ( V ∖ { 0 } ) ) )
31 5 fvexi ⊢ 𝐴 ∈ V
32 suppimacnv ⊢ ( ( 𝐴 ∈ V ∧ 0 ∈ V ) → ( 𝐴 supp 0 ) = ( ◡ 𝐴 “ ( V ∖ { 0 } ) ) )
33 32 eqcomd ⊢ ( ( 𝐴 ∈ V ∧ 0 ∈ V ) → ( ◡ 𝐴 “ ( V ∖ { 0 } ) ) = ( 𝐴 supp 0 ) )
34 31 12 33 mp2an ⊢ ( ◡ 𝐴 “ ( V ∖ { 0 } ) ) = ( 𝐴 supp 0 )
35 30 34 eqtrdi ⊢ ( 𝐹 ∈ 𝐵 → ( ( 𝑥 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑥 ‘ ∅ ) ) “ ( 𝐹 supp 0 ) ) = ( 𝐴 supp 0 ) )
36 35 supeq1d ⊢ ( 𝐹 ∈ 𝐵 → sup ( ( ( 𝑥 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑥 ‘ ∅ ) ) “ ( 𝐹 supp 0 ) ) , ℝ* , < ) = sup ( ( 𝐴 supp 0 ) , ℝ* , < ) )
37 11 36 eqtrd ⊢ ( 𝐹 ∈ 𝐵 → ( 𝐷 ‘ 𝐹 ) = sup ( ( 𝐴 supp 0 ) , ℝ* , < ) )