Metamath Proof Explorer

Theorem veronesev4lem

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