prjcrvfval

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

	Ref	Expression
Hypotheses	prjcrvfval.h	$⊢ H = (0 \dots N) mHomP K$
	prjcrvfval.e	$⊢ E = (0 \dots N) eval K$
	prjcrvfval.p	$⊢ P = N {ℙ𝕣𝕠𝕛}_{n} K$
	prjcrvfval.0	$⊢ \underset{˙}{0} = 0_{K}$
	prjcrvfval.n	$⊢ φ \to N \in ℕ_{0}$
	prjcrvfval.k	$⊢ φ \to K \in Field$
Assertion	prjcrvfval	$⊢ φ \to N PrjCrv K = (f \in ⋃ ran H ⟼ \{p \in P \| E (f) [p] = \{\underset{˙}{0}\}\})$

Proof

Step	Hyp	Ref	Expression
1		prjcrvfval.h	$⊢ H = (0 \dots N) mHomP K$
2		prjcrvfval.e	$⊢ E = (0 \dots N) eval K$
3		prjcrvfval.p	$⊢ P = N {ℙ𝕣𝕠𝕛}_{n} K$
4		prjcrvfval.0	$⊢ \underset{˙}{0} = 0_{K}$
5		prjcrvfval.n	$⊢ φ \to N \in ℕ_{0}$
6		prjcrvfval.k	$⊢ φ \to K \in Field$
7		oveq2	$⊢ n = N \to (0 \dots n) = (0 \dots N)$
8		oveq12	$⊢ ((0 \dots n) = (0 \dots N) \land k = K) \to (0 \dots n) mHomP k = (0 \dots N) mHomP K$
9	7 8	sylan	$⊢ (n = N \land k = K) \to (0 \dots n) mHomP k = (0 \dots N) mHomP K$
10	9 1	eqtr4di	$⊢ (n = N \land k = K) \to (0 \dots n) mHomP k = H$
11	10	rneqd	$⊢ (n = N \land k = K) \to ran ((0 \dots n) mHomP k) = ran H$
12	11	unieqd	$⊢ (n = N \land k = K) \to ⋃ ran ((0 \dots n) mHomP k) = ⋃ ran H$
13		oveq12	$⊢ (n = N \land k = K) \to n {ℙ𝕣𝕠𝕛}_{n} k = N {ℙ𝕣𝕠𝕛}_{n} K$
14	13 3	eqtr4di	$⊢ (n = N \land k = K) \to n {ℙ𝕣𝕠𝕛}_{n} k = P$
15		id	$⊢ k = K \to k = K$
16	7 15	oveqan12d	$⊢ (n = N \land k = K) \to (0 \dots n) eval k = (0 \dots N) eval K$
17	16 2	eqtr4di	$⊢ (n = N \land k = K) \to (0 \dots n) eval k = E$
18	17	fveq1d	$⊢ (n = N \land k = K) \to ((0 \dots n) eval k) (f) = E (f)$
19	18	imaeq1d	$⊢ (n = N \land k = K) \to ((0 \dots n) eval k) (f) [p] = E (f) [p]$
20		fveq2	$⊢ k = K \to 0_{k} = 0_{K}$
21	20 4	eqtr4di	$⊢ k = K \to 0_{k} = \underset{˙}{0}$
22	21	adantl	$⊢ (n = N \land k = K) \to 0_{k} = \underset{˙}{0}$
23	22	sneqd	$⊢ (n = N \land k = K) \to \{0_{k}\} = \{\underset{˙}{0}\}$
24	19 23	eqeq12d	$⊢ (n = N \land k = K) \to (((0 \dots n) eval k) (f) [p] = \{0_{k}\} \leftrightarrow E (f) [p] = \{\underset{˙}{0}\})$
25	14 24	rabeqbidv	$⊢ (n = N \land k = K) \to \{p \in (n {ℙ𝕣𝕠𝕛}_{n} k) \| ((0 \dots n) eval k) (f) [p] = \{0_{k}\}\} = \{p \in P \| E (f) [p] = \{\underset{˙}{0}\}\}$
26	12 25	mpteq12dv	$⊢ (n = N \land k = K) \to (f \in ⋃ ran ((0 \dots n) mHomP k) ⟼ \{p \in (n {ℙ𝕣𝕠𝕛}_{n} k) \| ((0 \dots n) eval k) (f) [p] = \{0_{k}\}\}) = (f \in ⋃ ran H ⟼ \{p \in P \| E (f) [p] = \{\underset{˙}{0}\}\})$
27		df-prjcrv	$⊢ PrjCrv = (n \in ℕ_{0}, k \in Field ⟼ (f \in ⋃ ran ((0 \dots n) mHomP k) ⟼ \{p \in (n {ℙ𝕣𝕠𝕛}_{n} k) \| ((0 \dots n) eval k) (f) [p] = \{0_{k}\}\}))$
28	1	ovexi	$⊢ H \in V$
29	28	rnex	$⊢ ran H \in V$
30	29	uniex	$⊢ ⋃ ran H \in V$
31	30	mptex	$⊢ (f \in ⋃ ran H ⟼ \{p \in P \| E (f) [p] = \{\underset{˙}{0}\}\}) \in V$
32	26 27 31	ovmpoa	$⊢ (N \in ℕ_{0} \land K \in Field) \to N PrjCrv K = (f \in ⋃ ran H ⟼ \{p \in P \| E (f) [p] = \{\underset{˙}{0}\}\})$
33	5 6 32	syl2anc	$⊢ φ \to N PrjCrv K = (f \in ⋃ ran H ⟼ \{p \in P \| E (f) [p] = \{\underset{˙}{0}\}\})$

Metamath Proof Explorer

Theorem prjcrvfval

Proof