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 38333

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 8860	. . . . . . . 8 ⊢ (𝑥 ∈ ((0[,]1) ↑_m (1...𝑁)) → 𝑥 Fn (1...𝑁))
5	4, 2	eleq2s 2880	. . . . . . 7 ⊢ (𝑥 ∈ 𝐼 → 𝑥 Fn (1...𝑁))
6	5	adantl 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑥 Fn (1...𝑁))
7		broucube.1	. . . . . . . . 9 ⊢ (𝜑 → 𝐹 ∈ ((𝑅 ↾_t 𝐼) Cn (𝑅 ↾_t 𝐼)))
8		ovex 7445	. . . . . . . . . . . . 13 ⊢ (1...𝑁) ∈ V
9		retopon 24931	. . . . . . . . . . . . 13 ⊢ (topGen‘ran (,)) ∈ (TopOn‘ℝ)
10	3	pttoponconst 23765	. . . . . . . . . . . . 13 ⊢ (((1...𝑁) ∈ V ∧ (topGen‘ran (,)) ∈ (TopOn‘ℝ)) → 𝑅 ∈ (TopOn‘(ℝ ↑_m (1...𝑁))))
11	8, 9, 10	mp2an 704	. . . . . . . . . . . 12 ⊢ 𝑅 ∈ (TopOn‘(ℝ ↑_m (1...𝑁)))
12		reex 11197	. . . . . . . . . . . . . 14 ⊢ ℝ ∈ V
13		unitssre 13532	. . . . . . . . . . . . . 14 ⊢ (0[,]1) ⊆ ℝ
14		mapss 8885	. . . . . . . . . . . . . 14 ⊢ ((ℝ ∈ V ∧ (0[,]1) ⊆ ℝ) → ((0[,]1) ↑_m (1...𝑁)) ⊆ (ℝ ↑_m (1...𝑁)))
15	12, 13, 14	mp2an 704	. . . . . . . . . . . . 13 ⊢ ((0[,]1) ↑_m (1...𝑁)) ⊆ (ℝ ↑_m (1...𝑁))
16	2, 15	eqsstri 3982	. . . . . . . . . . . 12 ⊢ 𝐼 ⊆ (ℝ ↑_m (1...𝑁))
17		resttopon 23329	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ (TopOn‘(ℝ ↑_m (1...𝑁))) ∧ 𝐼 ⊆ (ℝ ↑_m (1...𝑁))) → (𝑅 ↾_t 𝐼) ∈ (TopOn‘𝐼))
18	11, 16, 17	mp2an 704	. . . . . . . . . . 11 ⊢ (𝑅 ↾_t 𝐼) ∈ (TopOn‘𝐼)
19	18	toponunii 23084	. . . . . . . . . 10 ⊢ 𝐼 = ∪ (𝑅 ↾_t 𝐼)
20	19, 19	cnf 23414	. . . . . . . . 9 ⊢ (𝐹 ∈ ((𝑅 ↾_t 𝐼) Cn (𝑅 ↾_t 𝐼)) → 𝐹:𝐼⟶𝐼)
21	7, 20	syl 18	. . . . . . . 8 ⊢ (𝜑 → 𝐹:𝐼⟶𝐼)
22	21	ffvelcdmda 7079	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝐹‘𝑥) ∈ 𝐼)
23		elmapfn 8860	. . . . . . . 8 ⊢ ((𝐹‘𝑥) ∈ ((0[,]1) ↑_m (1...𝑁)) → (𝐹‘𝑥) Fn (1...𝑁))
24	23, 2	eleq2s 2880	. . . . . . 7 ⊢ ((𝐹‘𝑥) ∈ 𝐼 → (𝐹‘𝑥) Fn (1...𝑁))
25	22, 24	syl 18	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝐹‘𝑥) Fn (1...𝑁))
26		ovexd 7447	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (1...𝑁) ∈ V)
27		inidm 4178	. . . . . 6 ⊢ ((1...𝑁) ∩ (1...𝑁)) = (1...𝑁)
28		eqidd 2763	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → (𝑥‘𝑛) = (𝑥‘𝑛))
29		eqidd 2763	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → ((𝐹‘𝑥)‘𝑛) = ((𝐹‘𝑥)‘𝑛))
30	6, 25, 26, 26, 27, 28, 29	offval 7685	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑥 ∘_f − (𝐹‘𝑥)) = (𝑛 ∈ (1...𝑁) ↦ ((𝑥‘𝑛) − ((𝐹‘𝑥)‘𝑛))))
31	30	mpteq2dva 5203	. . . 4 ⊢ (𝜑 → (𝑥 ∈ 𝐼 ↦ (𝑥 ∘_f − (𝐹‘𝑥))) = (𝑥 ∈ 𝐼 ↦ (𝑛 ∈ (1...𝑁) ↦ ((𝑥‘𝑛) − ((𝐹‘𝑥)‘𝑛)))))
32	18	a1i 11	. . . . 5 ⊢ (𝜑 → (𝑅 ↾_t 𝐼) ∈ (TopOn‘𝐼))
33		ovexd 7447	. . . . 5 ⊢ (𝜑 → (1...𝑁) ∈ V)
34		retop 24929	. . . . . . 7 ⊢ (topGen‘ran (,)) ∈ Top
35	34	fconst6 6768	. . . . . 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 2762	. . . . . . . . . . . 12 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
39	38	cnfldtop 24951	. . . . . . . . . . 11 ⊢ (TopOpen‘ℂ_fld) ∈ Top
40		cnrest2r 23455	. . . . . . . . . . 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 6038	. . . . . . . . . . . . 13 ⊢ (𝐼 ⊆ (ℝ ↑_m (1...𝑁)) → ((𝑥 ∈ (ℝ ↑_m (1...𝑁)) ↦ (𝑥‘𝑛)) ↾ 𝐼) = (𝑥 ∈ 𝐼 ↦ (𝑥‘𝑛)))
43	16, 42	ax-mp 5	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ (ℝ ↑_m (1...𝑁)) ↦ (𝑥‘𝑛)) ↾ 𝐼) = (𝑥 ∈ 𝐼 ↦ (𝑥‘𝑛))
44	11	toponunii 23084	. . . . . . . . . . . . . . 15 ⊢ (ℝ ↑_m (1...𝑁)) = ∪ 𝑅
45	44, 3	ptpjcn 23779	. . . . . . . . . . . . . 14 ⊢ (((1...𝑁) ∈ V ∧ ((1...𝑁) × {(topGen‘ran (,))}):(1...𝑁)⟶Top ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ (ℝ ↑_m (1...𝑁)) ↦ (𝑥‘𝑛)) ∈ (𝑅 Cn (((1...𝑁) × {(topGen‘ran (,))})‘𝑛)))
46	8, 35, 45	mp3an12 1479	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ (1...𝑁) → (𝑥 ∈ (ℝ ↑_m (1...𝑁)) ↦ (𝑥‘𝑛)) ∈ (𝑅 Cn (((1...𝑁) × {(topGen‘ran (,))})‘𝑛)))
47	44	cnrest 23453	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ (ℝ ↑_m (1...𝑁)) ↦ (𝑥‘𝑛)) ∈ (𝑅 Cn (((1...𝑁) × {(topGen‘ran (,))})‘𝑛)) ∧ 𝐼 ⊆ (ℝ ↑_m (1...𝑁))) → ((𝑥 ∈ (ℝ ↑_m (1...𝑁)) ↦ (𝑥‘𝑛)) ↾ 𝐼) ∈ ((𝑅 ↾_t 𝐼) Cn (((1...𝑁) × {(topGen‘ran (,))})‘𝑛)))
48	46, 16, 47	sylancl 597	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ (1...𝑁) → ((𝑥 ∈ (ℝ ↑_m (1...𝑁)) ↦ (𝑥‘𝑛)) ↾ 𝐼) ∈ ((𝑅 ↾_t 𝐼) Cn (((1...𝑁) × {(topGen‘ran (,))})‘𝑛)))
49	43, 48	eqeltrrid 2867	. . . . . . . . . . 11 ⊢ (𝑛 ∈ (1...𝑁) → (𝑥 ∈ 𝐼 ↦ (𝑥‘𝑛)) ∈ ((𝑅 ↾_t 𝐼) Cn (((1...𝑁) × {(topGen‘ran (,))})‘𝑛)))
50		fvex 6894	. . . . . . . . . . . . . 14 ⊢ (topGen‘ran (,)) ∈ V
51	50	fvconst2 7202	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ (1...𝑁) → (((1...𝑁) × {(topGen‘ran (,))})‘𝑛) = (topGen‘ran (,)))
52		tgioo4 24973	. . . . . . . . . . . . 13 ⊢ (topGen‘ran (,)) = ((TopOpen‘ℂ_fld) ↾_t ℝ)
53	51, 52	eqtrdi 2813	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ (1...𝑁) → (((1...𝑁) × {(topGen‘ran (,))})‘𝑛) = ((TopOpen‘ℂ_fld) ↾_t ℝ))
54	53	oveq2d 7428	. . . . . . . . . . 11 ⊢ (𝑛 ∈ (1...𝑁) → ((𝑅 ↾_t 𝐼) Cn (((1...𝑁) × {(topGen‘ran (,))})‘𝑛)) = ((𝑅 ↾_t 𝐼) Cn ((TopOpen‘ℂ_fld) ↾_t ℝ)))
55	49, 54	eleqtrd 2864	. . . . . . . . . 10 ⊢ (𝑛 ∈ (1...𝑁) → (𝑥 ∈ 𝐼 ↦ (𝑥‘𝑛)) ∈ ((𝑅 ↾_t 𝐼) Cn ((TopOpen‘ℂ_fld) ↾_t ℝ)))
56	41, 55	sselid 3934	. . . . . . . . 9 ⊢ (𝑛 ∈ (1...𝑁) → (𝑥 ∈ 𝐼 ↦ (𝑥‘𝑛)) ∈ ((𝑅 ↾_t 𝐼) Cn (TopOpen‘ℂ_fld)))
57	56	adantl 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐼 ↦ (𝑥‘𝑛)) ∈ ((𝑅 ↾_t 𝐼) Cn (TopOpen‘ℂ_fld)))
58	21	feqmptd 6949	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐼 ↦ (𝐹‘𝑥)))
59	58, 7	eqeltrrd 2863	. . . . . . . . . 10 ⊢ (𝜑 → (𝑥 ∈ 𝐼 ↦ (𝐹‘𝑥)) ∈ ((𝑅 ↾_t 𝐼) Cn (𝑅 ↾_t 𝐼)))
60	59	adantr 485	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐼 ↦ (𝐹‘𝑥)) ∈ ((𝑅 ↾_t 𝐼) Cn (𝑅 ↾_t 𝐼)))
61		fveq1 6880	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑧 → (𝑥‘𝑛) = (𝑧‘𝑛))
62	61	cbvmptv 5214	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝐼 ↦ (𝑥‘𝑛)) = (𝑧 ∈ 𝐼 ↦ (𝑧‘𝑛))
63	62, 57	eqeltrrid 2867	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑧 ∈ 𝐼 ↦ (𝑧‘𝑛)) ∈ ((𝑅 ↾_t 𝐼) Cn (TopOpen‘ℂ_fld)))
64		fveq1 6880	. . . . . . . . 9 ⊢ (𝑧 = (𝐹‘𝑥) → (𝑧‘𝑛) = ((𝐹‘𝑥)‘𝑛))
65	37, 60, 37, 63, 64	cnmpt11 23831	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐼 ↦ ((𝐹‘𝑥)‘𝑛)) ∈ ((𝑅 ↾_t 𝐼) Cn (TopOpen‘ℂ_fld)))
66	38	subcn 25035	. . . . . . . . 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 23834	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐼 ↦ ((𝑥‘𝑛) − ((𝐹‘𝑥)‘𝑛))) ∈ ((𝑅 ↾_t 𝐼) Cn (TopOpen‘ℂ_fld)))
69		elmapi 8844	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ((0[,]1) ↑_m (1...𝑁)) → 𝑥:(1...𝑁)⟶(0[,]1))
70	69, 2	eleq2s 2880	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ 𝐼 → 𝑥:(1...𝑁)⟶(0[,]1))
71	70	ffvelcdmda 7079	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ 𝐼 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥‘𝑛) ∈ (0[,]1))
72	13, 71	sselid 3934	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ 𝐼 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥‘𝑛) ∈ ℝ)
73	72	adantll 726	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → (𝑥‘𝑛) ∈ ℝ)
74		elmapi 8844	. . . . . . . . . . . . . . 15 ⊢ ((𝐹‘𝑥) ∈ ((0[,]1) ↑_m (1...𝑁)) → (𝐹‘𝑥):(1...𝑁)⟶(0[,]1))
75	74, 2	eleq2s 2880	. . . . . . . . . . . . . 14 ⊢ ((𝐹‘𝑥) ∈ 𝐼 → (𝐹‘𝑥):(1...𝑁)⟶(0[,]1))
76	22, 75	syl 18	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝐹‘𝑥):(1...𝑁)⟶(0[,]1))
77	76	ffvelcdmda 7079	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → ((𝐹‘𝑥)‘𝑛) ∈ (0[,]1))
78	13, 77	sselid 3934	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → ((𝐹‘𝑥)‘𝑛) ∈ ℝ)
79	73, 78	resubcld 11648	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑥‘𝑛) − ((𝐹‘𝑥)‘𝑛)) ∈ ℝ)
80	79	an32s 664	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐼) → ((𝑥‘𝑛) − ((𝐹‘𝑥)‘𝑛)) ∈ ℝ)
81	80	fmpttd 7110	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐼 ↦ ((𝑥‘𝑛) − ((𝐹‘𝑥)‘𝑛))):𝐼⟶ℝ)
82		frn 6713	. . . . . . . 8 ⊢ ((𝑥 ∈ 𝐼 ↦ ((𝑥‘𝑛) − ((𝐹‘𝑥)‘𝑛))):𝐼⟶ℝ → ran (𝑥 ∈ 𝐼 ↦ ((𝑥‘𝑛) − ((𝐹‘𝑥)‘𝑛))) ⊆ ℝ)
83	38	cnfldtopon 24950	. . . . . . . . 9 ⊢ (TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ)
84		ax-resscn 11163	. . . . . . . . 9 ⊢ ℝ ⊆ ℂ
85		cnrest2 23454	. . . . . . . . 9 ⊢ (((TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ) ∧ ran (𝑥 ∈ 𝐼 ↦ ((𝑥‘𝑛) − ((𝐹‘𝑥)‘𝑛))) ⊆ ℝ ∧ ℝ ⊆ ℂ) → ((𝑥 ∈ 𝐼 ↦ ((𝑥‘𝑛) − ((𝐹‘𝑥)‘𝑛))) ∈ ((𝑅 ↾_t 𝐼) Cn (TopOpen‘ℂ_fld)) ↔ (𝑥 ∈ 𝐼 ↦ ((𝑥‘𝑛) − ((𝐹‘𝑥)‘𝑛))) ∈ ((𝑅 ↾_t 𝐼) Cn ((TopOpen‘ℂ_fld) ↾_t ℝ))))
86	83, 84, 85	mp3an13 1480	. . . . . . . 8 ⊢ (ran (𝑥 ∈ 𝐼 ↦ ((𝑥‘𝑛) − ((𝐹‘𝑥)‘𝑛))) ⊆ ℝ → ((𝑥 ∈ 𝐼 ↦ ((𝑥‘𝑛) − ((𝐹‘𝑥)‘𝑛))) ∈ ((𝑅 ↾_t 𝐼) Cn (TopOpen‘ℂ_fld)) ↔ (𝑥 ∈ 𝐼 ↦ ((𝑥‘𝑛) − ((𝐹‘𝑥)‘𝑛))) ∈ ((𝑅 ↾_t 𝐼) Cn ((TopOpen‘ℂ_fld) ↾_t ℝ))))
87	81, 82, 86	3syl 19	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((𝑥 ∈ 𝐼 ↦ ((𝑥‘𝑛) − ((𝐹‘𝑥)‘𝑛))) ∈ ((𝑅 ↾_t 𝐼) Cn (TopOpen‘ℂ_fld)) ↔ (𝑥 ∈ 𝐼 ↦ ((𝑥‘𝑛) − ((𝐹‘𝑥)‘𝑛))) ∈ ((𝑅 ↾_t 𝐼) Cn ((TopOpen‘ℂ_fld) ↾_t ℝ))))
88	68, 87	mpbid 235	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐼 ↦ ((𝑥‘𝑛) − ((𝐹‘𝑥)‘𝑛))) ∈ ((𝑅 ↾_t 𝐼) Cn ((TopOpen‘ℂ_fld) ↾_t ℝ)))
89	54	adantl 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((𝑅 ↾_t 𝐼) Cn (((1...𝑁) × {(topGen‘ran (,))})‘𝑛)) = ((𝑅 ↾_t 𝐼) Cn ((TopOpen‘ℂ_fld) ↾_t ℝ)))
90	88, 89	eleqtrrd 2865	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐼 ↦ ((𝑥‘𝑛) − ((𝐹‘𝑥)‘𝑛))) ∈ ((𝑅 ↾_t 𝐼) Cn (((1...𝑁) × {(topGen‘ran (,))})‘𝑛)))
91	3, 32, 33, 36, 90	ptcn 23795	. . . 4 ⊢ (𝜑 → (𝑥 ∈ 𝐼 ↦ (𝑛 ∈ (1...𝑁) ↦ ((𝑥‘𝑛) − ((𝐹‘𝑥)‘𝑛)))) ∈ ((𝑅 ↾_t 𝐼) Cn 𝑅))
92	31, 91	eqeltrd 2862	. . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐼 ↦ (𝑥 ∘_f − (𝐹‘𝑥))) ∈ ((𝑅 ↾_t 𝐼) Cn 𝑅))
93		simpr2 1213	. . . . . 6 ⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧 ∈ 𝐼 ∧ (𝑧‘𝑛) = 0)) → 𝑧 ∈ 𝐼)
94		id 23	. . . . . . . . 9 ⊢ (𝑥 = 𝑧 → 𝑥 = 𝑧)
95		fveq2 6881	. . . . . . . . 9 ⊢ (𝑥 = 𝑧 → (𝐹‘𝑥) = (𝐹‘𝑧))
96	94, 95	oveq12d 7430	. . . . . . . 8 ⊢ (𝑥 = 𝑧 → (𝑥 ∘_f − (𝐹‘𝑥)) = (𝑧 ∘_f − (𝐹‘𝑧)))
97		eqid 2762	. . . . . . . 8 ⊢ (𝑥 ∈ 𝐼 ↦ (𝑥 ∘_f − (𝐹‘𝑥))) = (𝑥 ∈ 𝐼 ↦ (𝑥 ∘_f − (𝐹‘𝑥)))
98		ovex 7445	. . . . . . . 8 ⊢ (𝑧 ∘_f − (𝐹‘𝑧)) ∈ V
99	96, 97, 98	fvmpt 6989	. . . . . . 7 ⊢ (𝑧 ∈ 𝐼 → ((𝑥 ∈ 𝐼 ↦ (𝑥 ∘_f − (𝐹‘𝑥)))‘𝑧) = (𝑧 ∘_f − (𝐹‘𝑧)))
100	99	fveq1d 6883	. . . . . 6 ⊢ (𝑧 ∈ 𝐼 → (((𝑥 ∈ 𝐼 ↦ (𝑥 ∘_f − (𝐹‘𝑥)))‘𝑧)‘𝑛) = ((𝑧 ∘_f − (𝐹‘𝑧))‘𝑛))
101	93, 100	syl 18	. . . . 5 ⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧 ∈ 𝐼 ∧ (𝑧‘𝑛) = 0)) → (((𝑥 ∈ 𝐼 ↦ (𝑥 ∘_f − (𝐹‘𝑥)))‘𝑧)‘𝑛) = ((𝑧 ∘_f − (𝐹‘𝑧))‘𝑛))
102		elmapfn 8860	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ ((0[,]1) ↑_m (1...𝑁)) → 𝑧 Fn (1...𝑁))
103	102, 2	eleq2s 2880	. . . . . . . . . . 11 ⊢ (𝑧 ∈ 𝐼 → 𝑧 Fn (1...𝑁))
104	103	adantl 486	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑧‘𝑛) = 0) ∧ 𝑧 ∈ 𝐼) → 𝑧 Fn (1...𝑁))
105	21	ffvelcdmda 7079	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐼) → (𝐹‘𝑧) ∈ 𝐼)
106		elmapfn 8860	. . . . . . . . . . . . 13 ⊢ ((𝐹‘𝑧) ∈ ((0[,]1) ↑_m (1...𝑁)) → (𝐹‘𝑧) Fn (1...𝑁))
107	106, 2	eleq2s 2880	. . . . . . . . . . . 12 ⊢ ((𝐹‘𝑧) ∈ 𝐼 → (𝐹‘𝑧) Fn (1...𝑁))
108	105, 107	syl 18	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐼) → (𝐹‘𝑧) Fn (1...𝑁))
109	108	adantlr 727	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑧‘𝑛) = 0) ∧ 𝑧 ∈ 𝐼) → (𝐹‘𝑧) Fn (1...𝑁))
110		ovexd 7447	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑧‘𝑛) = 0) ∧ 𝑧 ∈ 𝐼) → (1...𝑁) ∈ V)
111		simpllr 787	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑧‘𝑛) = 0) ∧ 𝑧 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → (𝑧‘𝑛) = 0)
112		eqidd 2763	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑧‘𝑛) = 0) ∧ 𝑧 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → ((𝐹‘𝑧)‘𝑛) = ((𝐹‘𝑧)‘𝑛))
113	104, 109, 110, 110, 27, 111, 112	ofval 7687	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑧‘𝑛) = 0) ∧ 𝑧 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑧 ∘_f − (𝐹‘𝑧))‘𝑛) = (0 − ((𝐹‘𝑧)‘𝑛)))
114		df-neg 11450	. . . . . . . . 9 ⊢ -((𝐹‘𝑧)‘𝑛) = (0 − ((𝐹‘𝑧)‘𝑛))
115	113, 114	eqtr4di 2815	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑧‘𝑛) = 0) ∧ 𝑧 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑧 ∘_f − (𝐹‘𝑧))‘𝑛) = -((𝐹‘𝑧)‘𝑛))
116	115	exp41 439	. . . . . . 7 ⊢ (𝜑 → ((𝑧‘𝑛) = 0 → (𝑧 ∈ 𝐼 → (𝑛 ∈ (1...𝑁) → ((𝑧 ∘_f − (𝐹‘𝑧))‘𝑛) = -((𝐹‘𝑧)‘𝑛)))))
117	116	com24 96	. . . . . 6 ⊢ (𝜑 → (𝑛 ∈ (1...𝑁) → (𝑧 ∈ 𝐼 → ((𝑧‘𝑛) = 0 → ((𝑧 ∘_f − (𝐹‘𝑧))‘𝑛) = -((𝐹‘𝑧)‘𝑛)))))
118	117	3imp2 1367	. . . . 5 ⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧 ∈ 𝐼 ∧ (𝑧‘𝑛) = 0)) → ((𝑧 ∘_f − (𝐹‘𝑧))‘𝑛) = -((𝐹‘𝑧)‘𝑛))
119	101, 118	eqtrd 2797	. . . 4 ⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧 ∈ 𝐼 ∧ (𝑧‘𝑛) = 0)) → (((𝑥 ∈ 𝐼 ↦ (𝑥 ∘_f − (𝐹‘𝑥)))‘𝑧)‘𝑛) = -((𝐹‘𝑧)‘𝑛))
120		elmapi 8844	. . . . . . . . . . . 12 ⊢ ((𝐹‘𝑧) ∈ ((0[,]1) ↑_m (1...𝑁)) → (𝐹‘𝑧):(1...𝑁)⟶(0[,]1))
121	120, 2	eleq2s 2880	. . . . . . . . . . 11 ⊢ ((𝐹‘𝑧) ∈ 𝐼 → (𝐹‘𝑧):(1...𝑁)⟶(0[,]1))
122	105, 121	syl 18	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐼) → (𝐹‘𝑧):(1...𝑁)⟶(0[,]1))
123	122	ffvelcdmda 7079	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → ((𝐹‘𝑧)‘𝑛) ∈ (0[,]1))
124		0xr 11262	. . . . . . . . . 10 ⊢ 0 ∈ ℝ^*
125		1xr 11274	. . . . . . . . . 10 ⊢ 1 ∈ ℝ^*
126		iccgelb 13435	. . . . . . . . . 10 ⊢ ((0 ∈ ℝ^* ∧ 1 ∈ ℝ^* ∧ ((𝐹‘𝑧)‘𝑛) ∈ (0[,]1)) → 0 ≤ ((𝐹‘𝑧)‘𝑛))
127	124, 125, 126	mp3an12 1479	. . . . . . . . 9 ⊢ (((𝐹‘𝑧)‘𝑛) ∈ (0[,]1) → 0 ≤ ((𝐹‘𝑧)‘𝑛))
128	123, 127	syl 18	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → 0 ≤ ((𝐹‘𝑧)‘𝑛))
129	13, 123	sselid 3934	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → ((𝐹‘𝑧)‘𝑛) ∈ ℝ)
130	129	le0neg2d 11792	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → (0 ≤ ((𝐹‘𝑧)‘𝑛) ↔ -((𝐹‘𝑧)‘𝑛) ≤ 0))
131	128, 130	mpbid 235	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → -((𝐹‘𝑧)‘𝑛) ≤ 0)
132	131	an32s 664	. . . . . 6 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑧 ∈ 𝐼) → -((𝐹‘𝑧)‘𝑛) ≤ 0)
133	132	anasss 471	. . . . 5 ⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧 ∈ 𝐼)) → -((𝐹‘𝑧)‘𝑛) ≤ 0)
134	133	3adantr3 1189	. . . 4 ⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧 ∈ 𝐼 ∧ (𝑧‘𝑛) = 0)) → -((𝐹‘𝑧)‘𝑛) ≤ 0)
135	119, 134	eqbrtrd 5132	. . 3 ⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧 ∈ 𝐼 ∧ (𝑧‘𝑛) = 0)) → (((𝑥 ∈ 𝐼 ↦ (𝑥 ∘_f − (𝐹‘𝑥)))‘𝑧)‘𝑛) ≤ 0)
136		iccleub 13434	. . . . . . . . . 10 ⊢ ((0 ∈ ℝ^* ∧ 1 ∈ ℝ^* ∧ ((𝐹‘𝑧)‘𝑛) ∈ (0[,]1)) → ((𝐹‘𝑧)‘𝑛) ≤ 1)
137	124, 125, 136	mp3an12 1479	. . . . . . . . 9 ⊢ (((𝐹‘𝑧)‘𝑛) ∈ (0[,]1) → ((𝐹‘𝑧)‘𝑛) ≤ 1)
138	123, 137	syl 18	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → ((𝐹‘𝑧)‘𝑛) ≤ 1)
139		1red 11215	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → 1 ∈ ℝ)
140	139, 129	subge0d 11810	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → (0 ≤ (1 − ((𝐹‘𝑧)‘𝑛)) ↔ ((𝐹‘𝑧)‘𝑛) ≤ 1))
141	138, 140	mpbird 260	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → 0 ≤ (1 − ((𝐹‘𝑧)‘𝑛)))
142	141	an32s 664	. . . . . 6 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑧 ∈ 𝐼) → 0 ≤ (1 − ((𝐹‘𝑧)‘𝑛)))
143	142	anasss 471	. . . . 5 ⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧 ∈ 𝐼)) → 0 ≤ (1 − ((𝐹‘𝑧)‘𝑛)))
144	143	3adantr3 1189	. . . 4 ⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧 ∈ 𝐼 ∧ (𝑧‘𝑛) = 1)) → 0 ≤ (1 − ((𝐹‘𝑧)‘𝑛)))
145		simpr2 1213	. . . . . 6 ⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧 ∈ 𝐼 ∧ (𝑧‘𝑛) = 1)) → 𝑧 ∈ 𝐼)
146	145, 100	syl 18	. . . . 5 ⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧 ∈ 𝐼 ∧ (𝑧‘𝑛) = 1)) → (((𝑥 ∈ 𝐼 ↦ (𝑥 ∘_f − (𝐹‘𝑥)))‘𝑧)‘𝑛) = ((𝑧 ∘_f − (𝐹‘𝑧))‘𝑛))
147	103	adantl 486	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑧‘𝑛) = 1) ∧ 𝑧 ∈ 𝐼) → 𝑧 Fn (1...𝑁))
148	108	adantlr 727	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑧‘𝑛) = 1) ∧ 𝑧 ∈ 𝐼) → (𝐹‘𝑧) Fn (1...𝑁))
149		ovexd 7447	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑧‘𝑛) = 1) ∧ 𝑧 ∈ 𝐼) → (1...𝑁) ∈ V)
150		simpllr 787	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑧‘𝑛) = 1) ∧ 𝑧 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → (𝑧‘𝑛) = 1)
151		eqidd 2763	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑧‘𝑛) = 1) ∧ 𝑧 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → ((𝐹‘𝑧)‘𝑛) = ((𝐹‘𝑧)‘𝑛))
152	147, 148, 149, 149, 27, 150, 151	ofval 7687	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑧‘𝑛) = 1) ∧ 𝑧 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑧 ∘_f − (𝐹‘𝑧))‘𝑛) = (1 − ((𝐹‘𝑧)‘𝑛)))
153	152	exp41 439	. . . . . . 7 ⊢ (𝜑 → ((𝑧‘𝑛) = 1 → (𝑧 ∈ 𝐼 → (𝑛 ∈ (1...𝑁) → ((𝑧 ∘_f − (𝐹‘𝑧))‘𝑛) = (1 − ((𝐹‘𝑧)‘𝑛))))))
154	153	com24 96	. . . . . 6 ⊢ (𝜑 → (𝑛 ∈ (1...𝑁) → (𝑧 ∈ 𝐼 → ((𝑧‘𝑛) = 1 → ((𝑧 ∘_f − (𝐹‘𝑧))‘𝑛) = (1 − ((𝐹‘𝑧)‘𝑛))))))
155	154	3imp2 1367	. . . . 5 ⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧 ∈ 𝐼 ∧ (𝑧‘𝑛) = 1)) → ((𝑧 ∘_f − (𝐹‘𝑧))‘𝑛) = (1 − ((𝐹‘𝑧)‘𝑛)))
156	146, 155	eqtrd 2797	. . . 4 ⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧 ∈ 𝐼 ∧ (𝑧‘𝑛) = 1)) → (((𝑥 ∈ 𝐼 ↦ (𝑥 ∘_f − (𝐹‘𝑥)))‘𝑧)‘𝑛) = (1 − ((𝐹‘𝑧)‘𝑛)))
157	144, 156	breqtrrd 5138	. . 3 ⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧 ∈ 𝐼 ∧ (𝑧‘𝑛) = 1)) → 0 ≤ (((𝑥 ∈ 𝐼 ↦ (𝑥 ∘_f − (𝐹‘𝑥)))‘𝑧)‘𝑛))
158	1, 2, 3, 92, 135, 157	poimir 38332	. 2 ⊢ (𝜑 → ∃𝑐 ∈ 𝐼 ((𝑥 ∈ 𝐼 ↦ (𝑥 ∘_f − (𝐹‘𝑥)))‘𝑐) = ((1...𝑁) × {0}))
159		id 23	. . . . . . . 8 ⊢ (𝑥 = 𝑐 → 𝑥 = 𝑐)
160		fveq2 6881	. . . . . . . 8 ⊢ (𝑥 = 𝑐 → (𝐹‘𝑥) = (𝐹‘𝑐))
161	159, 160	oveq12d 7430	. . . . . . 7 ⊢ (𝑥 = 𝑐 → (𝑥 ∘_f − (𝐹‘𝑥)) = (𝑐 ∘_f − (𝐹‘𝑐)))
162		ovex 7445	. . . . . . 7 ⊢ (𝑐 ∘_f − (𝐹‘𝑐)) ∈ V
163	161, 97, 162	fvmpt 6989	. . . . . 6 ⊢ (𝑐 ∈ 𝐼 → ((𝑥 ∈ 𝐼 ↦ (𝑥 ∘_f − (𝐹‘𝑥)))‘𝑐) = (𝑐 ∘_f − (𝐹‘𝑐)))
164	163	adantl 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐼) → ((𝑥 ∈ 𝐼 ↦ (𝑥 ∘_f − (𝐹‘𝑥)))‘𝑐) = (𝑐 ∘_f − (𝐹‘𝑐)))
165	164	eqeq1d 2764	. . . 4 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐼) → (((𝑥 ∈ 𝐼 ↦ (𝑥 ∘_f − (𝐹‘𝑥)))‘𝑐) = ((1...𝑁) × {0}) ↔ (𝑐 ∘_f − (𝐹‘𝑐)) = ((1...𝑁) × {0})))
166		elmapfn 8860	. . . . . . . . . . 11 ⊢ (𝑐 ∈ ((0[,]1) ↑_m (1...𝑁)) → 𝑐 Fn (1...𝑁))
167	166, 2	eleq2s 2880	. . . . . . . . . 10 ⊢ (𝑐 ∈ 𝐼 → 𝑐 Fn (1...𝑁))
168	167	adantl 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐼) → 𝑐 Fn (1...𝑁))
169	21	ffvelcdmda 7079	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐼) → (𝐹‘𝑐) ∈ 𝐼)
170		elmapfn 8860	. . . . . . . . . . 11 ⊢ ((𝐹‘𝑐) ∈ ((0[,]1) ↑_m (1...𝑁)) → (𝐹‘𝑐) Fn (1...𝑁))
171	170, 2	eleq2s 2880	. . . . . . . . . 10 ⊢ ((𝐹‘𝑐) ∈ 𝐼 → (𝐹‘𝑐) Fn (1...𝑁))
172	169, 171	syl 18	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐼) → (𝐹‘𝑐) Fn (1...𝑁))
173		ovexd 7447	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐼) → (1...𝑁) ∈ V)
174		eqidd 2763	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → (𝑐‘𝑛) = (𝑐‘𝑛))
175		eqidd 2763	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → ((𝐹‘𝑐)‘𝑛) = ((𝐹‘𝑐)‘𝑛))
176	168, 172, 173, 173, 27, 174, 175	ofval 7687	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑐 ∘_f − (𝐹‘𝑐))‘𝑛) = ((𝑐‘𝑛) − ((𝐹‘𝑐)‘𝑛)))
177		c0ex 11206	. . . . . . . . . 10 ⊢ 0 ∈ V
178	177	fvconst2 7202	. . . . . . . . 9 ⊢ (𝑛 ∈ (1...𝑁) → (((1...𝑁) × {0})‘𝑛) = 0)
179	178	adantl 486	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → (((1...𝑁) × {0})‘𝑛) = 0)
180	176, 179	eqeq12d 2778	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → (((𝑐 ∘_f − (𝐹‘𝑐))‘𝑛) = (((1...𝑁) × {0})‘𝑛) ↔ ((𝑐‘𝑛) − ((𝐹‘𝑐)‘𝑛)) = 0))
181	13, 84	sstri 3945	. . . . . . . . . 10 ⊢ (0[,]1) ⊆ ℂ
182		elmapi 8844	. . . . . . . . . . . 12 ⊢ (𝑐 ∈ ((0[,]1) ↑_m (1...𝑁)) → 𝑐:(1...𝑁)⟶(0[,]1))
183	182, 2	eleq2s 2880	. . . . . . . . . . 11 ⊢ (𝑐 ∈ 𝐼 → 𝑐:(1...𝑁)⟶(0[,]1))
184	183	ffvelcdmda 7079	. . . . . . . . . 10 ⊢ ((𝑐 ∈ 𝐼 ∧ 𝑛 ∈ (1...𝑁)) → (𝑐‘𝑛) ∈ (0[,]1))
185	181, 184	sselid 3934	. . . . . . . . 9 ⊢ ((𝑐 ∈ 𝐼 ∧ 𝑛 ∈ (1...𝑁)) → (𝑐‘𝑛) ∈ ℂ)
186	185	adantll 726	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → (𝑐‘𝑛) ∈ ℂ)
187		elmapi 8844	. . . . . . . . . . . 12 ⊢ ((𝐹‘𝑐) ∈ ((0[,]1) ↑_m (1...𝑁)) → (𝐹‘𝑐):(1...𝑁)⟶(0[,]1))
188	187, 2	eleq2s 2880	. . . . . . . . . . 11 ⊢ ((𝐹‘𝑐) ∈ 𝐼 → (𝐹‘𝑐):(1...𝑁)⟶(0[,]1))
189	169, 188	syl 18	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐼) → (𝐹‘𝑐):(1...𝑁)⟶(0[,]1))
190	189	ffvelcdmda 7079	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → ((𝐹‘𝑐)‘𝑛) ∈ (0[,]1))
191	181, 190	sselid 3934	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → ((𝐹‘𝑐)‘𝑛) ∈ ℂ)
192	186, 191	subeq0ad 11585	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → (((𝑐‘𝑛) − ((𝐹‘𝑐)‘𝑛)) = 0 ↔ (𝑐‘𝑛) = ((𝐹‘𝑐)‘𝑛)))
193	180, 192	bitrd 282	. . . . . 6 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → (((𝑐 ∘_f − (𝐹‘𝑐))‘𝑛) = (((1...𝑁) × {0})‘𝑛) ↔ (𝑐‘𝑛) = ((𝐹‘𝑐)‘𝑛)))
194	193	ralbidva 3185	. . . . 5 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐼) → (∀𝑛 ∈ (1...𝑁)((𝑐 ∘_f − (𝐹‘𝑐))‘𝑛) = (((1...𝑁) × {0})‘𝑛) ↔ ∀𝑛 ∈ (1...𝑁)(𝑐‘𝑛) = ((𝐹‘𝑐)‘𝑛)))
195	168, 172, 173, 173, 27	offn 7689	. . . . . 6 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐼) → (𝑐 ∘_f − (𝐹‘𝑐)) Fn (1...𝑁))
196		fnconstg 6766	. . . . . . 7 ⊢ (0 ∈ V → ((1...𝑁) × {0}) Fn (1...𝑁))
197	177, 196	ax-mp 5	. . . . . 6 ⊢ ((1...𝑁) × {0}) Fn (1...𝑁)
198		eqfnfv 7025	. . . . . 6 ⊢ (((𝑐 ∘_f − (𝐹‘𝑐)) Fn (1...𝑁) ∧ ((1...𝑁) × {0}) Fn (1...𝑁)) → ((𝑐 ∘_f − (𝐹‘𝑐)) = ((1...𝑁) × {0}) ↔ ∀𝑛 ∈ (1...𝑁)((𝑐 ∘_f − (𝐹‘𝑐))‘𝑛) = (((1...𝑁) × {0})‘𝑛)))
199	195, 197, 198	sylancl 597	. . . . 5 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐼) → ((𝑐 ∘_f − (𝐹‘𝑐)) = ((1...𝑁) × {0}) ↔ ∀𝑛 ∈ (1...𝑁)((𝑐 ∘_f − (𝐹‘𝑐))‘𝑛) = (((1...𝑁) × {0})‘𝑛)))
200		eqfnfv 7025	. . . . . 6 ⊢ ((𝑐 Fn (1...𝑁) ∧ (𝐹‘𝑐) Fn (1...𝑁)) → (𝑐 = (𝐹‘𝑐) ↔ ∀𝑛 ∈ (1...𝑁)(𝑐‘𝑛) = ((𝐹‘𝑐)‘𝑛)))
201	168, 172, 200	syl2anc 595	. . . . 5 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐼) → (𝑐 = (𝐹‘𝑐) ↔ ∀𝑛 ∈ (1...𝑁)(𝑐‘𝑛) = ((𝐹‘𝑐)‘𝑛)))
202	194, 199, 201	3bitr4d 314	. . . 4 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐼) → ((𝑐 ∘_f − (𝐹‘𝑐)) = ((1...𝑁) × {0}) ↔ 𝑐 = (𝐹‘𝑐)))
203	165, 202	bitrd 282	. . 3 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐼) → (((𝑥 ∈ 𝐼 ↦ (𝑥 ∘_f − (𝐹‘𝑥)))‘𝑐) = ((1...𝑁) × {0}) ↔ 𝑐 = (𝐹‘𝑐)))
204	203	rexbidva 3186	. 2 ⊢ (𝜑 → (∃𝑐 ∈ 𝐼 ((𝑥 ∈ 𝐼 ↦ (𝑥 ∘_f − (𝐹‘𝑥)))‘𝑐) = ((1...𝑁) × {0}) ↔ ∃𝑐 ∈ 𝐼 𝑐 = (𝐹‘𝑐)))
205	158, 204	mpbid 235	1 ⊢ (𝜑 → ∃𝑐 ∈ 𝐼 𝑐 = (𝐹‘𝑐))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 400 ∧ w3a 1102 = wceq 1569 ∈ wcel 2142 ∀wral 3078 ∃wrex 3088 Vcvv 3454 ⊆ wss 3904 {csn 4588 class class class wbr 5108 ↦ cmpt 5191 × cxp 5658 ran crn 5661 ↾ cres 5662 Fn wfn 6531 ⟶wf 6532 ‘cfv 6536 (class class class)co 7412 ∘_f cof 7674 ↑_m cmap 8822 ℂcc 11104 ℝcr 11105 0cc0 11106 1c1 11107 ℝ^*cxr 11248 ≤ cle 11250 − cmin 11447 -cneg 11448 ℕcn 12239 (,)cioo 13378 [,]cicc 13381 ...cfz 13541 ↾_t crest 17479 TopOpenctopn 17480 topGenctg 17496 ∏_tcpt 17497 ℂ_fldccnfld 21533 Topctop 23061 TopOnctopon 23078 Cn ccn 23392 ×_t ctx 23728

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1824 ax-4 1838 ax-5 1939 ax-6 1996 ax-7 2037 ax-8 2144 ax-9 2152 ax-10 2175 ax-11 2191 ax-12 2212 ax-ext 2734 ax-rep 5237 ax-sep 5256 ax-nul 5268 ax-pow 5335 ax-pr 5403 ax-un 7734 ax-inf2 9608 ax-cnex 11162 ax-resscn 11163 ax-1cn 11164 ax-icn 11165 ax-addcl 11166 ax-addrcl 11167 ax-mulcl 11168 ax-mulrcl 11169 ax-mulcom 11170 ax-addass 11171 ax-mulass 11172 ax-distr 11173 ax-i2m1 11174 ax-1ne0 11175 ax-1rid 11176 ax-rnegex 11177 ax-rrecex 11178 ax-cnre 11179 ax-pre-lttri 11180 ax-pre-lttrn 11181 ax-pre-ltadd 11182 ax-pre-mulgt0 11183 ax-pre-sup 11184

This proof depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1103 df-3an 1104 df-tru 1572 df-fal 1582 df-ex 1809 df-nf 1813 df-sb 2096 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-rmo 3368 df-reu 3369 df-rab 3416 df-v 3456 df-sbc 3744 df-csb 3853 df-dif 3907 df-un 3909 df-in 3911 df-ss 3921 df-pss 3924 df-nul 4286 df-if 4487 df-pw 4563 df-sn 4589 df-pr 4591 df-tp 4593 df-op 4595 df-uni 4872 df-int 4912 df-iun 4957 df-iin 4958 df-disj 5076 df-br 5109 df-opab 5173 df-mpt 5192 df-tr 5218 df-id 5555 df-eprel 5560 df-po 5568 df-so 5569 df-fr 5613 df-se 5614 df-we 5615 df-xp 5666 df-rel 5667 df-cnv 5668 df-co 5669 df-dm 5670 df-rn 5671 df-res 5672 df-ima 5673 df-pred 6302 df-ord 6363 df-on 6364 df-lim 6365 df-suc 6366 df-iota 6492 df-fun 6538 df-fn 6539 df-f 6540 df-f1 6541 df-fo 6542 df-f1o 6543 df-fv 6544 df-isom 6545 df-riota 7369 df-ov 7415 df-oprab 7416 df-mpo 7417 df-of 7676 df-om 7861 df-1st 7984 df-2nd 7985 df-supp 8155 df-frecs 8276 df-wrecs 8307 df-recs 8356 df-rdg 8395 df-1o 8451 df-2o 8452 df-oadd 8455 df-omul 8456 df-er 8692 df-map 8824 df-pm 8825 df-ixp 8894 df-en 8942 df-dom 8943 df-sdom 8944 df-fin 8945 df-fsupp 9320 df-fi 9369 df-sup 9400 df-inf 9401 df-oi 9470 df-dju 9894 df-card 9932 df-acn 9935 df-pnf 11251 df-mnf 11252 df-xr 11253 df-ltxr 11254 df-le 11255 df-sub 11449 df-neg 11450 df-div 11878 df-nn 12240 df-2 12309 df-3 12310 df-4 12311 df-5 12312 df-6 12313 df-7 12314 df-8 12315 df-9 12316 df-n0 12511 df-xnn0 12584 df-z 12598 df-dec 12718 df-uz 12869 df-q 12979 df-rp 13023 df-xneg 13143 df-xadd 13144 df-xmul 13145 df-ioo 13382 df-icc 13385 df-fz 13542 df-fzo 13690 df-fl 13832 df-seq 14045 df-exp 14105 df-fac 14317 df-bc 14346 df-hash 14374 df-cj 15157 df-re 15158 df-im 15159 df-sqrt 15293 df-abs 15294 df-clim 15546 df-sum 15745 df-dvds 16317 df-struct 17213 df-sets 17230 df-slot 17248 df-ndx 17260 df-base 17276 df-ress 17297 df-plusg 17329 df-mulr 17330 df-starv 17331 df-sca 17332 df-vsca 17333 df-ip 17334 df-tset 17335 df-ple 17336 df-ds 17338 df-unif 17339 df-hom 17340 df-cco 17341 df-rest 17481 df-topn 17482 df-0g 17500 df-gsum 17501 df-topgen 17502 df-pt 17503 df-prds 17506 df-xrs 17562 df-qtop 17567 df-imas 17568 df-xps 17570 df-mre 17644 df-mrc 17645 df-acs 17647 df-ps 18628 df-tsr 18629 df-mgm 18704 df-sgrp 18783 df-mnd 18799 df-submnd 18848 df-mulg 19140 df-cntz 19393 df-cmn 19858 df-psmet 21525 df-xmet 21526 df-met 21527 df-bl 21528 df-mopn 21529 df-cnfld 21534 df-top 23062 df-topon 23079 df-topsp 23101 df-bases 23114 df-cld 23187 df-ntr 23188 df-cls 23189 df-lp 23304 df-cn 23395 df-cnp 23396 df-t1 23482 df-haus 23483 df-cmp 23555 df-tx 23730 df-hmeo 23923 df-hmph 23924 df-xms 24488 df-ms 24489 df-tms 24490 df-ii 25047

This theorem is used by: (None)

W3C validator