broucube - Mathbox for Brendan Leahy

	Mathbox for Brendan Leahy		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > broucube		Structured version Visualization version GIF version

Theorem broucube 37648

Description: Brouwer - or as Kulpa calls it, "Bohl-Brouwer" - fixed point theorem for the unit cube. Theorem on [Kulpa] p. 548. (Contributed by Brendan Leahy, 21-Aug-2020.)

**Hypotheses**
Ref	Expression
poimir.0	⊢ (𝜑 → 𝑁 ∈ ℕ)
poimir.i	⊢ 𝐼 = ((0[,]1) ↑_m (1...𝑁))
poimir.r	⊢ 𝑅 = (∏_t‘((1...𝑁) × {(topGen‘ran (,))}))
broucube.1	⊢ (𝜑 → 𝐹 ∈ ((𝑅 ↾_t 𝐼) Cn (𝑅 ↾_t 𝐼)))

**Assertion**
Ref	Expression
broucube	⊢ (𝜑 → ∃𝑐 ∈ 𝐼 𝑐 = (𝐹‘𝑐))

Distinct variable groups: 𝜑,𝑐 𝐹,𝑐 𝐼,𝑐 𝑁,𝑐 𝑅,𝑐

Proof of Theorem broucube Dummy variables 𝑛 𝑥 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		poimir.0	. . 3 ⊢ (𝜑 → 𝑁 ∈ ℕ)
2		poimir.i	. . 3 ⊢ 𝐼 = ((0[,]1) ↑_m (1...𝑁))
3		poimir.r	. . 3 ⊢ 𝑅 = (∏_t‘((1...𝑁) × {(topGen‘ran (,))}))
4		elmapfn 8838	. . . . . . . 8 ⊢ (𝑥 ∈ ((0[,]1) ↑_m (1...𝑁)) → 𝑥 Fn (1...𝑁))
5	4, 2	eleq2s 2846	. . . . . . 7 ⊢ (𝑥 ∈ 𝐼 → 𝑥 Fn (1...𝑁))
6	5	adantl 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑥 Fn (1...𝑁))
7		broucube.1	. . . . . . . . 9 ⊢ (𝜑 → 𝐹 ∈ ((𝑅 ↾_t 𝐼) Cn (𝑅 ↾_t 𝐼)))
8		ovex 7420	. . . . . . . . . . . . 13 ⊢ (1...𝑁) ∈ V
9		retopon 24651	. . . . . . . . . . . . 13 ⊢ (topGen‘ran (,)) ∈ (TopOn‘ℝ)
10	3	pttoponconst 23484	. . . . . . . . . . . . 13 ⊢ (((1...𝑁) ∈ V ∧ (topGen‘ran (,)) ∈ (TopOn‘ℝ)) → 𝑅 ∈ (TopOn‘(ℝ ↑_m (1...𝑁))))
11	8, 9, 10	mp2an 692	. . . . . . . . . . . 12 ⊢ 𝑅 ∈ (TopOn‘(ℝ ↑_m (1...𝑁)))
12		reex 11159	. . . . . . . . . . . . . 14 ⊢ ℝ ∈ V
13		unitssre 13460	. . . . . . . . . . . . . 14 ⊢ (0[,]1) ⊆ ℝ
14		mapss 8862	. . . . . . . . . . . . . 14 ⊢ ((ℝ ∈ V ∧ (0[,]1) ⊆ ℝ) → ((0[,]1) ↑_m (1...𝑁)) ⊆ (ℝ ↑_m (1...𝑁)))
15	12, 13, 14	mp2an 692	. . . . . . . . . . . . 13 ⊢ ((0[,]1) ↑_m (1...𝑁)) ⊆ (ℝ ↑_m (1...𝑁))
16	2, 15	eqsstri 3993	. . . . . . . . . . . 12 ⊢ 𝐼 ⊆ (ℝ ↑_m (1...𝑁))
17		resttopon 23048	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ (TopOn‘(ℝ ↑_m (1...𝑁))) ∧ 𝐼 ⊆ (ℝ ↑_m (1...𝑁))) → (𝑅 ↾_t 𝐼) ∈ (TopOn‘𝐼))
18	11, 16, 17	mp2an 692	. . . . . . . . . . 11 ⊢ (𝑅 ↾_t 𝐼) ∈ (TopOn‘𝐼)
19	18	toponunii 22803	. . . . . . . . . 10 ⊢ 𝐼 = ∪ (𝑅 ↾_t 𝐼)
20	19, 19	cnf 23133	. . . . . . . . 9 ⊢ (𝐹 ∈ ((𝑅 ↾_t 𝐼) Cn (𝑅 ↾_t 𝐼)) → 𝐹:𝐼⟶𝐼)
21	7, 20	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝐹:𝐼⟶𝐼)
22	21	ffvelcdmda 7056	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝐹‘𝑥) ∈ 𝐼)
23		elmapfn 8838	. . . . . . . 8 ⊢ ((𝐹‘𝑥) ∈ ((0[,]1) ↑_m (1...𝑁)) → (𝐹‘𝑥) Fn (1...𝑁))
24	23, 2	eleq2s 2846	. . . . . . 7 ⊢ ((𝐹‘𝑥) ∈ 𝐼 → (𝐹‘𝑥) Fn (1...𝑁))
25	22, 24	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝐹‘𝑥) Fn (1...𝑁))
26		ovexd 7422	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (1...𝑁) ∈ V)
27		inidm 4190	. . . . . 6 ⊢ ((1...𝑁) ∩ (1...𝑁)) = (1...𝑁)
28		eqidd 2730	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → (𝑥‘𝑛) = (𝑥‘𝑛))
29		eqidd 2730	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → ((𝐹‘𝑥)‘𝑛) = ((𝐹‘𝑥)‘𝑛))
30	6, 25, 26, 26, 27, 28, 29	offval 7662	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑥 ∘_f − (𝐹‘𝑥)) = (𝑛 ∈ (1...𝑁) ↦ ((𝑥‘𝑛) − ((𝐹‘𝑥)‘𝑛))))
31	30	mpteq2dva 5200	. . . 4 ⊢ (𝜑 → (𝑥 ∈ 𝐼 ↦ (𝑥 ∘_f − (𝐹‘𝑥))) = (𝑥 ∈ 𝐼 ↦ (𝑛 ∈ (1...𝑁) ↦ ((𝑥‘𝑛) − ((𝐹‘𝑥)‘𝑛)))))
32	18	a1i 11	. . . . 5 ⊢ (𝜑 → (𝑅 ↾_t 𝐼) ∈ (TopOn‘𝐼))
33		ovexd 7422	. . . . 5 ⊢ (𝜑 → (1...𝑁) ∈ V)
34		retop 24649	. . . . . . 7 ⊢ (topGen‘ran (,)) ∈ Top
35	34	fconst6 6750	. . . . . 6 ⊢ ((1...𝑁) × {(topGen‘ran (,))}):(1...𝑁)⟶Top
36	35	a1i 11	. . . . 5 ⊢ (𝜑 → ((1...𝑁) × {(topGen‘ran (,))}):(1...𝑁)⟶Top)
37	18	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑅 ↾_t 𝐼) ∈ (TopOn‘𝐼))
38		eqid 2729	. . . . . . . . . . . 12 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
39	38	cnfldtop 24671	. . . . . . . . . . 11 ⊢ (TopOpen‘ℂ_fld) ∈ Top
40		cnrest2r 23174	. . . . . . . . . . 11 ⊢ ((TopOpen‘ℂ_fld) ∈ Top → ((𝑅 ↾_t 𝐼) Cn ((TopOpen‘ℂ_fld) ↾_t ℝ)) ⊆ ((𝑅 ↾_t 𝐼) Cn (TopOpen‘ℂ_fld)))
41	39, 40	ax-mp 5	. . . . . . . . . 10 ⊢ ((𝑅 ↾_t 𝐼) Cn ((TopOpen‘ℂ_fld) ↾_t ℝ)) ⊆ ((𝑅 ↾_t 𝐼) Cn (TopOpen‘ℂ_fld))
42		resmpt 6008	. . . . . . . . . . . . 13 ⊢ (𝐼 ⊆ (ℝ ↑_m (1...𝑁)) → ((𝑥 ∈ (ℝ ↑_m (1...𝑁)) ↦ (𝑥‘𝑛)) ↾ 𝐼) = (𝑥 ∈ 𝐼 ↦ (𝑥‘𝑛)))
43	16, 42	ax-mp 5	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ (ℝ ↑_m (1...𝑁)) ↦ (𝑥‘𝑛)) ↾ 𝐼) = (𝑥 ∈ 𝐼 ↦ (𝑥‘𝑛))
44	11	toponunii 22803	. . . . . . . . . . . . . . 15 ⊢ (ℝ ↑_m (1...𝑁)) = ∪ 𝑅
45	44, 3	ptpjcn 23498	. . . . . . . . . . . . . 14 ⊢ (((1...𝑁) ∈ V ∧ ((1...𝑁) × {(topGen‘ran (,))}):(1...𝑁)⟶Top ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ (ℝ ↑_m (1...𝑁)) ↦ (𝑥‘𝑛)) ∈ (𝑅 Cn (((1...𝑁) × {(topGen‘ran (,))})‘𝑛)))
46	8, 35, 45	mp3an12 1453	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ (1...𝑁) → (𝑥 ∈ (ℝ ↑_m (1...𝑁)) ↦ (𝑥‘𝑛)) ∈ (𝑅 Cn (((1...𝑁) × {(topGen‘ran (,))})‘𝑛)))
47	44	cnrest 23172	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ (ℝ ↑_m (1...𝑁)) ↦ (𝑥‘𝑛)) ∈ (𝑅 Cn (((1...𝑁) × {(topGen‘ran (,))})‘𝑛)) ∧ 𝐼 ⊆ (ℝ ↑_m (1...𝑁))) → ((𝑥 ∈ (ℝ ↑_m (1...𝑁)) ↦ (𝑥‘𝑛)) ↾ 𝐼) ∈ ((𝑅 ↾_t 𝐼) Cn (((1...𝑁) × {(topGen‘ran (,))})‘𝑛)))
48	46, 16, 47	sylancl 586	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ (1...𝑁) → ((𝑥 ∈ (ℝ ↑_m (1...𝑁)) ↦ (𝑥‘𝑛)) ↾ 𝐼) ∈ ((𝑅 ↾_t 𝐼) Cn (((1...𝑁) × {(topGen‘ran (,))})‘𝑛)))
49	43, 48	eqeltrrid 2833	. . . . . . . . . . 11 ⊢ (𝑛 ∈ (1...𝑁) → (𝑥 ∈ 𝐼 ↦ (𝑥‘𝑛)) ∈ ((𝑅 ↾_t 𝐼) Cn (((1...𝑁) × {(topGen‘ran (,))})‘𝑛)))
50		fvex 6871	. . . . . . . . . . . . . 14 ⊢ (topGen‘ran (,)) ∈ V
51	50	fvconst2 7178	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ (1...𝑁) → (((1...𝑁) × {(topGen‘ran (,))})‘𝑛) = (topGen‘ran (,)))
52		tgioo4 24693	. . . . . . . . . . . . 13 ⊢ (topGen‘ran (,)) = ((TopOpen‘ℂ_fld) ↾_t ℝ)
53	51, 52	eqtrdi 2780	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ (1...𝑁) → (((1...𝑁) × {(topGen‘ran (,))})‘𝑛) = ((TopOpen‘ℂ_fld) ↾_t ℝ))
54	53	oveq2d 7403	. . . . . . . . . . 11 ⊢ (𝑛 ∈ (1...𝑁) → ((𝑅 ↾_t 𝐼) Cn (((1...𝑁) × {(topGen‘ran (,))})‘𝑛)) = ((𝑅 ↾_t 𝐼) Cn ((TopOpen‘ℂ_fld) ↾_t ℝ)))
55	49, 54	eleqtrd 2830	. . . . . . . . . 10 ⊢ (𝑛 ∈ (1...𝑁) → (𝑥 ∈ 𝐼 ↦ (𝑥‘𝑛)) ∈ ((𝑅 ↾_t 𝐼) Cn ((TopOpen‘ℂ_fld) ↾_t ℝ)))
56	41, 55	sselid 3944	. . . . . . . . 9 ⊢ (𝑛 ∈ (1...𝑁) → (𝑥 ∈ 𝐼 ↦ (𝑥‘𝑛)) ∈ ((𝑅 ↾_t 𝐼) Cn (TopOpen‘ℂ_fld)))
57	56	adantl 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐼 ↦ (𝑥‘𝑛)) ∈ ((𝑅 ↾_t 𝐼) Cn (TopOpen‘ℂ_fld)))
58	21	feqmptd 6929	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐼 ↦ (𝐹‘𝑥)))
59	58, 7	eqeltrrd 2829	. . . . . . . . . 10 ⊢ (𝜑 → (𝑥 ∈ 𝐼 ↦ (𝐹‘𝑥)) ∈ ((𝑅 ↾_t 𝐼) Cn (𝑅 ↾_t 𝐼)))
60	59	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐼 ↦ (𝐹‘𝑥)) ∈ ((𝑅 ↾_t 𝐼) Cn (𝑅 ↾_t 𝐼)))
61		fveq1 6857	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑧 → (𝑥‘𝑛) = (𝑧‘𝑛))
62	61	cbvmptv 5211	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝐼 ↦ (𝑥‘𝑛)) = (𝑧 ∈ 𝐼 ↦ (𝑧‘𝑛))
63	62, 57	eqeltrrid 2833	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑧 ∈ 𝐼 ↦ (𝑧‘𝑛)) ∈ ((𝑅 ↾_t 𝐼) Cn (TopOpen‘ℂ_fld)))
64		fveq1 6857	. . . . . . . . 9 ⊢ (𝑧 = (𝐹‘𝑥) → (𝑧‘𝑛) = ((𝐹‘𝑥)‘𝑛))
65	37, 60, 37, 63, 64	cnmpt11 23550	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐼 ↦ ((𝐹‘𝑥)‘𝑛)) ∈ ((𝑅 ↾_t 𝐼) Cn (TopOpen‘ℂ_fld)))
66	38	subcn 24755	. . . . . . . . 9 ⊢ − ∈ (((TopOpen‘ℂ_fld) ×_t (TopOpen‘ℂ_fld)) Cn (TopOpen‘ℂ_fld))
67	66	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → − ∈ (((TopOpen‘ℂ_fld) ×_t (TopOpen‘ℂ_fld)) Cn (TopOpen‘ℂ_fld)))
68	37, 57, 65, 67	cnmpt12f 23553	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐼 ↦ ((𝑥‘𝑛) − ((𝐹‘𝑥)‘𝑛))) ∈ ((𝑅 ↾_t 𝐼) Cn (TopOpen‘ℂ_fld)))
69		elmapi 8822	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ((0[,]1) ↑_m (1...𝑁)) → 𝑥:(1...𝑁)⟶(0[,]1))
70	69, 2	eleq2s 2846	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ 𝐼 → 𝑥:(1...𝑁)⟶(0[,]1))
71	70	ffvelcdmda 7056	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ 𝐼 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥‘𝑛) ∈ (0[,]1))
72	13, 71	sselid 3944	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ 𝐼 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥‘𝑛) ∈ ℝ)
73	72	adantll 714	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → (𝑥‘𝑛) ∈ ℝ)
74		elmapi 8822	. . . . . . . . . . . . . . 15 ⊢ ((𝐹‘𝑥) ∈ ((0[,]1) ↑_m (1...𝑁)) → (𝐹‘𝑥):(1...𝑁)⟶(0[,]1))
75	74, 2	eleq2s 2846	. . . . . . . . . . . . . 14 ⊢ ((𝐹‘𝑥) ∈ 𝐼 → (𝐹‘𝑥):(1...𝑁)⟶(0[,]1))
76	22, 75	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝐹‘𝑥):(1...𝑁)⟶(0[,]1))
77	76	ffvelcdmda 7056	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → ((𝐹‘𝑥)‘𝑛) ∈ (0[,]1))
78	13, 77	sselid 3944	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → ((𝐹‘𝑥)‘𝑛) ∈ ℝ)
79	73, 78	resubcld 11606	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑥‘𝑛) − ((𝐹‘𝑥)‘𝑛)) ∈ ℝ)
80	79	an32s 652	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐼) → ((𝑥‘𝑛) − ((𝐹‘𝑥)‘𝑛)) ∈ ℝ)
81	80	fmpttd 7087	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐼 ↦ ((𝑥‘𝑛) − ((𝐹‘𝑥)‘𝑛))):𝐼⟶ℝ)
82		frn 6695	. . . . . . . 8 ⊢ ((𝑥 ∈ 𝐼 ↦ ((𝑥‘𝑛) − ((𝐹‘𝑥)‘𝑛))):𝐼⟶ℝ → ran (𝑥 ∈ 𝐼 ↦ ((𝑥‘𝑛) − ((𝐹‘𝑥)‘𝑛))) ⊆ ℝ)
83	38	cnfldtopon 24670	. . . . . . . . 9 ⊢ (TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ)
84		ax-resscn 11125	. . . . . . . . 9 ⊢ ℝ ⊆ ℂ
85		cnrest2 23173	. . . . . . . . 9 ⊢ (((TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ) ∧ ran (𝑥 ∈ 𝐼 ↦ ((𝑥‘𝑛) − ((𝐹‘𝑥)‘𝑛))) ⊆ ℝ ∧ ℝ ⊆ ℂ) → ((𝑥 ∈ 𝐼 ↦ ((𝑥‘𝑛) − ((𝐹‘𝑥)‘𝑛))) ∈ ((𝑅 ↾_t 𝐼) Cn (TopOpen‘ℂ_fld)) ↔ (𝑥 ∈ 𝐼 ↦ ((𝑥‘𝑛) − ((𝐹‘𝑥)‘𝑛))) ∈ ((𝑅 ↾_t 𝐼) Cn ((TopOpen‘ℂ_fld) ↾_t ℝ))))
86	83, 84, 85	mp3an13 1454	. . . . . . . 8 ⊢ (ran (𝑥 ∈ 𝐼 ↦ ((𝑥‘𝑛) − ((𝐹‘𝑥)‘𝑛))) ⊆ ℝ → ((𝑥 ∈ 𝐼 ↦ ((𝑥‘𝑛) − ((𝐹‘𝑥)‘𝑛))) ∈ ((𝑅 ↾_t 𝐼) Cn (TopOpen‘ℂ_fld)) ↔ (𝑥 ∈ 𝐼 ↦ ((𝑥‘𝑛) − ((𝐹‘𝑥)‘𝑛))) ∈ ((𝑅 ↾_t 𝐼) Cn ((TopOpen‘ℂ_fld) ↾_t ℝ))))
87	81, 82, 86	3syl 18	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((𝑥 ∈ 𝐼 ↦ ((𝑥‘𝑛) − ((𝐹‘𝑥)‘𝑛))) ∈ ((𝑅 ↾_t 𝐼) Cn (TopOpen‘ℂ_fld)) ↔ (𝑥 ∈ 𝐼 ↦ ((𝑥‘𝑛) − ((𝐹‘𝑥)‘𝑛))) ∈ ((𝑅 ↾_t 𝐼) Cn ((TopOpen‘ℂ_fld) ↾_t ℝ))))
88	68, 87	mpbid 232	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐼 ↦ ((𝑥‘𝑛) − ((𝐹‘𝑥)‘𝑛))) ∈ ((𝑅 ↾_t 𝐼) Cn ((TopOpen‘ℂ_fld) ↾_t ℝ)))
89	54	adantl 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((𝑅 ↾_t 𝐼) Cn (((1...𝑁) × {(topGen‘ran (,))})‘𝑛)) = ((𝑅 ↾_t 𝐼) Cn ((TopOpen‘ℂ_fld) ↾_t ℝ)))
90	88, 89	eleqtrrd 2831	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐼 ↦ ((𝑥‘𝑛) − ((𝐹‘𝑥)‘𝑛))) ∈ ((𝑅 ↾_t 𝐼) Cn (((1...𝑁) × {(topGen‘ran (,))})‘𝑛)))
91	3, 32, 33, 36, 90	ptcn 23514	. . . 4 ⊢ (𝜑 → (𝑥 ∈ 𝐼 ↦ (𝑛 ∈ (1...𝑁) ↦ ((𝑥‘𝑛) − ((𝐹‘𝑥)‘𝑛)))) ∈ ((𝑅 ↾_t 𝐼) Cn 𝑅))
92	31, 91	eqeltrd 2828	. . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐼 ↦ (𝑥 ∘_f − (𝐹‘𝑥))) ∈ ((𝑅 ↾_t 𝐼) Cn 𝑅))
93		simpr2 1196	. . . . . 6 ⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧 ∈ 𝐼 ∧ (𝑧‘𝑛) = 0)) → 𝑧 ∈ 𝐼)
94		id 22	. . . . . . . . 9 ⊢ (𝑥 = 𝑧 → 𝑥 = 𝑧)
95		fveq2 6858	. . . . . . . . 9 ⊢ (𝑥 = 𝑧 → (𝐹‘𝑥) = (𝐹‘𝑧))
96	94, 95	oveq12d 7405	. . . . . . . 8 ⊢ (𝑥 = 𝑧 → (𝑥 ∘_f − (𝐹‘𝑥)) = (𝑧 ∘_f − (𝐹‘𝑧)))
97		eqid 2729	. . . . . . . 8 ⊢ (𝑥 ∈ 𝐼 ↦ (𝑥 ∘_f − (𝐹‘𝑥))) = (𝑥 ∈ 𝐼 ↦ (𝑥 ∘_f − (𝐹‘𝑥)))
98		ovex 7420	. . . . . . . 8 ⊢ (𝑧 ∘_f − (𝐹‘𝑧)) ∈ V
99	96, 97, 98	fvmpt 6968	. . . . . . 7 ⊢ (𝑧 ∈ 𝐼 → ((𝑥 ∈ 𝐼 ↦ (𝑥 ∘_f − (𝐹‘𝑥)))‘𝑧) = (𝑧 ∘_f − (𝐹‘𝑧)))
100	99	fveq1d 6860	. . . . . 6 ⊢ (𝑧 ∈ 𝐼 → (((𝑥 ∈ 𝐼 ↦ (𝑥 ∘_f − (𝐹‘𝑥)))‘𝑧)‘𝑛) = ((𝑧 ∘_f − (𝐹‘𝑧))‘𝑛))
101	93, 100	syl 17	. . . . 5 ⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧 ∈ 𝐼 ∧ (𝑧‘𝑛) = 0)) → (((𝑥 ∈ 𝐼 ↦ (𝑥 ∘_f − (𝐹‘𝑥)))‘𝑧)‘𝑛) = ((𝑧 ∘_f − (𝐹‘𝑧))‘𝑛))
102		elmapfn 8838	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ ((0[,]1) ↑_m (1...𝑁)) → 𝑧 Fn (1...𝑁))
103	102, 2	eleq2s 2846	. . . . . . . . . . 11 ⊢ (𝑧 ∈ 𝐼 → 𝑧 Fn (1...𝑁))
104	103	adantl 481	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑧‘𝑛) = 0) ∧ 𝑧 ∈ 𝐼) → 𝑧 Fn (1...𝑁))
105	21	ffvelcdmda 7056	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐼) → (𝐹‘𝑧) ∈ 𝐼)
106		elmapfn 8838	. . . . . . . . . . . . 13 ⊢ ((𝐹‘𝑧) ∈ ((0[,]1) ↑_m (1...𝑁)) → (𝐹‘𝑧) Fn (1...𝑁))
107	106, 2	eleq2s 2846	. . . . . . . . . . . 12 ⊢ ((𝐹‘𝑧) ∈ 𝐼 → (𝐹‘𝑧) Fn (1...𝑁))
108	105, 107	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐼) → (𝐹‘𝑧) Fn (1...𝑁))
109	108	adantlr 715	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑧‘𝑛) = 0) ∧ 𝑧 ∈ 𝐼) → (𝐹‘𝑧) Fn (1...𝑁))
110		ovexd 7422	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑧‘𝑛) = 0) ∧ 𝑧 ∈ 𝐼) → (1...𝑁) ∈ V)
111		simpllr 775	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑧‘𝑛) = 0) ∧ 𝑧 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → (𝑧‘𝑛) = 0)
112		eqidd 2730	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑧‘𝑛) = 0) ∧ 𝑧 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → ((𝐹‘𝑧)‘𝑛) = ((𝐹‘𝑧)‘𝑛))
113	104, 109, 110, 110, 27, 111, 112	ofval 7664	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑧‘𝑛) = 0) ∧ 𝑧 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑧 ∘_f − (𝐹‘𝑧))‘𝑛) = (0 − ((𝐹‘𝑧)‘𝑛)))
114		df-neg 11408	. . . . . . . . 9 ⊢ -((𝐹‘𝑧)‘𝑛) = (0 − ((𝐹‘𝑧)‘𝑛))
115	113, 114	eqtr4di 2782	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑧‘𝑛) = 0) ∧ 𝑧 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑧 ∘_f − (𝐹‘𝑧))‘𝑛) = -((𝐹‘𝑧)‘𝑛))
116	115	exp41 434	. . . . . . 7 ⊢ (𝜑 → ((𝑧‘𝑛) = 0 → (𝑧 ∈ 𝐼 → (𝑛 ∈ (1...𝑁) → ((𝑧 ∘_f − (𝐹‘𝑧))‘𝑛) = -((𝐹‘𝑧)‘𝑛)))))
117	116	com24 95	. . . . . 6 ⊢ (𝜑 → (𝑛 ∈ (1...𝑁) → (𝑧 ∈ 𝐼 → ((𝑧‘𝑛) = 0 → ((𝑧 ∘_f − (𝐹‘𝑧))‘𝑛) = -((𝐹‘𝑧)‘𝑛)))))
118	117	3imp2 1350	. . . . 5 ⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧 ∈ 𝐼 ∧ (𝑧‘𝑛) = 0)) → ((𝑧 ∘_f − (𝐹‘𝑧))‘𝑛) = -((𝐹‘𝑧)‘𝑛))
119	101, 118	eqtrd 2764	. . . 4 ⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧 ∈ 𝐼 ∧ (𝑧‘𝑛) = 0)) → (((𝑥 ∈ 𝐼 ↦ (𝑥 ∘_f − (𝐹‘𝑥)))‘𝑧)‘𝑛) = -((𝐹‘𝑧)‘𝑛))
120		elmapi 8822	. . . . . . . . . . . 12 ⊢ ((𝐹‘𝑧) ∈ ((0[,]1) ↑_m (1...𝑁)) → (𝐹‘𝑧):(1...𝑁)⟶(0[,]1))
121	120, 2	eleq2s 2846	. . . . . . . . . . 11 ⊢ ((𝐹‘𝑧) ∈ 𝐼 → (𝐹‘𝑧):(1...𝑁)⟶(0[,]1))
122	105, 121	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐼) → (𝐹‘𝑧):(1...𝑁)⟶(0[,]1))
123	122	ffvelcdmda 7056	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → ((𝐹‘𝑧)‘𝑛) ∈ (0[,]1))
124		0xr 11221	. . . . . . . . . 10 ⊢ 0 ∈ ℝ^*
125		1xr 11233	. . . . . . . . . 10 ⊢ 1 ∈ ℝ^*
126		iccgelb 13363	. . . . . . . . . 10 ⊢ ((0 ∈ ℝ^* ∧ 1 ∈ ℝ^* ∧ ((𝐹‘𝑧)‘𝑛) ∈ (0[,]1)) → 0 ≤ ((𝐹‘𝑧)‘𝑛))
127	124, 125, 126	mp3an12 1453	. . . . . . . . 9 ⊢ (((𝐹‘𝑧)‘𝑛) ∈ (0[,]1) → 0 ≤ ((𝐹‘𝑧)‘𝑛))
128	123, 127	syl 17	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → 0 ≤ ((𝐹‘𝑧)‘𝑛))
129	13, 123	sselid 3944	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → ((𝐹‘𝑧)‘𝑛) ∈ ℝ)
130	129	le0neg2d 11750	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → (0 ≤ ((𝐹‘𝑧)‘𝑛) ↔ -((𝐹‘𝑧)‘𝑛) ≤ 0))
131	128, 130	mpbid 232	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → -((𝐹‘𝑧)‘𝑛) ≤ 0)
132	131	an32s 652	. . . . . 6 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑧 ∈ 𝐼) → -((𝐹‘𝑧)‘𝑛) ≤ 0)
133	132	anasss 466	. . . . 5 ⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧 ∈ 𝐼)) → -((𝐹‘𝑧)‘𝑛) ≤ 0)
134	133	3adantr3 1172	. . . 4 ⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧 ∈ 𝐼 ∧ (𝑧‘𝑛) = 0)) → -((𝐹‘𝑧)‘𝑛) ≤ 0)
135	119, 134	eqbrtrd 5129	. . 3 ⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧 ∈ 𝐼 ∧ (𝑧‘𝑛) = 0)) → (((𝑥 ∈ 𝐼 ↦ (𝑥 ∘_f − (𝐹‘𝑥)))‘𝑧)‘𝑛) ≤ 0)
136		iccleub 13362	. . . . . . . . . 10 ⊢ ((0 ∈ ℝ^* ∧ 1 ∈ ℝ^* ∧ ((𝐹‘𝑧)‘𝑛) ∈ (0[,]1)) → ((𝐹‘𝑧)‘𝑛) ≤ 1)
137	124, 125, 136	mp3an12 1453	. . . . . . . . 9 ⊢ (((𝐹‘𝑧)‘𝑛) ∈ (0[,]1) → ((𝐹‘𝑧)‘𝑛) ≤ 1)
138	123, 137	syl 17	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → ((𝐹‘𝑧)‘𝑛) ≤ 1)
139		1red 11175	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → 1 ∈ ℝ)
140	139, 129	subge0d 11768	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → (0 ≤ (1 − ((𝐹‘𝑧)‘𝑛)) ↔ ((𝐹‘𝑧)‘𝑛) ≤ 1))
141	138, 140	mpbird 257	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → 0 ≤ (1 − ((𝐹‘𝑧)‘𝑛)))
142	141	an32s 652	. . . . . 6 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑧 ∈ 𝐼) → 0 ≤ (1 − ((𝐹‘𝑧)‘𝑛)))
143	142	anasss 466	. . . . 5 ⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧 ∈ 𝐼)) → 0 ≤ (1 − ((𝐹‘𝑧)‘𝑛)))
144	143	3adantr3 1172	. . . 4 ⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧 ∈ 𝐼 ∧ (𝑧‘𝑛) = 1)) → 0 ≤ (1 − ((𝐹‘𝑧)‘𝑛)))
145		simpr2 1196	. . . . . 6 ⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧 ∈ 𝐼 ∧ (𝑧‘𝑛) = 1)) → 𝑧 ∈ 𝐼)
146	145, 100	syl 17	. . . . 5 ⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧 ∈ 𝐼 ∧ (𝑧‘𝑛) = 1)) → (((𝑥 ∈ 𝐼 ↦ (𝑥 ∘_f − (𝐹‘𝑥)))‘𝑧)‘𝑛) = ((𝑧 ∘_f − (𝐹‘𝑧))‘𝑛))
147	103	adantl 481	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑧‘𝑛) = 1) ∧ 𝑧 ∈ 𝐼) → 𝑧 Fn (1...𝑁))
148	108	adantlr 715	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑧‘𝑛) = 1) ∧ 𝑧 ∈ 𝐼) → (𝐹‘𝑧) Fn (1...𝑁))
149		ovexd 7422	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑧‘𝑛) = 1) ∧ 𝑧 ∈ 𝐼) → (1...𝑁) ∈ V)
150		simpllr 775	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑧‘𝑛) = 1) ∧ 𝑧 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → (𝑧‘𝑛) = 1)
151		eqidd 2730	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑧‘𝑛) = 1) ∧ 𝑧 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → ((𝐹‘𝑧)‘𝑛) = ((𝐹‘𝑧)‘𝑛))
152	147, 148, 149, 149, 27, 150, 151	ofval 7664	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑧‘𝑛) = 1) ∧ 𝑧 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑧 ∘_f − (𝐹‘𝑧))‘𝑛) = (1 − ((𝐹‘𝑧)‘𝑛)))
153	152	exp41 434	. . . . . . 7 ⊢ (𝜑 → ((𝑧‘𝑛) = 1 → (𝑧 ∈ 𝐼 → (𝑛 ∈ (1...𝑁) → ((𝑧 ∘_f − (𝐹‘𝑧))‘𝑛) = (1 − ((𝐹‘𝑧)‘𝑛))))))
154	153	com24 95	. . . . . 6 ⊢ (𝜑 → (𝑛 ∈ (1...𝑁) → (𝑧 ∈ 𝐼 → ((𝑧‘𝑛) = 1 → ((𝑧 ∘_f − (𝐹‘𝑧))‘𝑛) = (1 − ((𝐹‘𝑧)‘𝑛))))))
155	154	3imp2 1350	. . . . 5 ⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧 ∈ 𝐼 ∧ (𝑧‘𝑛) = 1)) → ((𝑧 ∘_f − (𝐹‘𝑧))‘𝑛) = (1 − ((𝐹‘𝑧)‘𝑛)))
156	146, 155	eqtrd 2764	. . . 4 ⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧 ∈ 𝐼 ∧ (𝑧‘𝑛) = 1)) → (((𝑥 ∈ 𝐼 ↦ (𝑥 ∘_f − (𝐹‘𝑥)))‘𝑧)‘𝑛) = (1 − ((𝐹‘𝑧)‘𝑛)))
157	144, 156	breqtrrd 5135	. . 3 ⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧 ∈ 𝐼 ∧ (𝑧‘𝑛) = 1)) → 0 ≤ (((𝑥 ∈ 𝐼 ↦ (𝑥 ∘_f − (𝐹‘𝑥)))‘𝑧)‘𝑛))
158	1, 2, 3, 92, 135, 157	poimir 37647	. 2 ⊢ (𝜑 → ∃𝑐 ∈ 𝐼 ((𝑥 ∈ 𝐼 ↦ (𝑥 ∘_f − (𝐹‘𝑥)))‘𝑐) = ((1...𝑁) × {0}))
159		id 22	. . . . . . . 8 ⊢ (𝑥 = 𝑐 → 𝑥 = 𝑐)
160		fveq2 6858	. . . . . . . 8 ⊢ (𝑥 = 𝑐 → (𝐹‘𝑥) = (𝐹‘𝑐))
161	159, 160	oveq12d 7405	. . . . . . 7 ⊢ (𝑥 = 𝑐 → (𝑥 ∘_f − (𝐹‘𝑥)) = (𝑐 ∘_f − (𝐹‘𝑐)))
162		ovex 7420	. . . . . . 7 ⊢ (𝑐 ∘_f − (𝐹‘𝑐)) ∈ V
163	161, 97, 162	fvmpt 6968	. . . . . 6 ⊢ (𝑐 ∈ 𝐼 → ((𝑥 ∈ 𝐼 ↦ (𝑥 ∘_f − (𝐹‘𝑥)))‘𝑐) = (𝑐 ∘_f − (𝐹‘𝑐)))
164	163	adantl 481	. . . . 5 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐼) → ((𝑥 ∈ 𝐼 ↦ (𝑥 ∘_f − (𝐹‘𝑥)))‘𝑐) = (𝑐 ∘_f − (𝐹‘𝑐)))
165	164	eqeq1d 2731	. . . 4 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐼) → (((𝑥 ∈ 𝐼 ↦ (𝑥 ∘_f − (𝐹‘𝑥)))‘𝑐) = ((1...𝑁) × {0}) ↔ (𝑐 ∘_f − (𝐹‘𝑐)) = ((1...𝑁) × {0})))
166		elmapfn 8838	. . . . . . . . . . 11 ⊢ (𝑐 ∈ ((0[,]1) ↑_m (1...𝑁)) → 𝑐 Fn (1...𝑁))
167	166, 2	eleq2s 2846	. . . . . . . . . 10 ⊢ (𝑐 ∈ 𝐼 → 𝑐 Fn (1...𝑁))
168	167	adantl 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐼) → 𝑐 Fn (1...𝑁))
169	21	ffvelcdmda 7056	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐼) → (𝐹‘𝑐) ∈ 𝐼)
170		elmapfn 8838	. . . . . . . . . . 11 ⊢ ((𝐹‘𝑐) ∈ ((0[,]1) ↑_m (1...𝑁)) → (𝐹‘𝑐) Fn (1...𝑁))
171	170, 2	eleq2s 2846	. . . . . . . . . 10 ⊢ ((𝐹‘𝑐) ∈ 𝐼 → (𝐹‘𝑐) Fn (1...𝑁))
172	169, 171	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐼) → (𝐹‘𝑐) Fn (1...𝑁))
173		ovexd 7422	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐼) → (1...𝑁) ∈ V)
174		eqidd 2730	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → (𝑐‘𝑛) = (𝑐‘𝑛))
175		eqidd 2730	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → ((𝐹‘𝑐)‘𝑛) = ((𝐹‘𝑐)‘𝑛))
176	168, 172, 173, 173, 27, 174, 175	ofval 7664	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑐 ∘_f − (𝐹‘𝑐))‘𝑛) = ((𝑐‘𝑛) − ((𝐹‘𝑐)‘𝑛)))
177		c0ex 11168	. . . . . . . . . 10 ⊢ 0 ∈ V
178	177	fvconst2 7178	. . . . . . . . 9 ⊢ (𝑛 ∈ (1...𝑁) → (((1...𝑁) × {0})‘𝑛) = 0)
179	178	adantl 481	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → (((1...𝑁) × {0})‘𝑛) = 0)
180	176, 179	eqeq12d 2745	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → (((𝑐 ∘_f − (𝐹‘𝑐))‘𝑛) = (((1...𝑁) × {0})‘𝑛) ↔ ((𝑐‘𝑛) − ((𝐹‘𝑐)‘𝑛)) = 0))
181	13, 84	sstri 3956	. . . . . . . . . 10 ⊢ (0[,]1) ⊆ ℂ
182		elmapi 8822	. . . . . . . . . . . 12 ⊢ (𝑐 ∈ ((0[,]1) ↑_m (1...𝑁)) → 𝑐:(1...𝑁)⟶(0[,]1))
183	182, 2	eleq2s 2846	. . . . . . . . . . 11 ⊢ (𝑐 ∈ 𝐼 → 𝑐:(1...𝑁)⟶(0[,]1))
184	183	ffvelcdmda 7056	. . . . . . . . . 10 ⊢ ((𝑐 ∈ 𝐼 ∧ 𝑛 ∈ (1...𝑁)) → (𝑐‘𝑛) ∈ (0[,]1))
185	181, 184	sselid 3944	. . . . . . . . 9 ⊢ ((𝑐 ∈ 𝐼 ∧ 𝑛 ∈ (1...𝑁)) → (𝑐‘𝑛) ∈ ℂ)
186	185	adantll 714	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → (𝑐‘𝑛) ∈ ℂ)
187		elmapi 8822	. . . . . . . . . . . 12 ⊢ ((𝐹‘𝑐) ∈ ((0[,]1) ↑_m (1...𝑁)) → (𝐹‘𝑐):(1...𝑁)⟶(0[,]1))
188	187, 2	eleq2s 2846	. . . . . . . . . . 11 ⊢ ((𝐹‘𝑐) ∈ 𝐼 → (𝐹‘𝑐):(1...𝑁)⟶(0[,]1))
189	169, 188	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐼) → (𝐹‘𝑐):(1...𝑁)⟶(0[,]1))
190	189	ffvelcdmda 7056	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → ((𝐹‘𝑐)‘𝑛) ∈ (0[,]1))
191	181, 190	sselid 3944	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → ((𝐹‘𝑐)‘𝑛) ∈ ℂ)
192	186, 191	subeq0ad 11543	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → (((𝑐‘𝑛) − ((𝐹‘𝑐)‘𝑛)) = 0 ↔ (𝑐‘𝑛) = ((𝐹‘𝑐)‘𝑛)))
193	180, 192	bitrd 279	. . . . . 6 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → (((𝑐 ∘_f − (𝐹‘𝑐))‘𝑛) = (((1...𝑁) × {0})‘𝑛) ↔ (𝑐‘𝑛) = ((𝐹‘𝑐)‘𝑛)))
194	193	ralbidva 3154	. . . . 5 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐼) → (∀𝑛 ∈ (1...𝑁)((𝑐 ∘_f − (𝐹‘𝑐))‘𝑛) = (((1...𝑁) × {0})‘𝑛) ↔ ∀𝑛 ∈ (1...𝑁)(𝑐‘𝑛) = ((𝐹‘𝑐)‘𝑛)))
195	168, 172, 173, 173, 27	offn 7666	. . . . . 6 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐼) → (𝑐 ∘_f − (𝐹‘𝑐)) Fn (1...𝑁))
196		fnconstg 6748	. . . . . . 7 ⊢ (0 ∈ V → ((1...𝑁) × {0}) Fn (1...𝑁))
197	177, 196	ax-mp 5	. . . . . 6 ⊢ ((1...𝑁) × {0}) Fn (1...𝑁)
198		eqfnfv 7003	. . . . . 6 ⊢ (((𝑐 ∘_f − (𝐹‘𝑐)) Fn (1...𝑁) ∧ ((1...𝑁) × {0}) Fn (1...𝑁)) → ((𝑐 ∘_f − (𝐹‘𝑐)) = ((1...𝑁) × {0}) ↔ ∀𝑛 ∈ (1...𝑁)((𝑐 ∘_f − (𝐹‘𝑐))‘𝑛) = (((1...𝑁) × {0})‘𝑛)))
199	195, 197, 198	sylancl 586	. . . . 5 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐼) → ((𝑐 ∘_f − (𝐹‘𝑐)) = ((1...𝑁) × {0}) ↔ ∀𝑛 ∈ (1...𝑁)((𝑐 ∘_f − (𝐹‘𝑐))‘𝑛) = (((1...𝑁) × {0})‘𝑛)))
200		eqfnfv 7003	. . . . . 6 ⊢ ((𝑐 Fn (1...𝑁) ∧ (𝐹‘𝑐) Fn (1...𝑁)) → (𝑐 = (𝐹‘𝑐) ↔ ∀𝑛 ∈ (1...𝑁)(𝑐‘𝑛) = ((𝐹‘𝑐)‘𝑛)))
201	168, 172, 200	syl2anc 584	. . . . 5 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐼) → (𝑐 = (𝐹‘𝑐) ↔ ∀𝑛 ∈ (1...𝑁)(𝑐‘𝑛) = ((𝐹‘𝑐)‘𝑛)))
202	194, 199, 201	3bitr4d 311	. . . 4 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐼) → ((𝑐 ∘_f − (𝐹‘𝑐)) = ((1...𝑁) × {0}) ↔ 𝑐 = (𝐹‘𝑐)))
203	165, 202	bitrd 279	. . 3 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐼) → (((𝑥 ∈ 𝐼 ↦ (𝑥 ∘_f − (𝐹‘𝑥)))‘𝑐) = ((1...𝑁) × {0}) ↔ 𝑐 = (𝐹‘𝑐)))
204	203	rexbidva 3155	. 2 ⊢ (𝜑 → (∃𝑐 ∈ 𝐼 ((𝑥 ∈ 𝐼 ↦ (𝑥 ∘_f − (𝐹‘𝑥)))‘𝑐) = ((1...𝑁) × {0}) ↔ ∃𝑐 ∈ 𝐼 𝑐 = (𝐹‘𝑐)))
205	158, 204	mpbid 232	1 ⊢ (𝜑 → ∃𝑐 ∈ 𝐼 𝑐 = (𝐹‘𝑐))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 = wceq 1540 ∈ wcel 2109 ∀wral 3044 ∃wrex 3053 Vcvv 3447 ⊆ wss 3914 {csn 4589 class class class wbr 5107 ↦ cmpt 5188 × cxp 5636 ran crn 5639 ↾ cres 5640 Fn wfn 6506 ⟶wf 6507 ‘cfv 6511 (class class class)co 7387 ∘_f cof 7651 ↑_m cmap 8799 ℂcc 11066 ℝcr 11067 0cc0 11068 1c1 11069 ℝ^*cxr 11207 ≤ cle 11209 − cmin 11405 -cneg 11406 ℕcn 12186 (,)cioo 13306 [,]cicc 13309 ...cfz 13468 ↾_t crest 17383 TopOpenctopn 17384 topGenctg 17400 ∏_tcpt 17401 ℂ_fldccnfld 21264 Topctop 22780 TopOnctopon 22797 Cn ccn 23111 ×_t ctx 23447

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-rep 5234 ax-sep 5251 ax-nul 5261 ax-pow 5320 ax-pr 5387 ax-un 7711 ax-inf2 9594 ax-cnex 11124 ax-resscn 11125 ax-1cn 11126 ax-icn 11127 ax-addcl 11128 ax-addrcl 11129 ax-mulcl 11130 ax-mulrcl 11131 ax-mulcom 11132 ax-addass 11133 ax-mulass 11134 ax-distr 11135 ax-i2m1 11136 ax-1ne0 11137 ax-1rid 11138 ax-rnegex 11139 ax-rrecex 11140 ax-cnre 11141 ax-pre-lttri 11142 ax-pre-lttrn 11143 ax-pre-ltadd 11144 ax-pre-mulgt0 11145 ax-pre-sup 11146

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-nel 3030 df-ral 3045 df-rex 3054 df-rmo 3354 df-reu 3355 df-rab 3406 df-v 3449 df-sbc 3754 df-csb 3863 df-dif 3917 df-un 3919 df-in 3921 df-ss 3931 df-pss 3934 df-nul 4297 df-if 4489 df-pw 4565 df-sn 4590 df-pr 4592 df-tp 4594 df-op 4596 df-uni 4872 df-int 4911 df-iun 4957 df-iin 4958 df-disj 5075 df-br 5108 df-opab 5170 df-mpt 5189 df-tr 5215 df-id 5533 df-eprel 5538 df-po 5546 df-so 5547 df-fr 5591 df-se 5592 df-we 5593 df-xp 5644 df-rel 5645 df-cnv 5646 df-co 5647 df-dm 5648 df-rn 5649 df-res 5650 df-ima 5651 df-pred 6274 df-ord 6335 df-on 6336 df-lim 6337 df-suc 6338 df-iota 6464 df-fun 6513 df-fn 6514 df-f 6515 df-f1 6516 df-fo 6517 df-f1o 6518 df-fv 6519 df-isom 6520 df-riota 7344 df-ov 7390 df-oprab 7391 df-mpo 7392 df-of 7653 df-om 7843 df-1st 7968 df-2nd 7969 df-supp 8140 df-frecs 8260 df-wrecs 8291 df-recs 8340 df-rdg 8378 df-1o 8434 df-2o 8435 df-oadd 8438 df-omul 8439 df-er 8671 df-map 8801 df-pm 8802 df-ixp 8871 df-en 8919 df-dom 8920 df-sdom 8921 df-fin 8922 df-fsupp 9313 df-fi 9362 df-sup 9393 df-inf 9394 df-oi 9463 df-dju 9854 df-card 9892 df-acn 9895 df-pnf 11210 df-mnf 11211 df-xr 11212 df-ltxr 11213 df-le 11214 df-sub 11407 df-neg 11408 df-div 11836 df-nn 12187 df-2 12249 df-3 12250 df-4 12251 df-5 12252 df-6 12253 df-7 12254 df-8 12255 df-9 12256 df-n0 12443 df-xnn0 12516 df-z 12530 df-dec 12650 df-uz 12794 df-q 12908 df-rp 12952 df-xneg 13072 df-xadd 13073 df-xmul 13074 df-ioo 13310 df-icc 13313 df-fz 13469 df-fzo 13616 df-fl 13754 df-seq 13967 df-exp 14027 df-fac 14239 df-bc 14268 df-hash 14296 df-cj 15065 df-re 15066 df-im 15067 df-sqrt 15201 df-abs 15202 df-clim 15454 df-sum 15653 df-dvds 16223 df-struct 17117 df-sets 17134 df-slot 17152 df-ndx 17164 df-base 17180 df-ress 17201 df-plusg 17233 df-mulr 17234 df-starv 17235 df-sca 17236 df-vsca 17237 df-ip 17238 df-tset 17239 df-ple 17240 df-ds 17242 df-unif 17243 df-hom 17244 df-cco 17245 df-rest 17385 df-topn 17386 df-0g 17404 df-gsum 17405 df-topgen 17406 df-pt 17407 df-prds 17410 df-xrs 17465 df-qtop 17470 df-imas 17471 df-xps 17473 df-mre 17547 df-mrc 17548 df-acs 17550 df-ps 18525 df-tsr 18526 df-mgm 18567 df-sgrp 18646 df-mnd 18662 df-submnd 18711 df-mulg 19000 df-cntz 19249 df-cmn 19712 df-psmet 21256 df-xmet 21257 df-met 21258 df-bl 21259 df-mopn 21260 df-cnfld 21265 df-top 22781 df-topon 22798 df-topsp 22820 df-bases 22833 df-cld 22906 df-ntr 22907 df-cls 22908 df-lp 23023 df-cn 23114 df-cnp 23115 df-t1 23201 df-haus 23202 df-cmp 23274 df-tx 23449 df-hmeo 23642 df-hmph 23643 df-xms 24208 df-ms 24209 df-tms 24210 df-ii 24770

This theorem is referenced by: (None)

W3C validator