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 50877

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 7449	. . . 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 2760	. . . 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 6678	. . 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 50869	. . . 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 6628	. . 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 7449	. . . . 5 ⊢ ((𝑃‘1)↑2) ∈ V
9		ovex 7449	. . . . . 6 ⊢ ((𝑃‘2)↑2) ∈ V
10		ovex 7449	. . . . . . 7 ⊢ ((𝑃‘3)↑2) ∈ V
11		ovex 7449	. . . . . . . 8 ⊢ ((𝑃‘1) · (𝑃‘2)) ∈ V
12		ovex 7449	. . . . . . . . 9 ⊢ ((𝑃‘2) · (𝑃‘3)) ∈ V
13		ovex 7449	. . . . . . . . 9 ⊢ ((𝑃‘3) · (𝑃‘1)) ∈ V
14	12, 13	ifex 4533	. . . . . . . 8 ⊢ if(𝑘 = 5, ((𝑃‘2) · (𝑃‘3)), ((𝑃‘3) · (𝑃‘1))) ∈ V
15	11, 14	ifex 4533	. . . . . . 7 ⊢ if(𝑘 = 4, ((𝑃‘1) · (𝑃‘2)), if(𝑘 = 5, ((𝑃‘2) · (𝑃‘3)), ((𝑃‘3) · (𝑃‘1)))) ∈ V
16	10, 15	ifex 4533	. . . . . 6 ⊢ if(𝑘 = 3, ((𝑃‘3)↑2), if(𝑘 = 4, ((𝑃‘1) · (𝑃‘2)), if(𝑘 = 5, ((𝑃‘2) · (𝑃‘3)), ((𝑃‘3) · (𝑃‘1))))) ∈ V
17	9, 16	ifex 4533	. . . . 5 ⊢ if(𝑘 = 2, ((𝑃‘2)↑2), if(𝑘 = 3, ((𝑃‘3)↑2), if(𝑘 = 4, ((𝑃‘1) · (𝑃‘2)), if(𝑘 = 5, ((𝑃‘2) · (𝑃‘3)), ((𝑃‘3) · (𝑃‘1)))))) ∈ V
18	8, 17	ifex 4533	. . . 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 2760	. . . 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 6678	. . 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 50871	. . . . . . . . 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 6885	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...6)) ∧ 𝑥 = 1) → ((veronese‘𝑃)‘𝑥) = ((veronese‘𝑃)‘1))
26	24	fveq2d 6885	. . . . . . . . 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 12293	. . . . . . . . . . 11 ⊢ 1 ∈ ℕ
28		6nn 12379	. . . . . . . . . . 11 ⊢ 6 ∈ ℕ
29		1re 11257	. . . . . . . . . . . 12 ⊢ 1 ∈ ℝ
30		6re 12380	. . . . . . . . . . . 12 ⊢ 6 ∈ ℝ
31		1lt6 12477	. . . . . . . . . . . 12 ⊢ 1 < 6
32	29, 30, 31	ltleii 11382	. . . . . . . . . . 11 ⊢ 1 ≤ 6
33		elfz1b 13673	. . . . . . . . . . 11 ⊢ (1 ∈ (1...6) ↔ (1 ∈ ℕ ∧ 6 ∈ ℕ ∧ 1 ≤ 6))
34	27, 28, 32, 33	mpbir3an 1360	. . . . . . . . . 10 ⊢ 1 ∈ (1...6)
35		iftrue 4488	. . . . . . . . . . 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 6995	. . . . . . . . . 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 2811	. . . . . . . 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 2805	. . . . . . 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 50872	. . . . . . . . 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 6885	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...6)) ∧ 𝑥 = 2) → ((veronese‘𝑃)‘𝑥) = ((veronese‘𝑃)‘2))
44	42	fveq2d 6885	. . . . . . . . 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 12363	. . . . . . . . . . 11 ⊢ 2 ∈ ℕ
46		2re 12364	. . . . . . . . . . . 12 ⊢ 2 ∈ ℝ
47		2lt6 12476	. . . . . . . . . . . 12 ⊢ 2 < 6
48	46, 30, 47	ltleii 11382	. . . . . . . . . . 11 ⊢ 2 ≤ 6
49		elfz1b 13673	. . . . . . . . . . 11 ⊢ (2 ∈ (1...6) ↔ (2 ∈ ℕ ∧ 6 ∈ ℕ ∧ 2 ≤ 6))
50	45, 28, 48, 49	mpbir3an 1360	. . . . . . . . . 10 ⊢ 2 ∈ (1...6)
51		1ne2 12500	. . . . . . . . . . . . . . . 16 ⊢ 1 ≠ 2
52	51	necomi 3009	. . . . . . . . . . . . . . 15 ⊢ 2 ≠ 1
53		neeq1 3017	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 2 → (𝑘 ≠ 1 ↔ 2 ≠ 1))
54	52, 53	mpbiri 261	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 2 → 𝑘 ≠ 1)
55	54	neneqd 2960	. . . . . . . . . . . . 13 ⊢ (𝑘 = 2 → ¬ 𝑘 = 1)
56	55	iffalsed 4493	. . . . . . . . . . . 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 4488	. . . . . . . . . . . 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 2795	. . . . . . . . . . 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 6995	. . . . . . . . . 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 2811	. . . . . . . 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 2805	. . . . . . 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 50873	. . . . . . . 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 6885	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...6)) ∧ 𝑥 = 3) → ((veronese‘𝑃)‘𝑥) = ((veronese‘𝑃)‘3))
68	66	fveq2d 6885	. . . . . . . 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 12369	. . . . . . . . . 10 ⊢ 3 ∈ ℕ
70		3re 12370	. . . . . . . . . . 11 ⊢ 3 ∈ ℝ
71		3lt6 12475	. . . . . . . . . . 11 ⊢ 3 < 6
72	70, 30, 71	ltleii 11382	. . . . . . . . . 10 ⊢ 3 ≤ 6
73		elfz1b 13673	. . . . . . . . . 10 ⊢ (3 ∈ (1...6) ↔ (3 ∈ ℕ ∧ 6 ∈ ℕ ∧ 3 ≤ 6))
74	69, 28, 72, 73	mpbir3an 1360	. . . . . . . . 9 ⊢ 3 ∈ (1...6)
75		1ne3 50839	. . . . . . . . . . . . . . 15 ⊢ 1 ≠ 3
76	75	necomi 3009	. . . . . . . . . . . . . 14 ⊢ 3 ≠ 1
77		neeq1 3017	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 3 → (𝑘 ≠ 1 ↔ 3 ≠ 1))
78	76, 77	mpbiri 261	. . . . . . . . . . . . 13 ⊢ (𝑘 = 3 → 𝑘 ≠ 1)
79	78	neneqd 2960	. . . . . . . . . . . 12 ⊢ (𝑘 = 3 → ¬ 𝑘 = 1)
80	79	iffalsed 4493	. . . . . . . . . . 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 50840	. . . . . . . . . . . . . . 15 ⊢ 2 ≠ 3
82	81	necomi 3009	. . . . . . . . . . . . . 14 ⊢ 3 ≠ 2
83		neeq1 3017	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 3 → (𝑘 ≠ 2 ↔ 3 ≠ 2))
84	82, 83	mpbiri 261	. . . . . . . . . . . . 13 ⊢ (𝑘 = 3 → 𝑘 ≠ 2)
85	84	neneqd 2960	. . . . . . . . . . . 12 ⊢ (𝑘 = 3 → ¬ 𝑘 = 2)
86	85	iffalsed 4493	. . . . . . . . . . 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 4488	. . . . . . . . . . 11 ⊢ (𝑘 = 3 → if(𝑘 = 3, ((𝑃‘3)↑2), if(𝑘 = 4, ((𝑃‘1) · (𝑃‘2)), if(𝑘 = 5, ((𝑃‘2) · (𝑃‘3)), ((𝑃‘3) · (𝑃‘1))))) = ((𝑃‘3)↑2))
88	80, 86, 87	3eqtrd 2799	. . . . . . . . . 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 6995	. . . . . . . . 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 2811	. . . . . . 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 2805	. . . . . 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 50874	. . . . . . 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 6885	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...6)) ∧ 𝑥 = 4) → ((veronese‘𝑃)‘𝑥) = ((veronese‘𝑃)‘4))
98	96	fveq2d 6885	. . . . . . 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 12373	. . . . . . . . 9 ⊢ 4 ∈ ℕ
100		4re 12374	. . . . . . . . . 10 ⊢ 4 ∈ ℝ
101		4lt6 12474	. . . . . . . . . 10 ⊢ 4 < 6
102	100, 30, 101	ltleii 11382	. . . . . . . . 9 ⊢ 4 ≤ 6
103		elfz1b 13673	. . . . . . . . 9 ⊢ (4 ∈ (1...6) ↔ (4 ∈ ℕ ∧ 6 ∈ ℕ ∧ 4 ≤ 6))
104	99, 28, 102, 103	mpbir3an 1360	. . . . . . . 8 ⊢ 4 ∈ (1...6)
105		1lt4 12468	. . . . . . . . . . . . . . 15 ⊢ 1 < 4
106	29, 105	gtneii 11371	. . . . . . . . . . . . . 14 ⊢ 4 ≠ 1
107		neeq1 3017	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 4 → (𝑘 ≠ 1 ↔ 4 ≠ 1))
108	106, 107	mpbiri 261	. . . . . . . . . . . . 13 ⊢ (𝑘 = 4 → 𝑘 ≠ 1)
109	108	neneqd 2960	. . . . . . . . . . . 12 ⊢ (𝑘 = 4 → ¬ 𝑘 = 1)
110	109	iffalsed 4493	. . . . . . . . . . 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 12467	. . . . . . . . . . . . . . 15 ⊢ 2 < 4
112	46, 111	gtneii 11371	. . . . . . . . . . . . . 14 ⊢ 4 ≠ 2
113		neeq1 3017	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 4 → (𝑘 ≠ 2 ↔ 4 ≠ 2))
114	112, 113	mpbiri 261	. . . . . . . . . . . . 13 ⊢ (𝑘 = 4 → 𝑘 ≠ 2)
115	114	neneqd 2960	. . . . . . . . . . . 12 ⊢ (𝑘 = 4 → ¬ 𝑘 = 2)
116	115	iffalsed 4493	. . . . . . . . . . 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 2795	. . . . . . . . . 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 12466	. . . . . . . . . . . . . 14 ⊢ 3 < 4
119	70, 118	gtneii 11371	. . . . . . . . . . . . 13 ⊢ 4 ≠ 3
120		neeq1 3017	. . . . . . . . . . . . 13 ⊢ (𝑘 = 4 → (𝑘 ≠ 3 ↔ 4 ≠ 3))
121	119, 120	mpbiri 261	. . . . . . . . . . . 12 ⊢ (𝑘 = 4 → 𝑘 ≠ 3)
122	121	neneqd 2960	. . . . . . . . . . 11 ⊢ (𝑘 = 4 → ¬ 𝑘 = 3)
123	122	iffalsed 4493	. . . . . . . . . 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 4488	. . . . . . . . . 10 ⊢ (𝑘 = 4 → if(𝑘 = 4, ((𝑃‘1) · (𝑃‘2)), if(𝑘 = 5, ((𝑃‘2) · (𝑃‘3)), ((𝑃‘3) · (𝑃‘1)))) = ((𝑃‘1) · (𝑃‘2)))
125	117, 123, 124	3eqtrd 2799	. . . . . . . . 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 6995	. . . . . . . 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 2811	. . . . . 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 2805	. . . . 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 50875	. . . . . 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 6885	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...6)) ∧ 𝑥 = 5) → ((veronese‘𝑃)‘𝑥) = ((veronese‘𝑃)‘5))
135	133	fveq2d 6885	. . . . . 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 12376	. . . . . . . 8 ⊢ 5 ∈ ℕ
137		5re 12377	. . . . . . . . 9 ⊢ 5 ∈ ℝ
138		5lt6 12473	. . . . . . . . 9 ⊢ 5 < 6
139	137, 30, 138	ltleii 11382	. . . . . . . 8 ⊢ 5 ≤ 6
140		elfz1b 13673	. . . . . . . 8 ⊢ (5 ∈ (1...6) ↔ (5 ∈ ℕ ∧ 6 ∈ ℕ ∧ 5 ≤ 6))
141	136, 28, 139, 140	mpbir3an 1360	. . . . . . 7 ⊢ 5 ∈ (1...6)
142		1lt5 12472	. . . . . . . . . . . . . 14 ⊢ 1 < 5
143	29, 142	gtneii 11371	. . . . . . . . . . . . 13 ⊢ 5 ≠ 1
144		neeq1 3017	. . . . . . . . . . . . 13 ⊢ (𝑘 = 5 → (𝑘 ≠ 1 ↔ 5 ≠ 1))
145	143, 144	mpbiri 261	. . . . . . . . . . . 12 ⊢ (𝑘 = 5 → 𝑘 ≠ 1)
146	145	neneqd 2960	. . . . . . . . . . 11 ⊢ (𝑘 = 5 → ¬ 𝑘 = 1)
147	146	iffalsed 4493	. . . . . . . . . 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 12471	. . . . . . . . . . . . . 14 ⊢ 2 < 5
149	46, 148	gtneii 11371	. . . . . . . . . . . . 13 ⊢ 5 ≠ 2
150		neeq1 3017	. . . . . . . . . . . . 13 ⊢ (𝑘 = 5 → (𝑘 ≠ 2 ↔ 5 ≠ 2))
151	149, 150	mpbiri 261	. . . . . . . . . . . 12 ⊢ (𝑘 = 5 → 𝑘 ≠ 2)
152	151	neneqd 2960	. . . . . . . . . . 11 ⊢ (𝑘 = 5 → ¬ 𝑘 = 2)
153	152	iffalsed 4493	. . . . . . . . . 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 12470	. . . . . . . . . . . . . 14 ⊢ 3 < 5
155	70, 154	gtneii 11371	. . . . . . . . . . . . 13 ⊢ 5 ≠ 3
156		neeq1 3017	. . . . . . . . . . . . 13 ⊢ (𝑘 = 5 → (𝑘 ≠ 3 ↔ 5 ≠ 3))
157	155, 156	mpbiri 261	. . . . . . . . . . . 12 ⊢ (𝑘 = 5 → 𝑘 ≠ 3)
158	157	neneqd 2960	. . . . . . . . . . 11 ⊢ (𝑘 = 5 → ¬ 𝑘 = 3)
159	158	iffalsed 4493	. . . . . . . . . 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 2799	. . . . . . . . 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 12469	. . . . . . . . . . . . 13 ⊢ 4 < 5
162	100, 161	gtneii 11371	. . . . . . . . . . . 12 ⊢ 5 ≠ 4
163		neeq1 3017	. . . . . . . . . . . 12 ⊢ (𝑘 = 5 → (𝑘 ≠ 4 ↔ 5 ≠ 4))
164	162, 163	mpbiri 261	. . . . . . . . . . 11 ⊢ (𝑘 = 5 → 𝑘 ≠ 4)
165	164	neneqd 2960	. . . . . . . . . 10 ⊢ (𝑘 = 5 → ¬ 𝑘 = 4)
166	165	iffalsed 4493	. . . . . . . . 9 ⊢ (𝑘 = 5 → if(𝑘 = 4, ((𝑃‘1) · (𝑃‘2)), if(𝑘 = 5, ((𝑃‘2) · (𝑃‘3)), ((𝑃‘3) · (𝑃‘1)))) = if(𝑘 = 5, ((𝑃‘2) · (𝑃‘3)), ((𝑃‘3) · (𝑃‘1))))
167		iftrue 4488	. . . . . . . . 9 ⊢ (𝑘 = 5 → if(𝑘 = 5, ((𝑃‘2) · (𝑃‘3)), ((𝑃‘3) · (𝑃‘1))) = ((𝑃‘2) · (𝑃‘3)))
168	160, 166, 167	3eqtrd 2799	. . . . . . . 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 6995	. . . . . . 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 2811	. . . . 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 2805	. . . 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 50876	. . . . 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 6885	. . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...6)) ∧ 𝑥 = 6) → ((veronese‘𝑃)‘𝑥) = ((veronese‘𝑃)‘6))
178	176	fveq2d 6885	. . . . 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 11797	. . . . . . 7 ⊢ 6 ≤ 6
180		elfz1b 13673	. . . . . . 7 ⊢ (6 ∈ (1...6) ↔ (6 ∈ ℕ ∧ 6 ∈ ℕ ∧ 6 ≤ 6))
181	28, 28, 179, 180	mpbir3an 1360	. . . . . 6 ⊢ 6 ∈ (1...6)
182	29, 31	gtneii 11371	. . . . . . . . . . . 12 ⊢ 6 ≠ 1
183		neeq1 3017	. . . . . . . . . . . 12 ⊢ (𝑘 = 6 → (𝑘 ≠ 1 ↔ 6 ≠ 1))
184	182, 183	mpbiri 261	. . . . . . . . . . 11 ⊢ (𝑘 = 6 → 𝑘 ≠ 1)
185	184	neneqd 2960	. . . . . . . . . 10 ⊢ (𝑘 = 6 → ¬ 𝑘 = 1)
186	185	iffalsed 4493	. . . . . . . . 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 11371	. . . . . . . . . . . 12 ⊢ 6 ≠ 2
188		neeq1 3017	. . . . . . . . . . . 12 ⊢ (𝑘 = 6 → (𝑘 ≠ 2 ↔ 6 ≠ 2))
189	187, 188	mpbiri 261	. . . . . . . . . . 11 ⊢ (𝑘 = 6 → 𝑘 ≠ 2)
190	189	neneqd 2960	. . . . . . . . . 10 ⊢ (𝑘 = 6 → ¬ 𝑘 = 2)
191	190	iffalsed 4493	. . . . . . . . 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 11371	. . . . . . . . . . . 12 ⊢ 6 ≠ 3
193		neeq1 3017	. . . . . . . . . . . 12 ⊢ (𝑘 = 6 → (𝑘 ≠ 3 ↔ 6 ≠ 3))
194	192, 193	mpbiri 261	. . . . . . . . . . 11 ⊢ (𝑘 = 6 → 𝑘 ≠ 3)
195	194	neneqd 2960	. . . . . . . . . 10 ⊢ (𝑘 = 6 → ¬ 𝑘 = 3)
196	195	iffalsed 4493	. . . . . . . . 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 2799	. . . . . . . 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 11371	. . . . . . . . . . 11 ⊢ 6 ≠ 4
199		neeq1 3017	. . . . . . . . . . 11 ⊢ (𝑘 = 6 → (𝑘 ≠ 4 ↔ 6 ≠ 4))
200	198, 199	mpbiri 261	. . . . . . . . . 10 ⊢ (𝑘 = 6 → 𝑘 ≠ 4)
201	200	neneqd 2960	. . . . . . . . 9 ⊢ (𝑘 = 6 → ¬ 𝑘 = 4)
202	201	iffalsed 4493	. . . . . . . 8 ⊢ (𝑘 = 6 → if(𝑘 = 4, ((𝑃‘1) · (𝑃‘2)), if(𝑘 = 5, ((𝑃‘2) · (𝑃‘3)), ((𝑃‘3) · (𝑃‘1)))) = if(𝑘 = 5, ((𝑃‘2) · (𝑃‘3)), ((𝑃‘3) · (𝑃‘1))))
203	137, 138	gtneii 11371	. . . . . . . . . . 11 ⊢ 6 ≠ 5
204		neeq1 3017	. . . . . . . . . . 11 ⊢ (𝑘 = 6 → (𝑘 ≠ 5 ↔ 6 ≠ 5))
205	203, 204	mpbiri 261	. . . . . . . . . 10 ⊢ (𝑘 = 6 → 𝑘 ≠ 5)
206	205	neneqd 2960	. . . . . . . . 9 ⊢ (𝑘 = 6 → ¬ 𝑘 = 5)
207	206	iffalsed 4493	. . . . . . . 8 ⊢ (𝑘 = 6 → if(𝑘 = 5, ((𝑃‘2) · (𝑃‘3)), ((𝑃‘3) · (𝑃‘1))) = ((𝑃‘3) · (𝑃‘1)))
208	197, 202, 207	3eqtrd 2799	. . . . . . 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 6995	. . . . . 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 2811	. . . 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 2805	. . 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 12952	. . . . . . . 8 ⊢ (5 ∈ ℕ ↔ 5 ∈ (ℤ_≥‘1))
215	136, 214	mpbi 233	. . . . . . 7 ⊢ 5 ∈ (ℤ_≥‘1)
216		elfzp1 13654	. . . . . . 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 12436	. . . . . . . 8 ⊢ (5 + 1) = 6
219	218	oveq2i 7427	. . . . . . 7 ⊢ (1...(5 + 1)) = (1...6)
220	219	eleq2i 2852	. . . . . 6 ⊢ (𝑥 ∈ (1...(5 + 1)) ↔ 𝑥 ∈ (1...6))
221	218	eqeq2i 2773	. . . . . . 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 12952	. . . . . . . . . 10 ⊢ (4 ∈ ℕ ↔ 4 ∈ (ℤ_≥‘1))
225	99, 224	mpbi 233	. . . . . . . . 9 ⊢ 4 ∈ (ℤ_≥‘1)
226		elfzp1 13654	. . . . . . . . 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 12435	. . . . . . . . . 10 ⊢ (4 + 1) = 5
229	228	oveq2i 7427	. . . . . . . . 9 ⊢ (1...(4 + 1)) = (1...5)
230	229	eleq2i 2852	. . . . . . . 8 ⊢ (𝑥 ∈ (1...(4 + 1)) ↔ 𝑥 ∈ (1...5))
231	228	eqeq2i 2773	. . . . . . . . 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 12952	. . . . . . . . . . . 12 ⊢ (3 ∈ ℕ ↔ 3 ∈ (ℤ_≥‘1))
235	69, 234	mpbi 233	. . . . . . . . . . 11 ⊢ 3 ∈ (ℤ_≥‘1)
236		elfzp1 13654	. . . . . . . . . . 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 12434	. . . . . . . . . . . 12 ⊢ (3 + 1) = 4
239	238	oveq2i 7427	. . . . . . . . . . 11 ⊢ (1...(3 + 1)) = (1...4)
240	239	eleq2i 2852	. . . . . . . . . 10 ⊢ (𝑥 ∈ (1...(3 + 1)) ↔ 𝑥 ∈ (1...4))
241	238	eqeq2i 2773	. . . . . . . . . . 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 12956	. . . . . . . . . . . . 13 ⊢ 2 ∈ (ℤ_≥‘1)
245		elfzp1 13654	. . . . . . . . . . . . 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 12431	. . . . . . . . . . . . . 14 ⊢ (2 + 1) = 3
248	247	oveq2i 7427	. . . . . . . . . . . . 13 ⊢ (1...(2 + 1)) = (1...3)
249	248	eleq2i 2852	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (1...(2 + 1)) ↔ 𝑥 ∈ (1...3))
250	247	eqeq2i 2773	. . . . . . . . . . . . 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 12952	. . . . . . . . . . . . . . . 16 ⊢ (1 ∈ ℕ ↔ 1 ∈ (ℤ_≥‘1))
254	27, 253	mpbi 233	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ (ℤ_≥‘1)
255		elfzp1 13654	. . . . . . . . . . . . . . 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 12413	. . . . . . . . . . . . . . . 16 ⊢ (1 + 1) = 2
258	257	oveq2i 7427	. . . . . . . . . . . . . . 15 ⊢ (1...(1 + 1)) = (1...2)
259	258	eleq2i 2852	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (1...(1 + 1)) ↔ 𝑥 ∈ (1...2))
260	257	eqeq2i 2773	. . . . . . . . . . . . . . 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 13614	. . . . . . . . . . . . . 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 7028	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 2145 ≠ wne 2955 ifcif 4482 class class class wbr 5103 ↦ cmpt 5186 Fn wfn 6530 ‘cfv 6535 (class class class)co 7416 ↑_m cmap 8833 ℝcr 11148 0cc0 11149 1c1 11150 + caddc 11152 · cmul 11154 ≤ cle 11293 ℕcn 12282 2c2 12344 3c3 12345 4c4 12346 5c5 12347 6c6 12348 ℤ_≥cuz 12912 ...cfz 13586 ↑cexp 14150 veronesecveronese 50866

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 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2732 ax-rep 5232 ax-sep 5251 ax-nul 5263 ax-pow 5330 ax-pr 5398 ax-un 7742 ax-cnex 11205 ax-resscn 11206 ax-1cn 11207 ax-icn 11208 ax-addcl 11209 ax-addrcl 11210 ax-mulcl 11211 ax-mulrcl 11212 ax-mulcom 11213 ax-addass 11214 ax-mulass 11215 ax-distr 11216 ax-i2m1 11217 ax-1ne0 11218 ax-1rid 11219 ax-rnegex 11220 ax-rrecex 11221 ax-cnre 11222 ax-pre-lttri 11223 ax-pre-lttrn 11224 ax-pre-ltadd 11225 ax-pre-mulgt0 11226

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 2100 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4868 df-iun 4953 df-br 5104 df-opab 5168 df-mpt 5187 df-tr 5213 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 6301 df-ord 6362 df-on 6363 df-lim 6364 df-suc 6365 df-iota 6491 df-fun 6537 df-fn 6538 df-f 6539 df-f1 6540 df-fo 6541 df-f1o 6542 df-fv 6543 df-riota 7373 df-ov 7419 df-oprab 7420 df-mpo 7421 df-om 7869 df-1st 7992 df-2nd 7993 df-frecs 8285 df-wrecs 8316 df-recs 8365 df-rdg 8404 df-er 8703 df-map 8835 df-en 8960 df-dom 8961 df-sdom 8962 df-pnf 11294 df-mnf 11295 df-xr 11296 df-ltxr 11297 df-le 11298 df-sub 11492 df-neg 11493 df-nn 12283 df-2 12352 df-3 12353 df-4 12354 df-5 12355 df-6 12356 df-n0 12554 df-z 12641 df-uz 12913 df-fz 13587 df-seq 14091 df-exp 14151 df-veronese 50867

This theorem is used by: veronesematrowexpd 50880

W3C validator