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 ( ( 𝑄 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝐾 ∈ ( 1 ... 6 ) ) → ( ( veronese ‘ 𝑄 ) ‘ 𝐾 ) ∈ ℝ )

Proof

Step Hyp Ref Expression
1 simpl ⊢ ( ( 𝑄 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝐾 ∈ ( 1 ... 6 ) ) → 𝑄 ∈ ( ℝ ↑m ( 1 ... 3 ) ) )
2 1 veronesevald ⊢ ( ( 𝑄 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝐾 ∈ ( 1 ... 6 ) ) → ( veronese ‘ 𝑄 ) = ( 𝑘 ∈ ( 1 ... 6 ) ↦ ( ( ( if ( 𝑘 = 1 , ( ( 𝑄 ‘ 1 ) ↑ 2 ) , 0 ) + if ( 𝑘 = 2 , ( ( 𝑄 ‘ 2 ) ↑ 2 ) , 0 ) ) + if ( 𝑘 = 3 , ( ( 𝑄 ‘ 3 ) ↑ 2 ) , 0 ) ) + ( ( if ( 𝑘 = 4 , ( ( 𝑄 ‘ 1 ) · ( 𝑄 ‘ 2 ) ) , 0 ) + if ( 𝑘 = 5 , ( ( 𝑄 ‘ 2 ) · ( 𝑄 ‘ 3 ) ) , 0 ) ) + if ( 𝑘 = 6 , ( ( 𝑄 ‘ 3 ) · ( 𝑄 ‘ 1 ) ) , 0 ) ) ) ) )
3 2 fveq1d ⊢ ( ( 𝑄 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝐾 ∈ ( 1 ... 6 ) ) → ( ( veronese ‘ 𝑄 ) ‘ 𝐾 ) = ( ( 𝑘 ∈ ( 1 ... 6 ) ↦ ( ( ( if ( 𝑘 = 1 , ( ( 𝑄 ‘ 1 ) ↑ 2 ) , 0 ) + if ( 𝑘 = 2 , ( ( 𝑄 ‘ 2 ) ↑ 2 ) , 0 ) ) + if ( 𝑘 = 3 , ( ( 𝑄 ‘ 3 ) ↑ 2 ) , 0 ) ) + ( ( if ( 𝑘 = 4 , ( ( 𝑄 ‘ 1 ) · ( 𝑄 ‘ 2 ) ) , 0 ) + if ( 𝑘 = 5 , ( ( 𝑄 ‘ 2 ) · ( 𝑄 ‘ 3 ) ) , 0 ) ) + if ( 𝑘 = 6 , ( ( 𝑄 ‘ 3 ) · ( 𝑄 ‘ 1 ) ) , 0 ) ) ) ) ‘ 𝐾 ) )
4 1 rr3fv1cld ⊢ ( ( 𝑄 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝐾 ∈ ( 1 ... 6 ) ) → ( 𝑄 ‘ 1 ) ∈ ℝ )
5 4 resqcld ⊢ ( ( 𝑄 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝐾 ∈ ( 1 ... 6 ) ) → ( ( 𝑄 ‘ 1 ) ↑ 2 ) ∈ ℝ )
6 5 adantr ⊢ ( ( ( 𝑄 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝐾 ∈ ( 1 ... 6 ) ) ∧ 𝑘 ∈ ( 1 ... 6 ) ) → ( ( 𝑄 ‘ 1 ) ↑ 2 ) ∈ ℝ )
7 0red ⊢ ( ( ( 𝑄 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝐾 ∈ ( 1 ... 6 ) ) ∧ 𝑘 ∈ ( 1 ... 6 ) ) → 0 ∈ ℝ )
8 6 7 ifcld ⊢ ( ( ( 𝑄 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝐾 ∈ ( 1 ... 6 ) ) ∧ 𝑘 ∈ ( 1 ... 6 ) ) → if ( 𝑘 = 1 , ( ( 𝑄 ‘ 1 ) ↑ 2 ) , 0 ) ∈ ℝ )
9 1 rr3fv2cld ⊢ ( ( 𝑄 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝐾 ∈ ( 1 ... 6 ) ) → ( 𝑄 ‘ 2 ) ∈ ℝ )
10 9 resqcld ⊢ ( ( 𝑄 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝐾 ∈ ( 1 ... 6 ) ) → ( ( 𝑄 ‘ 2 ) ↑ 2 ) ∈ ℝ )
11 10 adantr ⊢ ( ( ( 𝑄 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝐾 ∈ ( 1 ... 6 ) ) ∧ 𝑘 ∈ ( 1 ... 6 ) ) → ( ( 𝑄 ‘ 2 ) ↑ 2 ) ∈ ℝ )
12 11 7 ifcld ⊢ ( ( ( 𝑄 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝐾 ∈ ( 1 ... 6 ) ) ∧ 𝑘 ∈ ( 1 ... 6 ) ) → if ( 𝑘 = 2 , ( ( 𝑄 ‘ 2 ) ↑ 2 ) , 0 ) ∈ ℝ )
13 8 12 readdcld ⊢ ( ( ( 𝑄 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝐾 ∈ ( 1 ... 6 ) ) ∧ 𝑘 ∈ ( 1 ... 6 ) ) → ( if ( 𝑘 = 1 , ( ( 𝑄 ‘ 1 ) ↑ 2 ) , 0 ) + if ( 𝑘 = 2 , ( ( 𝑄 ‘ 2 ) ↑ 2 ) , 0 ) ) ∈ ℝ )
14 1 rr3fv3cld ⊢ ( ( 𝑄 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝐾 ∈ ( 1 ... 6 ) ) → ( 𝑄 ‘ 3 ) ∈ ℝ )
15 14 resqcld ⊢ ( ( 𝑄 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝐾 ∈ ( 1 ... 6 ) ) → ( ( 𝑄 ‘ 3 ) ↑ 2 ) ∈ ℝ )
16 15 adantr ⊢ ( ( ( 𝑄 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝐾 ∈ ( 1 ... 6 ) ) ∧ 𝑘 ∈ ( 1 ... 6 ) ) → ( ( 𝑄 ‘ 3 ) ↑ 2 ) ∈ ℝ )
17 16 7 ifcld ⊢ ( ( ( 𝑄 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝐾 ∈ ( 1 ... 6 ) ) ∧ 𝑘 ∈ ( 1 ... 6 ) ) → if ( 𝑘 = 3 , ( ( 𝑄 ‘ 3 ) ↑ 2 ) , 0 ) ∈ ℝ )
18 13 17 readdcld ⊢ ( ( ( 𝑄 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝐾 ∈ ( 1 ... 6 ) ) ∧ 𝑘 ∈ ( 1 ... 6 ) ) → ( ( if ( 𝑘 = 1 , ( ( 𝑄 ‘ 1 ) ↑ 2 ) , 0 ) + if ( 𝑘 = 2 , ( ( 𝑄 ‘ 2 ) ↑ 2 ) , 0 ) ) + if ( 𝑘 = 3 , ( ( 𝑄 ‘ 3 ) ↑ 2 ) , 0 ) ) ∈ ℝ )
19 4 9 remulcld ⊢ ( ( 𝑄 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝐾 ∈ ( 1 ... 6 ) ) → ( ( 𝑄 ‘ 1 ) · ( 𝑄 ‘ 2 ) ) ∈ ℝ )
20 19 adantr ⊢ ( ( ( 𝑄 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝐾 ∈ ( 1 ... 6 ) ) ∧ 𝑘 ∈ ( 1 ... 6 ) ) → ( ( 𝑄 ‘ 1 ) · ( 𝑄 ‘ 2 ) ) ∈ ℝ )
21 20 7 ifcld ⊢ ( ( ( 𝑄 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝐾 ∈ ( 1 ... 6 ) ) ∧ 𝑘 ∈ ( 1 ... 6 ) ) → if ( 𝑘 = 4 , ( ( 𝑄 ‘ 1 ) · ( 𝑄 ‘ 2 ) ) , 0 ) ∈ ℝ )
22 9 14 remulcld ⊢ ( ( 𝑄 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝐾 ∈ ( 1 ... 6 ) ) → ( ( 𝑄 ‘ 2 ) · ( 𝑄 ‘ 3 ) ) ∈ ℝ )
23 22 adantr ⊢ ( ( ( 𝑄 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝐾 ∈ ( 1 ... 6 ) ) ∧ 𝑘 ∈ ( 1 ... 6 ) ) → ( ( 𝑄 ‘ 2 ) · ( 𝑄 ‘ 3 ) ) ∈ ℝ )
24 23 7 ifcld ⊢ ( ( ( 𝑄 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝐾 ∈ ( 1 ... 6 ) ) ∧ 𝑘 ∈ ( 1 ... 6 ) ) → if ( 𝑘 = 5 , ( ( 𝑄 ‘ 2 ) · ( 𝑄 ‘ 3 ) ) , 0 ) ∈ ℝ )
25 21 24 readdcld ⊢ ( ( ( 𝑄 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝐾 ∈ ( 1 ... 6 ) ) ∧ 𝑘 ∈ ( 1 ... 6 ) ) → ( if ( 𝑘 = 4 , ( ( 𝑄 ‘ 1 ) · ( 𝑄 ‘ 2 ) ) , 0 ) + if ( 𝑘 = 5 , ( ( 𝑄 ‘ 2 ) · ( 𝑄 ‘ 3 ) ) , 0 ) ) ∈ ℝ )
26 14 4 remulcld ⊢ ( ( 𝑄 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝐾 ∈ ( 1 ... 6 ) ) → ( ( 𝑄 ‘ 3 ) · ( 𝑄 ‘ 1 ) ) ∈ ℝ )
27 26 adantr ⊢ ( ( ( 𝑄 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝐾 ∈ ( 1 ... 6 ) ) ∧ 𝑘 ∈ ( 1 ... 6 ) ) → ( ( 𝑄 ‘ 3 ) · ( 𝑄 ‘ 1 ) ) ∈ ℝ )
28 27 7 ifcld ⊢ ( ( ( 𝑄 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝐾 ∈ ( 1 ... 6 ) ) ∧ 𝑘 ∈ ( 1 ... 6 ) ) → if ( 𝑘 = 6 , ( ( 𝑄 ‘ 3 ) · ( 𝑄 ‘ 1 ) ) , 0 ) ∈ ℝ )
29 25 28 readdcld ⊢ ( ( ( 𝑄 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝐾 ∈ ( 1 ... 6 ) ) ∧ 𝑘 ∈ ( 1 ... 6 ) ) → ( ( if ( 𝑘 = 4 , ( ( 𝑄 ‘ 1 ) · ( 𝑄 ‘ 2 ) ) , 0 ) + if ( 𝑘 = 5 , ( ( 𝑄 ‘ 2 ) · ( 𝑄 ‘ 3 ) ) , 0 ) ) + if ( 𝑘 = 6 , ( ( 𝑄 ‘ 3 ) · ( 𝑄 ‘ 1 ) ) , 0 ) ) ∈ ℝ )
30 18 29 readdcld ⊢ ( ( ( 𝑄 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝐾 ∈ ( 1 ... 6 ) ) ∧ 𝑘 ∈ ( 1 ... 6 ) ) → ( ( ( if ( 𝑘 = 1 , ( ( 𝑄 ‘ 1 ) ↑ 2 ) , 0 ) + if ( 𝑘 = 2 , ( ( 𝑄 ‘ 2 ) ↑ 2 ) , 0 ) ) + if ( 𝑘 = 3 , ( ( 𝑄 ‘ 3 ) ↑ 2 ) , 0 ) ) + ( ( if ( 𝑘 = 4 , ( ( 𝑄 ‘ 1 ) · ( 𝑄 ‘ 2 ) ) , 0 ) + if ( 𝑘 = 5 , ( ( 𝑄 ‘ 2 ) · ( 𝑄 ‘ 3 ) ) , 0 ) ) + if ( 𝑘 = 6 , ( ( 𝑄 ‘ 3 ) · ( 𝑄 ‘ 1 ) ) , 0 ) ) ) ∈ ℝ )
31 30 fmpttd ⊢ ( ( 𝑄 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝐾 ∈ ( 1 ... 6 ) ) → ( 𝑘 ∈ ( 1 ... 6 ) ↦ ( ( ( if ( 𝑘 = 1 , ( ( 𝑄 ‘ 1 ) ↑ 2 ) , 0 ) + if ( 𝑘 = 2 , ( ( 𝑄 ‘ 2 ) ↑ 2 ) , 0 ) ) + if ( 𝑘 = 3 , ( ( 𝑄 ‘ 3 ) ↑ 2 ) , 0 ) ) + ( ( if ( 𝑘 = 4 , ( ( 𝑄 ‘ 1 ) · ( 𝑄 ‘ 2 ) ) , 0 ) + if ( 𝑘 = 5 , ( ( 𝑄 ‘ 2 ) · ( 𝑄 ‘ 3 ) ) , 0 ) ) + if ( 𝑘 = 6 , ( ( 𝑄 ‘ 3 ) · ( 𝑄 ‘ 1 ) ) , 0 ) ) ) ) : ( 1 ... 6 ) ⟶ ℝ )
32 simpr ⊢ ( ( 𝑄 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝐾 ∈ ( 1 ... 6 ) ) → 𝐾 ∈ ( 1 ... 6 ) )
33 31 32 ffvelcdmd ⊢ ( ( 𝑄 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝐾 ∈ ( 1 ... 6 ) ) → ( ( 𝑘 ∈ ( 1 ... 6 ) ↦ ( ( ( if ( 𝑘 = 1 , ( ( 𝑄 ‘ 1 ) ↑ 2 ) , 0 ) + if ( 𝑘 = 2 , ( ( 𝑄 ‘ 2 ) ↑ 2 ) , 0 ) ) + if ( 𝑘 = 3 , ( ( 𝑄 ‘ 3 ) ↑ 2 ) , 0 ) ) + ( ( if ( 𝑘 = 4 , ( ( 𝑄 ‘ 1 ) · ( 𝑄 ‘ 2 ) ) , 0 ) + if ( 𝑘 = 5 , ( ( 𝑄 ‘ 2 ) · ( 𝑄 ‘ 3 ) ) , 0 ) ) + if ( 𝑘 = 6 , ( ( 𝑄 ‘ 3 ) · ( 𝑄 ‘ 1 ) ) , 0 ) ) ) ) ‘ 𝐾 ) ∈ ℝ )
34 3 33 eqeltrd ⊢ ( ( 𝑄 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝐾 ∈ ( 1 ... 6 ) ) → ( ( veronese ‘ 𝑄 ) ‘ 𝐾 ) ∈ ℝ )