Definition df-prjcrv

Description: Define the projective curve function. This takes a homogeneous polynomial and outputs the homogeneous coordinates where the polynomial evaluates to zero (the "zero set"). (In other words, scalar multiples are collapsed into the same projective point. See mhphf4 and prjspvs ). (Contributed by SN, 23-Nov-2024)

	Ref	Expression
Assertion	df-prjcrv	⊢ ℙrojCrv = ( 𝑛 ∈ ℕ0 , 𝑘 ∈ Field ↦ ( 𝑓 ∈ ∪ ran ( ( 0 ... 𝑛 ) mHomP 𝑘 ) ↦ { 𝑝 ∈ ( 𝑛 ℙrojn 𝑘 ) ∣ ( ( ( ( 0 ... 𝑛 ) eval 𝑘 ) ‘ 𝑓 ) “ 𝑝 ) = { ( 0g ‘ 𝑘 ) } } ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cprjcrv	⊢ ℙrojCrv
1		vn	⊢ 𝑛
2		cn0	⊢ ℕ0
3		vk	⊢ 𝑘
4		cfield	⊢ Field
5		vf	⊢ 𝑓
6		cc0	⊢ 0
7		cfz	⊢ ...
8	1	cv	⊢ 𝑛
9	6 8 7	co	⊢ ( 0 ... 𝑛 )
10		cmhp	⊢ mHomP
11	3	cv	⊢ 𝑘
12	9 11 10	co	⊢ ( ( 0 ... 𝑛 ) mHomP 𝑘 )
13	12	crn	⊢ ran ( ( 0 ... 𝑛 ) mHomP 𝑘 )
14	13	cuni	⊢ ∪ ran ( ( 0 ... 𝑛 ) mHomP 𝑘 )
15		vp	⊢ 𝑝
16		cprjspn	⊢ ℙrojn
17	8 11 16	co	⊢ ( 𝑛 ℙrojn 𝑘 )
18		cevl	⊢ eval
19	9 11 18	co	⊢ ( ( 0 ... 𝑛 ) eval 𝑘 )
20	5	cv	⊢ 𝑓
21	20 19	cfv	⊢ ( ( ( 0 ... 𝑛 ) eval 𝑘 ) ‘ 𝑓 )
22	15	cv	⊢ 𝑝
23	21 22	cima	⊢ ( ( ( ( 0 ... 𝑛 ) eval 𝑘 ) ‘ 𝑓 ) “ 𝑝 )
24		c0g	⊢ 0g
25	11 24	cfv	⊢ ( 0g ‘ 𝑘 )
26	25	csn	⊢ { ( 0g ‘ 𝑘 ) }
27	23 26	wceq	⊢ ( ( ( ( 0 ... 𝑛 ) eval 𝑘 ) ‘ 𝑓 ) “ 𝑝 ) = { ( 0g ‘ 𝑘 ) }
28	27 15 17	crab	⊢ { 𝑝 ∈ ( 𝑛 ℙrojn 𝑘 ) ∣ ( ( ( ( 0 ... 𝑛 ) eval 𝑘 ) ‘ 𝑓 ) “ 𝑝 ) = { ( 0g ‘ 𝑘 ) } }
29	5 14 28	cmpt	⊢ ( 𝑓 ∈ ∪ ran ( ( 0 ... 𝑛 ) mHomP 𝑘 ) ↦ { 𝑝 ∈ ( 𝑛 ℙrojn 𝑘 ) ∣ ( ( ( ( 0 ... 𝑛 ) eval 𝑘 ) ‘ 𝑓 ) “ 𝑝 ) = { ( 0g ‘ 𝑘 ) } } )
30	1 3 2 4 29	cmpo	⊢ ( 𝑛 ∈ ℕ0 , 𝑘 ∈ Field ↦ ( 𝑓 ∈ ∪ ran ( ( 0 ... 𝑛 ) mHomP 𝑘 ) ↦ { 𝑝 ∈ ( 𝑛 ℙrojn 𝑘 ) ∣ ( ( ( ( 0 ... 𝑛 ) eval 𝑘 ) ‘ 𝑓 ) “ 𝑝 ) = { ( 0g ‘ 𝑘 ) } } ) )
31	0 30	wceq	⊢ ℙrojCrv = ( 𝑛 ∈ ℕ0 , 𝑘 ∈ Field ↦ ( 𝑓 ∈ ∪ ran ( ( 0 ... 𝑛 ) mHomP 𝑘 ) ↦ { 𝑝 ∈ ( 𝑛 ℙrojn 𝑘 ) ∣ ( ( ( ( 0 ... 𝑛 ) eval 𝑘 ) ‘ 𝑓 ) “ 𝑝 ) = { ( 0g ‘ 𝑘 ) } } ) )