Metamath Proof Explorer

Theorem veronesefvcl

Description: Every coordinate of the Veronese map of a real 3-vector is real. (Contributed by Jiamin Zhao, 19-Aug-2026)

Ref Expression
Assertion veronesefvcl 
|- ( ( Q e. ( RR ^m ( 1 ... 3 ) ) /\ K e. ( 1 ... 6 ) ) -> ( ( veronese ` Q ) ` K ) e. RR )

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( Q e. ( RR ^m ( 1 ... 3 ) ) /\ K e. ( 1 ... 6 ) ) -> Q e. ( RR ^m ( 1 ... 3 ) ) )
2 1 veronesevald 
 |-  ( ( Q e. ( RR ^m ( 1 ... 3 ) ) /\ K e. ( 1 ... 6 ) ) -> ( veronese ` Q ) = ( k e. ( 1 ... 6 ) |-> ( ( ( if ( k = 1 , ( ( Q ` 1 ) ^ 2 ) , 0 ) + if ( k = 2 , ( ( Q ` 2 ) ^ 2 ) , 0 ) ) + if ( k = 3 , ( ( Q ` 3 ) ^ 2 ) , 0 ) ) + ( ( if ( k = 4 , ( ( Q ` 1 ) x. ( Q ` 2 ) ) , 0 ) + if ( k = 5 , ( ( Q ` 2 ) x. ( Q ` 3 ) ) , 0 ) ) + if ( k = 6 , ( ( Q ` 3 ) x. ( Q ` 1 ) ) , 0 ) ) ) ) )
3 2 fveq1d 
 |-  ( ( Q e. ( RR ^m ( 1 ... 3 ) ) /\ K e. ( 1 ... 6 ) ) -> ( ( veronese ` Q ) ` K ) = ( ( k e. ( 1 ... 6 ) |-> ( ( ( if ( k = 1 , ( ( Q ` 1 ) ^ 2 ) , 0 ) + if ( k = 2 , ( ( Q ` 2 ) ^ 2 ) , 0 ) ) + if ( k = 3 , ( ( Q ` 3 ) ^ 2 ) , 0 ) ) + ( ( if ( k = 4 , ( ( Q ` 1 ) x. ( Q ` 2 ) ) , 0 ) + if ( k = 5 , ( ( Q ` 2 ) x. ( Q ` 3 ) ) , 0 ) ) + if ( k = 6 , ( ( Q ` 3 ) x. ( Q ` 1 ) ) , 0 ) ) ) ) ` K ) )
4 1 rr3fv1cld 
 |-  ( ( Q e. ( RR ^m ( 1 ... 3 ) ) /\ K e. ( 1 ... 6 ) ) -> ( Q ` 1 ) e. RR )
5 4 resqcld 
 |-  ( ( Q e. ( RR ^m ( 1 ... 3 ) ) /\ K e. ( 1 ... 6 ) ) -> ( ( Q ` 1 ) ^ 2 ) e. RR )
6 5 adantr 
 |-  ( ( ( Q e. ( RR ^m ( 1 ... 3 ) ) /\ K e. ( 1 ... 6 ) ) /\ k e. ( 1 ... 6 ) ) -> ( ( Q ` 1 ) ^ 2 ) e. RR )
7 0red 
 |-  ( ( ( Q e. ( RR ^m ( 1 ... 3 ) ) /\ K e. ( 1 ... 6 ) ) /\ k e. ( 1 ... 6 ) ) -> 0 e. RR )
8 6 7 ifcld 
 |-  ( ( ( Q e. ( RR ^m ( 1 ... 3 ) ) /\ K e. ( 1 ... 6 ) ) /\ k e. ( 1 ... 6 ) ) -> if ( k = 1 , ( ( Q ` 1 ) ^ 2 ) , 0 ) e. RR )
9 1 rr3fv2cld 
 |-  ( ( Q e. ( RR ^m ( 1 ... 3 ) ) /\ K e. ( 1 ... 6 ) ) -> ( Q ` 2 ) e. RR )
10 9 resqcld 
 |-  ( ( Q e. ( RR ^m ( 1 ... 3 ) ) /\ K e. ( 1 ... 6 ) ) -> ( ( Q ` 2 ) ^ 2 ) e. RR )
11 10 adantr 
 |-  ( ( ( Q e. ( RR ^m ( 1 ... 3 ) ) /\ K e. ( 1 ... 6 ) ) /\ k e. ( 1 ... 6 ) ) -> ( ( Q ` 2 ) ^ 2 ) e. RR )
12 11 7 ifcld 
 |-  ( ( ( Q e. ( RR ^m ( 1 ... 3 ) ) /\ K e. ( 1 ... 6 ) ) /\ k e. ( 1 ... 6 ) ) -> if ( k = 2 , ( ( Q ` 2 ) ^ 2 ) , 0 ) e. RR )
13 8 12 readdcld 
 |-  ( ( ( Q e. ( RR ^m ( 1 ... 3 ) ) /\ K e. ( 1 ... 6 ) ) /\ k e. ( 1 ... 6 ) ) -> ( if ( k = 1 , ( ( Q ` 1 ) ^ 2 ) , 0 ) + if ( k = 2 , ( ( Q ` 2 ) ^ 2 ) , 0 ) ) e. RR )
14 1 rr3fv3cld 
 |-  ( ( Q e. ( RR ^m ( 1 ... 3 ) ) /\ K e. ( 1 ... 6 ) ) -> ( Q ` 3 ) e. RR )
15 14 resqcld 
 |-  ( ( Q e. ( RR ^m ( 1 ... 3 ) ) /\ K e. ( 1 ... 6 ) ) -> ( ( Q ` 3 ) ^ 2 ) e. RR )
16 15 adantr 
 |-  ( ( ( Q e. ( RR ^m ( 1 ... 3 ) ) /\ K e. ( 1 ... 6 ) ) /\ k e. ( 1 ... 6 ) ) -> ( ( Q ` 3 ) ^ 2 ) e. RR )
17 16 7 ifcld 
 |-  ( ( ( Q e. ( RR ^m ( 1 ... 3 ) ) /\ K e. ( 1 ... 6 ) ) /\ k e. ( 1 ... 6 ) ) -> if ( k = 3 , ( ( Q ` 3 ) ^ 2 ) , 0 ) e. RR )
18 13 17 readdcld 
 |-  ( ( ( Q e. ( RR ^m ( 1 ... 3 ) ) /\ K e. ( 1 ... 6 ) ) /\ k e. ( 1 ... 6 ) ) -> ( ( if ( k = 1 , ( ( Q ` 1 ) ^ 2 ) , 0 ) + if ( k = 2 , ( ( Q ` 2 ) ^ 2 ) , 0 ) ) + if ( k = 3 , ( ( Q ` 3 ) ^ 2 ) , 0 ) ) e. RR )
19 4 9 remulcld 
 |-  ( ( Q e. ( RR ^m ( 1 ... 3 ) ) /\ K e. ( 1 ... 6 ) ) -> ( ( Q ` 1 ) x. ( Q ` 2 ) ) e. RR )
20 19 adantr 
 |-  ( ( ( Q e. ( RR ^m ( 1 ... 3 ) ) /\ K e. ( 1 ... 6 ) ) /\ k e. ( 1 ... 6 ) ) -> ( ( Q ` 1 ) x. ( Q ` 2 ) ) e. RR )
21 20 7 ifcld 
 |-  ( ( ( Q e. ( RR ^m ( 1 ... 3 ) ) /\ K e. ( 1 ... 6 ) ) /\ k e. ( 1 ... 6 ) ) -> if ( k = 4 , ( ( Q ` 1 ) x. ( Q ` 2 ) ) , 0 ) e. RR )
22 9 14 remulcld 
 |-  ( ( Q e. ( RR ^m ( 1 ... 3 ) ) /\ K e. ( 1 ... 6 ) ) -> ( ( Q ` 2 ) x. ( Q ` 3 ) ) e. RR )
23 22 adantr 
 |-  ( ( ( Q e. ( RR ^m ( 1 ... 3 ) ) /\ K e. ( 1 ... 6 ) ) /\ k e. ( 1 ... 6 ) ) -> ( ( Q ` 2 ) x. ( Q ` 3 ) ) e. RR )
24 23 7 ifcld 
 |-  ( ( ( Q e. ( RR ^m ( 1 ... 3 ) ) /\ K e. ( 1 ... 6 ) ) /\ k e. ( 1 ... 6 ) ) -> if ( k = 5 , ( ( Q ` 2 ) x. ( Q ` 3 ) ) , 0 ) e. RR )
25 21 24 readdcld 
 |-  ( ( ( Q e. ( RR ^m ( 1 ... 3 ) ) /\ K e. ( 1 ... 6 ) ) /\ k e. ( 1 ... 6 ) ) -> ( if ( k = 4 , ( ( Q ` 1 ) x. ( Q ` 2 ) ) , 0 ) + if ( k = 5 , ( ( Q ` 2 ) x. ( Q ` 3 ) ) , 0 ) ) e. RR )
26 14 4 remulcld 
 |-  ( ( Q e. ( RR ^m ( 1 ... 3 ) ) /\ K e. ( 1 ... 6 ) ) -> ( ( Q ` 3 ) x. ( Q ` 1 ) ) e. RR )
27 26 adantr 
 |-  ( ( ( Q e. ( RR ^m ( 1 ... 3 ) ) /\ K e. ( 1 ... 6 ) ) /\ k e. ( 1 ... 6 ) ) -> ( ( Q ` 3 ) x. ( Q ` 1 ) ) e. RR )
28 27 7 ifcld 
 |-  ( ( ( Q e. ( RR ^m ( 1 ... 3 ) ) /\ K e. ( 1 ... 6 ) ) /\ k e. ( 1 ... 6 ) ) -> if ( k = 6 , ( ( Q ` 3 ) x. ( Q ` 1 ) ) , 0 ) e. RR )
29 25 28 readdcld 
 |-  ( ( ( Q e. ( RR ^m ( 1 ... 3 ) ) /\ K e. ( 1 ... 6 ) ) /\ k e. ( 1 ... 6 ) ) -> ( ( if ( k = 4 , ( ( Q ` 1 ) x. ( Q ` 2 ) ) , 0 ) + if ( k = 5 , ( ( Q ` 2 ) x. ( Q ` 3 ) ) , 0 ) ) + if ( k = 6 , ( ( Q ` 3 ) x. ( Q ` 1 ) ) , 0 ) ) e. RR )
30 18 29 readdcld 
 |-  ( ( ( Q e. ( RR ^m ( 1 ... 3 ) ) /\ K e. ( 1 ... 6 ) ) /\ k e. ( 1 ... 6 ) ) -> ( ( ( if ( k = 1 , ( ( Q ` 1 ) ^ 2 ) , 0 ) + if ( k = 2 , ( ( Q ` 2 ) ^ 2 ) , 0 ) ) + if ( k = 3 , ( ( Q ` 3 ) ^ 2 ) , 0 ) ) + ( ( if ( k = 4 , ( ( Q ` 1 ) x. ( Q ` 2 ) ) , 0 ) + if ( k = 5 , ( ( Q ` 2 ) x. ( Q ` 3 ) ) , 0 ) ) + if ( k = 6 , ( ( Q ` 3 ) x. ( Q ` 1 ) ) , 0 ) ) ) e. RR )
31 30 fmpttd 
 |-  ( ( Q e. ( RR ^m ( 1 ... 3 ) ) /\ K e. ( 1 ... 6 ) ) -> ( k e. ( 1 ... 6 ) |-> ( ( ( if ( k = 1 , ( ( Q ` 1 ) ^ 2 ) , 0 ) + if ( k = 2 , ( ( Q ` 2 ) ^ 2 ) , 0 ) ) + if ( k = 3 , ( ( Q ` 3 ) ^ 2 ) , 0 ) ) + ( ( if ( k = 4 , ( ( Q ` 1 ) x. ( Q ` 2 ) ) , 0 ) + if ( k = 5 , ( ( Q ` 2 ) x. ( Q ` 3 ) ) , 0 ) ) + if ( k = 6 , ( ( Q ` 3 ) x. ( Q ` 1 ) ) , 0 ) ) ) ) : ( 1 ... 6 ) --> RR )
32 simpr 
 |-  ( ( Q e. ( RR ^m ( 1 ... 3 ) ) /\ K e. ( 1 ... 6 ) ) -> K e. ( 1 ... 6 ) )
33 31 32 ffvelcdmd 
 |-  ( ( Q e. ( RR ^m ( 1 ... 3 ) ) /\ K e. ( 1 ... 6 ) ) -> ( ( k e. ( 1 ... 6 ) |-> ( ( ( if ( k = 1 , ( ( Q ` 1 ) ^ 2 ) , 0 ) + if ( k = 2 , ( ( Q ` 2 ) ^ 2 ) , 0 ) ) + if ( k = 3 , ( ( Q ` 3 ) ^ 2 ) , 0 ) ) + ( ( if ( k = 4 , ( ( Q ` 1 ) x. ( Q ` 2 ) ) , 0 ) + if ( k = 5 , ( ( Q ` 2 ) x. ( Q ` 3 ) ) , 0 ) ) + if ( k = 6 , ( ( Q ` 3 ) x. ( Q ` 1 ) ) , 0 ) ) ) ) ` K ) e. RR )
34 3 33 eqeltrd 
 |-  ( ( Q e. ( RR ^m ( 1 ... 3 ) ) /\ K e. ( 1 ... 6 ) ) -> ( ( veronese ` Q ) ` K ) e. RR )