Metamath Proof Explorer

Theorem veronesev2lem

Description: Lemma for veronesevrowd . Value of the second coordinate of the Veronese map at a point. (Contributed by Jiamin Zhao, 16-Aug-2026)

Ref Expression
Hypothesis veronesevrow.1 ⊢ ( 𝜑 → 𝑃 ∈ ( ℝ ↑m ( 1 ... 3 ) ) )
Assertion veronesev2lem ( 𝜑 → ( ( veronese ‘ 𝑃 ) ‘ 2 ) = ( ( 𝑃 ‘ 2 ) ↑ 2 ) )

Proof

Step Hyp Ref Expression
1 veronesevrow.1 ⊢ ( 𝜑 → 𝑃 ∈ ( ℝ ↑m ( 1 ... 3 ) ) )
2 1 veronesevald ⊢ ( 𝜑 → ( 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 iftrue ⊢ ( 𝑥 = 2 → if ( 𝑥 = 2 , ( ( 𝑃 ‘ 2 ) ↑ 2 ) , 0 ) = ( ( 𝑃 ‘ 2 ) ↑ 2 ) )
4 3 oveq2d ⊢ ( 𝑥 = 2 → ( if ( 𝑥 = 1 , ( ( 𝑃 ‘ 1 ) ↑ 2 ) , 0 ) + if ( 𝑥 = 2 , ( ( 𝑃 ‘ 2 ) ↑ 2 ) , 0 ) ) = ( if ( 𝑥 = 1 , ( ( 𝑃 ‘ 1 ) ↑ 2 ) , 0 ) + ( ( 𝑃 ‘ 2 ) ↑ 2 ) ) )
5 4 oveq1d ⊢ ( 𝑥 = 2 → ( ( if ( 𝑥 = 1 , ( ( 𝑃 ‘ 1 ) ↑ 2 ) , 0 ) + if ( 𝑥 = 2 , ( ( 𝑃 ‘ 2 ) ↑ 2 ) , 0 ) ) + if ( 𝑥 = 3 , ( ( 𝑃 ‘ 3 ) ↑ 2 ) , 0 ) ) = ( ( if ( 𝑥 = 1 , ( ( 𝑃 ‘ 1 ) ↑ 2 ) , 0 ) + ( ( 𝑃 ‘ 2 ) ↑ 2 ) ) + if ( 𝑥 = 3 , ( ( 𝑃 ‘ 3 ) ↑ 2 ) , 0 ) ) )
6 5 oveq1d ⊢ ( 𝑥 = 2 → ( ( ( 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 ) ) ) = ( ( ( if ( 𝑥 = 1 , ( ( 𝑃 ‘ 1 ) ↑ 2 ) , 0 ) + ( ( 𝑃 ‘ 2 ) ↑ 2 ) ) + if ( 𝑥 = 3 , ( ( 𝑃 ‘ 3 ) ↑ 2 ) , 0 ) ) + ( ( if ( 𝑥 = 4 , ( ( 𝑃 ‘ 1 ) · ( 𝑃 ‘ 2 ) ) , 0 ) + if ( 𝑥 = 5 , ( ( 𝑃 ‘ 2 ) · ( 𝑃 ‘ 3 ) ) , 0 ) ) + if ( 𝑥 = 6 , ( ( 𝑃 ‘ 3 ) · ( 𝑃 ‘ 1 ) ) , 0 ) ) ) )
7 1ne2 ⊢ 1 ≠ 2
8 7 necomi ⊢ 2 ≠ 1
9 neeq1 ⊢ ( 𝑥 = 2 → ( 𝑥 ≠ 1 ↔ 2 ≠ 1 ) )
10 8 9 mpbiri ⊢ ( 𝑥 = 2 → 𝑥 ≠ 1 )
11 10 neneqd ⊢ ( 𝑥 = 2 → ¬ 𝑥 = 1 )
12 11 iffalsed ⊢ ( 𝑥 = 2 → if ( 𝑥 = 1 , ( ( 𝑃 ‘ 1 ) ↑ 2 ) , 0 ) = 0 )
13 12 oveq1d ⊢ ( 𝑥 = 2 → ( if ( 𝑥 = 1 , ( ( 𝑃 ‘ 1 ) ↑ 2 ) , 0 ) + ( ( 𝑃 ‘ 2 ) ↑ 2 ) ) = ( 0 + ( ( 𝑃 ‘ 2 ) ↑ 2 ) ) )
14 13 oveq1d ⊢ ( 𝑥 = 2 → ( ( if ( 𝑥 = 1 , ( ( 𝑃 ‘ 1 ) ↑ 2 ) , 0 ) + ( ( 𝑃 ‘ 2 ) ↑ 2 ) ) + if ( 𝑥 = 3 , ( ( 𝑃 ‘ 3 ) ↑ 2 ) , 0 ) ) = ( ( 0 + ( ( 𝑃 ‘ 2 ) ↑ 2 ) ) + if ( 𝑥 = 3 , ( ( 𝑃 ‘ 3 ) ↑ 2 ) , 0 ) ) )
15 14 oveq1d ⊢ ( 𝑥 = 2 → ( ( ( if ( 𝑥 = 1 , ( ( 𝑃 ‘ 1 ) ↑ 2 ) , 0 ) + ( ( 𝑃 ‘ 2 ) ↑ 2 ) ) + if ( 𝑥 = 3 , ( ( 𝑃 ‘ 3 ) ↑ 2 ) , 0 ) ) + ( ( if ( 𝑥 = 4 , ( ( 𝑃 ‘ 1 ) · ( 𝑃 ‘ 2 ) ) , 0 ) + if ( 𝑥 = 5 , ( ( 𝑃 ‘ 2 ) · ( 𝑃 ‘ 3 ) ) , 0 ) ) + if ( 𝑥 = 6 , ( ( 𝑃 ‘ 3 ) · ( 𝑃 ‘ 1 ) ) , 0 ) ) ) = ( ( ( 0 + ( ( 𝑃 ‘ 2 ) ↑ 2 ) ) + if ( 𝑥 = 3 , ( ( 𝑃 ‘ 3 ) ↑ 2 ) , 0 ) ) + ( ( if ( 𝑥 = 4 , ( ( 𝑃 ‘ 1 ) · ( 𝑃 ‘ 2 ) ) , 0 ) + if ( 𝑥 = 5 , ( ( 𝑃 ‘ 2 ) · ( 𝑃 ‘ 3 ) ) , 0 ) ) + if ( 𝑥 = 6 , ( ( 𝑃 ‘ 3 ) · ( 𝑃 ‘ 1 ) ) , 0 ) ) ) )
16 6 15 eqtrd ⊢ ( 𝑥 = 2 → ( ( ( 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 ) ) ) = ( ( ( 0 + ( ( 𝑃 ‘ 2 ) ↑ 2 ) ) + if ( 𝑥 = 3 , ( ( 𝑃 ‘ 3 ) ↑ 2 ) , 0 ) ) + ( ( if ( 𝑥 = 4 , ( ( 𝑃 ‘ 1 ) · ( 𝑃 ‘ 2 ) ) , 0 ) + if ( 𝑥 = 5 , ( ( 𝑃 ‘ 2 ) · ( 𝑃 ‘ 3 ) ) , 0 ) ) + if ( 𝑥 = 6 , ( ( 𝑃 ‘ 3 ) · ( 𝑃 ‘ 1 ) ) , 0 ) ) ) )
17 2ne3 ⊢ 2 ≠ 3
18 neeq1 ⊢ ( 𝑥 = 2 → ( 𝑥 ≠ 3 ↔ 2 ≠ 3 ) )
19 17 18 mpbiri ⊢ ( 𝑥 = 2 → 𝑥 ≠ 3 )
20 19 neneqd ⊢ ( 𝑥 = 2 → ¬ 𝑥 = 3 )
21 20 iffalsed ⊢ ( 𝑥 = 2 → if ( 𝑥 = 3 , ( ( 𝑃 ‘ 3 ) ↑ 2 ) , 0 ) = 0 )
22 21 oveq2d ⊢ ( 𝑥 = 2 → ( ( 0 + ( ( 𝑃 ‘ 2 ) ↑ 2 ) ) + if ( 𝑥 = 3 , ( ( 𝑃 ‘ 3 ) ↑ 2 ) , 0 ) ) = ( ( 0 + ( ( 𝑃 ‘ 2 ) ↑ 2 ) ) + 0 ) )
23 22 oveq1d ⊢ ( 𝑥 = 2 → ( ( ( 0 + ( ( 𝑃 ‘ 2 ) ↑ 2 ) ) + if ( 𝑥 = 3 , ( ( 𝑃 ‘ 3 ) ↑ 2 ) , 0 ) ) + ( ( if ( 𝑥 = 4 , ( ( 𝑃 ‘ 1 ) · ( 𝑃 ‘ 2 ) ) , 0 ) + if ( 𝑥 = 5 , ( ( 𝑃 ‘ 2 ) · ( 𝑃 ‘ 3 ) ) , 0 ) ) + if ( 𝑥 = 6 , ( ( 𝑃 ‘ 3 ) · ( 𝑃 ‘ 1 ) ) , 0 ) ) ) = ( ( ( 0 + ( ( 𝑃 ‘ 2 ) ↑ 2 ) ) + 0 ) + ( ( if ( 𝑥 = 4 , ( ( 𝑃 ‘ 1 ) · ( 𝑃 ‘ 2 ) ) , 0 ) + if ( 𝑥 = 5 , ( ( 𝑃 ‘ 2 ) · ( 𝑃 ‘ 3 ) ) , 0 ) ) + if ( 𝑥 = 6 , ( ( 𝑃 ‘ 3 ) · ( 𝑃 ‘ 1 ) ) , 0 ) ) ) )
24 2re ⊢ 2 ∈ ℝ
25 2lt4 ⊢ 2 < 4
26 24 25 ltneii ⊢ 2 ≠ 4
27 neeq1 ⊢ ( 𝑥 = 2 → ( 𝑥 ≠ 4 ↔ 2 ≠ 4 ) )
28 26 27 mpbiri ⊢ ( 𝑥 = 2 → 𝑥 ≠ 4 )
29 28 neneqd ⊢ ( 𝑥 = 2 → ¬ 𝑥 = 4 )
30 29 iffalsed ⊢ ( 𝑥 = 2 → if ( 𝑥 = 4 , ( ( 𝑃 ‘ 1 ) · ( 𝑃 ‘ 2 ) ) , 0 ) = 0 )
31 30 oveq1d ⊢ ( 𝑥 = 2 → ( if ( 𝑥 = 4 , ( ( 𝑃 ‘ 1 ) · ( 𝑃 ‘ 2 ) ) , 0 ) + if ( 𝑥 = 5 , ( ( 𝑃 ‘ 2 ) · ( 𝑃 ‘ 3 ) ) , 0 ) ) = ( 0 + if ( 𝑥 = 5 , ( ( 𝑃 ‘ 2 ) · ( 𝑃 ‘ 3 ) ) , 0 ) ) )
32 31 oveq1d ⊢ ( 𝑥 = 2 → ( ( if ( 𝑥 = 4 , ( ( 𝑃 ‘ 1 ) · ( 𝑃 ‘ 2 ) ) , 0 ) + if ( 𝑥 = 5 , ( ( 𝑃 ‘ 2 ) · ( 𝑃 ‘ 3 ) ) , 0 ) ) + if ( 𝑥 = 6 , ( ( 𝑃 ‘ 3 ) · ( 𝑃 ‘ 1 ) ) , 0 ) ) = ( ( 0 + if ( 𝑥 = 5 , ( ( 𝑃 ‘ 2 ) · ( 𝑃 ‘ 3 ) ) , 0 ) ) + if ( 𝑥 = 6 , ( ( 𝑃 ‘ 3 ) · ( 𝑃 ‘ 1 ) ) , 0 ) ) )
33 32 oveq2d ⊢ ( 𝑥 = 2 → ( ( ( 0 + ( ( 𝑃 ‘ 2 ) ↑ 2 ) ) + 0 ) + ( ( if ( 𝑥 = 4 , ( ( 𝑃 ‘ 1 ) · ( 𝑃 ‘ 2 ) ) , 0 ) + if ( 𝑥 = 5 , ( ( 𝑃 ‘ 2 ) · ( 𝑃 ‘ 3 ) ) , 0 ) ) + if ( 𝑥 = 6 , ( ( 𝑃 ‘ 3 ) · ( 𝑃 ‘ 1 ) ) , 0 ) ) ) = ( ( ( 0 + ( ( 𝑃 ‘ 2 ) ↑ 2 ) ) + 0 ) + ( ( 0 + if ( 𝑥 = 5 , ( ( 𝑃 ‘ 2 ) · ( 𝑃 ‘ 3 ) ) , 0 ) ) + if ( 𝑥 = 6 , ( ( 𝑃 ‘ 3 ) · ( 𝑃 ‘ 1 ) ) , 0 ) ) ) )
34 16 23 33 3eqtrd ⊢ ( 𝑥 = 2 → ( ( ( 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 ) ) ) = ( ( ( 0 + ( ( 𝑃 ‘ 2 ) ↑ 2 ) ) + 0 ) + ( ( 0 + if ( 𝑥 = 5 , ( ( 𝑃 ‘ 2 ) · ( 𝑃 ‘ 3 ) ) , 0 ) ) + if ( 𝑥 = 6 , ( ( 𝑃 ‘ 3 ) · ( 𝑃 ‘ 1 ) ) , 0 ) ) ) )
35 2lt5 ⊢ 2 < 5
36 24 35 ltneii ⊢ 2 ≠ 5
37 neeq1 ⊢ ( 𝑥 = 2 → ( 𝑥 ≠ 5 ↔ 2 ≠ 5 ) )
38 36 37 mpbiri ⊢ ( 𝑥 = 2 → 𝑥 ≠ 5 )
39 38 neneqd ⊢ ( 𝑥 = 2 → ¬ 𝑥 = 5 )
40 39 iffalsed ⊢ ( 𝑥 = 2 → if ( 𝑥 = 5 , ( ( 𝑃 ‘ 2 ) · ( 𝑃 ‘ 3 ) ) , 0 ) = 0 )
41 40 oveq2d ⊢ ( 𝑥 = 2 → ( 0 + if ( 𝑥 = 5 , ( ( 𝑃 ‘ 2 ) · ( 𝑃 ‘ 3 ) ) , 0 ) ) = ( 0 + 0 ) )
42 41 oveq1d ⊢ ( 𝑥 = 2 → ( ( 0 + if ( 𝑥 = 5 , ( ( 𝑃 ‘ 2 ) · ( 𝑃 ‘ 3 ) ) , 0 ) ) + if ( 𝑥 = 6 , ( ( 𝑃 ‘ 3 ) · ( 𝑃 ‘ 1 ) ) , 0 ) ) = ( ( 0 + 0 ) + if ( 𝑥 = 6 , ( ( 𝑃 ‘ 3 ) · ( 𝑃 ‘ 1 ) ) , 0 ) ) )
43 42 oveq2d ⊢ ( 𝑥 = 2 → ( ( ( 0 + ( ( 𝑃 ‘ 2 ) ↑ 2 ) ) + 0 ) + ( ( 0 + if ( 𝑥 = 5 , ( ( 𝑃 ‘ 2 ) · ( 𝑃 ‘ 3 ) ) , 0 ) ) + if ( 𝑥 = 6 , ( ( 𝑃 ‘ 3 ) · ( 𝑃 ‘ 1 ) ) , 0 ) ) ) = ( ( ( 0 + ( ( 𝑃 ‘ 2 ) ↑ 2 ) ) + 0 ) + ( ( 0 + 0 ) + if ( 𝑥 = 6 , ( ( 𝑃 ‘ 3 ) · ( 𝑃 ‘ 1 ) ) , 0 ) ) ) )
44 2lt6 ⊢ 2 < 6
45 24 44 ltneii ⊢ 2 ≠ 6
46 neeq1 ⊢ ( 𝑥 = 2 → ( 𝑥 ≠ 6 ↔ 2 ≠ 6 ) )
47 45 46 mpbiri ⊢ ( 𝑥 = 2 → 𝑥 ≠ 6 )
48 47 neneqd ⊢ ( 𝑥 = 2 → ¬ 𝑥 = 6 )
49 48 iffalsed ⊢ ( 𝑥 = 2 → if ( 𝑥 = 6 , ( ( 𝑃 ‘ 3 ) · ( 𝑃 ‘ 1 ) ) , 0 ) = 0 )
50 49 oveq2d ⊢ ( 𝑥 = 2 → ( ( 0 + 0 ) + if ( 𝑥 = 6 , ( ( 𝑃 ‘ 3 ) · ( 𝑃 ‘ 1 ) ) , 0 ) ) = ( ( 0 + 0 ) + 0 ) )
51 50 oveq2d ⊢ ( 𝑥 = 2 → ( ( ( 0 + ( ( 𝑃 ‘ 2 ) ↑ 2 ) ) + 0 ) + ( ( 0 + 0 ) + if ( 𝑥 = 6 , ( ( 𝑃 ‘ 3 ) · ( 𝑃 ‘ 1 ) ) , 0 ) ) ) = ( ( ( 0 + ( ( 𝑃 ‘ 2 ) ↑ 2 ) ) + 0 ) + ( ( 0 + 0 ) + 0 ) ) )
52 34 43 51 3eqtrd ⊢ ( 𝑥 = 2 → ( ( ( 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 ) ) ) = ( ( ( 0 + ( ( 𝑃 ‘ 2 ) ↑ 2 ) ) + 0 ) + ( ( 0 + 0 ) + 0 ) ) )
53 52 adantl ⊢ ( ( 𝜑 ∧ 𝑥 = 2 ) → ( ( ( 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 ) ) ) = ( ( ( 0 + ( ( 𝑃 ‘ 2 ) ↑ 2 ) ) + 0 ) + ( ( 0 + 0 ) + 0 ) ) )
54 0red ⊢ ( ( 𝜑 ∧ 𝑥 = 2 ) → 0 ∈ ℝ )
55 1 rr3fv2cld ⊢ ( 𝜑 → ( 𝑃 ‘ 2 ) ∈ ℝ )
56 55 adantr ⊢ ( ( 𝜑 ∧ 𝑥 = 2 ) → ( 𝑃 ‘ 2 ) ∈ ℝ )
57 56 resqcld ⊢ ( ( 𝜑 ∧ 𝑥 = 2 ) → ( ( 𝑃 ‘ 2 ) ↑ 2 ) ∈ ℝ )
58 54 57 readdcld ⊢ ( ( 𝜑 ∧ 𝑥 = 2 ) → ( 0 + ( ( 𝑃 ‘ 2 ) ↑ 2 ) ) ∈ ℝ )
59 58 recnd ⊢ ( ( 𝜑 ∧ 𝑥 = 2 ) → ( 0 + ( ( 𝑃 ‘ 2 ) ↑ 2 ) ) ∈ ℂ )
60 59 addridd ⊢ ( ( 𝜑 ∧ 𝑥 = 2 ) → ( ( 0 + ( ( 𝑃 ‘ 2 ) ↑ 2 ) ) + 0 ) = ( 0 + ( ( 𝑃 ‘ 2 ) ↑ 2 ) ) )
61 60 oveq1d ⊢ ( ( 𝜑 ∧ 𝑥 = 2 ) → ( ( ( 0 + ( ( 𝑃 ‘ 2 ) ↑ 2 ) ) + 0 ) + ( ( 0 + 0 ) + 0 ) ) = ( ( 0 + ( ( 𝑃 ‘ 2 ) ↑ 2 ) ) + ( ( 0 + 0 ) + 0 ) ) )
62 57 recnd ⊢ ( ( 𝜑 ∧ 𝑥 = 2 ) → ( ( 𝑃 ‘ 2 ) ↑ 2 ) ∈ ℂ )
63 62 addlidd ⊢ ( ( 𝜑 ∧ 𝑥 = 2 ) → ( 0 + ( ( 𝑃 ‘ 2 ) ↑ 2 ) ) = ( ( 𝑃 ‘ 2 ) ↑ 2 ) )
64 63 oveq1d ⊢ ( ( 𝜑 ∧ 𝑥 = 2 ) → ( ( 0 + ( ( 𝑃 ‘ 2 ) ↑ 2 ) ) + ( ( 0 + 0 ) + 0 ) ) = ( ( ( 𝑃 ‘ 2 ) ↑ 2 ) + ( ( 0 + 0 ) + 0 ) ) )
65 61 64 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 = 2 ) → ( ( ( 0 + ( ( 𝑃 ‘ 2 ) ↑ 2 ) ) + 0 ) + ( ( 0 + 0 ) + 0 ) ) = ( ( ( 𝑃 ‘ 2 ) ↑ 2 ) + ( ( 0 + 0 ) + 0 ) ) )
66 54 54 readdcld ⊢ ( ( 𝜑 ∧ 𝑥 = 2 ) → ( 0 + 0 ) ∈ ℝ )
67 66 recnd ⊢ ( ( 𝜑 ∧ 𝑥 = 2 ) → ( 0 + 0 ) ∈ ℂ )
68 67 addridd ⊢ ( ( 𝜑 ∧ 𝑥 = 2 ) → ( ( 0 + 0 ) + 0 ) = ( 0 + 0 ) )
69 68 oveq2d ⊢ ( ( 𝜑 ∧ 𝑥 = 2 ) → ( ( ( 𝑃 ‘ 2 ) ↑ 2 ) + ( ( 0 + 0 ) + 0 ) ) = ( ( ( 𝑃 ‘ 2 ) ↑ 2 ) + ( 0 + 0 ) ) )
70 00id ⊢ ( 0 + 0 ) = 0
71 70 a1i ⊢ ( ( 𝜑 ∧ 𝑥 = 2 ) → ( 0 + 0 ) = 0 )
72 71 oveq2d ⊢ ( ( 𝜑 ∧ 𝑥 = 2 ) → ( ( ( 𝑃 ‘ 2 ) ↑ 2 ) + ( 0 + 0 ) ) = ( ( ( 𝑃 ‘ 2 ) ↑ 2 ) + 0 ) )
73 65 69 72 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 = 2 ) → ( ( ( 0 + ( ( 𝑃 ‘ 2 ) ↑ 2 ) ) + 0 ) + ( ( 0 + 0 ) + 0 ) ) = ( ( ( 𝑃 ‘ 2 ) ↑ 2 ) + 0 ) )
74 62 addridd ⊢ ( ( 𝜑 ∧ 𝑥 = 2 ) → ( ( ( 𝑃 ‘ 2 ) ↑ 2 ) + 0 ) = ( ( 𝑃 ‘ 2 ) ↑ 2 ) )
75 53 73 74 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 = 2 ) → ( ( ( 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 ) ) ) = ( ( 𝑃 ‘ 2 ) ↑ 2 ) )
76 1zzd ⊢ ( 𝜑 → 1 ∈ ℤ )
77 6nn ⊢ 6 ∈ ℕ
78 77 nnzi ⊢ 6 ∈ ℤ
79 78 a1i ⊢ ( 𝜑 → 6 ∈ ℤ )
80 2z ⊢ 2 ∈ ℤ
81 80 a1i ⊢ ( 𝜑 → 2 ∈ ℤ )
82 1le2 ⊢ 1 ≤ 2
83 82 a1i ⊢ ( 𝜑 → 1 ≤ 2 )
84 6re ⊢ 6 ∈ ℝ
85 24 84 44 ltleii ⊢ 2 ≤ 6
86 85 a1i ⊢ ( 𝜑 → 2 ≤ 6 )
87 76 79 81 83 86 elfzd ⊢ ( 𝜑 → 2 ∈ ( 1 ... 6 ) )
88 55 resqcld ⊢ ( 𝜑 → ( ( 𝑃 ‘ 2 ) ↑ 2 ) ∈ ℝ )
89 2 75 87 88 fvmptd ⊢ ( 𝜑 → ( ( veronese ‘ 𝑃 ) ‘ 2 ) = ( ( 𝑃 ‘ 2 ) ↑ 2 ) )