Metamath Proof Explorer

Theorem veronesevrowd

Description: The Veronese map at a point, expressed explicitly as a piecewise maps-to function on the six coordinates. (Contributed by Jiamin Zhao, 17-Aug-2026)

Ref Expression
Hypothesis veronesevrow.1 
|- ( ph -> P e. ( RR ^m ( 1 ... 3 ) ) )
Assertion veronesevrowd 
|- ( ph -> ( veronese ` P ) = ( k e. ( 1 ... 6 ) |-> if ( k = 1 , ( ( P ` 1 ) ^ 2 ) , if ( k = 2 , ( ( P ` 2 ) ^ 2 ) , if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , ( ( P ` 3 ) x. ( P ` 1 ) ) ) ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 veronesevrow.1 
 |-  ( ph -> P e. ( RR ^m ( 1 ... 3 ) ) )
2 ovex 
 |-  ( ( ( if ( k = 1 , ( ( P ` 1 ) ^ 2 ) , 0 ) + if ( k = 2 , ( ( P ` 2 ) ^ 2 ) , 0 ) ) + if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , 0 ) ) + ( ( if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , 0 ) + if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , 0 ) ) + if ( k = 6 , ( ( P ` 3 ) x. ( P ` 1 ) ) , 0 ) ) ) e. _V
3 eqid 
 |-  ( k e. ( 1 ... 6 ) |-> ( ( ( if ( k = 1 , ( ( P ` 1 ) ^ 2 ) , 0 ) + if ( k = 2 , ( ( P ` 2 ) ^ 2 ) , 0 ) ) + if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , 0 ) ) + ( ( if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , 0 ) + if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , 0 ) ) + if ( k = 6 , ( ( P ` 3 ) x. ( P ` 1 ) ) , 0 ) ) ) ) = ( k e. ( 1 ... 6 ) |-> ( ( ( if ( k = 1 , ( ( P ` 1 ) ^ 2 ) , 0 ) + if ( k = 2 , ( ( P ` 2 ) ^ 2 ) , 0 ) ) + if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , 0 ) ) + ( ( if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , 0 ) + if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , 0 ) ) + if ( k = 6 , ( ( P ` 3 ) x. ( P ` 1 ) ) , 0 ) ) ) )
4 2 3 fnmpti 
 |-  ( k e. ( 1 ... 6 ) |-> ( ( ( if ( k = 1 , ( ( P ` 1 ) ^ 2 ) , 0 ) + if ( k = 2 , ( ( P ` 2 ) ^ 2 ) , 0 ) ) + if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , 0 ) ) + ( ( if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , 0 ) + if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , 0 ) ) + if ( k = 6 , ( ( P ` 3 ) x. ( P ` 1 ) ) , 0 ) ) ) ) Fn ( 1 ... 6 )
5 1 veronesevald 
 |-  ( ph -> ( veronese ` P ) = ( k e. ( 1 ... 6 ) |-> ( ( ( if ( k = 1 , ( ( P ` 1 ) ^ 2 ) , 0 ) + if ( k = 2 , ( ( P ` 2 ) ^ 2 ) , 0 ) ) + if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , 0 ) ) + ( ( if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , 0 ) + if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , 0 ) ) + if ( k = 6 , ( ( P ` 3 ) x. ( P ` 1 ) ) , 0 ) ) ) ) )
6 5 fneq1d 
 |-  ( ph -> ( ( veronese ` P ) Fn ( 1 ... 6 ) <-> ( k e. ( 1 ... 6 ) |-> ( ( ( if ( k = 1 , ( ( P ` 1 ) ^ 2 ) , 0 ) + if ( k = 2 , ( ( P ` 2 ) ^ 2 ) , 0 ) ) + if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , 0 ) ) + ( ( if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , 0 ) + if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , 0 ) ) + if ( k = 6 , ( ( P ` 3 ) x. ( P ` 1 ) ) , 0 ) ) ) ) Fn ( 1 ... 6 ) ) )
7 4 6 mpbiri 
 |-  ( ph -> ( veronese ` P ) Fn ( 1 ... 6 ) )
8 ovex 
 |-  ( ( P ` 1 ) ^ 2 ) e. _V
9 ovex 
 |-  ( ( P ` 2 ) ^ 2 ) e. _V
10 ovex 
 |-  ( ( P ` 3 ) ^ 2 ) e. _V
11 ovex 
 |-  ( ( P ` 1 ) x. ( P ` 2 ) ) e. _V
12 ovex 
 |-  ( ( P ` 2 ) x. ( P ` 3 ) ) e. _V
13 ovex 
 |-  ( ( P ` 3 ) x. ( P ` 1 ) ) e. _V
14 12 13 ifex 
 |-  if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , ( ( P ` 3 ) x. ( P ` 1 ) ) ) e. _V
15 11 14 ifex 
 |-  if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , ( ( P ` 3 ) x. ( P ` 1 ) ) ) ) e. _V
16 10 15 ifex 
 |-  if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , ( ( P ` 3 ) x. ( P ` 1 ) ) ) ) ) e. _V
17 9 16 ifex 
 |-  if ( k = 2 , ( ( P ` 2 ) ^ 2 ) , if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , ( ( P ` 3 ) x. ( P ` 1 ) ) ) ) ) ) e. _V
18 8 17 ifex 
 |-  if ( k = 1 , ( ( P ` 1 ) ^ 2 ) , if ( k = 2 , ( ( P ` 2 ) ^ 2 ) , if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , ( ( P ` 3 ) x. ( P ` 1 ) ) ) ) ) ) ) e. _V
19 eqid 
 |-  ( k e. ( 1 ... 6 ) |-> if ( k = 1 , ( ( P ` 1 ) ^ 2 ) , if ( k = 2 , ( ( P ` 2 ) ^ 2 ) , if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , ( ( P ` 3 ) x. ( P ` 1 ) ) ) ) ) ) ) ) = ( k e. ( 1 ... 6 ) |-> if ( k = 1 , ( ( P ` 1 ) ^ 2 ) , if ( k = 2 , ( ( P ` 2 ) ^ 2 ) , if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , ( ( P ` 3 ) x. ( P ` 1 ) ) ) ) ) ) ) )
20 18 19 fnmpti 
 |-  ( k e. ( 1 ... 6 ) |-> if ( k = 1 , ( ( P ` 1 ) ^ 2 ) , if ( k = 2 , ( ( P ` 2 ) ^ 2 ) , if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , ( ( P ` 3 ) x. ( P ` 1 ) ) ) ) ) ) ) ) Fn ( 1 ... 6 )
21 20 a1i 
 |-  ( ph -> ( k e. ( 1 ... 6 ) |-> if ( k = 1 , ( ( P ` 1 ) ^ 2 ) , if ( k = 2 , ( ( P ` 2 ) ^ 2 ) , if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , ( ( P ` 3 ) x. ( P ` 1 ) ) ) ) ) ) ) ) Fn ( 1 ... 6 ) )
22 1 veronesev1lem 
 |-  ( ph -> ( ( veronese ` P ) ` 1 ) = ( ( P ` 1 ) ^ 2 ) )
23 22 ad2antrr 
 |-  ( ( ( ph /\ x e. ( 1 ... 6 ) ) /\ x = 1 ) -> ( ( veronese ` P ) ` 1 ) = ( ( P ` 1 ) ^ 2 ) )
24 simpr 
 |-  ( ( ( ph /\ x e. ( 1 ... 6 ) ) /\ x = 1 ) -> x = 1 )
25 24 fveq2d 
 |-  ( ( ( ph /\ x e. ( 1 ... 6 ) ) /\ x = 1 ) -> ( ( veronese ` P ) ` x ) = ( ( veronese ` P ) ` 1 ) )
26 24 fveq2d 
 |-  ( ( ( ph /\ x e. ( 1 ... 6 ) ) /\ x = 1 ) -> ( ( k e. ( 1 ... 6 ) |-> if ( k = 1 , ( ( P ` 1 ) ^ 2 ) , if ( k = 2 , ( ( P ` 2 ) ^ 2 ) , if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , ( ( P ` 3 ) x. ( P ` 1 ) ) ) ) ) ) ) ) ` x ) = ( ( k e. ( 1 ... 6 ) |-> if ( k = 1 , ( ( P ` 1 ) ^ 2 ) , if ( k = 2 , ( ( P ` 2 ) ^ 2 ) , if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , ( ( P ` 3 ) x. ( P ` 1 ) ) ) ) ) ) ) ) ` 1 ) )
27 1nn 
 |-  1 e. NN
28 6nn 
 |-  6 e. NN
29 1re 
 |-  1 e. RR
30 6re 
 |-  6 e. RR
31 1lt6 
 |-  1 < 6
32 29 30 31 ltleii 
 |-  1 <_ 6
33 elfz1b 
 |-  ( 1 e. ( 1 ... 6 ) <-> ( 1 e. NN /\ 6 e. NN /\ 1 <_ 6 ) )
34 27 28 32 33 mpbir3an 
 |-  1 e. ( 1 ... 6 )
35 iftrue 
 |-  ( k = 1 -> if ( k = 1 , ( ( P ` 1 ) ^ 2 ) , if ( k = 2 , ( ( P ` 2 ) ^ 2 ) , if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , ( ( P ` 3 ) x. ( P ` 1 ) ) ) ) ) ) ) = ( ( P ` 1 ) ^ 2 ) )
36 35 19 18 fvmpt3i 
 |-  ( 1 e. ( 1 ... 6 ) -> ( ( k e. ( 1 ... 6 ) |-> if ( k = 1 , ( ( P ` 1 ) ^ 2 ) , if ( k = 2 , ( ( P ` 2 ) ^ 2 ) , if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , ( ( P ` 3 ) x. ( P ` 1 ) ) ) ) ) ) ) ) ` 1 ) = ( ( P ` 1 ) ^ 2 ) )
37 34 36 ax-mp 
 |-  ( ( k e. ( 1 ... 6 ) |-> if ( k = 1 , ( ( P ` 1 ) ^ 2 ) , if ( k = 2 , ( ( P ` 2 ) ^ 2 ) , if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , ( ( P ` 3 ) x. ( P ` 1 ) ) ) ) ) ) ) ) ` 1 ) = ( ( P ` 1 ) ^ 2 )
38 26 37 eqtrdi 
 |-  ( ( ( ph /\ x e. ( 1 ... 6 ) ) /\ x = 1 ) -> ( ( k e. ( 1 ... 6 ) |-> if ( k = 1 , ( ( P ` 1 ) ^ 2 ) , if ( k = 2 , ( ( P ` 2 ) ^ 2 ) , if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , ( ( P ` 3 ) x. ( P ` 1 ) ) ) ) ) ) ) ) ` x ) = ( ( P ` 1 ) ^ 2 ) )
39 23 25 38 3eqtr4d 
 |-  ( ( ( ph /\ x e. ( 1 ... 6 ) ) /\ x = 1 ) -> ( ( veronese ` P ) ` x ) = ( ( k e. ( 1 ... 6 ) |-> if ( k = 1 , ( ( P ` 1 ) ^ 2 ) , if ( k = 2 , ( ( P ` 2 ) ^ 2 ) , if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , ( ( P ` 3 ) x. ( P ` 1 ) ) ) ) ) ) ) ) ` x ) )
40 1 veronesev2lem 
 |-  ( ph -> ( ( veronese ` P ) ` 2 ) = ( ( P ` 2 ) ^ 2 ) )
41 40 ad2antrr 
 |-  ( ( ( ph /\ x e. ( 1 ... 6 ) ) /\ x = 2 ) -> ( ( veronese ` P ) ` 2 ) = ( ( P ` 2 ) ^ 2 ) )
42 simpr 
 |-  ( ( ( ph /\ x e. ( 1 ... 6 ) ) /\ x = 2 ) -> x = 2 )
43 42 fveq2d 
 |-  ( ( ( ph /\ x e. ( 1 ... 6 ) ) /\ x = 2 ) -> ( ( veronese ` P ) ` x ) = ( ( veronese ` P ) ` 2 ) )
44 42 fveq2d 
 |-  ( ( ( ph /\ x e. ( 1 ... 6 ) ) /\ x = 2 ) -> ( ( k e. ( 1 ... 6 ) |-> if ( k = 1 , ( ( P ` 1 ) ^ 2 ) , if ( k = 2 , ( ( P ` 2 ) ^ 2 ) , if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , ( ( P ` 3 ) x. ( P ` 1 ) ) ) ) ) ) ) ) ` x ) = ( ( k e. ( 1 ... 6 ) |-> if ( k = 1 , ( ( P ` 1 ) ^ 2 ) , if ( k = 2 , ( ( P ` 2 ) ^ 2 ) , if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , ( ( P ` 3 ) x. ( P ` 1 ) ) ) ) ) ) ) ) ` 2 ) )
45 2nn 
 |-  2 e. NN
46 2re 
 |-  2 e. RR
47 2lt6 
 |-  2 < 6
48 46 30 47 ltleii 
 |-  2 <_ 6
49 elfz1b 
 |-  ( 2 e. ( 1 ... 6 ) <-> ( 2 e. NN /\ 6 e. NN /\ 2 <_ 6 ) )
50 45 28 48 49 mpbir3an 
 |-  2 e. ( 1 ... 6 )
51 1ne2 
 |-  1 =/= 2
52 51 necomi 
 |-  2 =/= 1
53 neeq1 
 |-  ( k = 2 -> ( k =/= 1 <-> 2 =/= 1 ) )
54 52 53 mpbiri 
 |-  ( k = 2 -> k =/= 1 )
55 54 neneqd 
 |-  ( k = 2 -> -. k = 1 )
56 55 iffalsed 
 |-  ( k = 2 -> if ( k = 1 , ( ( P ` 1 ) ^ 2 ) , if ( k = 2 , ( ( P ` 2 ) ^ 2 ) , if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , ( ( P ` 3 ) x. ( P ` 1 ) ) ) ) ) ) ) = if ( k = 2 , ( ( P ` 2 ) ^ 2 ) , if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , ( ( P ` 3 ) x. ( P ` 1 ) ) ) ) ) ) )
57 iftrue 
 |-  ( k = 2 -> if ( k = 2 , ( ( P ` 2 ) ^ 2 ) , if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , ( ( P ` 3 ) x. ( P ` 1 ) ) ) ) ) ) = ( ( P ` 2 ) ^ 2 ) )
58 56 57 eqtrd 
 |-  ( k = 2 -> if ( k = 1 , ( ( P ` 1 ) ^ 2 ) , if ( k = 2 , ( ( P ` 2 ) ^ 2 ) , if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , ( ( P ` 3 ) x. ( P ` 1 ) ) ) ) ) ) ) = ( ( P ` 2 ) ^ 2 ) )
59 58 19 18 fvmpt3i 
 |-  ( 2 e. ( 1 ... 6 ) -> ( ( k e. ( 1 ... 6 ) |-> if ( k = 1 , ( ( P ` 1 ) ^ 2 ) , if ( k = 2 , ( ( P ` 2 ) ^ 2 ) , if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , ( ( P ` 3 ) x. ( P ` 1 ) ) ) ) ) ) ) ) ` 2 ) = ( ( P ` 2 ) ^ 2 ) )
60 50 59 ax-mp 
 |-  ( ( k e. ( 1 ... 6 ) |-> if ( k = 1 , ( ( P ` 1 ) ^ 2 ) , if ( k = 2 , ( ( P ` 2 ) ^ 2 ) , if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , ( ( P ` 3 ) x. ( P ` 1 ) ) ) ) ) ) ) ) ` 2 ) = ( ( P ` 2 ) ^ 2 )
61 44 60 eqtrdi 
 |-  ( ( ( ph /\ x e. ( 1 ... 6 ) ) /\ x = 2 ) -> ( ( k e. ( 1 ... 6 ) |-> if ( k = 1 , ( ( P ` 1 ) ^ 2 ) , if ( k = 2 , ( ( P ` 2 ) ^ 2 ) , if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , ( ( P ` 3 ) x. ( P ` 1 ) ) ) ) ) ) ) ) ` x ) = ( ( P ` 2 ) ^ 2 ) )
62 41 43 61 3eqtr4d 
 |-  ( ( ( ph /\ x e. ( 1 ... 6 ) ) /\ x = 2 ) -> ( ( veronese ` P ) ` x ) = ( ( k e. ( 1 ... 6 ) |-> if ( k = 1 , ( ( P ` 1 ) ^ 2 ) , if ( k = 2 , ( ( P ` 2 ) ^ 2 ) , if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , ( ( P ` 3 ) x. ( P ` 1 ) ) ) ) ) ) ) ) ` x ) )
63 39 62 jaodan 
 |-  ( ( ( ph /\ x e. ( 1 ... 6 ) ) /\ ( x = 1 \/ x = 2 ) ) -> ( ( veronese ` P ) ` x ) = ( ( k e. ( 1 ... 6 ) |-> if ( k = 1 , ( ( P ` 1 ) ^ 2 ) , if ( k = 2 , ( ( P ` 2 ) ^ 2 ) , if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , ( ( P ` 3 ) x. ( P ` 1 ) ) ) ) ) ) ) ) ` x ) )
64 1 veronesev3lem 
 |-  ( ph -> ( ( veronese ` P ) ` 3 ) = ( ( P ` 3 ) ^ 2 ) )
65 64 ad2antrr 
 |-  ( ( ( ph /\ x e. ( 1 ... 6 ) ) /\ x = 3 ) -> ( ( veronese ` P ) ` 3 ) = ( ( P ` 3 ) ^ 2 ) )
66 simpr 
 |-  ( ( ( ph /\ x e. ( 1 ... 6 ) ) /\ x = 3 ) -> x = 3 )
67 66 fveq2d 
 |-  ( ( ( ph /\ x e. ( 1 ... 6 ) ) /\ x = 3 ) -> ( ( veronese ` P ) ` x ) = ( ( veronese ` P ) ` 3 ) )
68 66 fveq2d 
 |-  ( ( ( ph /\ x e. ( 1 ... 6 ) ) /\ x = 3 ) -> ( ( k e. ( 1 ... 6 ) |-> if ( k = 1 , ( ( P ` 1 ) ^ 2 ) , if ( k = 2 , ( ( P ` 2 ) ^ 2 ) , if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , ( ( P ` 3 ) x. ( P ` 1 ) ) ) ) ) ) ) ) ` x ) = ( ( k e. ( 1 ... 6 ) |-> if ( k = 1 , ( ( P ` 1 ) ^ 2 ) , if ( k = 2 , ( ( P ` 2 ) ^ 2 ) , if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , ( ( P ` 3 ) x. ( P ` 1 ) ) ) ) ) ) ) ) ` 3 ) )
69 3nn 
 |-  3 e. NN
70 3re 
 |-  3 e. RR
71 3lt6 
 |-  3 < 6
72 70 30 71 ltleii 
 |-  3 <_ 6
73 elfz1b 
 |-  ( 3 e. ( 1 ... 6 ) <-> ( 3 e. NN /\ 6 e. NN /\ 3 <_ 6 ) )
74 69 28 72 73 mpbir3an 
 |-  3 e. ( 1 ... 6 )
75 1ne3 
 |-  1 =/= 3
76 75 necomi 
 |-  3 =/= 1
77 neeq1 
 |-  ( k = 3 -> ( k =/= 1 <-> 3 =/= 1 ) )
78 76 77 mpbiri 
 |-  ( k = 3 -> k =/= 1 )
79 78 neneqd 
 |-  ( k = 3 -> -. k = 1 )
80 79 iffalsed 
 |-  ( k = 3 -> if ( k = 1 , ( ( P ` 1 ) ^ 2 ) , if ( k = 2 , ( ( P ` 2 ) ^ 2 ) , if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , ( ( P ` 3 ) x. ( P ` 1 ) ) ) ) ) ) ) = if ( k = 2 , ( ( P ` 2 ) ^ 2 ) , if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , ( ( P ` 3 ) x. ( P ` 1 ) ) ) ) ) ) )
81 2ne3 
 |-  2 =/= 3
82 81 necomi 
 |-  3 =/= 2
83 neeq1 
 |-  ( k = 3 -> ( k =/= 2 <-> 3 =/= 2 ) )
84 82 83 mpbiri 
 |-  ( k = 3 -> k =/= 2 )
85 84 neneqd 
 |-  ( k = 3 -> -. k = 2 )
86 85 iffalsed 
 |-  ( k = 3 -> if ( k = 2 , ( ( P ` 2 ) ^ 2 ) , if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , ( ( P ` 3 ) x. ( P ` 1 ) ) ) ) ) ) = if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , ( ( P ` 3 ) x. ( P ` 1 ) ) ) ) ) )
87 iftrue 
 |-  ( k = 3 -> if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , ( ( P ` 3 ) x. ( P ` 1 ) ) ) ) ) = ( ( P ` 3 ) ^ 2 ) )
88 80 86 87 3eqtrd 
 |-  ( k = 3 -> if ( k = 1 , ( ( P ` 1 ) ^ 2 ) , if ( k = 2 , ( ( P ` 2 ) ^ 2 ) , if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , ( ( P ` 3 ) x. ( P ` 1 ) ) ) ) ) ) ) = ( ( P ` 3 ) ^ 2 ) )
89 88 19 18 fvmpt3i 
 |-  ( 3 e. ( 1 ... 6 ) -> ( ( k e. ( 1 ... 6 ) |-> if ( k = 1 , ( ( P ` 1 ) ^ 2 ) , if ( k = 2 , ( ( P ` 2 ) ^ 2 ) , if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , ( ( P ` 3 ) x. ( P ` 1 ) ) ) ) ) ) ) ) ` 3 ) = ( ( P ` 3 ) ^ 2 ) )
90 74 89 ax-mp 
 |-  ( ( k e. ( 1 ... 6 ) |-> if ( k = 1 , ( ( P ` 1 ) ^ 2 ) , if ( k = 2 , ( ( P ` 2 ) ^ 2 ) , if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , ( ( P ` 3 ) x. ( P ` 1 ) ) ) ) ) ) ) ) ` 3 ) = ( ( P ` 3 ) ^ 2 )
91 68 90 eqtrdi 
 |-  ( ( ( ph /\ x e. ( 1 ... 6 ) ) /\ x = 3 ) -> ( ( k e. ( 1 ... 6 ) |-> if ( k = 1 , ( ( P ` 1 ) ^ 2 ) , if ( k = 2 , ( ( P ` 2 ) ^ 2 ) , if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , ( ( P ` 3 ) x. ( P ` 1 ) ) ) ) ) ) ) ) ` x ) = ( ( P ` 3 ) ^ 2 ) )
92 65 67 91 3eqtr4d 
 |-  ( ( ( ph /\ x e. ( 1 ... 6 ) ) /\ x = 3 ) -> ( ( veronese ` P ) ` x ) = ( ( k e. ( 1 ... 6 ) |-> if ( k = 1 , ( ( P ` 1 ) ^ 2 ) , if ( k = 2 , ( ( P ` 2 ) ^ 2 ) , if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , ( ( P ` 3 ) x. ( P ` 1 ) ) ) ) ) ) ) ) ` x ) )
93 63 92 jaodan 
 |-  ( ( ( ph /\ x e. ( 1 ... 6 ) ) /\ ( ( x = 1 \/ x = 2 ) \/ x = 3 ) ) -> ( ( veronese ` P ) ` x ) = ( ( k e. ( 1 ... 6 ) |-> if ( k = 1 , ( ( P ` 1 ) ^ 2 ) , if ( k = 2 , ( ( P ` 2 ) ^ 2 ) , if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , ( ( P ` 3 ) x. ( P ` 1 ) ) ) ) ) ) ) ) ` x ) )
94 1 veronesev4lem 
 |-  ( ph -> ( ( veronese ` P ) ` 4 ) = ( ( P ` 1 ) x. ( P ` 2 ) ) )
95 94 ad2antrr 
 |-  ( ( ( ph /\ x e. ( 1 ... 6 ) ) /\ x = 4 ) -> ( ( veronese ` P ) ` 4 ) = ( ( P ` 1 ) x. ( P ` 2 ) ) )
96 simpr 
 |-  ( ( ( ph /\ x e. ( 1 ... 6 ) ) /\ x = 4 ) -> x = 4 )
97 96 fveq2d 
 |-  ( ( ( ph /\ x e. ( 1 ... 6 ) ) /\ x = 4 ) -> ( ( veronese ` P ) ` x ) = ( ( veronese ` P ) ` 4 ) )
98 96 fveq2d 
 |-  ( ( ( ph /\ x e. ( 1 ... 6 ) ) /\ x = 4 ) -> ( ( k e. ( 1 ... 6 ) |-> if ( k = 1 , ( ( P ` 1 ) ^ 2 ) , if ( k = 2 , ( ( P ` 2 ) ^ 2 ) , if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , ( ( P ` 3 ) x. ( P ` 1 ) ) ) ) ) ) ) ) ` x ) = ( ( k e. ( 1 ... 6 ) |-> if ( k = 1 , ( ( P ` 1 ) ^ 2 ) , if ( k = 2 , ( ( P ` 2 ) ^ 2 ) , if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , ( ( P ` 3 ) x. ( P ` 1 ) ) ) ) ) ) ) ) ` 4 ) )
99 4nn 
 |-  4 e. NN
100 4re 
 |-  4 e. RR
101 4lt6 
 |-  4 < 6
102 100 30 101 ltleii 
 |-  4 <_ 6
103 elfz1b 
 |-  ( 4 e. ( 1 ... 6 ) <-> ( 4 e. NN /\ 6 e. NN /\ 4 <_ 6 ) )
104 99 28 102 103 mpbir3an 
 |-  4 e. ( 1 ... 6 )
105 1lt4 
 |-  1 < 4
106 29 105 gtneii 
 |-  4 =/= 1
107 neeq1 
 |-  ( k = 4 -> ( k =/= 1 <-> 4 =/= 1 ) )
108 106 107 mpbiri 
 |-  ( k = 4 -> k =/= 1 )
109 108 neneqd 
 |-  ( k = 4 -> -. k = 1 )
110 109 iffalsed 
 |-  ( k = 4 -> if ( k = 1 , ( ( P ` 1 ) ^ 2 ) , if ( k = 2 , ( ( P ` 2 ) ^ 2 ) , if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , ( ( P ` 3 ) x. ( P ` 1 ) ) ) ) ) ) ) = if ( k = 2 , ( ( P ` 2 ) ^ 2 ) , if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , ( ( P ` 3 ) x. ( P ` 1 ) ) ) ) ) ) )
111 2lt4 
 |-  2 < 4
112 46 111 gtneii 
 |-  4 =/= 2
113 neeq1 
 |-  ( k = 4 -> ( k =/= 2 <-> 4 =/= 2 ) )
114 112 113 mpbiri 
 |-  ( k = 4 -> k =/= 2 )
115 114 neneqd 
 |-  ( k = 4 -> -. k = 2 )
116 115 iffalsed 
 |-  ( k = 4 -> if ( k = 2 , ( ( P ` 2 ) ^ 2 ) , if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , ( ( P ` 3 ) x. ( P ` 1 ) ) ) ) ) ) = if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , ( ( P ` 3 ) x. ( P ` 1 ) ) ) ) ) )
117 110 116 eqtrd 
 |-  ( k = 4 -> if ( k = 1 , ( ( P ` 1 ) ^ 2 ) , if ( k = 2 , ( ( P ` 2 ) ^ 2 ) , if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , ( ( P ` 3 ) x. ( P ` 1 ) ) ) ) ) ) ) = if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , ( ( P ` 3 ) x. ( P ` 1 ) ) ) ) ) )
118 3lt4 
 |-  3 < 4
119 70 118 gtneii 
 |-  4 =/= 3
120 neeq1 
 |-  ( k = 4 -> ( k =/= 3 <-> 4 =/= 3 ) )
121 119 120 mpbiri 
 |-  ( k = 4 -> k =/= 3 )
122 121 neneqd 
 |-  ( k = 4 -> -. k = 3 )
123 122 iffalsed 
 |-  ( k = 4 -> if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , ( ( P ` 3 ) x. ( P ` 1 ) ) ) ) ) = if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , ( ( P ` 3 ) x. ( P ` 1 ) ) ) ) )
124 iftrue 
 |-  ( k = 4 -> if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , ( ( P ` 3 ) x. ( P ` 1 ) ) ) ) = ( ( P ` 1 ) x. ( P ` 2 ) ) )
125 117 123 124 3eqtrd 
 |-  ( k = 4 -> if ( k = 1 , ( ( P ` 1 ) ^ 2 ) , if ( k = 2 , ( ( P ` 2 ) ^ 2 ) , if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , ( ( P ` 3 ) x. ( P ` 1 ) ) ) ) ) ) ) = ( ( P ` 1 ) x. ( P ` 2 ) ) )
126 125 19 18 fvmpt3i 
 |-  ( 4 e. ( 1 ... 6 ) -> ( ( k e. ( 1 ... 6 ) |-> if ( k = 1 , ( ( P ` 1 ) ^ 2 ) , if ( k = 2 , ( ( P ` 2 ) ^ 2 ) , if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , ( ( P ` 3 ) x. ( P ` 1 ) ) ) ) ) ) ) ) ` 4 ) = ( ( P ` 1 ) x. ( P ` 2 ) ) )
127 104 126 ax-mp 
 |-  ( ( k e. ( 1 ... 6 ) |-> if ( k = 1 , ( ( P ` 1 ) ^ 2 ) , if ( k = 2 , ( ( P ` 2 ) ^ 2 ) , if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , ( ( P ` 3 ) x. ( P ` 1 ) ) ) ) ) ) ) ) ` 4 ) = ( ( P ` 1 ) x. ( P ` 2 ) )
128 98 127 eqtrdi 
 |-  ( ( ( ph /\ x e. ( 1 ... 6 ) ) /\ x = 4 ) -> ( ( k e. ( 1 ... 6 ) |-> if ( k = 1 , ( ( P ` 1 ) ^ 2 ) , if ( k = 2 , ( ( P ` 2 ) ^ 2 ) , if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , ( ( P ` 3 ) x. ( P ` 1 ) ) ) ) ) ) ) ) ` x ) = ( ( P ` 1 ) x. ( P ` 2 ) ) )
129 95 97 128 3eqtr4d 
 |-  ( ( ( ph /\ x e. ( 1 ... 6 ) ) /\ x = 4 ) -> ( ( veronese ` P ) ` x ) = ( ( k e. ( 1 ... 6 ) |-> if ( k = 1 , ( ( P ` 1 ) ^ 2 ) , if ( k = 2 , ( ( P ` 2 ) ^ 2 ) , if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , ( ( P ` 3 ) x. ( P ` 1 ) ) ) ) ) ) ) ) ` x ) )
130 93 129 jaodan 
 |-  ( ( ( ph /\ x e. ( 1 ... 6 ) ) /\ ( ( ( x = 1 \/ x = 2 ) \/ x = 3 ) \/ x = 4 ) ) -> ( ( veronese ` P ) ` x ) = ( ( k e. ( 1 ... 6 ) |-> if ( k = 1 , ( ( P ` 1 ) ^ 2 ) , if ( k = 2 , ( ( P ` 2 ) ^ 2 ) , if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , ( ( P ` 3 ) x. ( P ` 1 ) ) ) ) ) ) ) ) ` x ) )
131 1 veronesev5lem 
 |-  ( ph -> ( ( veronese ` P ) ` 5 ) = ( ( P ` 2 ) x. ( P ` 3 ) ) )
132 131 ad2antrr 
 |-  ( ( ( ph /\ x e. ( 1 ... 6 ) ) /\ x = 5 ) -> ( ( veronese ` P ) ` 5 ) = ( ( P ` 2 ) x. ( P ` 3 ) ) )
133 simpr 
 |-  ( ( ( ph /\ x e. ( 1 ... 6 ) ) /\ x = 5 ) -> x = 5 )
134 133 fveq2d 
 |-  ( ( ( ph /\ x e. ( 1 ... 6 ) ) /\ x = 5 ) -> ( ( veronese ` P ) ` x ) = ( ( veronese ` P ) ` 5 ) )
135 133 fveq2d 
 |-  ( ( ( ph /\ x e. ( 1 ... 6 ) ) /\ x = 5 ) -> ( ( k e. ( 1 ... 6 ) |-> if ( k = 1 , ( ( P ` 1 ) ^ 2 ) , if ( k = 2 , ( ( P ` 2 ) ^ 2 ) , if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , ( ( P ` 3 ) x. ( P ` 1 ) ) ) ) ) ) ) ) ` x ) = ( ( k e. ( 1 ... 6 ) |-> if ( k = 1 , ( ( P ` 1 ) ^ 2 ) , if ( k = 2 , ( ( P ` 2 ) ^ 2 ) , if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , ( ( P ` 3 ) x. ( P ` 1 ) ) ) ) ) ) ) ) ` 5 ) )
136 5nn 
 |-  5 e. NN
137 5re 
 |-  5 e. RR
138 5lt6 
 |-  5 < 6
139 137 30 138 ltleii 
 |-  5 <_ 6
140 elfz1b 
 |-  ( 5 e. ( 1 ... 6 ) <-> ( 5 e. NN /\ 6 e. NN /\ 5 <_ 6 ) )
141 136 28 139 140 mpbir3an 
 |-  5 e. ( 1 ... 6 )
142 1lt5 
 |-  1 < 5
143 29 142 gtneii 
 |-  5 =/= 1
144 neeq1 
 |-  ( k = 5 -> ( k =/= 1 <-> 5 =/= 1 ) )
145 143 144 mpbiri 
 |-  ( k = 5 -> k =/= 1 )
146 145 neneqd 
 |-  ( k = 5 -> -. k = 1 )
147 146 iffalsed 
 |-  ( k = 5 -> if ( k = 1 , ( ( P ` 1 ) ^ 2 ) , if ( k = 2 , ( ( P ` 2 ) ^ 2 ) , if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , ( ( P ` 3 ) x. ( P ` 1 ) ) ) ) ) ) ) = if ( k = 2 , ( ( P ` 2 ) ^ 2 ) , if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , ( ( P ` 3 ) x. ( P ` 1 ) ) ) ) ) ) )
148 2lt5 
 |-  2 < 5
149 46 148 gtneii 
 |-  5 =/= 2
150 neeq1 
 |-  ( k = 5 -> ( k =/= 2 <-> 5 =/= 2 ) )
151 149 150 mpbiri 
 |-  ( k = 5 -> k =/= 2 )
152 151 neneqd 
 |-  ( k = 5 -> -. k = 2 )
153 152 iffalsed 
 |-  ( k = 5 -> if ( k = 2 , ( ( P ` 2 ) ^ 2 ) , if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , ( ( P ` 3 ) x. ( P ` 1 ) ) ) ) ) ) = if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , ( ( P ` 3 ) x. ( P ` 1 ) ) ) ) ) )
154 3lt5 
 |-  3 < 5
155 70 154 gtneii 
 |-  5 =/= 3
156 neeq1 
 |-  ( k = 5 -> ( k =/= 3 <-> 5 =/= 3 ) )
157 155 156 mpbiri 
 |-  ( k = 5 -> k =/= 3 )
158 157 neneqd 
 |-  ( k = 5 -> -. k = 3 )
159 158 iffalsed 
 |-  ( k = 5 -> if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , ( ( P ` 3 ) x. ( P ` 1 ) ) ) ) ) = if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , ( ( P ` 3 ) x. ( P ` 1 ) ) ) ) )
160 147 153 159 3eqtrd 
 |-  ( k = 5 -> if ( k = 1 , ( ( P ` 1 ) ^ 2 ) , if ( k = 2 , ( ( P ` 2 ) ^ 2 ) , if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , ( ( P ` 3 ) x. ( P ` 1 ) ) ) ) ) ) ) = if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , ( ( P ` 3 ) x. ( P ` 1 ) ) ) ) )
161 4lt5 
 |-  4 < 5
162 100 161 gtneii 
 |-  5 =/= 4
163 neeq1 
 |-  ( k = 5 -> ( k =/= 4 <-> 5 =/= 4 ) )
164 162 163 mpbiri 
 |-  ( k = 5 -> k =/= 4 )
165 164 neneqd 
 |-  ( k = 5 -> -. k = 4 )
166 165 iffalsed 
 |-  ( k = 5 -> if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , ( ( P ` 3 ) x. ( P ` 1 ) ) ) ) = if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , ( ( P ` 3 ) x. ( P ` 1 ) ) ) )
167 iftrue 
 |-  ( k = 5 -> if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , ( ( P ` 3 ) x. ( P ` 1 ) ) ) = ( ( P ` 2 ) x. ( P ` 3 ) ) )
168 160 166 167 3eqtrd 
 |-  ( k = 5 -> if ( k = 1 , ( ( P ` 1 ) ^ 2 ) , if ( k = 2 , ( ( P ` 2 ) ^ 2 ) , if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , ( ( P ` 3 ) x. ( P ` 1 ) ) ) ) ) ) ) = ( ( P ` 2 ) x. ( P ` 3 ) ) )
169 168 19 18 fvmpt3i 
 |-  ( 5 e. ( 1 ... 6 ) -> ( ( k e. ( 1 ... 6 ) |-> if ( k = 1 , ( ( P ` 1 ) ^ 2 ) , if ( k = 2 , ( ( P ` 2 ) ^ 2 ) , if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , ( ( P ` 3 ) x. ( P ` 1 ) ) ) ) ) ) ) ) ` 5 ) = ( ( P ` 2 ) x. ( P ` 3 ) ) )
170 141 169 ax-mp 
 |-  ( ( k e. ( 1 ... 6 ) |-> if ( k = 1 , ( ( P ` 1 ) ^ 2 ) , if ( k = 2 , ( ( P ` 2 ) ^ 2 ) , if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , ( ( P ` 3 ) x. ( P ` 1 ) ) ) ) ) ) ) ) ` 5 ) = ( ( P ` 2 ) x. ( P ` 3 ) )
171 135 170 eqtrdi 
 |-  ( ( ( ph /\ x e. ( 1 ... 6 ) ) /\ x = 5 ) -> ( ( k e. ( 1 ... 6 ) |-> if ( k = 1 , ( ( P ` 1 ) ^ 2 ) , if ( k = 2 , ( ( P ` 2 ) ^ 2 ) , if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , ( ( P ` 3 ) x. ( P ` 1 ) ) ) ) ) ) ) ) ` x ) = ( ( P ` 2 ) x. ( P ` 3 ) ) )
172 132 134 171 3eqtr4d 
 |-  ( ( ( ph /\ x e. ( 1 ... 6 ) ) /\ x = 5 ) -> ( ( veronese ` P ) ` x ) = ( ( k e. ( 1 ... 6 ) |-> if ( k = 1 , ( ( P ` 1 ) ^ 2 ) , if ( k = 2 , ( ( P ` 2 ) ^ 2 ) , if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , ( ( P ` 3 ) x. ( P ` 1 ) ) ) ) ) ) ) ) ` x ) )
173 130 172 jaodan 
 |-  ( ( ( ph /\ x e. ( 1 ... 6 ) ) /\ ( ( ( ( x = 1 \/ x = 2 ) \/ x = 3 ) \/ x = 4 ) \/ x = 5 ) ) -> ( ( veronese ` P ) ` x ) = ( ( k e. ( 1 ... 6 ) |-> if ( k = 1 , ( ( P ` 1 ) ^ 2 ) , if ( k = 2 , ( ( P ` 2 ) ^ 2 ) , if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , ( ( P ` 3 ) x. ( P ` 1 ) ) ) ) ) ) ) ) ` x ) )
174 1 veronesev6lem 
 |-  ( ph -> ( ( veronese ` P ) ` 6 ) = ( ( P ` 3 ) x. ( P ` 1 ) ) )
175 174 ad2antrr 
 |-  ( ( ( ph /\ x e. ( 1 ... 6 ) ) /\ x = 6 ) -> ( ( veronese ` P ) ` 6 ) = ( ( P ` 3 ) x. ( P ` 1 ) ) )
176 simpr 
 |-  ( ( ( ph /\ x e. ( 1 ... 6 ) ) /\ x = 6 ) -> x = 6 )
177 176 fveq2d 
 |-  ( ( ( ph /\ x e. ( 1 ... 6 ) ) /\ x = 6 ) -> ( ( veronese ` P ) ` x ) = ( ( veronese ` P ) ` 6 ) )
178 176 fveq2d 
 |-  ( ( ( ph /\ x e. ( 1 ... 6 ) ) /\ x = 6 ) -> ( ( k e. ( 1 ... 6 ) |-> if ( k = 1 , ( ( P ` 1 ) ^ 2 ) , if ( k = 2 , ( ( P ` 2 ) ^ 2 ) , if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , ( ( P ` 3 ) x. ( P ` 1 ) ) ) ) ) ) ) ) ` x ) = ( ( k e. ( 1 ... 6 ) |-> if ( k = 1 , ( ( P ` 1 ) ^ 2 ) , if ( k = 2 , ( ( P ` 2 ) ^ 2 ) , if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , ( ( P ` 3 ) x. ( P ` 1 ) ) ) ) ) ) ) ) ` 6 ) )
179 30 leidi 
 |-  6 <_ 6
180 elfz1b 
 |-  ( 6 e. ( 1 ... 6 ) <-> ( 6 e. NN /\ 6 e. NN /\ 6 <_ 6 ) )
181 28 28 179 180 mpbir3an 
 |-  6 e. ( 1 ... 6 )
182 29 31 gtneii 
 |-  6 =/= 1
183 neeq1 
 |-  ( k = 6 -> ( k =/= 1 <-> 6 =/= 1 ) )
184 182 183 mpbiri 
 |-  ( k = 6 -> k =/= 1 )
185 184 neneqd 
 |-  ( k = 6 -> -. k = 1 )
186 185 iffalsed 
 |-  ( k = 6 -> if ( k = 1 , ( ( P ` 1 ) ^ 2 ) , if ( k = 2 , ( ( P ` 2 ) ^ 2 ) , if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , ( ( P ` 3 ) x. ( P ` 1 ) ) ) ) ) ) ) = if ( k = 2 , ( ( P ` 2 ) ^ 2 ) , if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , ( ( P ` 3 ) x. ( P ` 1 ) ) ) ) ) ) )
187 46 47 gtneii 
 |-  6 =/= 2
188 neeq1 
 |-  ( k = 6 -> ( k =/= 2 <-> 6 =/= 2 ) )
189 187 188 mpbiri 
 |-  ( k = 6 -> k =/= 2 )
190 189 neneqd 
 |-  ( k = 6 -> -. k = 2 )
191 190 iffalsed 
 |-  ( k = 6 -> if ( k = 2 , ( ( P ` 2 ) ^ 2 ) , if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , ( ( P ` 3 ) x. ( P ` 1 ) ) ) ) ) ) = if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , ( ( P ` 3 ) x. ( P ` 1 ) ) ) ) ) )
192 70 71 gtneii 
 |-  6 =/= 3
193 neeq1 
 |-  ( k = 6 -> ( k =/= 3 <-> 6 =/= 3 ) )
194 192 193 mpbiri 
 |-  ( k = 6 -> k =/= 3 )
195 194 neneqd 
 |-  ( k = 6 -> -. k = 3 )
196 195 iffalsed 
 |-  ( k = 6 -> if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , ( ( P ` 3 ) x. ( P ` 1 ) ) ) ) ) = if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , ( ( P ` 3 ) x. ( P ` 1 ) ) ) ) )
197 186 191 196 3eqtrd 
 |-  ( k = 6 -> if ( k = 1 , ( ( P ` 1 ) ^ 2 ) , if ( k = 2 , ( ( P ` 2 ) ^ 2 ) , if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , ( ( P ` 3 ) x. ( P ` 1 ) ) ) ) ) ) ) = if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , ( ( P ` 3 ) x. ( P ` 1 ) ) ) ) )
198 100 101 gtneii 
 |-  6 =/= 4
199 neeq1 
 |-  ( k = 6 -> ( k =/= 4 <-> 6 =/= 4 ) )
200 198 199 mpbiri 
 |-  ( k = 6 -> k =/= 4 )
201 200 neneqd 
 |-  ( k = 6 -> -. k = 4 )
202 201 iffalsed 
 |-  ( k = 6 -> if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , ( ( P ` 3 ) x. ( P ` 1 ) ) ) ) = if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , ( ( P ` 3 ) x. ( P ` 1 ) ) ) )
203 137 138 gtneii 
 |-  6 =/= 5
204 neeq1 
 |-  ( k = 6 -> ( k =/= 5 <-> 6 =/= 5 ) )
205 203 204 mpbiri 
 |-  ( k = 6 -> k =/= 5 )
206 205 neneqd 
 |-  ( k = 6 -> -. k = 5 )
207 206 iffalsed 
 |-  ( k = 6 -> if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , ( ( P ` 3 ) x. ( P ` 1 ) ) ) = ( ( P ` 3 ) x. ( P ` 1 ) ) )
208 197 202 207 3eqtrd 
 |-  ( k = 6 -> if ( k = 1 , ( ( P ` 1 ) ^ 2 ) , if ( k = 2 , ( ( P ` 2 ) ^ 2 ) , if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , ( ( P ` 3 ) x. ( P ` 1 ) ) ) ) ) ) ) = ( ( P ` 3 ) x. ( P ` 1 ) ) )
209 208 19 18 fvmpt3i 
 |-  ( 6 e. ( 1 ... 6 ) -> ( ( k e. ( 1 ... 6 ) |-> if ( k = 1 , ( ( P ` 1 ) ^ 2 ) , if ( k = 2 , ( ( P ` 2 ) ^ 2 ) , if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , ( ( P ` 3 ) x. ( P ` 1 ) ) ) ) ) ) ) ) ` 6 ) = ( ( P ` 3 ) x. ( P ` 1 ) ) )
210 181 209 ax-mp 
 |-  ( ( k e. ( 1 ... 6 ) |-> if ( k = 1 , ( ( P ` 1 ) ^ 2 ) , if ( k = 2 , ( ( P ` 2 ) ^ 2 ) , if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , ( ( P ` 3 ) x. ( P ` 1 ) ) ) ) ) ) ) ) ` 6 ) = ( ( P ` 3 ) x. ( P ` 1 ) )
211 178 210 eqtrdi 
 |-  ( ( ( ph /\ x e. ( 1 ... 6 ) ) /\ x = 6 ) -> ( ( k e. ( 1 ... 6 ) |-> if ( k = 1 , ( ( P ` 1 ) ^ 2 ) , if ( k = 2 , ( ( P ` 2 ) ^ 2 ) , if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , ( ( P ` 3 ) x. ( P ` 1 ) ) ) ) ) ) ) ) ` x ) = ( ( P ` 3 ) x. ( P ` 1 ) ) )
212 175 177 211 3eqtr4d 
 |-  ( ( ( ph /\ x e. ( 1 ... 6 ) ) /\ x = 6 ) -> ( ( veronese ` P ) ` x ) = ( ( k e. ( 1 ... 6 ) |-> if ( k = 1 , ( ( P ` 1 ) ^ 2 ) , if ( k = 2 , ( ( P ` 2 ) ^ 2 ) , if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , ( ( P ` 3 ) x. ( P ` 1 ) ) ) ) ) ) ) ) ` x ) )
213 simpr 
 |-  ( ( ph /\ x e. ( 1 ... 6 ) ) -> x e. ( 1 ... 6 ) )
214 elnnuz 
 |-  ( 5 e. NN <-> 5 e. ( ZZ>= ` 1 ) )
215 136 214 mpbi 
 |-  5 e. ( ZZ>= ` 1 )
216 elfzp1 
 |-  ( 5 e. ( ZZ>= ` 1 ) -> ( x e. ( 1 ... ( 5 + 1 ) ) <-> ( x e. ( 1 ... 5 ) \/ x = ( 5 + 1 ) ) ) )
217 215 216 ax-mp 
 |-  ( x e. ( 1 ... ( 5 + 1 ) ) <-> ( x e. ( 1 ... 5 ) \/ x = ( 5 + 1 ) ) )
218 5p1e6 
 |-  ( 5 + 1 ) = 6
219 218 oveq2i 
 |-  ( 1 ... ( 5 + 1 ) ) = ( 1 ... 6 )
220 219 eleq2i 
 |-  ( x e. ( 1 ... ( 5 + 1 ) ) <-> x e. ( 1 ... 6 ) )
221 218 eqeq2i 
 |-  ( x = ( 5 + 1 ) <-> x = 6 )
222 221 orbi2i 
 |-  ( ( x e. ( 1 ... 5 ) \/ x = ( 5 + 1 ) ) <-> ( x e. ( 1 ... 5 ) \/ x = 6 ) )
223 217 220 222 3bitr3i 
 |-  ( x e. ( 1 ... 6 ) <-> ( x e. ( 1 ... 5 ) \/ x = 6 ) )
224 elnnuz 
 |-  ( 4 e. NN <-> 4 e. ( ZZ>= ` 1 ) )
225 99 224 mpbi 
 |-  4 e. ( ZZ>= ` 1 )
226 elfzp1 
 |-  ( 4 e. ( ZZ>= ` 1 ) -> ( x e. ( 1 ... ( 4 + 1 ) ) <-> ( x e. ( 1 ... 4 ) \/ x = ( 4 + 1 ) ) ) )
227 225 226 ax-mp 
 |-  ( x e. ( 1 ... ( 4 + 1 ) ) <-> ( x e. ( 1 ... 4 ) \/ x = ( 4 + 1 ) ) )
228 4p1e5 
 |-  ( 4 + 1 ) = 5
229 228 oveq2i 
 |-  ( 1 ... ( 4 + 1 ) ) = ( 1 ... 5 )
230 229 eleq2i 
 |-  ( x e. ( 1 ... ( 4 + 1 ) ) <-> x e. ( 1 ... 5 ) )
231 228 eqeq2i 
 |-  ( x = ( 4 + 1 ) <-> x = 5 )
232 231 orbi2i 
 |-  ( ( x e. ( 1 ... 4 ) \/ x = ( 4 + 1 ) ) <-> ( x e. ( 1 ... 4 ) \/ x = 5 ) )
233 227 230 232 3bitr3i 
 |-  ( x e. ( 1 ... 5 ) <-> ( x e. ( 1 ... 4 ) \/ x = 5 ) )
234 elnnuz 
 |-  ( 3 e. NN <-> 3 e. ( ZZ>= ` 1 ) )
235 69 234 mpbi 
 |-  3 e. ( ZZ>= ` 1 )
236 elfzp1 
 |-  ( 3 e. ( ZZ>= ` 1 ) -> ( x e. ( 1 ... ( 3 + 1 ) ) <-> ( x e. ( 1 ... 3 ) \/ x = ( 3 + 1 ) ) ) )
237 235 236 ax-mp 
 |-  ( x e. ( 1 ... ( 3 + 1 ) ) <-> ( x e. ( 1 ... 3 ) \/ x = ( 3 + 1 ) ) )
238 3p1e4 
 |-  ( 3 + 1 ) = 4
239 238 oveq2i 
 |-  ( 1 ... ( 3 + 1 ) ) = ( 1 ... 4 )
240 239 eleq2i 
 |-  ( x e. ( 1 ... ( 3 + 1 ) ) <-> x e. ( 1 ... 4 ) )
241 238 eqeq2i 
 |-  ( x = ( 3 + 1 ) <-> x = 4 )
242 241 orbi2i 
 |-  ( ( x e. ( 1 ... 3 ) \/ x = ( 3 + 1 ) ) <-> ( x e. ( 1 ... 3 ) \/ x = 4 ) )
243 237 240 242 3bitr3i 
 |-  ( x e. ( 1 ... 4 ) <-> ( x e. ( 1 ... 3 ) \/ x = 4 ) )
244 2eluzge1 
 |-  2 e. ( ZZ>= ` 1 )
245 elfzp1 
 |-  ( 2 e. ( ZZ>= ` 1 ) -> ( x e. ( 1 ... ( 2 + 1 ) ) <-> ( x e. ( 1 ... 2 ) \/ x = ( 2 + 1 ) ) ) )
246 244 245 ax-mp 
 |-  ( x e. ( 1 ... ( 2 + 1 ) ) <-> ( x e. ( 1 ... 2 ) \/ x = ( 2 + 1 ) ) )
247 2p1e3 
 |-  ( 2 + 1 ) = 3
248 247 oveq2i 
 |-  ( 1 ... ( 2 + 1 ) ) = ( 1 ... 3 )
249 248 eleq2i 
 |-  ( x e. ( 1 ... ( 2 + 1 ) ) <-> x e. ( 1 ... 3 ) )
250 247 eqeq2i 
 |-  ( x = ( 2 + 1 ) <-> x = 3 )
251 250 orbi2i 
 |-  ( ( x e. ( 1 ... 2 ) \/ x = ( 2 + 1 ) ) <-> ( x e. ( 1 ... 2 ) \/ x = 3 ) )
252 246 249 251 3bitr3i 
 |-  ( x e. ( 1 ... 3 ) <-> ( x e. ( 1 ... 2 ) \/ x = 3 ) )
253 elnnuz 
 |-  ( 1 e. NN <-> 1 e. ( ZZ>= ` 1 ) )
254 27 253 mpbi 
 |-  1 e. ( ZZ>= ` 1 )
255 elfzp1 
 |-  ( 1 e. ( ZZ>= ` 1 ) -> ( x e. ( 1 ... ( 1 + 1 ) ) <-> ( x e. ( 1 ... 1 ) \/ x = ( 1 + 1 ) ) ) )
256 254 255 ax-mp 
 |-  ( x e. ( 1 ... ( 1 + 1 ) ) <-> ( x e. ( 1 ... 1 ) \/ x = ( 1 + 1 ) ) )
257 1p1e2 
 |-  ( 1 + 1 ) = 2
258 257 oveq2i 
 |-  ( 1 ... ( 1 + 1 ) ) = ( 1 ... 2 )
259 258 eleq2i 
 |-  ( x e. ( 1 ... ( 1 + 1 ) ) <-> x e. ( 1 ... 2 ) )
260 257 eqeq2i 
 |-  ( x = ( 1 + 1 ) <-> x = 2 )
261 260 orbi2i 
 |-  ( ( x e. ( 1 ... 1 ) \/ x = ( 1 + 1 ) ) <-> ( x e. ( 1 ... 1 ) \/ x = 2 ) )
262 256 259 261 3bitr3i 
 |-  ( x e. ( 1 ... 2 ) <-> ( x e. ( 1 ... 1 ) \/ x = 2 ) )
263 elfz1eq 
 |-  ( x e. ( 1 ... 1 ) -> x = 1 )
264 263 orim1i 
 |-  ( ( x e. ( 1 ... 1 ) \/ x = 2 ) -> ( x = 1 \/ x = 2 ) )
265 262 264 sylbi 
 |-  ( x e. ( 1 ... 2 ) -> ( x = 1 \/ x = 2 ) )
266 265 orim1i 
 |-  ( ( x e. ( 1 ... 2 ) \/ x = 3 ) -> ( ( x = 1 \/ x = 2 ) \/ x = 3 ) )
267 252 266 sylbi 
 |-  ( x e. ( 1 ... 3 ) -> ( ( x = 1 \/ x = 2 ) \/ x = 3 ) )
268 267 orim1i 
 |-  ( ( x e. ( 1 ... 3 ) \/ x = 4 ) -> ( ( ( x = 1 \/ x = 2 ) \/ x = 3 ) \/ x = 4 ) )
269 243 268 sylbi 
 |-  ( x e. ( 1 ... 4 ) -> ( ( ( x = 1 \/ x = 2 ) \/ x = 3 ) \/ x = 4 ) )
270 269 orim1i 
 |-  ( ( x e. ( 1 ... 4 ) \/ x = 5 ) -> ( ( ( ( x = 1 \/ x = 2 ) \/ x = 3 ) \/ x = 4 ) \/ x = 5 ) )
271 233 270 sylbi 
 |-  ( x e. ( 1 ... 5 ) -> ( ( ( ( x = 1 \/ x = 2 ) \/ x = 3 ) \/ x = 4 ) \/ x = 5 ) )
272 271 orim1i 
 |-  ( ( x e. ( 1 ... 5 ) \/ x = 6 ) -> ( ( ( ( ( x = 1 \/ x = 2 ) \/ x = 3 ) \/ x = 4 ) \/ x = 5 ) \/ x = 6 ) )
273 223 272 sylbi 
 |-  ( x e. ( 1 ... 6 ) -> ( ( ( ( ( x = 1 \/ x = 2 ) \/ x = 3 ) \/ x = 4 ) \/ x = 5 ) \/ x = 6 ) )
274 213 273 syl 
 |-  ( ( ph /\ x e. ( 1 ... 6 ) ) -> ( ( ( ( ( x = 1 \/ x = 2 ) \/ x = 3 ) \/ x = 4 ) \/ x = 5 ) \/ x = 6 ) )
275 173 212 274 mpjaodan 
 |-  ( ( ph /\ x e. ( 1 ... 6 ) ) -> ( ( veronese ` P ) ` x ) = ( ( k e. ( 1 ... 6 ) |-> if ( k = 1 , ( ( P ` 1 ) ^ 2 ) , if ( k = 2 , ( ( P ` 2 ) ^ 2 ) , if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , ( ( P ` 3 ) x. ( P ` 1 ) ) ) ) ) ) ) ) ` x ) )
276 7 21 275 eqfnfvd 
 |-  ( ph -> ( veronese ` P ) = ( k e. ( 1 ... 6 ) |-> if ( k = 1 , ( ( P ` 1 ) ^ 2 ) , if ( k = 2 , ( ( P ` 2 ) ^ 2 ) , if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , ( ( P ` 3 ) x. ( P ` 1 ) ) ) ) ) ) ) ) )