Metamath Proof Explorer

Theorem veronesev3lem

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

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