Theorem prjcrvval

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

	Ref	Expression
Hypotheses	prjcrvfval.h	$$⊢H=\left(0\dots N\right)\mathrm{mHomP}K$$
	prjcrvfval.e	$$⊢E=\left(0\dots N\right)\mathrm{eval}K$$
	prjcrvfval.p	$$⊢P=N{\mathrm{\mathbb{P}𝕣𝕠𝕛}}_{n}K$$
	prjcrvfval.0	$$⊢\underset{\dot{}}{0}=0_K$$
	prjcrvfval.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
	prjcrvfval.k	$$⊢\phi \to K\in \mathrm{Field}$$
	prjcrvval.f	$$⊢\phi \to F\in \bigcup \mathrm{ran}H$$
Assertion	prjcrvval	$$⊢\phi \to \left(N\mathrm{PrjCrv}K\right)\left(F\right)=\left\{p\in P|E\left(F\right)\left[p\right]=\left\{\underset{\dot{}}{0}\right\}\right\}$$

Proof

Step	Hyp	Ref	Expression
1		prjcrvfval.h	$$⊢H=\left(0\dots N\right)\mathrm{mHomP}K$$
2		prjcrvfval.e	$$⊢E=\left(0\dots N\right)\mathrm{eval}K$$
3		prjcrvfval.p	$$⊢P=N{\mathrm{\mathbb{P}𝕣𝕠𝕛}}_{n}K$$
4		prjcrvfval.0	$$⊢\underset{\dot{}}{0}=0_K$$
5		prjcrvfval.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
6		prjcrvfval.k	$$⊢\phi \to K\in \mathrm{Field}$$
7		prjcrvval.f	$$⊢\phi \to F\in \bigcup \mathrm{ran}H$$
8		fveq2	$$⊢f=F\to E\left(f\right)=E\left(F\right)$$
9	8	imaeq1d	$$⊢f=F\to E\left(f\right)\left[p\right]=E\left(F\right)\left[p\right]$$
10	9	eqeq1d	$$⊢f=F\to \left(E\left(f\right)\left[p\right]=\left\{\underset{\dot{}}{0}\right\}\leftrightarrow E\left(F\right)\left[p\right]=\left\{\underset{\dot{}}{0}\right\}\right)$$
11	10	rabbidv	$$⊢f=F\to \left\{p\in P|E\left(f\right)\left[p\right]=\left\{\underset{\dot{}}{0}\right\}\right\}=\left\{p\in P|E\left(F\right)\left[p\right]=\left\{\underset{\dot{}}{0}\right\}\right\}$$
12	1 2 3 4 5 6	prjcrvfval	$$⊢\phi \to N\mathrm{PrjCrv}K=\left(f\in \bigcup \mathrm{ran}H⟼\left\{p\in P|E\left(f\right)\left[p\right]=\left\{\underset{\dot{}}{0}\right\}\right\}\right)$$
13	3	ovexi	$$⊢P\in \mathrm{V}$$
14	13	rabex	$$⊢\left\{p\in P|E\left(F\right)\left[p\right]=\left\{\underset{\dot{}}{0}\right\}\right\}\in \mathrm{V}$$
15	14	a1i	$$⊢\phi \to \left\{p\in P|E\left(F\right)\left[p\right]=\left\{\underset{\dot{}}{0}\right\}\right\}\in \mathrm{V}$$
16	11 12 7 15	fvmptd4	$$⊢\phi \to \left(N\mathrm{PrjCrv}K\right)\left(F\right)=\left\{p\in P|E\left(F\right)\left[p\right]=\left\{\underset{\dot{}}{0}\right\}\right\}$$