Metamath Proof Explorer

Theorem veronesev2lem

Description: Lemma for veronesevrowd . Value of the second coordinate of the Veronese map at a point. (Contributed by Jiamin Zhao, 16-Aug-2026)

Ref Expression
Hypothesis veronesevrow.1 
|- ( ph -> P e. ( RR ^m ( 1 ... 3 ) ) )
Assertion veronesev2lem 
|- ( ph -> ( ( veronese ` P ) ` 2 ) = ( ( P ` 2 ) ^ 2 ) )

Proof

Step Hyp Ref Expression
1 veronesevrow.1 
 |-  ( ph -> P e. ( RR ^m ( 1 ... 3 ) ) )
2 1 veronesevald 
 |-  ( ph -> ( veronese ` P ) = ( x e. ( 1 ... 6 ) |-> ( ( ( if ( x = 1 , ( ( P ` 1 ) ^ 2 ) , 0 ) + if ( x = 2 , ( ( P ` 2 ) ^ 2 ) , 0 ) ) + if ( x = 3 , ( ( P ` 3 ) ^ 2 ) , 0 ) ) + ( ( if ( x = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , 0 ) + if ( x = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , 0 ) ) + if ( x = 6 , ( ( P ` 3 ) x. ( P ` 1 ) ) , 0 ) ) ) ) )
3 iftrue 
 |-  ( x = 2 -> if ( x = 2 , ( ( P ` 2 ) ^ 2 ) , 0 ) = ( ( P ` 2 ) ^ 2 ) )
4 3 oveq2d 
 |-  ( x = 2 -> ( if ( x = 1 , ( ( P ` 1 ) ^ 2 ) , 0 ) + if ( x = 2 , ( ( P ` 2 ) ^ 2 ) , 0 ) ) = ( if ( x = 1 , ( ( P ` 1 ) ^ 2 ) , 0 ) + ( ( P ` 2 ) ^ 2 ) ) )
5 4 oveq1d 
 |-  ( x = 2 -> ( ( if ( x = 1 , ( ( P ` 1 ) ^ 2 ) , 0 ) + if ( x = 2 , ( ( P ` 2 ) ^ 2 ) , 0 ) ) + if ( x = 3 , ( ( P ` 3 ) ^ 2 ) , 0 ) ) = ( ( if ( x = 1 , ( ( P ` 1 ) ^ 2 ) , 0 ) + ( ( P ` 2 ) ^ 2 ) ) + if ( x = 3 , ( ( P ` 3 ) ^ 2 ) , 0 ) ) )
6 5 oveq1d 
 |-  ( x = 2 -> ( ( ( if ( x = 1 , ( ( P ` 1 ) ^ 2 ) , 0 ) + if ( x = 2 , ( ( P ` 2 ) ^ 2 ) , 0 ) ) + if ( x = 3 , ( ( P ` 3 ) ^ 2 ) , 0 ) ) + ( ( if ( x = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , 0 ) + if ( x = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , 0 ) ) + if ( x = 6 , ( ( P ` 3 ) x. ( P ` 1 ) ) , 0 ) ) ) = ( ( ( if ( x = 1 , ( ( P ` 1 ) ^ 2 ) , 0 ) + ( ( P ` 2 ) ^ 2 ) ) + if ( x = 3 , ( ( P ` 3 ) ^ 2 ) , 0 ) ) + ( ( if ( x = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , 0 ) + if ( x = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , 0 ) ) + if ( x = 6 , ( ( P ` 3 ) x. ( P ` 1 ) ) , 0 ) ) ) )
7 1ne2 
 |-  1 =/= 2
8 7 necomi 
 |-  2 =/= 1
9 neeq1 
 |-  ( x = 2 -> ( x =/= 1 <-> 2 =/= 1 ) )
10 8 9 mpbiri 
 |-  ( x = 2 -> x =/= 1 )
11 10 neneqd 
 |-  ( x = 2 -> -. x = 1 )
12 11 iffalsed 
 |-  ( x = 2 -> if ( x = 1 , ( ( P ` 1 ) ^ 2 ) , 0 ) = 0 )
13 12 oveq1d 
 |-  ( x = 2 -> ( if ( x = 1 , ( ( P ` 1 ) ^ 2 ) , 0 ) + ( ( P ` 2 ) ^ 2 ) ) = ( 0 + ( ( P ` 2 ) ^ 2 ) ) )
14 13 oveq1d 
 |-  ( x = 2 -> ( ( if ( x = 1 , ( ( P ` 1 ) ^ 2 ) , 0 ) + ( ( P ` 2 ) ^ 2 ) ) + if ( x = 3 , ( ( P ` 3 ) ^ 2 ) , 0 ) ) = ( ( 0 + ( ( P ` 2 ) ^ 2 ) ) + if ( x = 3 , ( ( P ` 3 ) ^ 2 ) , 0 ) ) )
15 14 oveq1d 
 |-  ( x = 2 -> ( ( ( if ( x = 1 , ( ( P ` 1 ) ^ 2 ) , 0 ) + ( ( P ` 2 ) ^ 2 ) ) + if ( x = 3 , ( ( P ` 3 ) ^ 2 ) , 0 ) ) + ( ( if ( x = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , 0 ) + if ( x = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , 0 ) ) + if ( x = 6 , ( ( P ` 3 ) x. ( P ` 1 ) ) , 0 ) ) ) = ( ( ( 0 + ( ( P ` 2 ) ^ 2 ) ) + if ( x = 3 , ( ( P ` 3 ) ^ 2 ) , 0 ) ) + ( ( if ( x = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , 0 ) + if ( x = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , 0 ) ) + if ( x = 6 , ( ( P ` 3 ) x. ( P ` 1 ) ) , 0 ) ) ) )
16 6 15 eqtrd 
 |-  ( x = 2 -> ( ( ( if ( x = 1 , ( ( P ` 1 ) ^ 2 ) , 0 ) + if ( x = 2 , ( ( P ` 2 ) ^ 2 ) , 0 ) ) + if ( x = 3 , ( ( P ` 3 ) ^ 2 ) , 0 ) ) + ( ( if ( x = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , 0 ) + if ( x = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , 0 ) ) + if ( x = 6 , ( ( P ` 3 ) x. ( P ` 1 ) ) , 0 ) ) ) = ( ( ( 0 + ( ( P ` 2 ) ^ 2 ) ) + if ( x = 3 , ( ( P ` 3 ) ^ 2 ) , 0 ) ) + ( ( if ( x = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , 0 ) + if ( x = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , 0 ) ) + if ( x = 6 , ( ( P ` 3 ) x. ( P ` 1 ) ) , 0 ) ) ) )
17 2ne3 
 |-  2 =/= 3
18 neeq1 
 |-  ( x = 2 -> ( x =/= 3 <-> 2 =/= 3 ) )
19 17 18 mpbiri 
 |-  ( x = 2 -> x =/= 3 )
20 19 neneqd 
 |-  ( x = 2 -> -. x = 3 )
21 20 iffalsed 
 |-  ( x = 2 -> if ( x = 3 , ( ( P ` 3 ) ^ 2 ) , 0 ) = 0 )
22 21 oveq2d 
 |-  ( x = 2 -> ( ( 0 + ( ( P ` 2 ) ^ 2 ) ) + if ( x = 3 , ( ( P ` 3 ) ^ 2 ) , 0 ) ) = ( ( 0 + ( ( P ` 2 ) ^ 2 ) ) + 0 ) )
23 22 oveq1d 
 |-  ( x = 2 -> ( ( ( 0 + ( ( P ` 2 ) ^ 2 ) ) + if ( x = 3 , ( ( P ` 3 ) ^ 2 ) , 0 ) ) + ( ( if ( x = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , 0 ) + if ( x = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , 0 ) ) + if ( x = 6 , ( ( P ` 3 ) x. ( P ` 1 ) ) , 0 ) ) ) = ( ( ( 0 + ( ( P ` 2 ) ^ 2 ) ) + 0 ) + ( ( if ( x = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , 0 ) + if ( x = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , 0 ) ) + if ( x = 6 , ( ( P ` 3 ) x. ( P ` 1 ) ) , 0 ) ) ) )
24 2re 
 |-  2 e. RR
25 2lt4 
 |-  2 < 4
26 24 25 ltneii 
 |-  2 =/= 4
27 neeq1 
 |-  ( x = 2 -> ( x =/= 4 <-> 2 =/= 4 ) )
28 26 27 mpbiri 
 |-  ( x = 2 -> x =/= 4 )
29 28 neneqd 
 |-  ( x = 2 -> -. x = 4 )
30 29 iffalsed 
 |-  ( x = 2 -> if ( x = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , 0 ) = 0 )
31 30 oveq1d 
 |-  ( x = 2 -> ( if ( x = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , 0 ) + if ( x = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , 0 ) ) = ( 0 + if ( x = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , 0 ) ) )
32 31 oveq1d 
 |-  ( x = 2 -> ( ( if ( x = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , 0 ) + if ( x = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , 0 ) ) + if ( x = 6 , ( ( P ` 3 ) x. ( P ` 1 ) ) , 0 ) ) = ( ( 0 + if ( x = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , 0 ) ) + if ( x = 6 , ( ( P ` 3 ) x. ( P ` 1 ) ) , 0 ) ) )
33 32 oveq2d 
 |-  ( x = 2 -> ( ( ( 0 + ( ( P ` 2 ) ^ 2 ) ) + 0 ) + ( ( if ( x = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , 0 ) + if ( x = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , 0 ) ) + if ( x = 6 , ( ( P ` 3 ) x. ( P ` 1 ) ) , 0 ) ) ) = ( ( ( 0 + ( ( P ` 2 ) ^ 2 ) ) + 0 ) + ( ( 0 + if ( x = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , 0 ) ) + if ( x = 6 , ( ( P ` 3 ) x. ( P ` 1 ) ) , 0 ) ) ) )
34 16 23 33 3eqtrd 
 |-  ( x = 2 -> ( ( ( if ( x = 1 , ( ( P ` 1 ) ^ 2 ) , 0 ) + if ( x = 2 , ( ( P ` 2 ) ^ 2 ) , 0 ) ) + if ( x = 3 , ( ( P ` 3 ) ^ 2 ) , 0 ) ) + ( ( if ( x = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , 0 ) + if ( x = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , 0 ) ) + if ( x = 6 , ( ( P ` 3 ) x. ( P ` 1 ) ) , 0 ) ) ) = ( ( ( 0 + ( ( P ` 2 ) ^ 2 ) ) + 0 ) + ( ( 0 + if ( x = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , 0 ) ) + if ( x = 6 , ( ( P ` 3 ) x. ( P ` 1 ) ) , 0 ) ) ) )
35 2lt5 
 |-  2 < 5
36 24 35 ltneii 
 |-  2 =/= 5
37 neeq1 
 |-  ( x = 2 -> ( x =/= 5 <-> 2 =/= 5 ) )
38 36 37 mpbiri 
 |-  ( x = 2 -> x =/= 5 )
39 38 neneqd 
 |-  ( x = 2 -> -. x = 5 )
40 39 iffalsed 
 |-  ( x = 2 -> if ( x = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , 0 ) = 0 )
41 40 oveq2d 
 |-  ( x = 2 -> ( 0 + if ( x = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , 0 ) ) = ( 0 + 0 ) )
42 41 oveq1d 
 |-  ( x = 2 -> ( ( 0 + if ( x = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , 0 ) ) + if ( x = 6 , ( ( P ` 3 ) x. ( P ` 1 ) ) , 0 ) ) = ( ( 0 + 0 ) + if ( x = 6 , ( ( P ` 3 ) x. ( P ` 1 ) ) , 0 ) ) )
43 42 oveq2d 
 |-  ( x = 2 -> ( ( ( 0 + ( ( P ` 2 ) ^ 2 ) ) + 0 ) + ( ( 0 + if ( x = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , 0 ) ) + if ( x = 6 , ( ( P ` 3 ) x. ( P ` 1 ) ) , 0 ) ) ) = ( ( ( 0 + ( ( P ` 2 ) ^ 2 ) ) + 0 ) + ( ( 0 + 0 ) + if ( x = 6 , ( ( P ` 3 ) x. ( P ` 1 ) ) , 0 ) ) ) )
44 2lt6 
 |-  2 < 6
45 24 44 ltneii 
 |-  2 =/= 6
46 neeq1 
 |-  ( x = 2 -> ( x =/= 6 <-> 2 =/= 6 ) )
47 45 46 mpbiri 
 |-  ( x = 2 -> x =/= 6 )
48 47 neneqd 
 |-  ( x = 2 -> -. x = 6 )
49 48 iffalsed 
 |-  ( x = 2 -> if ( x = 6 , ( ( P ` 3 ) x. ( P ` 1 ) ) , 0 ) = 0 )
50 49 oveq2d 
 |-  ( x = 2 -> ( ( 0 + 0 ) + if ( x = 6 , ( ( P ` 3 ) x. ( P ` 1 ) ) , 0 ) ) = ( ( 0 + 0 ) + 0 ) )
51 50 oveq2d 
 |-  ( x = 2 -> ( ( ( 0 + ( ( P ` 2 ) ^ 2 ) ) + 0 ) + ( ( 0 + 0 ) + if ( x = 6 , ( ( P ` 3 ) x. ( P ` 1 ) ) , 0 ) ) ) = ( ( ( 0 + ( ( P ` 2 ) ^ 2 ) ) + 0 ) + ( ( 0 + 0 ) + 0 ) ) )
52 34 43 51 3eqtrd 
 |-  ( x = 2 -> ( ( ( if ( x = 1 , ( ( P ` 1 ) ^ 2 ) , 0 ) + if ( x = 2 , ( ( P ` 2 ) ^ 2 ) , 0 ) ) + if ( x = 3 , ( ( P ` 3 ) ^ 2 ) , 0 ) ) + ( ( if ( x = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , 0 ) + if ( x = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , 0 ) ) + if ( x = 6 , ( ( P ` 3 ) x. ( P ` 1 ) ) , 0 ) ) ) = ( ( ( 0 + ( ( P ` 2 ) ^ 2 ) ) + 0 ) + ( ( 0 + 0 ) + 0 ) ) )
53 52 adantl 
 |-  ( ( ph /\ x = 2 ) -> ( ( ( if ( x = 1 , ( ( P ` 1 ) ^ 2 ) , 0 ) + if ( x = 2 , ( ( P ` 2 ) ^ 2 ) , 0 ) ) + if ( x = 3 , ( ( P ` 3 ) ^ 2 ) , 0 ) ) + ( ( if ( x = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , 0 ) + if ( x = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , 0 ) ) + if ( x = 6 , ( ( P ` 3 ) x. ( P ` 1 ) ) , 0 ) ) ) = ( ( ( 0 + ( ( P ` 2 ) ^ 2 ) ) + 0 ) + ( ( 0 + 0 ) + 0 ) ) )
54 0red 
 |-  ( ( ph /\ x = 2 ) -> 0 e. RR )
55 1 rr3fv2cld 
 |-  ( ph -> ( P ` 2 ) e. RR )
56 55 adantr 
 |-  ( ( ph /\ x = 2 ) -> ( P ` 2 ) e. RR )
57 56 resqcld 
 |-  ( ( ph /\ x = 2 ) -> ( ( P ` 2 ) ^ 2 ) e. RR )
58 54 57 readdcld 
 |-  ( ( ph /\ x = 2 ) -> ( 0 + ( ( P ` 2 ) ^ 2 ) ) e. RR )
59 58 recnd 
 |-  ( ( ph /\ x = 2 ) -> ( 0 + ( ( P ` 2 ) ^ 2 ) ) e. CC )
60 59 addridd 
 |-  ( ( ph /\ x = 2 ) -> ( ( 0 + ( ( P ` 2 ) ^ 2 ) ) + 0 ) = ( 0 + ( ( P ` 2 ) ^ 2 ) ) )
61 60 oveq1d 
 |-  ( ( ph /\ x = 2 ) -> ( ( ( 0 + ( ( P ` 2 ) ^ 2 ) ) + 0 ) + ( ( 0 + 0 ) + 0 ) ) = ( ( 0 + ( ( P ` 2 ) ^ 2 ) ) + ( ( 0 + 0 ) + 0 ) ) )
62 57 recnd 
 |-  ( ( ph /\ x = 2 ) -> ( ( P ` 2 ) ^ 2 ) e. CC )
63 62 addlidd 
 |-  ( ( ph /\ x = 2 ) -> ( 0 + ( ( P ` 2 ) ^ 2 ) ) = ( ( P ` 2 ) ^ 2 ) )
64 63 oveq1d 
 |-  ( ( ph /\ x = 2 ) -> ( ( 0 + ( ( P ` 2 ) ^ 2 ) ) + ( ( 0 + 0 ) + 0 ) ) = ( ( ( P ` 2 ) ^ 2 ) + ( ( 0 + 0 ) + 0 ) ) )
65 61 64 eqtrd 
 |-  ( ( ph /\ x = 2 ) -> ( ( ( 0 + ( ( P ` 2 ) ^ 2 ) ) + 0 ) + ( ( 0 + 0 ) + 0 ) ) = ( ( ( P ` 2 ) ^ 2 ) + ( ( 0 + 0 ) + 0 ) ) )
66 54 54 readdcld 
 |-  ( ( ph /\ x = 2 ) -> ( 0 + 0 ) e. RR )
67 66 recnd 
 |-  ( ( ph /\ x = 2 ) -> ( 0 + 0 ) e. CC )
68 67 addridd 
 |-  ( ( ph /\ x = 2 ) -> ( ( 0 + 0 ) + 0 ) = ( 0 + 0 ) )
69 68 oveq2d 
 |-  ( ( ph /\ x = 2 ) -> ( ( ( P ` 2 ) ^ 2 ) + ( ( 0 + 0 ) + 0 ) ) = ( ( ( P ` 2 ) ^ 2 ) + ( 0 + 0 ) ) )
70 00id 
 |-  ( 0 + 0 ) = 0
71 70 a1i 
 |-  ( ( ph /\ x = 2 ) -> ( 0 + 0 ) = 0 )
72 71 oveq2d 
 |-  ( ( ph /\ x = 2 ) -> ( ( ( P ` 2 ) ^ 2 ) + ( 0 + 0 ) ) = ( ( ( P ` 2 ) ^ 2 ) + 0 ) )
73 65 69 72 3eqtrd 
 |-  ( ( ph /\ x = 2 ) -> ( ( ( 0 + ( ( P ` 2 ) ^ 2 ) ) + 0 ) + ( ( 0 + 0 ) + 0 ) ) = ( ( ( P ` 2 ) ^ 2 ) + 0 ) )
74 62 addridd 
 |-  ( ( ph /\ x = 2 ) -> ( ( ( P ` 2 ) ^ 2 ) + 0 ) = ( ( P ` 2 ) ^ 2 ) )
75 53 73 74 3eqtrd 
 |-  ( ( ph /\ x = 2 ) -> ( ( ( if ( x = 1 , ( ( P ` 1 ) ^ 2 ) , 0 ) + if ( x = 2 , ( ( P ` 2 ) ^ 2 ) , 0 ) ) + if ( x = 3 , ( ( P ` 3 ) ^ 2 ) , 0 ) ) + ( ( if ( x = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , 0 ) + if ( x = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , 0 ) ) + if ( x = 6 , ( ( P ` 3 ) x. ( P ` 1 ) ) , 0 ) ) ) = ( ( P ` 2 ) ^ 2 ) )
76 1zzd 
 |-  ( ph -> 1 e. ZZ )
77 6nn 
 |-  6 e. NN
78 77 nnzi 
 |-  6 e. ZZ
79 78 a1i 
 |-  ( ph -> 6 e. ZZ )
80 2z 
 |-  2 e. ZZ
81 80 a1i 
 |-  ( ph -> 2 e. ZZ )
82 1le2 
 |-  1 <_ 2
83 82 a1i 
 |-  ( ph -> 1 <_ 2 )
84 6re 
 |-  6 e. RR
85 24 84 44 ltleii 
 |-  2 <_ 6
86 85 a1i 
 |-  ( ph -> 2 <_ 6 )
87 76 79 81 83 86 elfzd 
 |-  ( ph -> 2 e. ( 1 ... 6 ) )
88 55 resqcld 
 |-  ( ph -> ( ( P ` 2 ) ^ 2 ) e. RR )
89 2 75 87 88 fvmptd 
 |-  ( ph -> ( ( veronese ` P ) ` 2 ) = ( ( P ` 2 ) ^ 2 ) )