veronesevrowd - Mathbox for Jiamin Zhao

	Mathbox for Jiamin Zhao		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > veronesevrowd		Structured version Visualization version GIF version

Theorem veronesevrowd 51257

Description: The Veronese map at a point, expressed explicitly as a piecewise maps-to function on the six coordinates. (Contributed by Jiamin Zhao, 17-Aug-2026.)

**Hypothesis**
Ref	Expression
veronesevrow.1	⊢ (𝜑 → 𝑃 ∈ (ℝ ↑_m (1...3)))

**Assertion**
Ref	Expression
veronesevrowd	⊢ (𝜑 → (veronese‘𝑃) = (𝑘 ∈ (1...6) ↦ if(𝑘 = 1, ((𝑃‘1)↑2), if(𝑘 = 2, ((𝑃‘2)↑2), if(𝑘 = 3, ((𝑃‘3)↑2), if(𝑘 = 4, ((𝑃‘1) · (𝑃‘2)), if(𝑘 = 5, ((𝑃‘2) · (𝑃‘3)), ((𝑃‘3) · (𝑃‘1)))))))))

Distinct variable group: 𝑃,𝑘 Allowed substitution hint: 𝜑(𝑘)

Proof of Theorem veronesevrowd Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		ovex 7473	. . . 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))) ∈ V
2		eqid 2763	. . . 4 ⊢ (𝑘 ∈ (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)))) = (𝑘 ∈ (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	1, 2	fnmpti 6701	. . 3 ⊢ (𝑘 ∈ (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)))) Fn (1...6)
4		veronesevrow.1	. . . . 5 ⊢ (𝜑 → 𝑃 ∈ (ℝ ↑_m (1...3)))
5	4	veronesevald 51249	. . . 4 ⊢ (𝜑 → (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)))))
6	5	fneq1d 6651	. . 3 ⊢ (𝜑 → ((veronese‘𝑃) Fn (1...6) ↔ (𝑘 ∈ (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)))) Fn (1...6)))
7	3, 6	mpbiri 261	. 2 ⊢ (𝜑 → (veronese‘𝑃) Fn (1...6))
8		ovex 7473	. . . . 5 ⊢ ((𝑃‘1)↑2) ∈ V
9		ovex 7473	. . . . . 6 ⊢ ((𝑃‘2)↑2) ∈ V
10		ovex 7473	. . . . . . 7 ⊢ ((𝑃‘3)↑2) ∈ V
11		ovex 7473	. . . . . . . 8 ⊢ ((𝑃‘1) · (𝑃‘2)) ∈ V
12		ovex 7473	. . . . . . . . 9 ⊢ ((𝑃‘2) · (𝑃‘3)) ∈ V
13		ovex 7473	. . . . . . . . 9 ⊢ ((𝑃‘3) · (𝑃‘1)) ∈ V
14	12, 13	ifex 4536	. . . . . . . 8 ⊢ if(𝑘 = 5, ((𝑃‘2) · (𝑃‘3)), ((𝑃‘3) · (𝑃‘1))) ∈ V
15	11, 14	ifex 4536	. . . . . . 7 ⊢ if(𝑘 = 4, ((𝑃‘1) · (𝑃‘2)), if(𝑘 = 5, ((𝑃‘2) · (𝑃‘3)), ((𝑃‘3) · (𝑃‘1)))) ∈ V
16	10, 15	ifex 4536	. . . . . 6 ⊢ if(𝑘 = 3, ((𝑃‘3)↑2), if(𝑘 = 4, ((𝑃‘1) · (𝑃‘2)), if(𝑘 = 5, ((𝑃‘2) · (𝑃‘3)), ((𝑃‘3) · (𝑃‘1))))) ∈ V
17	9, 16	ifex 4536	. . . . 5 ⊢ if(𝑘 = 2, ((𝑃‘2)↑2), if(𝑘 = 3, ((𝑃‘3)↑2), if(𝑘 = 4, ((𝑃‘1) · (𝑃‘2)), if(𝑘 = 5, ((𝑃‘2) · (𝑃‘3)), ((𝑃‘3) · (𝑃‘1)))))) ∈ V
18	8, 17	ifex 4536	. . . 4 ⊢ if(𝑘 = 1, ((𝑃‘1)↑2), if(𝑘 = 2, ((𝑃‘2)↑2), if(𝑘 = 3, ((𝑃‘3)↑2), if(𝑘 = 4, ((𝑃‘1) · (𝑃‘2)), if(𝑘 = 5, ((𝑃‘2) · (𝑃‘3)), ((𝑃‘3) · (𝑃‘1))))))) ∈ V
19		eqid 2763	. . . 4 ⊢ (𝑘 ∈ (1...6) ↦ if(𝑘 = 1, ((𝑃‘1)↑2), if(𝑘 = 2, ((𝑃‘2)↑2), if(𝑘 = 3, ((𝑃‘3)↑2), if(𝑘 = 4, ((𝑃‘1) · (𝑃‘2)), if(𝑘 = 5, ((𝑃‘2) · (𝑃‘3)), ((𝑃‘3) · (𝑃‘1)))))))) = (𝑘 ∈ (1...6) ↦ if(𝑘 = 1, ((𝑃‘1)↑2), if(𝑘 = 2, ((𝑃‘2)↑2), if(𝑘 = 3, ((𝑃‘3)↑2), if(𝑘 = 4, ((𝑃‘1) · (𝑃‘2)), if(𝑘 = 5, ((𝑃‘2) · (𝑃‘3)), ((𝑃‘3) · (𝑃‘1))))))))
20	18, 19	fnmpti 6701	. . 3 ⊢ (𝑘 ∈ (1...6) ↦ if(𝑘 = 1, ((𝑃‘1)↑2), if(𝑘 = 2, ((𝑃‘2)↑2), if(𝑘 = 3, ((𝑃‘3)↑2), if(𝑘 = 4, ((𝑃‘1) · (𝑃‘2)), if(𝑘 = 5, ((𝑃‘2) · (𝑃‘3)), ((𝑃‘3) · (𝑃‘1)))))))) Fn (1...6)
21	20	a1i 11	. 2 ⊢ (𝜑 → (𝑘 ∈ (1...6) ↦ if(𝑘 = 1, ((𝑃‘1)↑2), if(𝑘 = 2, ((𝑃‘2)↑2), if(𝑘 = 3, ((𝑃‘3)↑2), if(𝑘 = 4, ((𝑃‘1) · (𝑃‘2)), if(𝑘 = 5, ((𝑃‘2) · (𝑃‘3)), ((𝑃‘3) · (𝑃‘1)))))))) Fn (1...6))
22	4	veronesev1lem 51251	. . . . . . . . 9 ⊢ (𝜑 → ((veronese‘𝑃)‘1) = ((𝑃‘1)↑2))
23	22	ad2antrr 739	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...6)) ∧ 𝑥 = 1) → ((veronese‘𝑃)‘1) = ((𝑃‘1)↑2))
24		simpr 490	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...6)) ∧ 𝑥 = 1) → 𝑥 = 1)
25	24	fveq2d 6909	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...6)) ∧ 𝑥 = 1) → ((veronese‘𝑃)‘𝑥) = ((veronese‘𝑃)‘1))
26	24	fveq2d 6909	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...6)) ∧ 𝑥 = 1) → ((𝑘 ∈ (1...6) ↦ if(𝑘 = 1, ((𝑃‘1)↑2), if(𝑘 = 2, ((𝑃‘2)↑2), if(𝑘 = 3, ((𝑃‘3)↑2), if(𝑘 = 4, ((𝑃‘1) · (𝑃‘2)), if(𝑘 = 5, ((𝑃‘2) · (𝑃‘3)), ((𝑃‘3) · (𝑃‘1))))))))‘𝑥) = ((𝑘 ∈ (1...6) ↦ if(𝑘 = 1, ((𝑃‘1)↑2), if(𝑘 = 2, ((𝑃‘2)↑2), if(𝑘 = 3, ((𝑃‘3)↑2), if(𝑘 = 4, ((𝑃‘1) · (𝑃‘2)), if(𝑘 = 5, ((𝑃‘2) · (𝑃‘3)), ((𝑃‘3) · (𝑃‘1))))))))‘1))
27		1nn 12370	. . . . . . . . . . 11 ⊢ 1 ∈ ℕ
28		6nn 12456	. . . . . . . . . . 11 ⊢ 6 ∈ ℕ
29		1re 11332	. . . . . . . . . . . 12 ⊢ 1 ∈ ℝ
30		6re 12457	. . . . . . . . . . . 12 ⊢ 6 ∈ ℝ
31		1lt6 12554	. . . . . . . . . . . 12 ⊢ 1 < 6
32	29, 30, 31	ltleii 11457	. . . . . . . . . . 11 ⊢ 1 ≤ 6
33		elfz1b 13751	. . . . . . . . . . 11 ⊢ (1 ∈ (1...6) ↔ (1 ∈ ℕ ∧ 6 ∈ ℕ ∧ 1 ≤ 6))
34	27, 28, 32, 33	mpbir3an 1360	. . . . . . . . . 10 ⊢ 1 ∈ (1...6)
35		iftrue 4491	. . . . . . . . . . 11 ⊢ (𝑘 = 1 → if(𝑘 = 1, ((𝑃‘1)↑2), if(𝑘 = 2, ((𝑃‘2)↑2), if(𝑘 = 3, ((𝑃‘3)↑2), if(𝑘 = 4, ((𝑃‘1) · (𝑃‘2)), if(𝑘 = 5, ((𝑃‘2) · (𝑃‘3)), ((𝑃‘3) · (𝑃‘1))))))) = ((𝑃‘1)↑2))
36	35, 19, 18	fvmpt3i 7019	. . . . . . . . . 10 ⊢ (1 ∈ (1...6) → ((𝑘 ∈ (1...6) ↦ if(𝑘 = 1, ((𝑃‘1)↑2), if(𝑘 = 2, ((𝑃‘2)↑2), if(𝑘 = 3, ((𝑃‘3)↑2), if(𝑘 = 4, ((𝑃‘1) · (𝑃‘2)), if(𝑘 = 5, ((𝑃‘2) · (𝑃‘3)), ((𝑃‘3) · (𝑃‘1))))))))‘1) = ((𝑃‘1)↑2))
37	34, 36	ax-mp 5	. . . . . . . . 9 ⊢ ((𝑘 ∈ (1...6) ↦ if(𝑘 = 1, ((𝑃‘1)↑2), if(𝑘 = 2, ((𝑃‘2)↑2), if(𝑘 = 3, ((𝑃‘3)↑2), if(𝑘 = 4, ((𝑃‘1) · (𝑃‘2)), if(𝑘 = 5, ((𝑃‘2) · (𝑃‘3)), ((𝑃‘3) · (𝑃‘1))))))))‘1) = ((𝑃‘1)↑2)
38	26, 37	eqtrdi 2814	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...6)) ∧ 𝑥 = 1) → ((𝑘 ∈ (1...6) ↦ if(𝑘 = 1, ((𝑃‘1)↑2), if(𝑘 = 2, ((𝑃‘2)↑2), if(𝑘 = 3, ((𝑃‘3)↑2), if(𝑘 = 4, ((𝑃‘1) · (𝑃‘2)), if(𝑘 = 5, ((𝑃‘2) · (𝑃‘3)), ((𝑃‘3) · (𝑃‘1))))))))‘𝑥) = ((𝑃‘1)↑2))
39	23, 25, 38	3eqtr4d 2808	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...6)) ∧ 𝑥 = 1) → ((veronese‘𝑃)‘𝑥) = ((𝑘 ∈ (1...6) ↦ if(𝑘 = 1, ((𝑃‘1)↑2), if(𝑘 = 2, ((𝑃‘2)↑2), if(𝑘 = 3, ((𝑃‘3)↑2), if(𝑘 = 4, ((𝑃‘1) · (𝑃‘2)), if(𝑘 = 5, ((𝑃‘2) · (𝑃‘3)), ((𝑃‘3) · (𝑃‘1))))))))‘𝑥))
40	4	veronesev2lem 51252	. . . . . . . . 9 ⊢ (𝜑 → ((veronese‘𝑃)‘2) = ((𝑃‘2)↑2))
41	40	ad2antrr 739	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...6)) ∧ 𝑥 = 2) → ((veronese‘𝑃)‘2) = ((𝑃‘2)↑2))
42		simpr 490	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...6)) ∧ 𝑥 = 2) → 𝑥 = 2)
43	42	fveq2d 6909	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...6)) ∧ 𝑥 = 2) → ((veronese‘𝑃)‘𝑥) = ((veronese‘𝑃)‘2))
44	42	fveq2d 6909	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...6)) ∧ 𝑥 = 2) → ((𝑘 ∈ (1...6) ↦ if(𝑘 = 1, ((𝑃‘1)↑2), if(𝑘 = 2, ((𝑃‘2)↑2), if(𝑘 = 3, ((𝑃‘3)↑2), if(𝑘 = 4, ((𝑃‘1) · (𝑃‘2)), if(𝑘 = 5, ((𝑃‘2) · (𝑃‘3)), ((𝑃‘3) · (𝑃‘1))))))))‘𝑥) = ((𝑘 ∈ (1...6) ↦ if(𝑘 = 1, ((𝑃‘1)↑2), if(𝑘 = 2, ((𝑃‘2)↑2), if(𝑘 = 3, ((𝑃‘3)↑2), if(𝑘 = 4, ((𝑃‘1) · (𝑃‘2)), if(𝑘 = 5, ((𝑃‘2) · (𝑃‘3)), ((𝑃‘3) · (𝑃‘1))))))))‘2))
45		2nn 12440	. . . . . . . . . . 11 ⊢ 2 ∈ ℕ
46		2re 12441	. . . . . . . . . . . 12 ⊢ 2 ∈ ℝ
47		2lt6 12553	. . . . . . . . . . . 12 ⊢ 2 < 6
48	46, 30, 47	ltleii 11457	. . . . . . . . . . 11 ⊢ 2 ≤ 6
49		elfz1b 13751	. . . . . . . . . . 11 ⊢ (2 ∈ (1...6) ↔ (2 ∈ ℕ ∧ 6 ∈ ℕ ∧ 2 ≤ 6))
50	45, 28, 48, 49	mpbir3an 1360	. . . . . . . . . 10 ⊢ 2 ∈ (1...6)
51		1ne2 12577	. . . . . . . . . . . . . . . 16 ⊢ 1 ≠ 2
52	51	necomi 3013	. . . . . . . . . . . . . . 15 ⊢ 2 ≠ 1
53		neeq1 3021	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 2 → (𝑘 ≠ 1 ↔ 2 ≠ 1))
54	52, 53	mpbiri 261	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 2 → 𝑘 ≠ 1)
55	54	neneqd 2964	. . . . . . . . . . . . 13 ⊢ (𝑘 = 2 → ¬ 𝑘 = 1)
56	55	iffalsed 4496	. . . . . . . . . . . 12 ⊢ (𝑘 = 2 → if(𝑘 = 1, ((𝑃‘1)↑2), if(𝑘 = 2, ((𝑃‘2)↑2), if(𝑘 = 3, ((𝑃‘3)↑2), if(𝑘 = 4, ((𝑃‘1) · (𝑃‘2)), if(𝑘 = 5, ((𝑃‘2) · (𝑃‘3)), ((𝑃‘3) · (𝑃‘1))))))) = if(𝑘 = 2, ((𝑃‘2)↑2), if(𝑘 = 3, ((𝑃‘3)↑2), if(𝑘 = 4, ((𝑃‘1) · (𝑃‘2)), if(𝑘 = 5, ((𝑃‘2) · (𝑃‘3)), ((𝑃‘3) · (𝑃‘1)))))))
57		iftrue 4491	. . . . . . . . . . . 12 ⊢ (𝑘 = 2 → if(𝑘 = 2, ((𝑃‘2)↑2), if(𝑘 = 3, ((𝑃‘3)↑2), if(𝑘 = 4, ((𝑃‘1) · (𝑃‘2)), if(𝑘 = 5, ((𝑃‘2) · (𝑃‘3)), ((𝑃‘3) · (𝑃‘1)))))) = ((𝑃‘2)↑2))
58	56, 57	eqtrd 2798	. . . . . . . . . . 11 ⊢ (𝑘 = 2 → if(𝑘 = 1, ((𝑃‘1)↑2), if(𝑘 = 2, ((𝑃‘2)↑2), if(𝑘 = 3, ((𝑃‘3)↑2), if(𝑘 = 4, ((𝑃‘1) · (𝑃‘2)), if(𝑘 = 5, ((𝑃‘2) · (𝑃‘3)), ((𝑃‘3) · (𝑃‘1))))))) = ((𝑃‘2)↑2))
59	58, 19, 18	fvmpt3i 7019	. . . . . . . . . 10 ⊢ (2 ∈ (1...6) → ((𝑘 ∈ (1...6) ↦ if(𝑘 = 1, ((𝑃‘1)↑2), if(𝑘 = 2, ((𝑃‘2)↑2), if(𝑘 = 3, ((𝑃‘3)↑2), if(𝑘 = 4, ((𝑃‘1) · (𝑃‘2)), if(𝑘 = 5, ((𝑃‘2) · (𝑃‘3)), ((𝑃‘3) · (𝑃‘1))))))))‘2) = ((𝑃‘2)↑2))
60	50, 59	ax-mp 5	. . . . . . . . 9 ⊢ ((𝑘 ∈ (1...6) ↦ if(𝑘 = 1, ((𝑃‘1)↑2), if(𝑘 = 2, ((𝑃‘2)↑2), if(𝑘 = 3, ((𝑃‘3)↑2), if(𝑘 = 4, ((𝑃‘1) · (𝑃‘2)), if(𝑘 = 5, ((𝑃‘2) · (𝑃‘3)), ((𝑃‘3) · (𝑃‘1))))))))‘2) = ((𝑃‘2)↑2)
61	44, 60	eqtrdi 2814	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...6)) ∧ 𝑥 = 2) → ((𝑘 ∈ (1...6) ↦ if(𝑘 = 1, ((𝑃‘1)↑2), if(𝑘 = 2, ((𝑃‘2)↑2), if(𝑘 = 3, ((𝑃‘3)↑2), if(𝑘 = 4, ((𝑃‘1) · (𝑃‘2)), if(𝑘 = 5, ((𝑃‘2) · (𝑃‘3)), ((𝑃‘3) · (𝑃‘1))))))))‘𝑥) = ((𝑃‘2)↑2))
62	41, 43, 61	3eqtr4d 2808	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...6)) ∧ 𝑥 = 2) → ((veronese‘𝑃)‘𝑥) = ((𝑘 ∈ (1...6) ↦ if(𝑘 = 1, ((𝑃‘1)↑2), if(𝑘 = 2, ((𝑃‘2)↑2), if(𝑘 = 3, ((𝑃‘3)↑2), if(𝑘 = 4, ((𝑃‘1) · (𝑃‘2)), if(𝑘 = 5, ((𝑃‘2) · (𝑃‘3)), ((𝑃‘3) · (𝑃‘1))))))))‘𝑥))
63	39, 62	jaodan 972	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...6)) ∧ (𝑥 = 1 ∨ 𝑥 = 2)) → ((veronese‘𝑃)‘𝑥) = ((𝑘 ∈ (1...6) ↦ if(𝑘 = 1, ((𝑃‘1)↑2), if(𝑘 = 2, ((𝑃‘2)↑2), if(𝑘 = 3, ((𝑃‘3)↑2), if(𝑘 = 4, ((𝑃‘1) · (𝑃‘2)), if(𝑘 = 5, ((𝑃‘2) · (𝑃‘3)), ((𝑃‘3) · (𝑃‘1))))))))‘𝑥))
64	4	veronesev3lem 51253	. . . . . . . 8 ⊢ (𝜑 → ((veronese‘𝑃)‘3) = ((𝑃‘3)↑2))
65	64	ad2antrr 739	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...6)) ∧ 𝑥 = 3) → ((veronese‘𝑃)‘3) = ((𝑃‘3)↑2))
66		simpr 490	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...6)) ∧ 𝑥 = 3) → 𝑥 = 3)
67	66	fveq2d 6909	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...6)) ∧ 𝑥 = 3) → ((veronese‘𝑃)‘𝑥) = ((veronese‘𝑃)‘3))
68	66	fveq2d 6909	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...6)) ∧ 𝑥 = 3) → ((𝑘 ∈ (1...6) ↦ if(𝑘 = 1, ((𝑃‘1)↑2), if(𝑘 = 2, ((𝑃‘2)↑2), if(𝑘 = 3, ((𝑃‘3)↑2), if(𝑘 = 4, ((𝑃‘1) · (𝑃‘2)), if(𝑘 = 5, ((𝑃‘2) · (𝑃‘3)), ((𝑃‘3) · (𝑃‘1))))))))‘𝑥) = ((𝑘 ∈ (1...6) ↦ if(𝑘 = 1, ((𝑃‘1)↑2), if(𝑘 = 2, ((𝑃‘2)↑2), if(𝑘 = 3, ((𝑃‘3)↑2), if(𝑘 = 4, ((𝑃‘1) · (𝑃‘2)), if(𝑘 = 5, ((𝑃‘2) · (𝑃‘3)), ((𝑃‘3) · (𝑃‘1))))))))‘3))
69		3nn 12446	. . . . . . . . . 10 ⊢ 3 ∈ ℕ
70		3re 12447	. . . . . . . . . . 11 ⊢ 3 ∈ ℝ
71		3lt6 12552	. . . . . . . . . . 11 ⊢ 3 < 6
72	70, 30, 71	ltleii 11457	. . . . . . . . . 10 ⊢ 3 ≤ 6
73		elfz1b 13751	. . . . . . . . . 10 ⊢ (3 ∈ (1...6) ↔ (3 ∈ ℕ ∧ 6 ∈ ℕ ∧ 3 ≤ 6))
74	69, 28, 72, 73	mpbir3an 1360	. . . . . . . . 9 ⊢ 3 ∈ (1...6)
75		1ne3 51219	. . . . . . . . . . . . . . 15 ⊢ 1 ≠ 3
76	75	necomi 3013	. . . . . . . . . . . . . 14 ⊢ 3 ≠ 1
77		neeq1 3021	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 3 → (𝑘 ≠ 1 ↔ 3 ≠ 1))
78	76, 77	mpbiri 261	. . . . . . . . . . . . 13 ⊢ (𝑘 = 3 → 𝑘 ≠ 1)
79	78	neneqd 2964	. . . . . . . . . . . 12 ⊢ (𝑘 = 3 → ¬ 𝑘 = 1)
80	79	iffalsed 4496	. . . . . . . . . . 11 ⊢ (𝑘 = 3 → if(𝑘 = 1, ((𝑃‘1)↑2), if(𝑘 = 2, ((𝑃‘2)↑2), if(𝑘 = 3, ((𝑃‘3)↑2), if(𝑘 = 4, ((𝑃‘1) · (𝑃‘2)), if(𝑘 = 5, ((𝑃‘2) · (𝑃‘3)), ((𝑃‘3) · (𝑃‘1))))))) = if(𝑘 = 2, ((𝑃‘2)↑2), if(𝑘 = 3, ((𝑃‘3)↑2), if(𝑘 = 4, ((𝑃‘1) · (𝑃‘2)), if(𝑘 = 5, ((𝑃‘2) · (𝑃‘3)), ((𝑃‘3) · (𝑃‘1)))))))
81		2ne3 51220	. . . . . . . . . . . . . . 15 ⊢ 2 ≠ 3
82	81	necomi 3013	. . . . . . . . . . . . . 14 ⊢ 3 ≠ 2
83		neeq1 3021	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 3 → (𝑘 ≠ 2 ↔ 3 ≠ 2))
84	82, 83	mpbiri 261	. . . . . . . . . . . . 13 ⊢ (𝑘 = 3 → 𝑘 ≠ 2)
85	84	neneqd 2964	. . . . . . . . . . . 12 ⊢ (𝑘 = 3 → ¬ 𝑘 = 2)
86	85	iffalsed 4496	. . . . . . . . . . 11 ⊢ (𝑘 = 3 → if(𝑘 = 2, ((𝑃‘2)↑2), if(𝑘 = 3, ((𝑃‘3)↑2), if(𝑘 = 4, ((𝑃‘1) · (𝑃‘2)), if(𝑘 = 5, ((𝑃‘2) · (𝑃‘3)), ((𝑃‘3) · (𝑃‘1)))))) = if(𝑘 = 3, ((𝑃‘3)↑2), if(𝑘 = 4, ((𝑃‘1) · (𝑃‘2)), if(𝑘 = 5, ((𝑃‘2) · (𝑃‘3)), ((𝑃‘3) · (𝑃‘1))))))
87		iftrue 4491	. . . . . . . . . . 11 ⊢ (𝑘 = 3 → if(𝑘 = 3, ((𝑃‘3)↑2), if(𝑘 = 4, ((𝑃‘1) · (𝑃‘2)), if(𝑘 = 5, ((𝑃‘2) · (𝑃‘3)), ((𝑃‘3) · (𝑃‘1))))) = ((𝑃‘3)↑2))
88	80, 86, 87	3eqtrd 2802	. . . . . . . . . 10 ⊢ (𝑘 = 3 → if(𝑘 = 1, ((𝑃‘1)↑2), if(𝑘 = 2, ((𝑃‘2)↑2), if(𝑘 = 3, ((𝑃‘3)↑2), if(𝑘 = 4, ((𝑃‘1) · (𝑃‘2)), if(𝑘 = 5, ((𝑃‘2) · (𝑃‘3)), ((𝑃‘3) · (𝑃‘1))))))) = ((𝑃‘3)↑2))
89	88, 19, 18	fvmpt3i 7019	. . . . . . . . 9 ⊢ (3 ∈ (1...6) → ((𝑘 ∈ (1...6) ↦ if(𝑘 = 1, ((𝑃‘1)↑2), if(𝑘 = 2, ((𝑃‘2)↑2), if(𝑘 = 3, ((𝑃‘3)↑2), if(𝑘 = 4, ((𝑃‘1) · (𝑃‘2)), if(𝑘 = 5, ((𝑃‘2) · (𝑃‘3)), ((𝑃‘3) · (𝑃‘1))))))))‘3) = ((𝑃‘3)↑2))
90	74, 89	ax-mp 5	. . . . . . . 8 ⊢ ((𝑘 ∈ (1...6) ↦ if(𝑘 = 1, ((𝑃‘1)↑2), if(𝑘 = 2, ((𝑃‘2)↑2), if(𝑘 = 3, ((𝑃‘3)↑2), if(𝑘 = 4, ((𝑃‘1) · (𝑃‘2)), if(𝑘 = 5, ((𝑃‘2) · (𝑃‘3)), ((𝑃‘3) · (𝑃‘1))))))))‘3) = ((𝑃‘3)↑2)
91	68, 90	eqtrdi 2814	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...6)) ∧ 𝑥 = 3) → ((𝑘 ∈ (1...6) ↦ if(𝑘 = 1, ((𝑃‘1)↑2), if(𝑘 = 2, ((𝑃‘2)↑2), if(𝑘 = 3, ((𝑃‘3)↑2), if(𝑘 = 4, ((𝑃‘1) · (𝑃‘2)), if(𝑘 = 5, ((𝑃‘2) · (𝑃‘3)), ((𝑃‘3) · (𝑃‘1))))))))‘𝑥) = ((𝑃‘3)↑2))
92	65, 67, 91	3eqtr4d 2808	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...6)) ∧ 𝑥 = 3) → ((veronese‘𝑃)‘𝑥) = ((𝑘 ∈ (1...6) ↦ if(𝑘 = 1, ((𝑃‘1)↑2), if(𝑘 = 2, ((𝑃‘2)↑2), if(𝑘 = 3, ((𝑃‘3)↑2), if(𝑘 = 4, ((𝑃‘1) · (𝑃‘2)), if(𝑘 = 5, ((𝑃‘2) · (𝑃‘3)), ((𝑃‘3) · (𝑃‘1))))))))‘𝑥))
93	63, 92	jaodan 972	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...6)) ∧ ((𝑥 = 1 ∨ 𝑥 = 2) ∨ 𝑥 = 3)) → ((veronese‘𝑃)‘𝑥) = ((𝑘 ∈ (1...6) ↦ if(𝑘 = 1, ((𝑃‘1)↑2), if(𝑘 = 2, ((𝑃‘2)↑2), if(𝑘 = 3, ((𝑃‘3)↑2), if(𝑘 = 4, ((𝑃‘1) · (𝑃‘2)), if(𝑘 = 5, ((𝑃‘2) · (𝑃‘3)), ((𝑃‘3) · (𝑃‘1))))))))‘𝑥))
94	4	veronesev4lem 51254	. . . . . . 7 ⊢ (𝜑 → ((veronese‘𝑃)‘4) = ((𝑃‘1) · (𝑃‘2)))
95	94	ad2antrr 739	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...6)) ∧ 𝑥 = 4) → ((veronese‘𝑃)‘4) = ((𝑃‘1) · (𝑃‘2)))
96		simpr 490	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...6)) ∧ 𝑥 = 4) → 𝑥 = 4)
97	96	fveq2d 6909	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...6)) ∧ 𝑥 = 4) → ((veronese‘𝑃)‘𝑥) = ((veronese‘𝑃)‘4))
98	96	fveq2d 6909	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...6)) ∧ 𝑥 = 4) → ((𝑘 ∈ (1...6) ↦ if(𝑘 = 1, ((𝑃‘1)↑2), if(𝑘 = 2, ((𝑃‘2)↑2), if(𝑘 = 3, ((𝑃‘3)↑2), if(𝑘 = 4, ((𝑃‘1) · (𝑃‘2)), if(𝑘 = 5, ((𝑃‘2) · (𝑃‘3)), ((𝑃‘3) · (𝑃‘1))))))))‘𝑥) = ((𝑘 ∈ (1...6) ↦ if(𝑘 = 1, ((𝑃‘1)↑2), if(𝑘 = 2, ((𝑃‘2)↑2), if(𝑘 = 3, ((𝑃‘3)↑2), if(𝑘 = 4, ((𝑃‘1) · (𝑃‘2)), if(𝑘 = 5, ((𝑃‘2) · (𝑃‘3)), ((𝑃‘3) · (𝑃‘1))))))))‘4))
99		4nn 12450	. . . . . . . . 9 ⊢ 4 ∈ ℕ
100		4re 12451	. . . . . . . . . 10 ⊢ 4 ∈ ℝ
101		4lt6 12551	. . . . . . . . . 10 ⊢ 4 < 6
102	100, 30, 101	ltleii 11457	. . . . . . . . 9 ⊢ 4 ≤ 6
103		elfz1b 13751	. . . . . . . . 9 ⊢ (4 ∈ (1...6) ↔ (4 ∈ ℕ ∧ 6 ∈ ℕ ∧ 4 ≤ 6))
104	99, 28, 102, 103	mpbir3an 1360	. . . . . . . 8 ⊢ 4 ∈ (1...6)
105		1lt4 12545	. . . . . . . . . . . . . . 15 ⊢ 1 < 4
106	29, 105	gtneii 11446	. . . . . . . . . . . . . 14 ⊢ 4 ≠ 1
107		neeq1 3021	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 4 → (𝑘 ≠ 1 ↔ 4 ≠ 1))
108	106, 107	mpbiri 261	. . . . . . . . . . . . 13 ⊢ (𝑘 = 4 → 𝑘 ≠ 1)
109	108	neneqd 2964	. . . . . . . . . . . 12 ⊢ (𝑘 = 4 → ¬ 𝑘 = 1)
110	109	iffalsed 4496	. . . . . . . . . . 11 ⊢ (𝑘 = 4 → if(𝑘 = 1, ((𝑃‘1)↑2), if(𝑘 = 2, ((𝑃‘2)↑2), if(𝑘 = 3, ((𝑃‘3)↑2), if(𝑘 = 4, ((𝑃‘1) · (𝑃‘2)), if(𝑘 = 5, ((𝑃‘2) · (𝑃‘3)), ((𝑃‘3) · (𝑃‘1))))))) = if(𝑘 = 2, ((𝑃‘2)↑2), if(𝑘 = 3, ((𝑃‘3)↑2), if(𝑘 = 4, ((𝑃‘1) · (𝑃‘2)), if(𝑘 = 5, ((𝑃‘2) · (𝑃‘3)), ((𝑃‘3) · (𝑃‘1)))))))
111		2lt4 12544	. . . . . . . . . . . . . . 15 ⊢ 2 < 4
112	46, 111	gtneii 11446	. . . . . . . . . . . . . 14 ⊢ 4 ≠ 2
113		neeq1 3021	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 4 → (𝑘 ≠ 2 ↔ 4 ≠ 2))
114	112, 113	mpbiri 261	. . . . . . . . . . . . 13 ⊢ (𝑘 = 4 → 𝑘 ≠ 2)
115	114	neneqd 2964	. . . . . . . . . . . 12 ⊢ (𝑘 = 4 → ¬ 𝑘 = 2)
116	115	iffalsed 4496	. . . . . . . . . . 11 ⊢ (𝑘 = 4 → if(𝑘 = 2, ((𝑃‘2)↑2), if(𝑘 = 3, ((𝑃‘3)↑2), if(𝑘 = 4, ((𝑃‘1) · (𝑃‘2)), if(𝑘 = 5, ((𝑃‘2) · (𝑃‘3)), ((𝑃‘3) · (𝑃‘1)))))) = if(𝑘 = 3, ((𝑃‘3)↑2), if(𝑘 = 4, ((𝑃‘1) · (𝑃‘2)), if(𝑘 = 5, ((𝑃‘2) · (𝑃‘3)), ((𝑃‘3) · (𝑃‘1))))))
117	110, 116	eqtrd 2798	. . . . . . . . . 10 ⊢ (𝑘 = 4 → if(𝑘 = 1, ((𝑃‘1)↑2), if(𝑘 = 2, ((𝑃‘2)↑2), if(𝑘 = 3, ((𝑃‘3)↑2), if(𝑘 = 4, ((𝑃‘1) · (𝑃‘2)), if(𝑘 = 5, ((𝑃‘2) · (𝑃‘3)), ((𝑃‘3) · (𝑃‘1))))))) = if(𝑘 = 3, ((𝑃‘3)↑2), if(𝑘 = 4, ((𝑃‘1) · (𝑃‘2)), if(𝑘 = 5, ((𝑃‘2) · (𝑃‘3)), ((𝑃‘3) · (𝑃‘1))))))
118		3lt4 12543	. . . . . . . . . . . . . 14 ⊢ 3 < 4
119	70, 118	gtneii 11446	. . . . . . . . . . . . 13 ⊢ 4 ≠ 3
120		neeq1 3021	. . . . . . . . . . . . 13 ⊢ (𝑘 = 4 → (𝑘 ≠ 3 ↔ 4 ≠ 3))
121	119, 120	mpbiri 261	. . . . . . . . . . . 12 ⊢ (𝑘 = 4 → 𝑘 ≠ 3)
122	121	neneqd 2964	. . . . . . . . . . 11 ⊢ (𝑘 = 4 → ¬ 𝑘 = 3)
123	122	iffalsed 4496	. . . . . . . . . 10 ⊢ (𝑘 = 4 → if(𝑘 = 3, ((𝑃‘3)↑2), if(𝑘 = 4, ((𝑃‘1) · (𝑃‘2)), if(𝑘 = 5, ((𝑃‘2) · (𝑃‘3)), ((𝑃‘3) · (𝑃‘1))))) = if(𝑘 = 4, ((𝑃‘1) · (𝑃‘2)), if(𝑘 = 5, ((𝑃‘2) · (𝑃‘3)), ((𝑃‘3) · (𝑃‘1)))))
124		iftrue 4491	. . . . . . . . . 10 ⊢ (𝑘 = 4 → if(𝑘 = 4, ((𝑃‘1) · (𝑃‘2)), if(𝑘 = 5, ((𝑃‘2) · (𝑃‘3)), ((𝑃‘3) · (𝑃‘1)))) = ((𝑃‘1) · (𝑃‘2)))
125	117, 123, 124	3eqtrd 2802	. . . . . . . . 9 ⊢ (𝑘 = 4 → if(𝑘 = 1, ((𝑃‘1)↑2), if(𝑘 = 2, ((𝑃‘2)↑2), if(𝑘 = 3, ((𝑃‘3)↑2), if(𝑘 = 4, ((𝑃‘1) · (𝑃‘2)), if(𝑘 = 5, ((𝑃‘2) · (𝑃‘3)), ((𝑃‘3) · (𝑃‘1))))))) = ((𝑃‘1) · (𝑃‘2)))
126	125, 19, 18	fvmpt3i 7019	. . . . . . . 8 ⊢ (4 ∈ (1...6) → ((𝑘 ∈ (1...6) ↦ if(𝑘 = 1, ((𝑃‘1)↑2), if(𝑘 = 2, ((𝑃‘2)↑2), if(𝑘 = 3, ((𝑃‘3)↑2), if(𝑘 = 4, ((𝑃‘1) · (𝑃‘2)), if(𝑘 = 5, ((𝑃‘2) · (𝑃‘3)), ((𝑃‘3) · (𝑃‘1))))))))‘4) = ((𝑃‘1) · (𝑃‘2)))
127	104, 126	ax-mp 5	. . . . . . 7 ⊢ ((𝑘 ∈ (1...6) ↦ if(𝑘 = 1, ((𝑃‘1)↑2), if(𝑘 = 2, ((𝑃‘2)↑2), if(𝑘 = 3, ((𝑃‘3)↑2), if(𝑘 = 4, ((𝑃‘1) · (𝑃‘2)), if(𝑘 = 5, ((𝑃‘2) · (𝑃‘3)), ((𝑃‘3) · (𝑃‘1))))))))‘4) = ((𝑃‘1) · (𝑃‘2))
128	98, 127	eqtrdi 2814	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...6)) ∧ 𝑥 = 4) → ((𝑘 ∈ (1...6) ↦ if(𝑘 = 1, ((𝑃‘1)↑2), if(𝑘 = 2, ((𝑃‘2)↑2), if(𝑘 = 3, ((𝑃‘3)↑2), if(𝑘 = 4, ((𝑃‘1) · (𝑃‘2)), if(𝑘 = 5, ((𝑃‘2) · (𝑃‘3)), ((𝑃‘3) · (𝑃‘1))))))))‘𝑥) = ((𝑃‘1) · (𝑃‘2)))
129	95, 97, 128	3eqtr4d 2808	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...6)) ∧ 𝑥 = 4) → ((veronese‘𝑃)‘𝑥) = ((𝑘 ∈ (1...6) ↦ if(𝑘 = 1, ((𝑃‘1)↑2), if(𝑘 = 2, ((𝑃‘2)↑2), if(𝑘 = 3, ((𝑃‘3)↑2), if(𝑘 = 4, ((𝑃‘1) · (𝑃‘2)), if(𝑘 = 5, ((𝑃‘2) · (𝑃‘3)), ((𝑃‘3) · (𝑃‘1))))))))‘𝑥))
130	93, 129	jaodan 972	. . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...6)) ∧ (((𝑥 = 1 ∨ 𝑥 = 2) ∨ 𝑥 = 3) ∨ 𝑥 = 4)) → ((veronese‘𝑃)‘𝑥) = ((𝑘 ∈ (1...6) ↦ if(𝑘 = 1, ((𝑃‘1)↑2), if(𝑘 = 2, ((𝑃‘2)↑2), if(𝑘 = 3, ((𝑃‘3)↑2), if(𝑘 = 4, ((𝑃‘1) · (𝑃‘2)), if(𝑘 = 5, ((𝑃‘2) · (𝑃‘3)), ((𝑃‘3) · (𝑃‘1))))))))‘𝑥))
131	4	veronesev5lem 51255	. . . . . 6 ⊢ (𝜑 → ((veronese‘𝑃)‘5) = ((𝑃‘2) · (𝑃‘3)))
132	131	ad2antrr 739	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...6)) ∧ 𝑥 = 5) → ((veronese‘𝑃)‘5) = ((𝑃‘2) · (𝑃‘3)))
133		simpr 490	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...6)) ∧ 𝑥 = 5) → 𝑥 = 5)
134	133	fveq2d 6909	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...6)) ∧ 𝑥 = 5) → ((veronese‘𝑃)‘𝑥) = ((veronese‘𝑃)‘5))
135	133	fveq2d 6909	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...6)) ∧ 𝑥 = 5) → ((𝑘 ∈ (1...6) ↦ if(𝑘 = 1, ((𝑃‘1)↑2), if(𝑘 = 2, ((𝑃‘2)↑2), if(𝑘 = 3, ((𝑃‘3)↑2), if(𝑘 = 4, ((𝑃‘1) · (𝑃‘2)), if(𝑘 = 5, ((𝑃‘2) · (𝑃‘3)), ((𝑃‘3) · (𝑃‘1))))))))‘𝑥) = ((𝑘 ∈ (1...6) ↦ if(𝑘 = 1, ((𝑃‘1)↑2), if(𝑘 = 2, ((𝑃‘2)↑2), if(𝑘 = 3, ((𝑃‘3)↑2), if(𝑘 = 4, ((𝑃‘1) · (𝑃‘2)), if(𝑘 = 5, ((𝑃‘2) · (𝑃‘3)), ((𝑃‘3) · (𝑃‘1))))))))‘5))
136		5nn 12453	. . . . . . . 8 ⊢ 5 ∈ ℕ
137		5re 12454	. . . . . . . . 9 ⊢ 5 ∈ ℝ
138		5lt6 12550	. . . . . . . . 9 ⊢ 5 < 6
139	137, 30, 138	ltleii 11457	. . . . . . . 8 ⊢ 5 ≤ 6
140		elfz1b 13751	. . . . . . . 8 ⊢ (5 ∈ (1...6) ↔ (5 ∈ ℕ ∧ 6 ∈ ℕ ∧ 5 ≤ 6))
141	136, 28, 139, 140	mpbir3an 1360	. . . . . . 7 ⊢ 5 ∈ (1...6)
142		1lt5 12549	. . . . . . . . . . . . . 14 ⊢ 1 < 5
143	29, 142	gtneii 11446	. . . . . . . . . . . . 13 ⊢ 5 ≠ 1
144		neeq1 3021	. . . . . . . . . . . . 13 ⊢ (𝑘 = 5 → (𝑘 ≠ 1 ↔ 5 ≠ 1))
145	143, 144	mpbiri 261	. . . . . . . . . . . 12 ⊢ (𝑘 = 5 → 𝑘 ≠ 1)
146	145	neneqd 2964	. . . . . . . . . . 11 ⊢ (𝑘 = 5 → ¬ 𝑘 = 1)
147	146	iffalsed 4496	. . . . . . . . . 10 ⊢ (𝑘 = 5 → if(𝑘 = 1, ((𝑃‘1)↑2), if(𝑘 = 2, ((𝑃‘2)↑2), if(𝑘 = 3, ((𝑃‘3)↑2), if(𝑘 = 4, ((𝑃‘1) · (𝑃‘2)), if(𝑘 = 5, ((𝑃‘2) · (𝑃‘3)), ((𝑃‘3) · (𝑃‘1))))))) = if(𝑘 = 2, ((𝑃‘2)↑2), if(𝑘 = 3, ((𝑃‘3)↑2), if(𝑘 = 4, ((𝑃‘1) · (𝑃‘2)), if(𝑘 = 5, ((𝑃‘2) · (𝑃‘3)), ((𝑃‘3) · (𝑃‘1)))))))
148		2lt5 12548	. . . . . . . . . . . . . 14 ⊢ 2 < 5
149	46, 148	gtneii 11446	. . . . . . . . . . . . 13 ⊢ 5 ≠ 2
150		neeq1 3021	. . . . . . . . . . . . 13 ⊢ (𝑘 = 5 → (𝑘 ≠ 2 ↔ 5 ≠ 2))
151	149, 150	mpbiri 261	. . . . . . . . . . . 12 ⊢ (𝑘 = 5 → 𝑘 ≠ 2)
152	151	neneqd 2964	. . . . . . . . . . 11 ⊢ (𝑘 = 5 → ¬ 𝑘 = 2)
153	152	iffalsed 4496	. . . . . . . . . 10 ⊢ (𝑘 = 5 → if(𝑘 = 2, ((𝑃‘2)↑2), if(𝑘 = 3, ((𝑃‘3)↑2), if(𝑘 = 4, ((𝑃‘1) · (𝑃‘2)), if(𝑘 = 5, ((𝑃‘2) · (𝑃‘3)), ((𝑃‘3) · (𝑃‘1)))))) = if(𝑘 = 3, ((𝑃‘3)↑2), if(𝑘 = 4, ((𝑃‘1) · (𝑃‘2)), if(𝑘 = 5, ((𝑃‘2) · (𝑃‘3)), ((𝑃‘3) · (𝑃‘1))))))
154		3lt5 12547	. . . . . . . . . . . . . 14 ⊢ 3 < 5
155	70, 154	gtneii 11446	. . . . . . . . . . . . 13 ⊢ 5 ≠ 3
156		neeq1 3021	. . . . . . . . . . . . 13 ⊢ (𝑘 = 5 → (𝑘 ≠ 3 ↔ 5 ≠ 3))
157	155, 156	mpbiri 261	. . . . . . . . . . . 12 ⊢ (𝑘 = 5 → 𝑘 ≠ 3)
158	157	neneqd 2964	. . . . . . . . . . 11 ⊢ (𝑘 = 5 → ¬ 𝑘 = 3)
159	158	iffalsed 4496	. . . . . . . . . 10 ⊢ (𝑘 = 5 → if(𝑘 = 3, ((𝑃‘3)↑2), if(𝑘 = 4, ((𝑃‘1) · (𝑃‘2)), if(𝑘 = 5, ((𝑃‘2) · (𝑃‘3)), ((𝑃‘3) · (𝑃‘1))))) = if(𝑘 = 4, ((𝑃‘1) · (𝑃‘2)), if(𝑘 = 5, ((𝑃‘2) · (𝑃‘3)), ((𝑃‘3) · (𝑃‘1)))))
160	147, 153, 159	3eqtrd 2802	. . . . . . . . 9 ⊢ (𝑘 = 5 → if(𝑘 = 1, ((𝑃‘1)↑2), if(𝑘 = 2, ((𝑃‘2)↑2), if(𝑘 = 3, ((𝑃‘3)↑2), if(𝑘 = 4, ((𝑃‘1) · (𝑃‘2)), if(𝑘 = 5, ((𝑃‘2) · (𝑃‘3)), ((𝑃‘3) · (𝑃‘1))))))) = if(𝑘 = 4, ((𝑃‘1) · (𝑃‘2)), if(𝑘 = 5, ((𝑃‘2) · (𝑃‘3)), ((𝑃‘3) · (𝑃‘1)))))
161		4lt5 12546	. . . . . . . . . . . . 13 ⊢ 4 < 5
162	100, 161	gtneii 11446	. . . . . . . . . . . 12 ⊢ 5 ≠ 4
163		neeq1 3021	. . . . . . . . . . . 12 ⊢ (𝑘 = 5 → (𝑘 ≠ 4 ↔ 5 ≠ 4))
164	162, 163	mpbiri 261	. . . . . . . . . . 11 ⊢ (𝑘 = 5 → 𝑘 ≠ 4)
165	164	neneqd 2964	. . . . . . . . . 10 ⊢ (𝑘 = 5 → ¬ 𝑘 = 4)
166	165	iffalsed 4496	. . . . . . . . 9 ⊢ (𝑘 = 5 → if(𝑘 = 4, ((𝑃‘1) · (𝑃‘2)), if(𝑘 = 5, ((𝑃‘2) · (𝑃‘3)), ((𝑃‘3) · (𝑃‘1)))) = if(𝑘 = 5, ((𝑃‘2) · (𝑃‘3)), ((𝑃‘3) · (𝑃‘1))))
167		iftrue 4491	. . . . . . . . 9 ⊢ (𝑘 = 5 → if(𝑘 = 5, ((𝑃‘2) · (𝑃‘3)), ((𝑃‘3) · (𝑃‘1))) = ((𝑃‘2) · (𝑃‘3)))
168	160, 166, 167	3eqtrd 2802	. . . . . . . 8 ⊢ (𝑘 = 5 → if(𝑘 = 1, ((𝑃‘1)↑2), if(𝑘 = 2, ((𝑃‘2)↑2), if(𝑘 = 3, ((𝑃‘3)↑2), if(𝑘 = 4, ((𝑃‘1) · (𝑃‘2)), if(𝑘 = 5, ((𝑃‘2) · (𝑃‘3)), ((𝑃‘3) · (𝑃‘1))))))) = ((𝑃‘2) · (𝑃‘3)))
169	168, 19, 18	fvmpt3i 7019	. . . . . . 7 ⊢ (5 ∈ (1...6) → ((𝑘 ∈ (1...6) ↦ if(𝑘 = 1, ((𝑃‘1)↑2), if(𝑘 = 2, ((𝑃‘2)↑2), if(𝑘 = 3, ((𝑃‘3)↑2), if(𝑘 = 4, ((𝑃‘1) · (𝑃‘2)), if(𝑘 = 5, ((𝑃‘2) · (𝑃‘3)), ((𝑃‘3) · (𝑃‘1))))))))‘5) = ((𝑃‘2) · (𝑃‘3)))
170	141, 169	ax-mp 5	. . . . . 6 ⊢ ((𝑘 ∈ (1...6) ↦ if(𝑘 = 1, ((𝑃‘1)↑2), if(𝑘 = 2, ((𝑃‘2)↑2), if(𝑘 = 3, ((𝑃‘3)↑2), if(𝑘 = 4, ((𝑃‘1) · (𝑃‘2)), if(𝑘 = 5, ((𝑃‘2) · (𝑃‘3)), ((𝑃‘3) · (𝑃‘1))))))))‘5) = ((𝑃‘2) · (𝑃‘3))
171	135, 170	eqtrdi 2814	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...6)) ∧ 𝑥 = 5) → ((𝑘 ∈ (1...6) ↦ if(𝑘 = 1, ((𝑃‘1)↑2), if(𝑘 = 2, ((𝑃‘2)↑2), if(𝑘 = 3, ((𝑃‘3)↑2), if(𝑘 = 4, ((𝑃‘1) · (𝑃‘2)), if(𝑘 = 5, ((𝑃‘2) · (𝑃‘3)), ((𝑃‘3) · (𝑃‘1))))))))‘𝑥) = ((𝑃‘2) · (𝑃‘3)))
172	132, 134, 171	3eqtr4d 2808	. . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...6)) ∧ 𝑥 = 5) → ((veronese‘𝑃)‘𝑥) = ((𝑘 ∈ (1...6) ↦ if(𝑘 = 1, ((𝑃‘1)↑2), if(𝑘 = 2, ((𝑃‘2)↑2), if(𝑘 = 3, ((𝑃‘3)↑2), if(𝑘 = 4, ((𝑃‘1) · (𝑃‘2)), if(𝑘 = 5, ((𝑃‘2) · (𝑃‘3)), ((𝑃‘3) · (𝑃‘1))))))))‘𝑥))
173	130, 172	jaodan 972	. . 3 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...6)) ∧ ((((𝑥 = 1 ∨ 𝑥 = 2) ∨ 𝑥 = 3) ∨ 𝑥 = 4) ∨ 𝑥 = 5)) → ((veronese‘𝑃)‘𝑥) = ((𝑘 ∈ (1...6) ↦ if(𝑘 = 1, ((𝑃‘1)↑2), if(𝑘 = 2, ((𝑃‘2)↑2), if(𝑘 = 3, ((𝑃‘3)↑2), if(𝑘 = 4, ((𝑃‘1) · (𝑃‘2)), if(𝑘 = 5, ((𝑃‘2) · (𝑃‘3)), ((𝑃‘3) · (𝑃‘1))))))))‘𝑥))
174	4	veronesev6lem 51256	. . . . 5 ⊢ (𝜑 → ((veronese‘𝑃)‘6) = ((𝑃‘3) · (𝑃‘1)))
175	174	ad2antrr 739	. . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...6)) ∧ 𝑥 = 6) → ((veronese‘𝑃)‘6) = ((𝑃‘3) · (𝑃‘1)))
176		simpr 490	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...6)) ∧ 𝑥 = 6) → 𝑥 = 6)
177	176	fveq2d 6909	. . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...6)) ∧ 𝑥 = 6) → ((veronese‘𝑃)‘𝑥) = ((veronese‘𝑃)‘6))
178	176	fveq2d 6909	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...6)) ∧ 𝑥 = 6) → ((𝑘 ∈ (1...6) ↦ if(𝑘 = 1, ((𝑃‘1)↑2), if(𝑘 = 2, ((𝑃‘2)↑2), if(𝑘 = 3, ((𝑃‘3)↑2), if(𝑘 = 4, ((𝑃‘1) · (𝑃‘2)), if(𝑘 = 5, ((𝑃‘2) · (𝑃‘3)), ((𝑃‘3) · (𝑃‘1))))))))‘𝑥) = ((𝑘 ∈ (1...6) ↦ if(𝑘 = 1, ((𝑃‘1)↑2), if(𝑘 = 2, ((𝑃‘2)↑2), if(𝑘 = 3, ((𝑃‘3)↑2), if(𝑘 = 4, ((𝑃‘1) · (𝑃‘2)), if(𝑘 = 5, ((𝑃‘2) · (𝑃‘3)), ((𝑃‘3) · (𝑃‘1))))))))‘6))
179	30	leidi 11874	. . . . . . 7 ⊢ 6 ≤ 6
180		elfz1b 13751	. . . . . . 7 ⊢ (6 ∈ (1...6) ↔ (6 ∈ ℕ ∧ 6 ∈ ℕ ∧ 6 ≤ 6))
181	28, 28, 179, 180	mpbir3an 1360	. . . . . 6 ⊢ 6 ∈ (1...6)
182	29, 31	gtneii 11446	. . . . . . . . . . . 12 ⊢ 6 ≠ 1
183		neeq1 3021	. . . . . . . . . . . 12 ⊢ (𝑘 = 6 → (𝑘 ≠ 1 ↔ 6 ≠ 1))
184	182, 183	mpbiri 261	. . . . . . . . . . 11 ⊢ (𝑘 = 6 → 𝑘 ≠ 1)
185	184	neneqd 2964	. . . . . . . . . 10 ⊢ (𝑘 = 6 → ¬ 𝑘 = 1)
186	185	iffalsed 4496	. . . . . . . . 9 ⊢ (𝑘 = 6 → if(𝑘 = 1, ((𝑃‘1)↑2), if(𝑘 = 2, ((𝑃‘2)↑2), if(𝑘 = 3, ((𝑃‘3)↑2), if(𝑘 = 4, ((𝑃‘1) · (𝑃‘2)), if(𝑘 = 5, ((𝑃‘2) · (𝑃‘3)), ((𝑃‘3) · (𝑃‘1))))))) = if(𝑘 = 2, ((𝑃‘2)↑2), if(𝑘 = 3, ((𝑃‘3)↑2), if(𝑘 = 4, ((𝑃‘1) · (𝑃‘2)), if(𝑘 = 5, ((𝑃‘2) · (𝑃‘3)), ((𝑃‘3) · (𝑃‘1)))))))
187	46, 47	gtneii 11446	. . . . . . . . . . . 12 ⊢ 6 ≠ 2
188		neeq1 3021	. . . . . . . . . . . 12 ⊢ (𝑘 = 6 → (𝑘 ≠ 2 ↔ 6 ≠ 2))
189	187, 188	mpbiri 261	. . . . . . . . . . 11 ⊢ (𝑘 = 6 → 𝑘 ≠ 2)
190	189	neneqd 2964	. . . . . . . . . 10 ⊢ (𝑘 = 6 → ¬ 𝑘 = 2)
191	190	iffalsed 4496	. . . . . . . . 9 ⊢ (𝑘 = 6 → if(𝑘 = 2, ((𝑃‘2)↑2), if(𝑘 = 3, ((𝑃‘3)↑2), if(𝑘 = 4, ((𝑃‘1) · (𝑃‘2)), if(𝑘 = 5, ((𝑃‘2) · (𝑃‘3)), ((𝑃‘3) · (𝑃‘1)))))) = if(𝑘 = 3, ((𝑃‘3)↑2), if(𝑘 = 4, ((𝑃‘1) · (𝑃‘2)), if(𝑘 = 5, ((𝑃‘2) · (𝑃‘3)), ((𝑃‘3) · (𝑃‘1))))))
192	70, 71	gtneii 11446	. . . . . . . . . . . 12 ⊢ 6 ≠ 3
193		neeq1 3021	. . . . . . . . . . . 12 ⊢ (𝑘 = 6 → (𝑘 ≠ 3 ↔ 6 ≠ 3))
194	192, 193	mpbiri 261	. . . . . . . . . . 11 ⊢ (𝑘 = 6 → 𝑘 ≠ 3)
195	194	neneqd 2964	. . . . . . . . . 10 ⊢ (𝑘 = 6 → ¬ 𝑘 = 3)
196	195	iffalsed 4496	. . . . . . . . 9 ⊢ (𝑘 = 6 → if(𝑘 = 3, ((𝑃‘3)↑2), if(𝑘 = 4, ((𝑃‘1) · (𝑃‘2)), if(𝑘 = 5, ((𝑃‘2) · (𝑃‘3)), ((𝑃‘3) · (𝑃‘1))))) = if(𝑘 = 4, ((𝑃‘1) · (𝑃‘2)), if(𝑘 = 5, ((𝑃‘2) · (𝑃‘3)), ((𝑃‘3) · (𝑃‘1)))))
197	186, 191, 196	3eqtrd 2802	. . . . . . . 8 ⊢ (𝑘 = 6 → if(𝑘 = 1, ((𝑃‘1)↑2), if(𝑘 = 2, ((𝑃‘2)↑2), if(𝑘 = 3, ((𝑃‘3)↑2), if(𝑘 = 4, ((𝑃‘1) · (𝑃‘2)), if(𝑘 = 5, ((𝑃‘2) · (𝑃‘3)), ((𝑃‘3) · (𝑃‘1))))))) = if(𝑘 = 4, ((𝑃‘1) · (𝑃‘2)), if(𝑘 = 5, ((𝑃‘2) · (𝑃‘3)), ((𝑃‘3) · (𝑃‘1)))))
198	100, 101	gtneii 11446	. . . . . . . . . . 11 ⊢ 6 ≠ 4
199		neeq1 3021	. . . . . . . . . . 11 ⊢ (𝑘 = 6 → (𝑘 ≠ 4 ↔ 6 ≠ 4))
200	198, 199	mpbiri 261	. . . . . . . . . 10 ⊢ (𝑘 = 6 → 𝑘 ≠ 4)
201	200	neneqd 2964	. . . . . . . . 9 ⊢ (𝑘 = 6 → ¬ 𝑘 = 4)
202	201	iffalsed 4496	. . . . . . . 8 ⊢ (𝑘 = 6 → if(𝑘 = 4, ((𝑃‘1) · (𝑃‘2)), if(𝑘 = 5, ((𝑃‘2) · (𝑃‘3)), ((𝑃‘3) · (𝑃‘1)))) = if(𝑘 = 5, ((𝑃‘2) · (𝑃‘3)), ((𝑃‘3) · (𝑃‘1))))
203	137, 138	gtneii 11446	. . . . . . . . . . 11 ⊢ 6 ≠ 5
204		neeq1 3021	. . . . . . . . . . 11 ⊢ (𝑘 = 6 → (𝑘 ≠ 5 ↔ 6 ≠ 5))
205	203, 204	mpbiri 261	. . . . . . . . . 10 ⊢ (𝑘 = 6 → 𝑘 ≠ 5)
206	205	neneqd 2964	. . . . . . . . 9 ⊢ (𝑘 = 6 → ¬ 𝑘 = 5)
207	206	iffalsed 4496	. . . . . . . 8 ⊢ (𝑘 = 6 → if(𝑘 = 5, ((𝑃‘2) · (𝑃‘3)), ((𝑃‘3) · (𝑃‘1))) = ((𝑃‘3) · (𝑃‘1)))
208	197, 202, 207	3eqtrd 2802	. . . . . . 7 ⊢ (𝑘 = 6 → if(𝑘 = 1, ((𝑃‘1)↑2), if(𝑘 = 2, ((𝑃‘2)↑2), if(𝑘 = 3, ((𝑃‘3)↑2), if(𝑘 = 4, ((𝑃‘1) · (𝑃‘2)), if(𝑘 = 5, ((𝑃‘2) · (𝑃‘3)), ((𝑃‘3) · (𝑃‘1))))))) = ((𝑃‘3) · (𝑃‘1)))
209	208, 19, 18	fvmpt3i 7019	. . . . . 6 ⊢ (6 ∈ (1...6) → ((𝑘 ∈ (1...6) ↦ if(𝑘 = 1, ((𝑃‘1)↑2), if(𝑘 = 2, ((𝑃‘2)↑2), if(𝑘 = 3, ((𝑃‘3)↑2), if(𝑘 = 4, ((𝑃‘1) · (𝑃‘2)), if(𝑘 = 5, ((𝑃‘2) · (𝑃‘3)), ((𝑃‘3) · (𝑃‘1))))))))‘6) = ((𝑃‘3) · (𝑃‘1)))
210	181, 209	ax-mp 5	. . . . 5 ⊢ ((𝑘 ∈ (1...6) ↦ if(𝑘 = 1, ((𝑃‘1)↑2), if(𝑘 = 2, ((𝑃‘2)↑2), if(𝑘 = 3, ((𝑃‘3)↑2), if(𝑘 = 4, ((𝑃‘1) · (𝑃‘2)), if(𝑘 = 5, ((𝑃‘2) · (𝑃‘3)), ((𝑃‘3) · (𝑃‘1))))))))‘6) = ((𝑃‘3) · (𝑃‘1))
211	178, 210	eqtrdi 2814	. . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...6)) ∧ 𝑥 = 6) → ((𝑘 ∈ (1...6) ↦ if(𝑘 = 1, ((𝑃‘1)↑2), if(𝑘 = 2, ((𝑃‘2)↑2), if(𝑘 = 3, ((𝑃‘3)↑2), if(𝑘 = 4, ((𝑃‘1) · (𝑃‘2)), if(𝑘 = 5, ((𝑃‘2) · (𝑃‘3)), ((𝑃‘3) · (𝑃‘1))))))))‘𝑥) = ((𝑃‘3) · (𝑃‘1)))
212	175, 177, 211	3eqtr4d 2808	. . 3 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...6)) ∧ 𝑥 = 6) → ((veronese‘𝑃)‘𝑥) = ((𝑘 ∈ (1...6) ↦ if(𝑘 = 1, ((𝑃‘1)↑2), if(𝑘 = 2, ((𝑃‘2)↑2), if(𝑘 = 3, ((𝑃‘3)↑2), if(𝑘 = 4, ((𝑃‘1) · (𝑃‘2)), if(𝑘 = 5, ((𝑃‘2) · (𝑃‘3)), ((𝑃‘3) · (𝑃‘1))))))))‘𝑥))
213		simpr 490	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...6)) → 𝑥 ∈ (1...6))
214		elnnuz 13029	. . . . . . . 8 ⊢ (5 ∈ ℕ ↔ 5 ∈ (ℤ_≥‘1))
215	136, 214	mpbi 233	. . . . . . 7 ⊢ 5 ∈ (ℤ_≥‘1)
216		elfzp1 13732	. . . . . . 7 ⊢ (5 ∈ (ℤ_≥‘1) → (𝑥 ∈ (1...(5 + 1)) ↔ (𝑥 ∈ (1...5) ∨ 𝑥 = (5 + 1))))
217	215, 216	ax-mp 5	. . . . . 6 ⊢ (𝑥 ∈ (1...(5 + 1)) ↔ (𝑥 ∈ (1...5) ∨ 𝑥 = (5 + 1)))
218		5p1e6 12513	. . . . . . . 8 ⊢ (5 + 1) = 6
219	218	oveq2i 7451	. . . . . . 7 ⊢ (1...(5 + 1)) = (1...6)
220	219	eleq2i 2856	. . . . . 6 ⊢ (𝑥 ∈ (1...(5 + 1)) ↔ 𝑥 ∈ (1...6))
221	218	eqeq2i 2776	. . . . . . 7 ⊢ (𝑥 = (5 + 1) ↔ 𝑥 = 6)
222	221	orbi2i 926	. . . . . 6 ⊢ ((𝑥 ∈ (1...5) ∨ 𝑥 = (5 + 1)) ↔ (𝑥 ∈ (1...5) ∨ 𝑥 = 6))
223	217, 220, 222	3bitr3i 304	. . . . 5 ⊢ (𝑥 ∈ (1...6) ↔ (𝑥 ∈ (1...5) ∨ 𝑥 = 6))
224		elnnuz 13029	. . . . . . . . . 10 ⊢ (4 ∈ ℕ ↔ 4 ∈ (ℤ_≥‘1))
225	99, 224	mpbi 233	. . . . . . . . 9 ⊢ 4 ∈ (ℤ_≥‘1)
226		elfzp1 13732	. . . . . . . . 9 ⊢ (4 ∈ (ℤ_≥‘1) → (𝑥 ∈ (1...(4 + 1)) ↔ (𝑥 ∈ (1...4) ∨ 𝑥 = (4 + 1))))
227	225, 226	ax-mp 5	. . . . . . . 8 ⊢ (𝑥 ∈ (1...(4 + 1)) ↔ (𝑥 ∈ (1...4) ∨ 𝑥 = (4 + 1)))
228		4p1e5 12512	. . . . . . . . . 10 ⊢ (4 + 1) = 5
229	228	oveq2i 7451	. . . . . . . . 9 ⊢ (1...(4 + 1)) = (1...5)
230	229	eleq2i 2856	. . . . . . . 8 ⊢ (𝑥 ∈ (1...(4 + 1)) ↔ 𝑥 ∈ (1...5))
231	228	eqeq2i 2776	. . . . . . . . 9 ⊢ (𝑥 = (4 + 1) ↔ 𝑥 = 5)
232	231	orbi2i 926	. . . . . . . 8 ⊢ ((𝑥 ∈ (1...4) ∨ 𝑥 = (4 + 1)) ↔ (𝑥 ∈ (1...4) ∨ 𝑥 = 5))
233	227, 230, 232	3bitr3i 304	. . . . . . 7 ⊢ (𝑥 ∈ (1...5) ↔ (𝑥 ∈ (1...4) ∨ 𝑥 = 5))
234		elnnuz 13029	. . . . . . . . . . . 12 ⊢ (3 ∈ ℕ ↔ 3 ∈ (ℤ_≥‘1))
235	69, 234	mpbi 233	. . . . . . . . . . 11 ⊢ 3 ∈ (ℤ_≥‘1)
236		elfzp1 13732	. . . . . . . . . . 11 ⊢ (3 ∈ (ℤ_≥‘1) → (𝑥 ∈ (1...(3 + 1)) ↔ (𝑥 ∈ (1...3) ∨ 𝑥 = (3 + 1))))
237	235, 236	ax-mp 5	. . . . . . . . . 10 ⊢ (𝑥 ∈ (1...(3 + 1)) ↔ (𝑥 ∈ (1...3) ∨ 𝑥 = (3 + 1)))
238		3p1e4 12511	. . . . . . . . . . . 12 ⊢ (3 + 1) = 4
239	238	oveq2i 7451	. . . . . . . . . . 11 ⊢ (1...(3 + 1)) = (1...4)
240	239	eleq2i 2856	. . . . . . . . . 10 ⊢ (𝑥 ∈ (1...(3 + 1)) ↔ 𝑥 ∈ (1...4))
241	238	eqeq2i 2776	. . . . . . . . . . 11 ⊢ (𝑥 = (3 + 1) ↔ 𝑥 = 4)
242	241	orbi2i 926	. . . . . . . . . 10 ⊢ ((𝑥 ∈ (1...3) ∨ 𝑥 = (3 + 1)) ↔ (𝑥 ∈ (1...3) ∨ 𝑥 = 4))
243	237, 240, 242	3bitr3i 304	. . . . . . . . 9 ⊢ (𝑥 ∈ (1...4) ↔ (𝑥 ∈ (1...3) ∨ 𝑥 = 4))
244		2eluzge1 13033	. . . . . . . . . . . . 13 ⊢ 2 ∈ (ℤ_≥‘1)
245		elfzp1 13732	. . . . . . . . . . . . 13 ⊢ (2 ∈ (ℤ_≥‘1) → (𝑥 ∈ (1...(2 + 1)) ↔ (𝑥 ∈ (1...2) ∨ 𝑥 = (2 + 1))))
246	244, 245	ax-mp 5	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (1...(2 + 1)) ↔ (𝑥 ∈ (1...2) ∨ 𝑥 = (2 + 1)))
247		2p1e3 12508	. . . . . . . . . . . . . 14 ⊢ (2 + 1) = 3
248	247	oveq2i 7451	. . . . . . . . . . . . 13 ⊢ (1...(2 + 1)) = (1...3)
249	248	eleq2i 2856	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (1...(2 + 1)) ↔ 𝑥 ∈ (1...3))
250	247	eqeq2i 2776	. . . . . . . . . . . . 13 ⊢ (𝑥 = (2 + 1) ↔ 𝑥 = 3)
251	250	orbi2i 926	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ (1...2) ∨ 𝑥 = (2 + 1)) ↔ (𝑥 ∈ (1...2) ∨ 𝑥 = 3))
252	246, 249, 251	3bitr3i 304	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (1...3) ↔ (𝑥 ∈ (1...2) ∨ 𝑥 = 3))
253		elnnuz 13029	. . . . . . . . . . . . . . . 16 ⊢ (1 ∈ ℕ ↔ 1 ∈ (ℤ_≥‘1))
254	27, 253	mpbi 233	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ (ℤ_≥‘1)
255		elfzp1 13732	. . . . . . . . . . . . . . 15 ⊢ (1 ∈ (ℤ_≥‘1) → (𝑥 ∈ (1...(1 + 1)) ↔ (𝑥 ∈ (1...1) ∨ 𝑥 = (1 + 1))))
256	254, 255	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (1...(1 + 1)) ↔ (𝑥 ∈ (1...1) ∨ 𝑥 = (1 + 1)))
257		1p1e2 12490	. . . . . . . . . . . . . . . 16 ⊢ (1 + 1) = 2
258	257	oveq2i 7451	. . . . . . . . . . . . . . 15 ⊢ (1...(1 + 1)) = (1...2)
259	258	eleq2i 2856	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (1...(1 + 1)) ↔ 𝑥 ∈ (1...2))
260	257	eqeq2i 2776	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = (1 + 1) ↔ 𝑥 = 2)
261	260	orbi2i 926	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ (1...1) ∨ 𝑥 = (1 + 1)) ↔ (𝑥 ∈ (1...1) ∨ 𝑥 = 2))
262	256, 259, 261	3bitr3i 304	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (1...2) ↔ (𝑥 ∈ (1...1) ∨ 𝑥 = 2))
263		elfz1eq 13692	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (1...1) → 𝑥 = 1)
264	263	orim1i 923	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ (1...1) ∨ 𝑥 = 2) → (𝑥 = 1 ∨ 𝑥 = 2))
265	262, 264	sylbi 220	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (1...2) → (𝑥 = 1 ∨ 𝑥 = 2))
266	265	orim1i 923	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ (1...2) ∨ 𝑥 = 3) → ((𝑥 = 1 ∨ 𝑥 = 2) ∨ 𝑥 = 3))
267	252, 266	sylbi 220	. . . . . . . . . 10 ⊢ (𝑥 ∈ (1...3) → ((𝑥 = 1 ∨ 𝑥 = 2) ∨ 𝑥 = 3))
268	267	orim1i 923	. . . . . . . . 9 ⊢ ((𝑥 ∈ (1...3) ∨ 𝑥 = 4) → (((𝑥 = 1 ∨ 𝑥 = 2) ∨ 𝑥 = 3) ∨ 𝑥 = 4))
269	243, 268	sylbi 220	. . . . . . . 8 ⊢ (𝑥 ∈ (1...4) → (((𝑥 = 1 ∨ 𝑥 = 2) ∨ 𝑥 = 3) ∨ 𝑥 = 4))
270	269	orim1i 923	. . . . . . 7 ⊢ ((𝑥 ∈ (1...4) ∨ 𝑥 = 5) → ((((𝑥 = 1 ∨ 𝑥 = 2) ∨ 𝑥 = 3) ∨ 𝑥 = 4) ∨ 𝑥 = 5))
271	233, 270	sylbi 220	. . . . . 6 ⊢ (𝑥 ∈ (1...5) → ((((𝑥 = 1 ∨ 𝑥 = 2) ∨ 𝑥 = 3) ∨ 𝑥 = 4) ∨ 𝑥 = 5))
272	271	orim1i 923	. . . . 5 ⊢ ((𝑥 ∈ (1...5) ∨ 𝑥 = 6) → (((((𝑥 = 1 ∨ 𝑥 = 2) ∨ 𝑥 = 3) ∨ 𝑥 = 4) ∨ 𝑥 = 5) ∨ 𝑥 = 6))
273	223, 272	sylbi 220	. . . 4 ⊢ (𝑥 ∈ (1...6) → (((((𝑥 = 1 ∨ 𝑥 = 2) ∨ 𝑥 = 3) ∨ 𝑥 = 4) ∨ 𝑥 = 5) ∨ 𝑥 = 6))
274	213, 273	syl 18	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...6)) → (((((𝑥 = 1 ∨ 𝑥 = 2) ∨ 𝑥 = 3) ∨ 𝑥 = 4) ∨ 𝑥 = 5) ∨ 𝑥 = 6))
275	173, 212, 274	mpjaodan 973	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...6)) → ((veronese‘𝑃)‘𝑥) = ((𝑘 ∈ (1...6) ↦ if(𝑘 = 1, ((𝑃‘1)↑2), if(𝑘 = 2, ((𝑃‘2)↑2), if(𝑘 = 3, ((𝑃‘3)↑2), if(𝑘 = 4, ((𝑃‘1) · (𝑃‘2)), if(𝑘 = 5, ((𝑃‘2) · (𝑃‘3)), ((𝑃‘3) · (𝑃‘1))))))))‘𝑥))
276	7, 21, 275	eqfnfvd 7052	1 ⊢ (𝜑 → (veronese‘𝑃) = (𝑘 ∈ (1...6) ↦ if(𝑘 = 1, ((𝑃‘1)↑2), if(𝑘 = 2, ((𝑃‘2)↑2), if(𝑘 = 3, ((𝑃‘3)↑2), if(𝑘 = 4, ((𝑃‘1) · (𝑃‘2)), if(𝑘 = 5, ((𝑃‘2) · (𝑃‘3)), ((𝑃‘3) · (𝑃‘1)))))))))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 ∨ wo 861 = wceq 1570 ∈ wcel 2147 ≠ wne 2959 ifcif 4485 class class class wbr 5106 ↦ cmpt 5189 Fn wfn 6550 ‘cfv 6555 (class class class)co 7440 ↑_m cmap 8872 ℝcr 11223 0cc0 11224 1c1 11225 + caddc 11227 · cmul 11229 ≤ cle 11368 ℕcn 12359 2c2 12421 3c3 12422 4c4 12423 5c5 12424 6c6 12425 ℤ_≥cuz 12989 ...cfz 13663 ↑cexp 14228 veronesecveronese 51246

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1945 ax-6 2002 ax-7 2043 ax-8 2149 ax-9 2157 ax-10 2180 ax-11 2197 ax-12 2216 ax-ext 2735 ax-rep 5235 ax-sep 5252 ax-nul 5263 ax-pow 5331 ax-pr 5395 ax-un 7772 ax-cnex 11280 ax-resscn 11281 ax-1cn 11282 ax-icn 11283 ax-addcl 11284 ax-addrcl 11285 ax-mulcl 11286 ax-mulrcl 11287 ax-mulcom 11288 ax-addass 11289 ax-mulass 11290 ax-distr 11291 ax-i2m1 11292 ax-1ne0 11293 ax-1rid 11294 ax-rnegex 11295 ax-rrecex 11296 ax-cnre 11297 ax-pre-lttri 11298 ax-pre-lttrn 11299 ax-pre-ltadd 11300 ax-pre-mulgt0 11301

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2102 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2839 df-nfc 2913 df-ne 2960 df-nel 3066 df-ral 3081 df-rex 3091 df-reu 3370 df-rab 3417 df-v 3456 df-sbc 3743 df-csb 3852 df-ss 3901 df-pss 4017 df-dif 4050 df-in 4094 df-un 4154 df-nul 4282 df-if 4486 df-pw 4562 df-sn 4589 df-pr 4591 df-op 4839 df-uni 4871 df-iun 4956 df-br 5107 df-opab 5171 df-mpt 5190 df-tr 5216 df-id 5550 df-eprel 5555 df-po 5563 df-so 5564 df-fr 5608 df-we 5610 df-xp 5661 df-rel 5662 df-cnv 5663 df-co 5664 df-dm 5665 df-rn 5666 df-res 5667 df-ima 5668 df-pred 6319 df-ord 6380 df-on 6381 df-lim 6382 df-suc 6383 df-iota 6509 df-fun 6557 df-fn 6558 df-f 6559 df-f1 6560 df-fo 6561 df-f1o 6562 df-fv 6563 df-riota 7397 df-ov 7443 df-oprab 7444 df-mpo 7445 df-om 7899 df-1st 8022 df-2nd 8023 df-frecs 8324 df-wrecs 8355 df-recs 8404 df-rdg 8443 df-er 8742 df-map 8874 df-en 8999 df-dom 9000 df-sdom 9001 df-pnf 11369 df-mnf 11370 df-xr 11371 df-ltxr 11372 df-le 11373 df-sub 11567 df-neg 11568 df-nn 12360 df-2 12429 df-3 12430 df-4 12431 df-5 12432 df-6 12433 df-n0 12631 df-z 12718 df-uz 12990 df-fz 13664 df-seq 14169 df-exp 14229 df-veronese 51247

This theorem is used by: veronesematrowexpd 51260

W3C validator