Metamath Proof Explorer

Theorem prjcrvfval

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

Ref Expression
Hypotheses prjcrvfval.h 
|- H = ( ( 0 ... N ) mHomP K )
prjcrvfval.e 
|- E = ( ( 0 ... N ) eval K )
prjcrvfval.p 
|- P = ( N PrjSpn K )
prjcrvfval.0 
|- .0. = ( 0g ` K )
prjcrvfval.n 
|- ( ph -> N e. NN0 )
prjcrvfval.k 
|- ( ph -> K e. Field )
Assertion prjcrvfval 
|- ( ph -> ( N PrjCrv K ) = ( f e. U. ran H |-> { p e. P | ( ( E ` f ) " p ) = { .0. } } ) )

Proof

Step Hyp Ref Expression
1 prjcrvfval.h 
 |-  H = ( ( 0 ... N ) mHomP K )
2 prjcrvfval.e 
 |-  E = ( ( 0 ... N ) eval K )
3 prjcrvfval.p 
 |-  P = ( N PrjSpn K )
4 prjcrvfval.0 
 |-  .0. = ( 0g ` K )
5 prjcrvfval.n 
 |-  ( ph -> N e. NN0 )
6 prjcrvfval.k 
 |-  ( ph -> K e. Field )
7 oveq2 
 |-  ( n = N -> ( 0 ... n ) = ( 0 ... N ) )
8 oveq12 
 |-  ( ( ( 0 ... n ) = ( 0 ... N ) /\ k = K ) -> ( ( 0 ... n ) mHomP k ) = ( ( 0 ... N ) mHomP K ) )
9 7 8 sylan 
 |-  ( ( n = N /\ k = K ) -> ( ( 0 ... n ) mHomP k ) = ( ( 0 ... N ) mHomP K ) )
10 9 1 eqtr4di 
 |-  ( ( n = N /\ k = K ) -> ( ( 0 ... n ) mHomP k ) = H )
11 10 rneqd 
 |-  ( ( n = N /\ k = K ) -> ran ( ( 0 ... n ) mHomP k ) = ran H )
12 11 unieqd 
 |-  ( ( n = N /\ k = K ) -> U. ran ( ( 0 ... n ) mHomP k ) = U. ran H )
13 oveq12 
 |-  ( ( n = N /\ k = K ) -> ( n PrjSpn k ) = ( N PrjSpn K ) )
14 13 3 eqtr4di 
 |-  ( ( n = N /\ k = K ) -> ( n PrjSpn k ) = P )
15 id 
 |-  ( k = K -> k = K )
16 7 15 oveqan12d 
 |-  ( ( n = N /\ k = K ) -> ( ( 0 ... n ) eval k ) = ( ( 0 ... N ) eval K ) )
17 16 2 eqtr4di 
 |-  ( ( n = N /\ k = K ) -> ( ( 0 ... n ) eval k ) = E )
18 17 fveq1d 
 |-  ( ( n = N /\ k = K ) -> ( ( ( 0 ... n ) eval k ) ` f ) = ( E ` f ) )
19 18 imaeq1d 
 |-  ( ( n = N /\ k = K ) -> ( ( ( ( 0 ... n ) eval k ) ` f ) " p ) = ( ( E ` f ) " p ) )
20 fveq2 
 |-  ( k = K -> ( 0g ` k ) = ( 0g ` K ) )
21 20 4 eqtr4di 
 |-  ( k = K -> ( 0g ` k ) = .0. )
22 21 adantl 
 |-  ( ( n = N /\ k = K ) -> ( 0g ` k ) = .0. )
23 22 sneqd 
 |-  ( ( n = N /\ k = K ) -> { ( 0g ` k ) } = { .0. } )
24 19 23 eqeq12d 
 |-  ( ( n = N /\ k = K ) -> ( ( ( ( ( 0 ... n ) eval k ) ` f ) " p ) = { ( 0g ` k ) } <-> ( ( E ` f ) " p ) = { .0. } ) )
25 14 24 rabeqbidv 
 |-  ( ( n = N /\ k = K ) -> { p e. ( n PrjSpn k ) | ( ( ( ( 0 ... n ) eval k ) ` f ) " p ) = { ( 0g ` k ) } } = { p e. P | ( ( E ` f ) " p ) = { .0. } } )
26 12 25 mpteq12dv 
 |-  ( ( n = N /\ k = K ) -> ( f e. U. ran ( ( 0 ... n ) mHomP k ) |-> { p e. ( n PrjSpn k ) | ( ( ( ( 0 ... n ) eval k ) ` f ) " p ) = { ( 0g ` k ) } } ) = ( f e. U. ran H |-> { p e. P | ( ( E ` f ) " p ) = { .0. } } ) )
27 df-prjcrv 
 |-  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 ) } } ) )
28 1 ovexi 
 |-  H e. _V
29 28 rnex 
 |-  ran H e. _V
30 29 uniex 
 |-  U. ran H e. _V
31 30 mptex 
 |-  ( f e. U. ran H |-> { p e. P | ( ( E ` f ) " p ) = { .0. } } ) e. _V
32 26 27 31 ovmpoa 
 |-  ( ( N e. NN0 /\ K e. Field ) -> ( N PrjCrv K ) = ( f e. U. ran H |-> { p e. P | ( ( E ` f ) " p ) = { .0. } } ) )
33 5 6 32 syl2anc 
 |-  ( ph -> ( N PrjCrv K ) = ( f e. U. ran H |-> { p e. P | ( ( E ` f ) " p ) = { .0. } } ) )