Metamath Proof Explorer

Theorem veronesev6lem

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

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

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