Theorem prjcrvfval 43804

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

Hypotheses

Ref	Expression
prjcrvfval.h	⊢ 𝐻 = ((0...𝑁) mHomP 𝐾)
prjcrvfval.e	⊢ 𝐸 = ((0...𝑁) eval 𝐾)
prjcrvfval.p	⊢ 𝑃 = (𝑁 ℙrojn 𝐾)
prjcrvfval.0	⊢ 0 = (0g‘𝐾)
prjcrvfval.n	⊢ (𝜑 → 𝑁 ∈ ℕ0)
prjcrvfval.k	⊢ (𝜑 → 𝐾 ∈ Field)

Assertion

Ref	Expression
prjcrvfval	⊢ (𝜑 → (𝑁 ℙrojCrv 𝐾) = (𝑓 ∈ ∪ ran 𝐻 ↦ {𝑝 ∈ 𝑃 ∣ ((𝐸‘𝑓) “ 𝑝) = { 0 }}))

Distinct variable groups:   𝑓,𝑁,𝑝   𝑓,𝐾,𝑝   𝑃,𝑝   𝑓,𝐻

Allowed substitution hints:   𝜑(𝑓, 𝑝)   𝑃(𝑓)   𝐸(𝑓, 𝑝)   𝐻(𝑝)   0 (𝑓, 𝑝)

Proof of Theorem prjcrvfval

Dummy variables 𝑛 𝑘 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		prjcrvfval.n	. 2 ⊢ (𝜑 → 𝑁 ∈ ℕ0)
2		prjcrvfval.k	. 2 ⊢ (𝜑 → 𝐾 ∈ Field)
3		oveq2 7432	. . . . . . . 8 ⊢ (𝑛 = 𝑁 → (0...𝑛) = (0...𝑁))
4		oveq12 7433	. . . . . . . 8 ⊢ (((0...𝑛) = (0...𝑁) ∧ 𝑘 = 𝐾) → ((0...𝑛) mHomP 𝑘) = ((0...𝑁) mHomP 𝐾))
5	3, 4	sylan 592	. . . . . . 7 ⊢ ((𝑛 = 𝑁 ∧ 𝑘 = 𝐾) → ((0...𝑛) mHomP 𝑘) = ((0...𝑁) mHomP 𝐾))
6		prjcrvfval.h	. . . . . . 7 ⊢ 𝐻 = ((0...𝑁) mHomP 𝐾)
7	5, 6	eqtr4di 2813	. . . . . 6 ⊢ ((𝑛 = 𝑁 ∧ 𝑘 = 𝐾) → ((0...𝑛) mHomP 𝑘) = 𝐻)
8	7	rneqd 5921	. . . . 5 ⊢ ((𝑛 = 𝑁 ∧ 𝑘 = 𝐾) → ran ((0...𝑛) mHomP 𝑘) = ran 𝐻)
9	8	unieqd 4879	. . . 4 ⊢ ((𝑛 = 𝑁 ∧ 𝑘 = 𝐾) → ∪ ran ((0...𝑛) mHomP 𝑘) = ∪ ran 𝐻)
10		oveq12 7433	. . . . . 6 ⊢ ((𝑛 = 𝑁 ∧ 𝑘 = 𝐾) → (𝑛 ℙrojn 𝑘) = (𝑁 ℙrojn 𝐾))
11		prjcrvfval.p	. . . . . 6 ⊢ 𝑃 = (𝑁 ℙrojn 𝐾)
12	10, 11	eqtr4di 2813	. . . . 5 ⊢ ((𝑛 = 𝑁 ∧ 𝑘 = 𝐾) → (𝑛 ℙrojn 𝑘) = 𝑃)
13		id 23	. . . . . . . . . 10 ⊢ (𝑘 = 𝐾 → 𝑘 = 𝐾)
14	3, 13	oveqan12d 7443	. . . . . . . . 9 ⊢ ((𝑛 = 𝑁 ∧ 𝑘 = 𝐾) → ((0...𝑛) eval 𝑘) = ((0...𝑁) eval 𝐾))
15		prjcrvfval.e	. . . . . . . . 9 ⊢ 𝐸 = ((0...𝑁) eval 𝐾)
16	14, 15	eqtr4di 2813	. . . . . . . 8 ⊢ ((𝑛 = 𝑁 ∧ 𝑘 = 𝐾) → ((0...𝑛) eval 𝑘) = 𝐸)
17	16	fveq1d 6892	. . . . . . 7 ⊢ ((𝑛 = 𝑁 ∧ 𝑘 = 𝐾) → (((0...𝑛) eval 𝑘)‘𝑓) = (𝐸‘𝑓))
18	17	imaeq1d 6053	. . . . . 6 ⊢ ((𝑛 = 𝑁 ∧ 𝑘 = 𝐾) → ((((0...𝑛) eval 𝑘)‘𝑓) “ 𝑝) = ((𝐸‘𝑓) “ 𝑝))
19		fveq2 6890	. . . . . . . . 9 ⊢ (𝑘 = 𝐾 → (0g‘𝑘) = (0g‘𝐾))
20		prjcrvfval.0	. . . . . . . . 9 ⊢ 0 = (0g‘𝐾)
21	19, 20	eqtr4di 2813	. . . . . . . 8 ⊢ (𝑘 = 𝐾 → (0g‘𝑘) = 0 )
22	21	adantl 487	. . . . . . 7 ⊢ ((𝑛 = 𝑁 ∧ 𝑘 = 𝐾) → (0g‘𝑘) = 0 )
23	22	sneqd 4592	. . . . . 6 ⊢ ((𝑛 = 𝑁 ∧ 𝑘 = 𝐾) → {(0g‘𝑘)} = { 0 })
24	18, 23	eqeq12d 2776	. . . . 5 ⊢ ((𝑛 = 𝑁 ∧ 𝑘 = 𝐾) → (((((0...𝑛) eval 𝑘)‘𝑓) “ 𝑝) = {(0g‘𝑘)} ↔ ((𝐸‘𝑓) “ 𝑝) = { 0 }))
25	12, 24	rabeqbidv 3429	. . . 4 ⊢ ((𝑛 = 𝑁 ∧ 𝑘 = 𝐾) → {𝑝 ∈ (𝑛 ℙrojn 𝑘) ∣ ((((0...𝑛) eval 𝑘)‘𝑓) “ 𝑝) = {(0g‘𝑘)}} = {𝑝 ∈ 𝑃 ∣ ((𝐸‘𝑓) “ 𝑝) = { 0 }})
26	9, 25	mpteq12dv 5191	. . 3 ⊢ ((𝑛 = 𝑁 ∧ 𝑘 = 𝐾) → (𝑓 ∈ ∪ ran ((0...𝑛) mHomP 𝑘) ↦ {𝑝 ∈ (𝑛 ℙrojn 𝑘) ∣ ((((0...𝑛) eval 𝑘)‘𝑓) “ 𝑝) = {(0g‘𝑘)}}) = (𝑓 ∈ ∪ ran 𝐻 ↦ {𝑝 ∈ 𝑃 ∣ ((𝐸‘𝑓) “ 𝑝) = { 0 }}))
27		df-prjcrv 43803	. . 3 ⊢ ℙrojCrv = (𝑛 ∈ ℕ0, 𝑘 ∈ Field ↦ (𝑓 ∈ ∪ ran ((0...𝑛) mHomP 𝑘) ↦ {𝑝 ∈ (𝑛 ℙrojn 𝑘) ∣ ((((0...𝑛) eval 𝑘)‘𝑓) “ 𝑝) = {(0g‘𝑘)}}))
28	6	ovexi 7458	. . . . . 6 ⊢ 𝐻 ∈ V
29	28	rnex 7926	. . . . 5 ⊢ ran 𝐻 ∈ V
30	29	uniex 7762	. . . 4 ⊢ ∪ ran 𝐻 ∈ V
31	30	mptex 7233	. . 3 ⊢ (𝑓 ∈ ∪ ran 𝐻 ↦ {𝑝 ∈ 𝑃 ∣ ((𝐸‘𝑓) “ 𝑝) = { 0 }}) ∈ V
32	26, 27, 31	ovmpoa 7579	. 2 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐾 ∈ Field) → (𝑁 ℙrojCrv 𝐾) = (𝑓 ∈ ∪ ran 𝐻 ↦ {𝑝 ∈ 𝑃 ∣ ((𝐸‘𝑓) “ 𝑝) = { 0 }}))
33	1, 2, 32	syl2anc 596	1 ⊢ (𝜑 → (𝑁 ℙrojCrv 𝐾) = (𝑓 ∈ ∪ ran 𝐻 ↦ {𝑝 ∈ 𝑃 ∣ ((𝐸‘𝑓) “ 𝑝) = { 0 }}))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1569   ∈ wcel 2144  {crab 3412  {csn 4584  ∪ cuni 4866   ↦ cmpt 5185  ran crn 5652   “ cima 5654  ‘cfv 6543  (class class class)co 7424  0cc0 11207  ℕ₀cn0 12613  ...cfz 13646  0_gc0g 17619  Fieldcfield 20990   eval cevl 22391   mHomP cmhp 22463   ℙroj_n cprjspn 43779   ℙrojCrv cprjcrv 43802

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-rep 5231  ax-sep 5248  ax-nul 5259  ax-pr 5391  ax-un 7755

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3848  df-ss 3897  df-dif 4046  df-in 4090  df-un 4150  df-nul 4278  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-iun 4952  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-iota 6497  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-ov 7427  df-oprab 7428  df-mpo 7429  df-prjcrv 43803

This theorem is used by:  prjcrvval  43805