Theorem prjcrvval

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 )
	prjcrvval.f	⊢ ( 𝜑 → 𝐹 ∈ ∪ ran 𝐻 )
Assertion	prjcrvval	⊢ ( 𝜑 → ( ( 𝑁 ℙ𝕣𝕠𝕛Crv 𝐾 ) ‘ 𝐹 ) = { 𝑝 ∈ 𝑃 ∣ ( ( 𝐸 ‘ 𝐹 ) “ 𝑝 ) = { 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		prjcrvval.f	⊢ ( 𝜑 → 𝐹 ∈ ∪ ran 𝐻 )
8		fveq2	⊢ ( 𝑓 = 𝐹 → ( 𝐸 ‘ 𝑓 ) = ( 𝐸 ‘ 𝐹 ) )
9	8	imaeq1d	⊢ ( 𝑓 = 𝐹 → ( ( 𝐸 ‘ 𝑓 ) “ 𝑝 ) = ( ( 𝐸 ‘ 𝐹 ) “ 𝑝 ) )
10	9	eqeq1d	⊢ ( 𝑓 = 𝐹 → ( ( ( 𝐸 ‘ 𝑓 ) “ 𝑝 ) = { 0 } ↔ ( ( 𝐸 ‘ 𝐹 ) “ 𝑝 ) = { 0 } ) )
11	10	rabbidv	⊢ ( 𝑓 = 𝐹 → { 𝑝 ∈ 𝑃 ∣ ( ( 𝐸 ‘ 𝑓 ) “ 𝑝 ) = { 0 } } = { 𝑝 ∈ 𝑃 ∣ ( ( 𝐸 ‘ 𝐹 ) “ 𝑝 ) = { 0 } } )
12	1 2 3 4 5 6	prjcrvfval	⊢ ( 𝜑 → ( 𝑁 ℙ𝕣𝕠𝕛Crv 𝐾 ) = ( 𝑓 ∈ ∪ ran 𝐻 ↦ { 𝑝 ∈ 𝑃 ∣ ( ( 𝐸 ‘ 𝑓 ) “ 𝑝 ) = { 0 } } ) )
13	3	ovexi	⊢ 𝑃 ∈ V
14	13	rabex	⊢ { 𝑝 ∈ 𝑃 ∣ ( ( 𝐸 ‘ 𝐹 ) “ 𝑝 ) = { 0 } } ∈ V
15	14	a1i	⊢ ( 𝜑 → { 𝑝 ∈ 𝑃 ∣ ( ( 𝐸 ‘ 𝐹 ) “ 𝑝 ) = { 0 } } ∈ V )
16	11 12 7 15	fvmptd4	⊢ ( 𝜑 → ( ( 𝑁 ℙ𝕣𝕠𝕛Crv 𝐾 ) ‘ 𝐹 ) = { 𝑝 ∈ 𝑃 ∣ ( ( 𝐸 ‘ 𝐹 ) “ 𝑝 ) = { 0 } } )