Metamath Proof Explorer

Theorem veronesev4lem

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

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