Metamath Proof Explorer

Theorem veronesev1lem

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

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