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 50794

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 2762	. . . 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 6679	. . 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 50786	. . . 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 6629	. . 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 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 2762	. . . 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 6679	. . 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 50788	. . . . . . . . 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 6886	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...6)) ∧ 𝑥 = 1) → ((veronese‘𝑃)‘𝑥) = ((veronese‘𝑃)‘1))
26	24	fveq2d 6886	. . . . . . . . 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 12269	. . . . . . . . . . 11 ⊢ 1 ∈ ℕ
28		6nn 12355	. . . . . . . . . . 11 ⊢ 6 ∈ ℕ
29		1re 11233	. . . . . . . . . . . 12 ⊢ 1 ∈ ℝ
30		6re 12356	. . . . . . . . . . . 12 ⊢ 6 ∈ ℝ
31		1lt6 12453	. . . . . . . . . . . 12 ⊢ 1 < 6
32	29, 30, 31	ltleii 11358	. . . . . . . . . . 11 ⊢ 1 ≤ 6
33		elfz1b 13648	. . . . . . . . . . 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 6996	. . . . . . . . . 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 2813	. . . . . . . 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 2807	. . . . . . 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 50789	. . . . . . . . 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 6886	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...6)) ∧ 𝑥 = 2) → ((veronese‘𝑃)‘𝑥) = ((veronese‘𝑃)‘2))
44	42	fveq2d 6886	. . . . . . . . 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 12339	. . . . . . . . . . 11 ⊢ 2 ∈ ℕ
46		2re 12340	. . . . . . . . . . . 12 ⊢ 2 ∈ ℝ
47		2lt6 12452	. . . . . . . . . . . 12 ⊢ 2 < 6
48	46, 30, 47	ltleii 11358	. . . . . . . . . . 11 ⊢ 2 ≤ 6
49		elfz1b 13648	. . . . . . . . . . 11 ⊢ (2 ∈ (1...6) ↔ (2 ∈ ℕ ∧ 6 ∈ ℕ ∧ 2 ≤ 6))
50	45, 28, 48, 49	mpbir3an 1360	. . . . . . . . . 10 ⊢ 2 ∈ (1...6)
51		1ne2 12476	. . . . . . . . . . . . . . . 16 ⊢ 1 ≠ 2
52	51	necomi 3011	. . . . . . . . . . . . . . 15 ⊢ 2 ≠ 1
53		neeq1 3019	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 2 → (𝑘 ≠ 1 ↔ 2 ≠ 1))
54	52, 53	mpbiri 261	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 2 → 𝑘 ≠ 1)
55	54	neneqd 2962	. . . . . . . . . . . . 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 2797	. . . . . . . . . . 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 6996	. . . . . . . . . 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 2813	. . . . . . . 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 2807	. . . . . . 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 50790	. . . . . . . 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 6886	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...6)) ∧ 𝑥 = 3) → ((veronese‘𝑃)‘𝑥) = ((veronese‘𝑃)‘3))
68	66	fveq2d 6886	. . . . . . . 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 12345	. . . . . . . . . 10 ⊢ 3 ∈ ℕ
70		3re 12346	. . . . . . . . . . 11 ⊢ 3 ∈ ℝ
71		3lt6 12451	. . . . . . . . . . 11 ⊢ 3 < 6
72	70, 30, 71	ltleii 11358	. . . . . . . . . 10 ⊢ 3 ≤ 6
73		elfz1b 13648	. . . . . . . . . 10 ⊢ (3 ∈ (1...6) ↔ (3 ∈ ℕ ∧ 6 ∈ ℕ ∧ 3 ≤ 6))
74	69, 28, 72, 73	mpbir3an 1360	. . . . . . . . 9 ⊢ 3 ∈ (1...6)
75		1ne3 50756	. . . . . . . . . . . . . . 15 ⊢ 1 ≠ 3
76	75	necomi 3011	. . . . . . . . . . . . . 14 ⊢ 3 ≠ 1
77		neeq1 3019	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 3 → (𝑘 ≠ 1 ↔ 3 ≠ 1))
78	76, 77	mpbiri 261	. . . . . . . . . . . . 13 ⊢ (𝑘 = 3 → 𝑘 ≠ 1)
79	78	neneqd 2962	. . . . . . . . . . . 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 50757	. . . . . . . . . . . . . . 15 ⊢ 2 ≠ 3
82	81	necomi 3011	. . . . . . . . . . . . . 14 ⊢ 3 ≠ 2
83		neeq1 3019	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 3 → (𝑘 ≠ 2 ↔ 3 ≠ 2))
84	82, 83	mpbiri 261	. . . . . . . . . . . . 13 ⊢ (𝑘 = 3 → 𝑘 ≠ 2)
85	84	neneqd 2962	. . . . . . . . . . . 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 2801	. . . . . . . . . 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 6996	. . . . . . . . 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 2813	. . . . . . 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 2807	. . . . . 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 50791	. . . . . . 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 6886	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...6)) ∧ 𝑥 = 4) → ((veronese‘𝑃)‘𝑥) = ((veronese‘𝑃)‘4))
98	96	fveq2d 6886	. . . . . . 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 12349	. . . . . . . . 9 ⊢ 4 ∈ ℕ
100		4re 12350	. . . . . . . . . 10 ⊢ 4 ∈ ℝ
101		4lt6 12450	. . . . . . . . . 10 ⊢ 4 < 6
102	100, 30, 101	ltleii 11358	. . . . . . . . 9 ⊢ 4 ≤ 6
103		elfz1b 13648	. . . . . . . . 9 ⊢ (4 ∈ (1...6) ↔ (4 ∈ ℕ ∧ 6 ∈ ℕ ∧ 4 ≤ 6))
104	99, 28, 102, 103	mpbir3an 1360	. . . . . . . 8 ⊢ 4 ∈ (1...6)
105		1lt4 12444	. . . . . . . . . . . . . . 15 ⊢ 1 < 4
106	29, 105	gtneii 11347	. . . . . . . . . . . . . 14 ⊢ 4 ≠ 1
107		neeq1 3019	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 4 → (𝑘 ≠ 1 ↔ 4 ≠ 1))
108	106, 107	mpbiri 261	. . . . . . . . . . . . 13 ⊢ (𝑘 = 4 → 𝑘 ≠ 1)
109	108	neneqd 2962	. . . . . . . . . . . 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 12443	. . . . . . . . . . . . . . 15 ⊢ 2 < 4
112	46, 111	gtneii 11347	. . . . . . . . . . . . . 14 ⊢ 4 ≠ 2
113		neeq1 3019	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 4 → (𝑘 ≠ 2 ↔ 4 ≠ 2))
114	112, 113	mpbiri 261	. . . . . . . . . . . . 13 ⊢ (𝑘 = 4 → 𝑘 ≠ 2)
115	114	neneqd 2962	. . . . . . . . . . . 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 2797	. . . . . . . . . 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 12442	. . . . . . . . . . . . . 14 ⊢ 3 < 4
119	70, 118	gtneii 11347	. . . . . . . . . . . . 13 ⊢ 4 ≠ 3
120		neeq1 3019	. . . . . . . . . . . . 13 ⊢ (𝑘 = 4 → (𝑘 ≠ 3 ↔ 4 ≠ 3))
121	119, 120	mpbiri 261	. . . . . . . . . . . 12 ⊢ (𝑘 = 4 → 𝑘 ≠ 3)
122	121	neneqd 2962	. . . . . . . . . . 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 2801	. . . . . . . . 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 6996	. . . . . . . 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 2813	. . . . . 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 2807	. . . . 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 50792	. . . . . 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 6886	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...6)) ∧ 𝑥 = 5) → ((veronese‘𝑃)‘𝑥) = ((veronese‘𝑃)‘5))
135	133	fveq2d 6886	. . . . . 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 12352	. . . . . . . 8 ⊢ 5 ∈ ℕ
137		5re 12353	. . . . . . . . 9 ⊢ 5 ∈ ℝ
138		5lt6 12449	. . . . . . . . 9 ⊢ 5 < 6
139	137, 30, 138	ltleii 11358	. . . . . . . 8 ⊢ 5 ≤ 6
140		elfz1b 13648	. . . . . . . 8 ⊢ (5 ∈ (1...6) ↔ (5 ∈ ℕ ∧ 6 ∈ ℕ ∧ 5 ≤ 6))
141	136, 28, 139, 140	mpbir3an 1360	. . . . . . 7 ⊢ 5 ∈ (1...6)
142		1lt5 12448	. . . . . . . . . . . . . 14 ⊢ 1 < 5
143	29, 142	gtneii 11347	. . . . . . . . . . . . 13 ⊢ 5 ≠ 1
144		neeq1 3019	. . . . . . . . . . . . 13 ⊢ (𝑘 = 5 → (𝑘 ≠ 1 ↔ 5 ≠ 1))
145	143, 144	mpbiri 261	. . . . . . . . . . . 12 ⊢ (𝑘 = 5 → 𝑘 ≠ 1)
146	145	neneqd 2962	. . . . . . . . . . 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 12447	. . . . . . . . . . . . . 14 ⊢ 2 < 5
149	46, 148	gtneii 11347	. . . . . . . . . . . . 13 ⊢ 5 ≠ 2
150		neeq1 3019	. . . . . . . . . . . . 13 ⊢ (𝑘 = 5 → (𝑘 ≠ 2 ↔ 5 ≠ 2))
151	149, 150	mpbiri 261	. . . . . . . . . . . 12 ⊢ (𝑘 = 5 → 𝑘 ≠ 2)
152	151	neneqd 2962	. . . . . . . . . . 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 12446	. . . . . . . . . . . . . 14 ⊢ 3 < 5
155	70, 154	gtneii 11347	. . . . . . . . . . . . 13 ⊢ 5 ≠ 3
156		neeq1 3019	. . . . . . . . . . . . 13 ⊢ (𝑘 = 5 → (𝑘 ≠ 3 ↔ 5 ≠ 3))
157	155, 156	mpbiri 261	. . . . . . . . . . . 12 ⊢ (𝑘 = 5 → 𝑘 ≠ 3)
158	157	neneqd 2962	. . . . . . . . . . 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 2801	. . . . . . . . 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 12445	. . . . . . . . . . . . 13 ⊢ 4 < 5
162	100, 161	gtneii 11347	. . . . . . . . . . . 12 ⊢ 5 ≠ 4
163		neeq1 3019	. . . . . . . . . . . 12 ⊢ (𝑘 = 5 → (𝑘 ≠ 4 ↔ 5 ≠ 4))
164	162, 163	mpbiri 261	. . . . . . . . . . 11 ⊢ (𝑘 = 5 → 𝑘 ≠ 4)
165	164	neneqd 2962	. . . . . . . . . 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 2801	. . . . . . . 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 6996	. . . . . . 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 2813	. . . . 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 2807	. . . 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 50793	. . . . 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 6886	. . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...6)) ∧ 𝑥 = 6) → ((veronese‘𝑃)‘𝑥) = ((veronese‘𝑃)‘6))
178	176	fveq2d 6886	. . . . 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 11773	. . . . . . 7 ⊢ 6 ≤ 6
180		elfz1b 13648	. . . . . . 7 ⊢ (6 ∈ (1...6) ↔ (6 ∈ ℕ ∧ 6 ∈ ℕ ∧ 6 ≤ 6))
181	28, 28, 179, 180	mpbir3an 1360	. . . . . 6 ⊢ 6 ∈ (1...6)
182	29, 31	gtneii 11347	. . . . . . . . . . . 12 ⊢ 6 ≠ 1
183		neeq1 3019	. . . . . . . . . . . 12 ⊢ (𝑘 = 6 → (𝑘 ≠ 1 ↔ 6 ≠ 1))
184	182, 183	mpbiri 261	. . . . . . . . . . 11 ⊢ (𝑘 = 6 → 𝑘 ≠ 1)
185	184	neneqd 2962	. . . . . . . . . 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 11347	. . . . . . . . . . . 12 ⊢ 6 ≠ 2
188		neeq1 3019	. . . . . . . . . . . 12 ⊢ (𝑘 = 6 → (𝑘 ≠ 2 ↔ 6 ≠ 2))
189	187, 188	mpbiri 261	. . . . . . . . . . 11 ⊢ (𝑘 = 6 → 𝑘 ≠ 2)
190	189	neneqd 2962	. . . . . . . . . 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 11347	. . . . . . . . . . . 12 ⊢ 6 ≠ 3
193		neeq1 3019	. . . . . . . . . . . 12 ⊢ (𝑘 = 6 → (𝑘 ≠ 3 ↔ 6 ≠ 3))
194	192, 193	mpbiri 261	. . . . . . . . . . 11 ⊢ (𝑘 = 6 → 𝑘 ≠ 3)
195	194	neneqd 2962	. . . . . . . . . 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 2801	. . . . . . . 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 11347	. . . . . . . . . . 11 ⊢ 6 ≠ 4
199		neeq1 3019	. . . . . . . . . . 11 ⊢ (𝑘 = 6 → (𝑘 ≠ 4 ↔ 6 ≠ 4))
200	198, 199	mpbiri 261	. . . . . . . . . 10 ⊢ (𝑘 = 6 → 𝑘 ≠ 4)
201	200	neneqd 2962	. . . . . . . . 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 11347	. . . . . . . . . . 11 ⊢ 6 ≠ 5
204		neeq1 3019	. . . . . . . . . . 11 ⊢ (𝑘 = 6 → (𝑘 ≠ 5 ↔ 6 ≠ 5))
205	203, 204	mpbiri 261	. . . . . . . . . 10 ⊢ (𝑘 = 6 → 𝑘 ≠ 5)
206	205	neneqd 2962	. . . . . . . . 9 ⊢ (𝑘 = 6 → ¬ 𝑘 = 5)
207	206	iffalsed 4496	. . . . . . . 8 ⊢ (𝑘 = 6 → if(𝑘 = 5, ((𝑃‘2) · (𝑃‘3)), ((𝑃‘3) · (𝑃‘1))) = ((𝑃‘3) · (𝑃‘1)))
208	197, 202, 207	3eqtrd 2801	. . . . . . 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 6996	. . . . . 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 2813	. . . 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 2807	. . 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 12928	. . . . . . . 8 ⊢ (5 ∈ ℕ ↔ 5 ∈ (ℤ_≥‘1))
215	136, 214	mpbi 233	. . . . . . 7 ⊢ 5 ∈ (ℤ_≥‘1)
216		elfzp1 13629	. . . . . . 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 12412	. . . . . . . 8 ⊢ (5 + 1) = 6
219	218	oveq2i 7427	. . . . . . 7 ⊢ (1...(5 + 1)) = (1...6)
220	219	eleq2i 2854	. . . . . 6 ⊢ (𝑥 ∈ (1...(5 + 1)) ↔ 𝑥 ∈ (1...6))
221	218	eqeq2i 2775	. . . . . . 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 12928	. . . . . . . . . 10 ⊢ (4 ∈ ℕ ↔ 4 ∈ (ℤ_≥‘1))
225	99, 224	mpbi 233	. . . . . . . . 9 ⊢ 4 ∈ (ℤ_≥‘1)
226		elfzp1 13629	. . . . . . . . 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 12411	. . . . . . . . . 10 ⊢ (4 + 1) = 5
229	228	oveq2i 7427	. . . . . . . . 9 ⊢ (1...(4 + 1)) = (1...5)
230	229	eleq2i 2854	. . . . . . . 8 ⊢ (𝑥 ∈ (1...(4 + 1)) ↔ 𝑥 ∈ (1...5))
231	228	eqeq2i 2775	. . . . . . . . 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 12928	. . . . . . . . . . . 12 ⊢ (3 ∈ ℕ ↔ 3 ∈ (ℤ_≥‘1))
235	69, 234	mpbi 233	. . . . . . . . . . 11 ⊢ 3 ∈ (ℤ_≥‘1)
236		elfzp1 13629	. . . . . . . . . . 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 12410	. . . . . . . . . . . 12 ⊢ (3 + 1) = 4
239	238	oveq2i 7427	. . . . . . . . . . 11 ⊢ (1...(3 + 1)) = (1...4)
240	239	eleq2i 2854	. . . . . . . . . 10 ⊢ (𝑥 ∈ (1...(3 + 1)) ↔ 𝑥 ∈ (1...4))
241	238	eqeq2i 2775	. . . . . . . . . . 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 12932	. . . . . . . . . . . . 13 ⊢ 2 ∈ (ℤ_≥‘1)
245		elfzp1 13629	. . . . . . . . . . . . 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 12407	. . . . . . . . . . . . . 14 ⊢ (2 + 1) = 3
248	247	oveq2i 7427	. . . . . . . . . . . . 13 ⊢ (1...(2 + 1)) = (1...3)
249	248	eleq2i 2854	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (1...(2 + 1)) ↔ 𝑥 ∈ (1...3))
250	247	eqeq2i 2775	. . . . . . . . . . . . 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 12928	. . . . . . . . . . . . . . . 16 ⊢ (1 ∈ ℕ ↔ 1 ∈ (ℤ_≥‘1))
254	27, 253	mpbi 233	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ (ℤ_≥‘1)
255		elfzp1 13629	. . . . . . . . . . . . . . 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 12389	. . . . . . . . . . . . . . . 16 ⊢ (1 + 1) = 2
258	257	oveq2i 7427	. . . . . . . . . . . . . . 15 ⊢ (1...(1 + 1)) = (1...2)
259	258	eleq2i 2854	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (1...(1 + 1)) ↔ 𝑥 ∈ (1...2))
260	257	eqeq2i 2775	. . . . . . . . . . . . . . 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 13589	. . . . . . . . . . . . . 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 7029	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 2957 ifcif 4485 class class class wbr 5107 ↦ cmpt 5190 Fn wfn 6532 ‘cfv 6537 (class class class)co 7416 ↑_m cmap 8829 ℝcr 11124 0cc0 11125 1c1 11126 + caddc 11128 · cmul 11130 ≤ cle 11269 ℕcn 12258 2c2 12320 3c3 12321 4c4 12322 5c5 12323 6c6 12324 ℤ_≥cuz 12888 ...cfz 13561 ↑cexp 14125 veronesecveronese 50783

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 2215 ax-ext 2734 ax-rep 5236 ax-sep 5255 ax-nul 5267 ax-pow 5334 ax-pr 5402 ax-un 7739 ax-cnex 11181 ax-resscn 11182 ax-1cn 11183 ax-icn 11184 ax-addcl 11185 ax-addrcl 11186 ax-mulcl 11187 ax-mulrcl 11188 ax-mulcom 11189 ax-addass 11190 ax-mulass 11191 ax-distr 11192 ax-i2m1 11193 ax-1ne0 11194 ax-1rid 11195 ax-rnegex 11196 ax-rrecex 11197 ax-cnre 11198 ax-pre-lttri 11199 ax-pre-lttrn 11200 ax-pre-ltadd 11201 ax-pre-mulgt0 11202

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 2566 df-eu 2596 df-clab 2741 df-cleq 2754 df-clel 2837 df-nfc 2911 df-ne 2958 df-nel 3064 df-ral 3079 df-rex 3089 df-reu 3368 df-rab 3415 df-v 3455 df-sbc 3743 df-csb 3851 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-pss 3922 df-nul 4283 df-if 4486 df-pw 4562 df-sn 4588 df-pr 4590 df-op 4594 df-uni 4871 df-iun 4956 df-br 5108 df-opab 5172 df-mpt 5191 df-tr 5217 df-id 5554 df-eprel 5559 df-po 5567 df-so 5568 df-fr 5612 df-we 5614 df-xp 5665 df-rel 5666 df-cnv 5667 df-co 5668 df-dm 5669 df-rn 5670 df-res 5671 df-ima 5672 df-pred 6303 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-riota 7373 df-ov 7419 df-oprab 7420 df-mpo 7421 df-om 7866 df-1st 7989 df-2nd 7990 df-frecs 8283 df-wrecs 8314 df-recs 8363 df-rdg 8402 df-er 8699 df-map 8831 df-en 8956 df-dom 8957 df-sdom 8958 df-pnf 11270 df-mnf 11271 df-xr 11272 df-ltxr 11273 df-le 11274 df-sub 11468 df-neg 11469 df-nn 12259 df-2 12328 df-3 12329 df-4 12330 df-5 12331 df-6 12332 df-n0 12530 df-z 12617 df-uz 12889 df-fz 13562 df-seq 14066 df-exp 14126 df-veronese 50784

This theorem is used by: veronesematrowexpd 50797

W3C validator