Theorem prjcrvfval

Description: Value of the projective curve function. (Contributed by SN, 23-Nov-2024)

	Ref	Expression
Hypotheses	prjcrvfval.h	⊢ 𝐻 = ( ( 0 ... 𝑁 ) mHomP 𝐾 )
	prjcrvfval.e	⊢ 𝐸 = ( ( 0 ... 𝑁 ) eval 𝐾 )
	prjcrvfval.p	⊢ 𝑃 = ( 𝑁 ℙ𝕣𝕠𝕛n 𝐾 )
	prjcrvfval.0	⊢ 0 = ( 0g ‘ 𝐾 )
	prjcrvfval.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
	prjcrvfval.k	⊢ ( 𝜑 → 𝐾 ∈ Field )
Assertion	prjcrvfval	⊢ ( 𝜑 → ( 𝑁 ℙ𝕣𝕠𝕛Crv 𝐾 ) = ( 𝑓 ∈ ∪ ran 𝐻 ↦ { 𝑝 ∈ 𝑃 ∣ ( ( 𝐸 ‘ 𝑓 ) “ 𝑝 ) = { 0 } } ) )

Proof

Step	Hyp	Ref	Expression
1		prjcrvfval.h	⊢ 𝐻 = ( ( 0 ... 𝑁 ) mHomP 𝐾 )
2		prjcrvfval.e	⊢ 𝐸 = ( ( 0 ... 𝑁 ) eval 𝐾 )
3		prjcrvfval.p	⊢ 𝑃 = ( 𝑁 ℙ𝕣𝕠𝕛n 𝐾 )
4		prjcrvfval.0	⊢ 0 = ( 0g ‘ 𝐾 )
5		prjcrvfval.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
6		prjcrvfval.k	⊢ ( 𝜑 → 𝐾 ∈ Field )
7		oveq2	⊢ ( 𝑛 = 𝑁 → ( 0 ... 𝑛 ) = ( 0 ... 𝑁 ) )
8		oveq12	⊢ ( ( ( 0 ... 𝑛 ) = ( 0 ... 𝑁 ) ∧ 𝑘 = 𝐾 ) → ( ( 0 ... 𝑛 ) mHomP 𝑘 ) = ( ( 0 ... 𝑁 ) mHomP 𝐾 ) )
9	7 8	sylan	⊢ ( ( 𝑛 = 𝑁 ∧ 𝑘 = 𝐾 ) → ( ( 0 ... 𝑛 ) mHomP 𝑘 ) = ( ( 0 ... 𝑁 ) mHomP 𝐾 ) )
10	9 1	eqtr4di	⊢ ( ( 𝑛 = 𝑁 ∧ 𝑘 = 𝐾 ) → ( ( 0 ... 𝑛 ) mHomP 𝑘 ) = 𝐻 )
11	10	rneqd	⊢ ( ( 𝑛 = 𝑁 ∧ 𝑘 = 𝐾 ) → ran ( ( 0 ... 𝑛 ) mHomP 𝑘 ) = ran 𝐻 )
12	11	unieqd	⊢ ( ( 𝑛 = 𝑁 ∧ 𝑘 = 𝐾 ) → ∪ ran ( ( 0 ... 𝑛 ) mHomP 𝑘 ) = ∪ ran 𝐻 )
13		oveq12	⊢ ( ( 𝑛 = 𝑁 ∧ 𝑘 = 𝐾 ) → ( 𝑛 ℙ𝕣𝕠𝕛n 𝑘 ) = ( 𝑁 ℙ𝕣𝕠𝕛n 𝐾 ) )
14	13 3	eqtr4di	⊢ ( ( 𝑛 = 𝑁 ∧ 𝑘 = 𝐾 ) → ( 𝑛 ℙ𝕣𝕠𝕛n 𝑘 ) = 𝑃 )
15		id	⊢ ( 𝑘 = 𝐾 → 𝑘 = 𝐾 )
16	7 15	oveqan12d	⊢ ( ( 𝑛 = 𝑁 ∧ 𝑘 = 𝐾 ) → ( ( 0 ... 𝑛 ) eval 𝑘 ) = ( ( 0 ... 𝑁 ) eval 𝐾 ) )
17	16 2	eqtr4di	⊢ ( ( 𝑛 = 𝑁 ∧ 𝑘 = 𝐾 ) → ( ( 0 ... 𝑛 ) eval 𝑘 ) = 𝐸 )
18	17	fveq1d	⊢ ( ( 𝑛 = 𝑁 ∧ 𝑘 = 𝐾 ) → ( ( ( 0 ... 𝑛 ) eval 𝑘 ) ‘ 𝑓 ) = ( 𝐸 ‘ 𝑓 ) )
19	18	imaeq1d	⊢ ( ( 𝑛 = 𝑁 ∧ 𝑘 = 𝐾 ) → ( ( ( ( 0 ... 𝑛 ) eval 𝑘 ) ‘ 𝑓 ) “ 𝑝 ) = ( ( 𝐸 ‘ 𝑓 ) “ 𝑝 ) )
20		fveq2	⊢ ( 𝑘 = 𝐾 → ( 0g ‘ 𝑘 ) = ( 0g ‘ 𝐾 ) )
21	20 4	eqtr4di	⊢ ( 𝑘 = 𝐾 → ( 0g ‘ 𝑘 ) = 0 )
22	21	adantl	⊢ ( ( 𝑛 = 𝑁 ∧ 𝑘 = 𝐾 ) → ( 0g ‘ 𝑘 ) = 0 )
23	22	sneqd	⊢ ( ( 𝑛 = 𝑁 ∧ 𝑘 = 𝐾 ) → { ( 0g ‘ 𝑘 ) } = { 0 } )
24	19 23	eqeq12d	⊢ ( ( 𝑛 = 𝑁 ∧ 𝑘 = 𝐾 ) → ( ( ( ( ( 0 ... 𝑛 ) eval 𝑘 ) ‘ 𝑓 ) “ 𝑝 ) = { ( 0g ‘ 𝑘 ) } ↔ ( ( 𝐸 ‘ 𝑓 ) “ 𝑝 ) = { 0 } ) )
25	14 24	rabeqbidv	⊢ ( ( 𝑛 = 𝑁 ∧ 𝑘 = 𝐾 ) → { 𝑝 ∈ ( 𝑛 ℙ𝕣𝕠𝕛n 𝑘 ) ∣ ( ( ( ( 0 ... 𝑛 ) eval 𝑘 ) ‘ 𝑓 ) “ 𝑝 ) = { ( 0g ‘ 𝑘 ) } } = { 𝑝 ∈ 𝑃 ∣ ( ( 𝐸 ‘ 𝑓 ) “ 𝑝 ) = { 0 } } )
26	12 25	mpteq12dv	⊢ ( ( 𝑛 = 𝑁 ∧ 𝑘 = 𝐾 ) → ( 𝑓 ∈ ∪ ran ( ( 0 ... 𝑛 ) mHomP 𝑘 ) ↦ { 𝑝 ∈ ( 𝑛 ℙ𝕣𝕠𝕛n 𝑘 ) ∣ ( ( ( ( 0 ... 𝑛 ) eval 𝑘 ) ‘ 𝑓 ) “ 𝑝 ) = { ( 0g ‘ 𝑘 ) } } ) = ( 𝑓 ∈ ∪ ran 𝐻 ↦ { 𝑝 ∈ 𝑃 ∣ ( ( 𝐸 ‘ 𝑓 ) “ 𝑝 ) = { 0 } } ) )
27		df-prjcrv	⊢ ℙ𝕣𝕠𝕛Crv = ( 𝑛 ∈ ℕ0 , 𝑘 ∈ Field ↦ ( 𝑓 ∈ ∪ ran ( ( 0 ... 𝑛 ) mHomP 𝑘 ) ↦ { 𝑝 ∈ ( 𝑛 ℙ𝕣𝕠𝕛n 𝑘 ) ∣ ( ( ( ( 0 ... 𝑛 ) eval 𝑘 ) ‘ 𝑓 ) “ 𝑝 ) = { ( 0g ‘ 𝑘 ) } } ) )
28	1	ovexi	⊢ 𝐻 ∈ V
29	28	rnex	⊢ ran 𝐻 ∈ V
30	29	uniex	⊢ ∪ ran 𝐻 ∈ V
31	30	mptex	⊢ ( 𝑓 ∈ ∪ ran 𝐻 ↦ { 𝑝 ∈ 𝑃 ∣ ( ( 𝐸 ‘ 𝑓 ) “ 𝑝 ) = { 0 } } ) ∈ V
32	26 27 31	ovmpoa	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ Field ) → ( 𝑁 ℙ𝕣𝕠𝕛Crv 𝐾 ) = ( 𝑓 ∈ ∪ ran 𝐻 ↦ { 𝑝 ∈ 𝑃 ∣ ( ( 𝐸 ‘ 𝑓 ) “ 𝑝 ) = { 0 } } ) )
33	5 6 32	syl2anc	⊢ ( 𝜑 → ( 𝑁 ℙ𝕣𝕠𝕛Crv 𝐾 ) = ( 𝑓 ∈ ∪ ran 𝐻 ↦ { 𝑝 ∈ 𝑃 ∣ ( ( 𝐸 ‘ 𝑓 ) “ 𝑝 ) = { 0 } } ) )