Theorem prjcrvval

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

	Ref	Expression
Hypotheses	prjcrvfval.h	|- H = ( ( 0 ... N ) mHomP K )
	prjcrvfval.e	|- E = ( ( 0 ... N ) eval K )
	prjcrvfval.p	|- P = ( N PrjSpn K )
	prjcrvfval.0	|- .0. = ( 0g ` K )
	prjcrvfval.n	|- ( ph -> N e. NN0 )
	prjcrvfval.k	|- ( ph -> K e. Field )
	prjcrvval.f	|- ( ph -> F e. U. ran H )
Assertion	prjcrvval	|- ( ph -> ( ( N PrjCrv K ) ` F ) = { p e. P | ( ( E ` F ) " p ) = { .0. } } )

Proof

Step	Hyp	Ref	Expression
1		prjcrvfval.h	|- H = ( ( 0 ... N ) mHomP K )
2		prjcrvfval.e	|- E = ( ( 0 ... N ) eval K )
3		prjcrvfval.p	|- P = ( N PrjSpn K )
4		prjcrvfval.0	|- .0. = ( 0g ` K )
5		prjcrvfval.n	|- ( ph -> N e. NN0 )
6		prjcrvfval.k	|- ( ph -> K e. Field )
7		prjcrvval.f	|- ( ph -> F e. U. ran H )
8		fveq2	|- ( f = F -> ( E ` f ) = ( E ` F ) )
9	8	imaeq1d	|- ( f = F -> ( ( E ` f ) " p ) = ( ( E ` F ) " p ) )
10	9	eqeq1d	|- ( f = F -> ( ( ( E ` f ) " p ) = { .0. } <-> ( ( E ` F ) " p ) = { .0. } ) )
11	10	rabbidv	|- ( f = F -> { p e. P | ( ( E ` f ) " p ) = { .0. } } = { p e. P | ( ( E ` F ) " p ) = { .0. } } )
12	1 2 3 4 5 6	prjcrvfval	|- ( ph -> ( N PrjCrv K ) = ( f e. U. ran H |-> { p e. P | ( ( E ` f ) " p ) = { .0. } } ) )
13	3	ovexi	|- P e. _V
14	13	rabex	|- { p e. P | ( ( E ` F ) " p ) = { .0. } } e. _V
15	14	a1i	|- ( ph -> { p e. P | ( ( E ` F ) " p ) = { .0. } } e. _V )
16	11 12 7 15	fvmptd4	|- ( ph -> ( ( N PrjCrv K ) ` F ) = { p e. P | ( ( E ` F ) " p ) = { .0. } } )