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 ) , ℝ* , < ) )