Theorem prjcrvfval

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}$$
Assertion	prjcrvfval	Could not format assertion : No typesetting found for |- ( ph -> ( N PrjCrv K ) = ( f e. U. ran H |-> { p e. P | ( ( E ` f ) " p ) = { .0. } } ) ) with typecode |-

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		oveq2	$$⊢n=N\to \left(0\dots n\right)=\left(0\dots N\right)$$
8		oveq12	$$⊢\left(\left(0\dots n\right)=\left(0\dots N\right)\wedge k=K\right)\to \left(0\dots n\right)\mathrm{mHomP}k=\left(0\dots N\right)\mathrm{mHomP}K$$
9	7 8	sylan	$$⊢\left(n=N\wedge k=K\right)\to \left(0\dots n\right)\mathrm{mHomP}k=\left(0\dots N\right)\mathrm{mHomP}K$$
10	9 1	eqtr4di	$$⊢\left(n=N\wedge k=K\right)\to \left(0\dots n\right)\mathrm{mHomP}k=H$$
11	10	rneqd	$$⊢\left(n=N\wedge k=K\right)\to \mathrm{ran}\left(\left(0\dots n\right)\mathrm{mHomP}k\right)=\mathrm{ran}H$$
12	11	unieqd	$$⊢\left(n=N\wedge k=K\right)\to \bigcup \mathrm{ran}\left(\left(0\dots n\right)\mathrm{mHomP}k\right)=\bigcup \mathrm{ran}H$$
13		oveq12	$$⊢\left(n=N\wedge k=K\right)\to n{\mathrm{\mathbb{P}𝕣𝕠𝕛}}_{n}k=N{\mathrm{\mathbb{P}𝕣𝕠𝕛}}_{n}K$$
14	13 3	eqtr4di	$$⊢\left(n=N\wedge k=K\right)\to n{\mathrm{\mathbb{P}𝕣𝕠𝕛}}_{n}k=P$$
15		id	$$⊢k=K\to k=K$$
16	7 15	oveqan12d	$$⊢\left(n=N\wedge k=K\right)\to \left(0\dots n\right)\mathrm{eval}k=\left(0\dots N\right)\mathrm{eval}K$$
17	16 2	eqtr4di	$$⊢\left(n=N\wedge k=K\right)\to \left(0\dots n\right)\mathrm{eval}k=E$$
18	17	fveq1d	$$⊢\left(n=N\wedge k=K\right)\to \left(\left(0\dots n\right)\mathrm{eval}k\right)\left(f\right)=E\left(f\right)$$
19	18	imaeq1d	$$⊢\left(n=N\wedge k=K\right)\to \left(\left(0\dots n\right)\mathrm{eval}k\right)\left(f\right)\left[p\right]=E\left(f\right)\left[p\right]$$
20		fveq2	$$⊢k=K\to 0_k=0_K$$
21	20 4	eqtr4di	$$⊢k=K\to 0_k=\underset{\dot{}}{0}$$
22	21	adantl	$$⊢\left(n=N\wedge k=K\right)\to 0_k=\underset{\dot{}}{0}$$
23	22	sneqd	$$⊢\left(n=N\wedge k=K\right)\to \left\{0_k\right\}=\left\{\underset{\dot{}}{0}\right\}$$
24	19 23	eqeq12d	$$⊢\left(n=N\wedge k=K\right)\to \left(\left(\left(0\dots n\right)\mathrm{eval}k\right)\left(f\right)\left[p\right]=\left\{0_k\right\}\leftrightarrow E\left(f\right)\left[p\right]=\left\{\underset{\dot{}}{0}\right\}\right)$$
25	14 24	rabeqbidv	$$⊢\left(n=N\wedge k=K\right)\to \left\{p\in \left(n{\mathrm{\mathbb{P}𝕣𝕠𝕛}}_{n}k\right)|\left(\left(0\dots n\right)\mathrm{eval}k\right)\left(f\right)\left[p\right]=\left\{0_k\right\}\right\}=\left\{p\in P|E\left(f\right)\left[p\right]=\left\{\underset{\dot{}}{0}\right\}\right\}$$
26	12 25	mpteq12dv	$$⊢\left(n=N\wedge k=K\right)\to \left(f\in \bigcup \mathrm{ran}\left(\left(0\dots n\right)\mathrm{mHomP}k\right)⟼\left\{p\in \left(n{\mathrm{\mathbb{P}𝕣𝕠𝕛}}_{n}k\right)|\left(\left(0\dots n\right)\mathrm{eval}k\right)\left(f\right)\left[p\right]=\left\{0_k\right\}\right\}\right)=\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)$$
27		df-prjcrv	Could not format PrjCrv = ( n e. NN0 , k e. Field |-> ( f e. U. ran ( ( 0 ... n ) mHomP k ) |-> { p e. ( n PrjSpn k ) | ( ( ( ( 0 ... n ) eval k ) ` f ) " p ) = { ( 0g ` k ) } } ) ) : No typesetting found for |- PrjCrv = ( n e. NN0 , k e. Field |-> ( f e. U. ran ( ( 0 ... n ) mHomP k ) |-> { p e. ( n PrjSpn k ) | ( ( ( ( 0 ... n ) eval k ) ` f ) " p ) = { ( 0g ` k ) } } ) ) with typecode |-
28	1	ovexi	$$⊢H\in \mathrm{V}$$
29	28	rnex	$$⊢\mathrm{ran}H\in \mathrm{V}$$
30	29	uniex	$$⊢\bigcup \mathrm{ran}H\in \mathrm{V}$$
31	30	mptex	$$⊢\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)\in \mathrm{V}$$
32	26 27 31	ovmpoa	Could not format ( ( N e. NN0 /\ K e. Field ) -> ( N PrjCrv K ) = ( f e. U. ran H |-> { p e. P | ( ( E ` f ) " p ) = { .0. } } ) ) : No typesetting found for |- ( ( N e. NN0 /\ K e. Field ) -> ( N PrjCrv K ) = ( f e. U. ran H |-> { p e. P | ( ( E ` f ) " p ) = { .0. } } ) ) with typecode |-
33	5 6 32	syl2anc	Could not format ( ph -> ( N PrjCrv K ) = ( f e. U. ran H |-> { p e. P | ( ( E ` f ) " p ) = { .0. } } ) ) : No typesetting found for |- ( ph -> ( N PrjCrv K ) = ( f e. U. ran H |-> { p e. P | ( ( E ` f ) " p ) = { .0. } } ) ) with typecode |-