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