Metamath Proof Explorer

Theorem veronesev3lem

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

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