Metamath Proof Explorer

Theorem veronesev6lem

Description: Lemma for veronesevrowd . Value of the sixth 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 veronesev6lem 
|- ( ph -> ( ( veronese ` P ) ` 6 ) = ( ( P ` 3 ) x. ( P ` 1 ) ) )

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