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 35456

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 8477	. . . . . . . 8 ⊢ (𝑥 ∈ ((0[,]1) ↑_m (1...𝑁)) → 𝑥 Fn (1...𝑁))
5	4, 2	eleq2s 2851	. . . . . . 7 ⊢ (𝑥 ∈ 𝐼 → 𝑥 Fn (1...𝑁))
6	5	adantl 485	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑥 Fn (1...𝑁))
7		broucube.1	. . . . . . . . 9 ⊢ (𝜑 → 𝐹 ∈ ((𝑅 ↾_t 𝐼) Cn (𝑅 ↾_t 𝐼)))
8		ovex 7205	. . . . . . . . . . . . 13 ⊢ (1...𝑁) ∈ V
9		retopon 23518	. . . . . . . . . . . . 13 ⊢ (topGen‘ran (,)) ∈ (TopOn‘ℝ)
10	3	pttoponconst 22350	. . . . . . . . . . . . 13 ⊢ (((1...𝑁) ∈ V ∧ (topGen‘ran (,)) ∈ (TopOn‘ℝ)) → 𝑅 ∈ (TopOn‘(ℝ ↑_m (1...𝑁))))
11	8, 9, 10	mp2an 692	. . . . . . . . . . . 12 ⊢ 𝑅 ∈ (TopOn‘(ℝ ↑_m (1...𝑁)))
12		reex 10708	. . . . . . . . . . . . . 14 ⊢ ℝ ∈ V
13		unitssre 12975	. . . . . . . . . . . . . 14 ⊢ (0[,]1) ⊆ ℝ
14		mapss 8501	. . . . . . . . . . . . . 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 3911	. . . . . . . . . . . 12 ⊢ 𝐼 ⊆ (ℝ ↑_m (1...𝑁))
17		resttopon 21914	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ (TopOn‘(ℝ ↑_m (1...𝑁))) ∧ 𝐼 ⊆ (ℝ ↑_m (1...𝑁))) → (𝑅 ↾_t 𝐼) ∈ (TopOn‘𝐼))
18	11, 16, 17	mp2an 692	. . . . . . . . . . 11 ⊢ (𝑅 ↾_t 𝐼) ∈ (TopOn‘𝐼)
19	18	toponunii 21669	. . . . . . . . . 10 ⊢ 𝐼 = ∪ (𝑅 ↾_t 𝐼)
20	19, 19	cnf 21999	. . . . . . . . 9 ⊢ (𝐹 ∈ ((𝑅 ↾_t 𝐼) Cn (𝑅 ↾_t 𝐼)) → 𝐹:𝐼⟶𝐼)
21	7, 20	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝐹:𝐼⟶𝐼)
22	21	ffvelrnda 6863	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝐹‘𝑥) ∈ 𝐼)
23		elmapfn 8477	. . . . . . . 8 ⊢ ((𝐹‘𝑥) ∈ ((0[,]1) ↑_m (1...𝑁)) → (𝐹‘𝑥) Fn (1...𝑁))
24	23, 2	eleq2s 2851	. . . . . . 7 ⊢ ((𝐹‘𝑥) ∈ 𝐼 → (𝐹‘𝑥) Fn (1...𝑁))
25	22, 24	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝐹‘𝑥) Fn (1...𝑁))
26		ovexd 7207	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (1...𝑁) ∈ V)
27		inidm 4109	. . . . . 6 ⊢ ((1...𝑁) ∩ (1...𝑁)) = (1...𝑁)
28		eqidd 2739	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → (𝑥‘𝑛) = (𝑥‘𝑛))
29		eqidd 2739	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → ((𝐹‘𝑥)‘𝑛) = ((𝐹‘𝑥)‘𝑛))
30	6, 25, 26, 26, 27, 28, 29	offval 7435	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑥 ∘_f − (𝐹‘𝑥)) = (𝑛 ∈ (1...𝑁) ↦ ((𝑥‘𝑛) − ((𝐹‘𝑥)‘𝑛))))
31	30	mpteq2dva 5125	. . . 4 ⊢ (𝜑 → (𝑥 ∈ 𝐼 ↦ (𝑥 ∘_f − (𝐹‘𝑥))) = (𝑥 ∈ 𝐼 ↦ (𝑛 ∈ (1...𝑁) ↦ ((𝑥‘𝑛) − ((𝐹‘𝑥)‘𝑛)))))
32	18	a1i 11	. . . . 5 ⊢ (𝜑 → (𝑅 ↾_t 𝐼) ∈ (TopOn‘𝐼))
33		ovexd 7207	. . . . 5 ⊢ (𝜑 → (1...𝑁) ∈ V)
34		retop 23516	. . . . . . 7 ⊢ (topGen‘ran (,)) ∈ Top
35	34	fconst6 6568	. . . . . 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 2738	. . . . . . . . . . . 12 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
39	38	cnfldtop 23538	. . . . . . . . . . 11 ⊢ (TopOpen‘ℂ_fld) ∈ Top
40		cnrest2r 22040	. . . . . . . . . . 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 5879	. . . . . . . . . . . . 13 ⊢ (𝐼 ⊆ (ℝ ↑_m (1...𝑁)) → ((𝑥 ∈ (ℝ ↑_m (1...𝑁)) ↦ (𝑥‘𝑛)) ↾ 𝐼) = (𝑥 ∈ 𝐼 ↦ (𝑥‘𝑛)))
43	16, 42	ax-mp 5	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ (ℝ ↑_m (1...𝑁)) ↦ (𝑥‘𝑛)) ↾ 𝐼) = (𝑥 ∈ 𝐼 ↦ (𝑥‘𝑛))
44	11	toponunii 21669	. . . . . . . . . . . . . . 15 ⊢ (ℝ ↑_m (1...𝑁)) = ∪ 𝑅
45	44, 3	ptpjcn 22364	. . . . . . . . . . . . . 14 ⊢ (((1...𝑁) ∈ V ∧ ((1...𝑁) × {(topGen‘ran (,))}):(1...𝑁)⟶Top ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ (ℝ ↑_m (1...𝑁)) ↦ (𝑥‘𝑛)) ∈ (𝑅 Cn (((1...𝑁) × {(topGen‘ran (,))})‘𝑛)))
46	8, 35, 45	mp3an12 1452	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ (1...𝑁) → (𝑥 ∈ (ℝ ↑_m (1...𝑁)) ↦ (𝑥‘𝑛)) ∈ (𝑅 Cn (((1...𝑁) × {(topGen‘ran (,))})‘𝑛)))
47	44	cnrest 22038	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ (ℝ ↑_m (1...𝑁)) ↦ (𝑥‘𝑛)) ∈ (𝑅 Cn (((1...𝑁) × {(topGen‘ran (,))})‘𝑛)) ∧ 𝐼 ⊆ (ℝ ↑_m (1...𝑁))) → ((𝑥 ∈ (ℝ ↑_m (1...𝑁)) ↦ (𝑥‘𝑛)) ↾ 𝐼) ∈ ((𝑅 ↾_t 𝐼) Cn (((1...𝑁) × {(topGen‘ran (,))})‘𝑛)))
48	46, 16, 47	sylancl 589	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ (1...𝑁) → ((𝑥 ∈ (ℝ ↑_m (1...𝑁)) ↦ (𝑥‘𝑛)) ↾ 𝐼) ∈ ((𝑅 ↾_t 𝐼) Cn (((1...𝑁) × {(topGen‘ran (,))})‘𝑛)))
49	43, 48	eqeltrrid 2838	. . . . . . . . . . 11 ⊢ (𝑛 ∈ (1...𝑁) → (𝑥 ∈ 𝐼 ↦ (𝑥‘𝑛)) ∈ ((𝑅 ↾_t 𝐼) Cn (((1...𝑁) × {(topGen‘ran (,))})‘𝑛)))
50		fvex 6689	. . . . . . . . . . . . . 14 ⊢ (topGen‘ran (,)) ∈ V
51	50	fvconst2 6978	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ (1...𝑁) → (((1...𝑁) × {(topGen‘ran (,))})‘𝑛) = (topGen‘ran (,)))
52	38	tgioo2 23557	. . . . . . . . . . . . 13 ⊢ (topGen‘ran (,)) = ((TopOpen‘ℂ_fld) ↾_t ℝ)
53	51, 52	eqtrdi 2789	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ (1...𝑁) → (((1...𝑁) × {(topGen‘ran (,))})‘𝑛) = ((TopOpen‘ℂ_fld) ↾_t ℝ))
54	53	oveq2d 7188	. . . . . . . . . . 11 ⊢ (𝑛 ∈ (1...𝑁) → ((𝑅 ↾_t 𝐼) Cn (((1...𝑁) × {(topGen‘ran (,))})‘𝑛)) = ((𝑅 ↾_t 𝐼) Cn ((TopOpen‘ℂ_fld) ↾_t ℝ)))
55	49, 54	eleqtrd 2835	. . . . . . . . . 10 ⊢ (𝑛 ∈ (1...𝑁) → (𝑥 ∈ 𝐼 ↦ (𝑥‘𝑛)) ∈ ((𝑅 ↾_t 𝐼) Cn ((TopOpen‘ℂ_fld) ↾_t ℝ)))
56	41, 55	sseldi 3875	. . . . . . . . 9 ⊢ (𝑛 ∈ (1...𝑁) → (𝑥 ∈ 𝐼 ↦ (𝑥‘𝑛)) ∈ ((𝑅 ↾_t 𝐼) Cn (TopOpen‘ℂ_fld)))
57	56	adantl 485	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐼 ↦ (𝑥‘𝑛)) ∈ ((𝑅 ↾_t 𝐼) Cn (TopOpen‘ℂ_fld)))
58	21	feqmptd 6739	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐼 ↦ (𝐹‘𝑥)))
59	58, 7	eqeltrrd 2834	. . . . . . . . . 10 ⊢ (𝜑 → (𝑥 ∈ 𝐼 ↦ (𝐹‘𝑥)) ∈ ((𝑅 ↾_t 𝐼) Cn (𝑅 ↾_t 𝐼)))
60	59	adantr 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐼 ↦ (𝐹‘𝑥)) ∈ ((𝑅 ↾_t 𝐼) Cn (𝑅 ↾_t 𝐼)))
61		fveq1 6675	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑧 → (𝑥‘𝑛) = (𝑧‘𝑛))
62	61	cbvmptv 5133	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝐼 ↦ (𝑥‘𝑛)) = (𝑧 ∈ 𝐼 ↦ (𝑧‘𝑛))
63	62, 57	eqeltrrid 2838	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑧 ∈ 𝐼 ↦ (𝑧‘𝑛)) ∈ ((𝑅 ↾_t 𝐼) Cn (TopOpen‘ℂ_fld)))
64		fveq1 6675	. . . . . . . . 9 ⊢ (𝑧 = (𝐹‘𝑥) → (𝑧‘𝑛) = ((𝐹‘𝑥)‘𝑛))
65	37, 60, 37, 63, 64	cnmpt11 22416	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐼 ↦ ((𝐹‘𝑥)‘𝑛)) ∈ ((𝑅 ↾_t 𝐼) Cn (TopOpen‘ℂ_fld)))
66	38	subcn 23620	. . . . . . . . 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 22419	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐼 ↦ ((𝑥‘𝑛) − ((𝐹‘𝑥)‘𝑛))) ∈ ((𝑅 ↾_t 𝐼) Cn (TopOpen‘ℂ_fld)))
69		elmapi 8461	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ((0[,]1) ↑_m (1...𝑁)) → 𝑥:(1...𝑁)⟶(0[,]1))
70	69, 2	eleq2s 2851	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ 𝐼 → 𝑥:(1...𝑁)⟶(0[,]1))
71	70	ffvelrnda 6863	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ 𝐼 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥‘𝑛) ∈ (0[,]1))
72	13, 71	sseldi 3875	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ 𝐼 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥‘𝑛) ∈ ℝ)
73	72	adantll 714	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → (𝑥‘𝑛) ∈ ℝ)
74		elmapi 8461	. . . . . . . . . . . . . . 15 ⊢ ((𝐹‘𝑥) ∈ ((0[,]1) ↑_m (1...𝑁)) → (𝐹‘𝑥):(1...𝑁)⟶(0[,]1))
75	74, 2	eleq2s 2851	. . . . . . . . . . . . . 14 ⊢ ((𝐹‘𝑥) ∈ 𝐼 → (𝐹‘𝑥):(1...𝑁)⟶(0[,]1))
76	22, 75	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝐹‘𝑥):(1...𝑁)⟶(0[,]1))
77	76	ffvelrnda 6863	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → ((𝐹‘𝑥)‘𝑛) ∈ (0[,]1))
78	13, 77	sseldi 3875	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → ((𝐹‘𝑥)‘𝑛) ∈ ℝ)
79	73, 78	resubcld 11148	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑥‘𝑛) − ((𝐹‘𝑥)‘𝑛)) ∈ ℝ)
80	79	an32s 652	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐼) → ((𝑥‘𝑛) − ((𝐹‘𝑥)‘𝑛)) ∈ ℝ)
81	80	fmpttd 6891	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐼 ↦ ((𝑥‘𝑛) − ((𝐹‘𝑥)‘𝑛))):𝐼⟶ℝ)
82		frn 6511	. . . . . . . 8 ⊢ ((𝑥 ∈ 𝐼 ↦ ((𝑥‘𝑛) − ((𝐹‘𝑥)‘𝑛))):𝐼⟶ℝ → ran (𝑥 ∈ 𝐼 ↦ ((𝑥‘𝑛) − ((𝐹‘𝑥)‘𝑛))) ⊆ ℝ)
83	38	cnfldtopon 23537	. . . . . . . . 9 ⊢ (TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ)
84		ax-resscn 10674	. . . . . . . . 9 ⊢ ℝ ⊆ ℂ
85		cnrest2 22039	. . . . . . . . 9 ⊢ (((TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ) ∧ ran (𝑥 ∈ 𝐼 ↦ ((𝑥‘𝑛) − ((𝐹‘𝑥)‘𝑛))) ⊆ ℝ ∧ ℝ ⊆ ℂ) → ((𝑥 ∈ 𝐼 ↦ ((𝑥‘𝑛) − ((𝐹‘𝑥)‘𝑛))) ∈ ((𝑅 ↾_t 𝐼) Cn (TopOpen‘ℂ_fld)) ↔ (𝑥 ∈ 𝐼 ↦ ((𝑥‘𝑛) − ((𝐹‘𝑥)‘𝑛))) ∈ ((𝑅 ↾_t 𝐼) Cn ((TopOpen‘ℂ_fld) ↾_t ℝ))))
86	83, 84, 85	mp3an13 1453	. . . . . . . 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 235	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐼 ↦ ((𝑥‘𝑛) − ((𝐹‘𝑥)‘𝑛))) ∈ ((𝑅 ↾_t 𝐼) Cn ((TopOpen‘ℂ_fld) ↾_t ℝ)))
89	54	adantl 485	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((𝑅 ↾_t 𝐼) Cn (((1...𝑁) × {(topGen‘ran (,))})‘𝑛)) = ((𝑅 ↾_t 𝐼) Cn ((TopOpen‘ℂ_fld) ↾_t ℝ)))
90	88, 89	eleqtrrd 2836	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐼 ↦ ((𝑥‘𝑛) − ((𝐹‘𝑥)‘𝑛))) ∈ ((𝑅 ↾_t 𝐼) Cn (((1...𝑁) × {(topGen‘ran (,))})‘𝑛)))
91	3, 32, 33, 36, 90	ptcn 22380	. . . 4 ⊢ (𝜑 → (𝑥 ∈ 𝐼 ↦ (𝑛 ∈ (1...𝑁) ↦ ((𝑥‘𝑛) − ((𝐹‘𝑥)‘𝑛)))) ∈ ((𝑅 ↾_t 𝐼) Cn 𝑅))
92	31, 91	eqeltrd 2833	. . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐼 ↦ (𝑥 ∘_f − (𝐹‘𝑥))) ∈ ((𝑅 ↾_t 𝐼) Cn 𝑅))
93		simpr2 1196	. . . . . 6 ⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧 ∈ 𝐼 ∧ (𝑧‘𝑛) = 0)) → 𝑧 ∈ 𝐼)
94		id 22	. . . . . . . . 9 ⊢ (𝑥 = 𝑧 → 𝑥 = 𝑧)
95		fveq2 6676	. . . . . . . . 9 ⊢ (𝑥 = 𝑧 → (𝐹‘𝑥) = (𝐹‘𝑧))
96	94, 95	oveq12d 7190	. . . . . . . 8 ⊢ (𝑥 = 𝑧 → (𝑥 ∘_f − (𝐹‘𝑥)) = (𝑧 ∘_f − (𝐹‘𝑧)))
97		eqid 2738	. . . . . . . 8 ⊢ (𝑥 ∈ 𝐼 ↦ (𝑥 ∘_f − (𝐹‘𝑥))) = (𝑥 ∈ 𝐼 ↦ (𝑥 ∘_f − (𝐹‘𝑥)))
98		ovex 7205	. . . . . . . 8 ⊢ (𝑧 ∘_f − (𝐹‘𝑧)) ∈ V
99	96, 97, 98	fvmpt 6777	. . . . . . 7 ⊢ (𝑧 ∈ 𝐼 → ((𝑥 ∈ 𝐼 ↦ (𝑥 ∘_f − (𝐹‘𝑥)))‘𝑧) = (𝑧 ∘_f − (𝐹‘𝑧)))
100	99	fveq1d 6678	. . . . . 6 ⊢ (𝑧 ∈ 𝐼 → (((𝑥 ∈ 𝐼 ↦ (𝑥 ∘_f − (𝐹‘𝑥)))‘𝑧)‘𝑛) = ((𝑧 ∘_f − (𝐹‘𝑧))‘𝑛))
101	93, 100	syl 17	. . . . 5 ⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧 ∈ 𝐼 ∧ (𝑧‘𝑛) = 0)) → (((𝑥 ∈ 𝐼 ↦ (𝑥 ∘_f − (𝐹‘𝑥)))‘𝑧)‘𝑛) = ((𝑧 ∘_f − (𝐹‘𝑧))‘𝑛))
102		elmapfn 8477	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ ((0[,]1) ↑_m (1...𝑁)) → 𝑧 Fn (1...𝑁))
103	102, 2	eleq2s 2851	. . . . . . . . . . 11 ⊢ (𝑧 ∈ 𝐼 → 𝑧 Fn (1...𝑁))
104	103	adantl 485	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑧‘𝑛) = 0) ∧ 𝑧 ∈ 𝐼) → 𝑧 Fn (1...𝑁))
105	21	ffvelrnda 6863	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐼) → (𝐹‘𝑧) ∈ 𝐼)
106		elmapfn 8477	. . . . . . . . . . . . 13 ⊢ ((𝐹‘𝑧) ∈ ((0[,]1) ↑_m (1...𝑁)) → (𝐹‘𝑧) Fn (1...𝑁))
107	106, 2	eleq2s 2851	. . . . . . . . . . . 12 ⊢ ((𝐹‘𝑧) ∈ 𝐼 → (𝐹‘𝑧) Fn (1...𝑁))
108	105, 107	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐼) → (𝐹‘𝑧) Fn (1...𝑁))
109	108	adantlr 715	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑧‘𝑛) = 0) ∧ 𝑧 ∈ 𝐼) → (𝐹‘𝑧) Fn (1...𝑁))
110		ovexd 7207	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑧‘𝑛) = 0) ∧ 𝑧 ∈ 𝐼) → (1...𝑁) ∈ V)
111		simpllr 776	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑧‘𝑛) = 0) ∧ 𝑧 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → (𝑧‘𝑛) = 0)
112		eqidd 2739	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑧‘𝑛) = 0) ∧ 𝑧 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → ((𝐹‘𝑧)‘𝑛) = ((𝐹‘𝑧)‘𝑛))
113	104, 109, 110, 110, 27, 111, 112	ofval 7437	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑧‘𝑛) = 0) ∧ 𝑧 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑧 ∘_f − (𝐹‘𝑧))‘𝑛) = (0 − ((𝐹‘𝑧)‘𝑛)))
114		df-neg 10953	. . . . . . . . 9 ⊢ -((𝐹‘𝑧)‘𝑛) = (0 − ((𝐹‘𝑧)‘𝑛))
115	113, 114	eqtr4di 2791	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑧‘𝑛) = 0) ∧ 𝑧 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑧 ∘_f − (𝐹‘𝑧))‘𝑛) = -((𝐹‘𝑧)‘𝑛))
116	115	exp41 438	. . . . . . 7 ⊢ (𝜑 → ((𝑧‘𝑛) = 0 → (𝑧 ∈ 𝐼 → (𝑛 ∈ (1...𝑁) → ((𝑧 ∘_f − (𝐹‘𝑧))‘𝑛) = -((𝐹‘𝑧)‘𝑛)))))
117	116	com24 95	. . . . . 6 ⊢ (𝜑 → (𝑛 ∈ (1...𝑁) → (𝑧 ∈ 𝐼 → ((𝑧‘𝑛) = 0 → ((𝑧 ∘_f − (𝐹‘𝑧))‘𝑛) = -((𝐹‘𝑧)‘𝑛)))))
118	117	3imp2 1350	. . . . 5 ⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧 ∈ 𝐼 ∧ (𝑧‘𝑛) = 0)) → ((𝑧 ∘_f − (𝐹‘𝑧))‘𝑛) = -((𝐹‘𝑧)‘𝑛))
119	101, 118	eqtrd 2773	. . . 4 ⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧 ∈ 𝐼 ∧ (𝑧‘𝑛) = 0)) → (((𝑥 ∈ 𝐼 ↦ (𝑥 ∘_f − (𝐹‘𝑥)))‘𝑧)‘𝑛) = -((𝐹‘𝑧)‘𝑛))
120		elmapi 8461	. . . . . . . . . . . 12 ⊢ ((𝐹‘𝑧) ∈ ((0[,]1) ↑_m (1...𝑁)) → (𝐹‘𝑧):(1...𝑁)⟶(0[,]1))
121	120, 2	eleq2s 2851	. . . . . . . . . . 11 ⊢ ((𝐹‘𝑧) ∈ 𝐼 → (𝐹‘𝑧):(1...𝑁)⟶(0[,]1))
122	105, 121	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐼) → (𝐹‘𝑧):(1...𝑁)⟶(0[,]1))
123	122	ffvelrnda 6863	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → ((𝐹‘𝑧)‘𝑛) ∈ (0[,]1))
124		0xr 10768	. . . . . . . . . 10 ⊢ 0 ∈ ℝ^*
125		1xr 10780	. . . . . . . . . 10 ⊢ 1 ∈ ℝ^*
126		iccgelb 12879	. . . . . . . . . 10 ⊢ ((0 ∈ ℝ^* ∧ 1 ∈ ℝ^* ∧ ((𝐹‘𝑧)‘𝑛) ∈ (0[,]1)) → 0 ≤ ((𝐹‘𝑧)‘𝑛))
127	124, 125, 126	mp3an12 1452	. . . . . . . . 9 ⊢ (((𝐹‘𝑧)‘𝑛) ∈ (0[,]1) → 0 ≤ ((𝐹‘𝑧)‘𝑛))
128	123, 127	syl 17	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → 0 ≤ ((𝐹‘𝑧)‘𝑛))
129	13, 123	sseldi 3875	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → ((𝐹‘𝑧)‘𝑛) ∈ ℝ)
130	129	le0neg2d 11292	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → (0 ≤ ((𝐹‘𝑧)‘𝑛) ↔ -((𝐹‘𝑧)‘𝑛) ≤ 0))
131	128, 130	mpbid 235	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → -((𝐹‘𝑧)‘𝑛) ≤ 0)
132	131	an32s 652	. . . . . 6 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑧 ∈ 𝐼) → -((𝐹‘𝑧)‘𝑛) ≤ 0)
133	132	anasss 470	. . . . 5 ⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧 ∈ 𝐼)) → -((𝐹‘𝑧)‘𝑛) ≤ 0)
134	133	3adantr3 1172	. . . 4 ⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧 ∈ 𝐼 ∧ (𝑧‘𝑛) = 0)) → -((𝐹‘𝑧)‘𝑛) ≤ 0)
135	119, 134	eqbrtrd 5052	. . 3 ⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧 ∈ 𝐼 ∧ (𝑧‘𝑛) = 0)) → (((𝑥 ∈ 𝐼 ↦ (𝑥 ∘_f − (𝐹‘𝑥)))‘𝑧)‘𝑛) ≤ 0)
136		iccleub 12878	. . . . . . . . . 10 ⊢ ((0 ∈ ℝ^* ∧ 1 ∈ ℝ^* ∧ ((𝐹‘𝑧)‘𝑛) ∈ (0[,]1)) → ((𝐹‘𝑧)‘𝑛) ≤ 1)
137	124, 125, 136	mp3an12 1452	. . . . . . . . 9 ⊢ (((𝐹‘𝑧)‘𝑛) ∈ (0[,]1) → ((𝐹‘𝑧)‘𝑛) ≤ 1)
138	123, 137	syl 17	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → ((𝐹‘𝑧)‘𝑛) ≤ 1)
139		1red 10722	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → 1 ∈ ℝ)
140	139, 129	subge0d 11310	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → (0 ≤ (1 − ((𝐹‘𝑧)‘𝑛)) ↔ ((𝐹‘𝑧)‘𝑛) ≤ 1))
141	138, 140	mpbird 260	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → 0 ≤ (1 − ((𝐹‘𝑧)‘𝑛)))
142	141	an32s 652	. . . . . 6 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑧 ∈ 𝐼) → 0 ≤ (1 − ((𝐹‘𝑧)‘𝑛)))
143	142	anasss 470	. . . . 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 485	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑧‘𝑛) = 1) ∧ 𝑧 ∈ 𝐼) → 𝑧 Fn (1...𝑁))
148	108	adantlr 715	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑧‘𝑛) = 1) ∧ 𝑧 ∈ 𝐼) → (𝐹‘𝑧) Fn (1...𝑁))
149		ovexd 7207	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑧‘𝑛) = 1) ∧ 𝑧 ∈ 𝐼) → (1...𝑁) ∈ V)
150		simpllr 776	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑧‘𝑛) = 1) ∧ 𝑧 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → (𝑧‘𝑛) = 1)
151		eqidd 2739	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑧‘𝑛) = 1) ∧ 𝑧 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → ((𝐹‘𝑧)‘𝑛) = ((𝐹‘𝑧)‘𝑛))
152	147, 148, 149, 149, 27, 150, 151	ofval 7437	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑧‘𝑛) = 1) ∧ 𝑧 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑧 ∘_f − (𝐹‘𝑧))‘𝑛) = (1 − ((𝐹‘𝑧)‘𝑛)))
153	152	exp41 438	. . . . . . 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 2773	. . . 4 ⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧 ∈ 𝐼 ∧ (𝑧‘𝑛) = 1)) → (((𝑥 ∈ 𝐼 ↦ (𝑥 ∘_f − (𝐹‘𝑥)))‘𝑧)‘𝑛) = (1 − ((𝐹‘𝑧)‘𝑛)))
157	144, 156	breqtrrd 5058	. . 3 ⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧 ∈ 𝐼 ∧ (𝑧‘𝑛) = 1)) → 0 ≤ (((𝑥 ∈ 𝐼 ↦ (𝑥 ∘_f − (𝐹‘𝑥)))‘𝑧)‘𝑛))
158	1, 2, 3, 92, 135, 157	poimir 35455	. 2 ⊢ (𝜑 → ∃𝑐 ∈ 𝐼 ((𝑥 ∈ 𝐼 ↦ (𝑥 ∘_f − (𝐹‘𝑥)))‘𝑐) = ((1...𝑁) × {0}))
159		id 22	. . . . . . . 8 ⊢ (𝑥 = 𝑐 → 𝑥 = 𝑐)
160		fveq2 6676	. . . . . . . 8 ⊢ (𝑥 = 𝑐 → (𝐹‘𝑥) = (𝐹‘𝑐))
161	159, 160	oveq12d 7190	. . . . . . 7 ⊢ (𝑥 = 𝑐 → (𝑥 ∘_f − (𝐹‘𝑥)) = (𝑐 ∘_f − (𝐹‘𝑐)))
162		ovex 7205	. . . . . . 7 ⊢ (𝑐 ∘_f − (𝐹‘𝑐)) ∈ V
163	161, 97, 162	fvmpt 6777	. . . . . 6 ⊢ (𝑐 ∈ 𝐼 → ((𝑥 ∈ 𝐼 ↦ (𝑥 ∘_f − (𝐹‘𝑥)))‘𝑐) = (𝑐 ∘_f − (𝐹‘𝑐)))
164	163	adantl 485	. . . . 5 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐼) → ((𝑥 ∈ 𝐼 ↦ (𝑥 ∘_f − (𝐹‘𝑥)))‘𝑐) = (𝑐 ∘_f − (𝐹‘𝑐)))
165	164	eqeq1d 2740	. . . 4 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐼) → (((𝑥 ∈ 𝐼 ↦ (𝑥 ∘_f − (𝐹‘𝑥)))‘𝑐) = ((1...𝑁) × {0}) ↔ (𝑐 ∘_f − (𝐹‘𝑐)) = ((1...𝑁) × {0})))
166		elmapfn 8477	. . . . . . . . . . 11 ⊢ (𝑐 ∈ ((0[,]1) ↑_m (1...𝑁)) → 𝑐 Fn (1...𝑁))
167	166, 2	eleq2s 2851	. . . . . . . . . 10 ⊢ (𝑐 ∈ 𝐼 → 𝑐 Fn (1...𝑁))
168	167	adantl 485	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐼) → 𝑐 Fn (1...𝑁))
169	21	ffvelrnda 6863	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐼) → (𝐹‘𝑐) ∈ 𝐼)
170		elmapfn 8477	. . . . . . . . . . 11 ⊢ ((𝐹‘𝑐) ∈ ((0[,]1) ↑_m (1...𝑁)) → (𝐹‘𝑐) Fn (1...𝑁))
171	170, 2	eleq2s 2851	. . . . . . . . . 10 ⊢ ((𝐹‘𝑐) ∈ 𝐼 → (𝐹‘𝑐) Fn (1...𝑁))
172	169, 171	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐼) → (𝐹‘𝑐) Fn (1...𝑁))
173		ovexd 7207	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐼) → (1...𝑁) ∈ V)
174		eqidd 2739	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → (𝑐‘𝑛) = (𝑐‘𝑛))
175		eqidd 2739	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → ((𝐹‘𝑐)‘𝑛) = ((𝐹‘𝑐)‘𝑛))
176	168, 172, 173, 173, 27, 174, 175	ofval 7437	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑐 ∘_f − (𝐹‘𝑐))‘𝑛) = ((𝑐‘𝑛) − ((𝐹‘𝑐)‘𝑛)))
177		c0ex 10715	. . . . . . . . . 10 ⊢ 0 ∈ V
178	177	fvconst2 6978	. . . . . . . . 9 ⊢ (𝑛 ∈ (1...𝑁) → (((1...𝑁) × {0})‘𝑛) = 0)
179	178	adantl 485	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → (((1...𝑁) × {0})‘𝑛) = 0)
180	176, 179	eqeq12d 2754	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → (((𝑐 ∘_f − (𝐹‘𝑐))‘𝑛) = (((1...𝑁) × {0})‘𝑛) ↔ ((𝑐‘𝑛) − ((𝐹‘𝑐)‘𝑛)) = 0))
181	13, 84	sstri 3886	. . . . . . . . . 10 ⊢ (0[,]1) ⊆ ℂ
182		elmapi 8461	. . . . . . . . . . . 12 ⊢ (𝑐 ∈ ((0[,]1) ↑_m (1...𝑁)) → 𝑐:(1...𝑁)⟶(0[,]1))
183	182, 2	eleq2s 2851	. . . . . . . . . . 11 ⊢ (𝑐 ∈ 𝐼 → 𝑐:(1...𝑁)⟶(0[,]1))
184	183	ffvelrnda 6863	. . . . . . . . . 10 ⊢ ((𝑐 ∈ 𝐼 ∧ 𝑛 ∈ (1...𝑁)) → (𝑐‘𝑛) ∈ (0[,]1))
185	181, 184	sseldi 3875	. . . . . . . . 9 ⊢ ((𝑐 ∈ 𝐼 ∧ 𝑛 ∈ (1...𝑁)) → (𝑐‘𝑛) ∈ ℂ)
186	185	adantll 714	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → (𝑐‘𝑛) ∈ ℂ)
187		elmapi 8461	. . . . . . . . . . . 12 ⊢ ((𝐹‘𝑐) ∈ ((0[,]1) ↑_m (1...𝑁)) → (𝐹‘𝑐):(1...𝑁)⟶(0[,]1))
188	187, 2	eleq2s 2851	. . . . . . . . . . 11 ⊢ ((𝐹‘𝑐) ∈ 𝐼 → (𝐹‘𝑐):(1...𝑁)⟶(0[,]1))
189	169, 188	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐼) → (𝐹‘𝑐):(1...𝑁)⟶(0[,]1))
190	189	ffvelrnda 6863	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → ((𝐹‘𝑐)‘𝑛) ∈ (0[,]1))
191	181, 190	sseldi 3875	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → ((𝐹‘𝑐)‘𝑛) ∈ ℂ)
192	186, 191	subeq0ad 11087	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → (((𝑐‘𝑛) − ((𝐹‘𝑐)‘𝑛)) = 0 ↔ (𝑐‘𝑛) = ((𝐹‘𝑐)‘𝑛)))
193	180, 192	bitrd 282	. . . . . 6 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → (((𝑐 ∘_f − (𝐹‘𝑐))‘𝑛) = (((1...𝑁) × {0})‘𝑛) ↔ (𝑐‘𝑛) = ((𝐹‘𝑐)‘𝑛)))
194	193	ralbidva 3108	. . . . 5 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐼) → (∀𝑛 ∈ (1...𝑁)((𝑐 ∘_f − (𝐹‘𝑐))‘𝑛) = (((1...𝑁) × {0})‘𝑛) ↔ ∀𝑛 ∈ (1...𝑁)(𝑐‘𝑛) = ((𝐹‘𝑐)‘𝑛)))
195	168, 172, 173, 173, 27	offn 7439	. . . . . 6 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐼) → (𝑐 ∘_f − (𝐹‘𝑐)) Fn (1...𝑁))
196		fnconstg 6566	. . . . . . 7 ⊢ (0 ∈ V → ((1...𝑁) × {0}) Fn (1...𝑁))
197	177, 196	ax-mp 5	. . . . . 6 ⊢ ((1...𝑁) × {0}) Fn (1...𝑁)
198		eqfnfv 6811	. . . . . 6 ⊢ (((𝑐 ∘_f − (𝐹‘𝑐)) Fn (1...𝑁) ∧ ((1...𝑁) × {0}) Fn (1...𝑁)) → ((𝑐 ∘_f − (𝐹‘𝑐)) = ((1...𝑁) × {0}) ↔ ∀𝑛 ∈ (1...𝑁)((𝑐 ∘_f − (𝐹‘𝑐))‘𝑛) = (((1...𝑁) × {0})‘𝑛)))
199	195, 197, 198	sylancl 589	. . . . 5 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐼) → ((𝑐 ∘_f − (𝐹‘𝑐)) = ((1...𝑁) × {0}) ↔ ∀𝑛 ∈ (1...𝑁)((𝑐 ∘_f − (𝐹‘𝑐))‘𝑛) = (((1...𝑁) × {0})‘𝑛)))
200		eqfnfv 6811	. . . . . 6 ⊢ ((𝑐 Fn (1...𝑁) ∧ (𝐹‘𝑐) Fn (1...𝑁)) → (𝑐 = (𝐹‘𝑐) ↔ ∀𝑛 ∈ (1...𝑁)(𝑐‘𝑛) = ((𝐹‘𝑐)‘𝑛)))
201	168, 172, 200	syl2anc 587	. . . . 5 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐼) → (𝑐 = (𝐹‘𝑐) ↔ ∀𝑛 ∈ (1...𝑁)(𝑐‘𝑛) = ((𝐹‘𝑐)‘𝑛)))
202	194, 199, 201	3bitr4d 314	. . . 4 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐼) → ((𝑐 ∘_f − (𝐹‘𝑐)) = ((1...𝑁) × {0}) ↔ 𝑐 = (𝐹‘𝑐)))
203	165, 202	bitrd 282	. . 3 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐼) → (((𝑥 ∈ 𝐼 ↦ (𝑥 ∘_f − (𝐹‘𝑥)))‘𝑐) = ((1...𝑁) × {0}) ↔ 𝑐 = (𝐹‘𝑐)))
204	203	rexbidva 3206	. 2 ⊢ (𝜑 → (∃𝑐 ∈ 𝐼 ((𝑥 ∈ 𝐼 ↦ (𝑥 ∘_f − (𝐹‘𝑥)))‘𝑐) = ((1...𝑁) × {0}) ↔ ∃𝑐 ∈ 𝐼 𝑐 = (𝐹‘𝑐)))
205	158, 204	mpbid 235	1 ⊢ (𝜑 → ∃𝑐 ∈ 𝐼 𝑐 = (𝐹‘𝑐))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 209 ∧ wa 399 ∧ w3a 1088 = wceq 1542 ∈ wcel 2114 ∀wral 3053 ∃wrex 3054 Vcvv 3398 ⊆ wss 3843 {csn 4516 class class class wbr 5030 ↦ cmpt 5110 × cxp 5523 ran crn 5526 ↾ cres 5527 Fn wfn 6334 ⟶wf 6335 ‘cfv 6339 (class class class)co 7172 ∘_f cof 7425 ↑_m cmap 8439 ℂcc 10615 ℝcr 10616 0cc0 10617 1c1 10618 ℝ^*cxr 10754 ≤ cle 10756 − cmin 10950 -cneg 10951 ℕcn 11718 (,)cioo 12823 [,]cicc 12826 ...cfz 12983 ↾_t crest 16799 TopOpenctopn 16800 topGenctg 16816 ∏_tcpt 16817 ℂ_fldccnfld 20219 Topctop 21646 TopOnctopon 21663 Cn ccn 21977 ×_t ctx 22313

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1975 ax-7 2020 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2162 ax-12 2179 ax-ext 2710 ax-rep 5154 ax-sep 5167 ax-nul 5174 ax-pow 5232 ax-pr 5296 ax-un 7481 ax-inf2 9179 ax-cnex 10673 ax-resscn 10674 ax-1cn 10675 ax-icn 10676 ax-addcl 10677 ax-addrcl 10678 ax-mulcl 10679 ax-mulrcl 10680 ax-mulcom 10681 ax-addass 10682 ax-mulass 10683 ax-distr 10684 ax-i2m1 10685 ax-1ne0 10686 ax-1rid 10687 ax-rnegex 10688 ax-rrecex 10689 ax-cnre 10690 ax-pre-lttri 10691 ax-pre-lttrn 10692 ax-pre-ltadd 10693 ax-pre-mulgt0 10694 ax-pre-sup 10695

This theorem depends on definitions: df-bi 210 df-an 400 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1787 df-nf 1791 df-sb 2075 df-mo 2540 df-eu 2570 df-clab 2717 df-cleq 2730 df-clel 2811 df-nfc 2881 df-ne 2935 df-nel 3039 df-ral 3058 df-rex 3059 df-reu 3060 df-rmo 3061 df-rab 3062 df-v 3400 df-sbc 3681 df-csb 3791 df-dif 3846 df-un 3848 df-in 3850 df-ss 3860 df-pss 3862 df-nul 4212 df-if 4415 df-pw 4490 df-sn 4517 df-pr 4519 df-tp 4521 df-op 4523 df-uni 4797 df-int 4837 df-iun 4883 df-iin 4884 df-disj 4996 df-br 5031 df-opab 5093 df-mpt 5111 df-tr 5137 df-id 5429 df-eprel 5434 df-po 5442 df-so 5443 df-fr 5483 df-se 5484 df-we 5485 df-xp 5531 df-rel 5532 df-cnv 5533 df-co 5534 df-dm 5535 df-rn 5536 df-res 5537 df-ima 5538 df-pred 6129 df-ord 6175 df-on 6176 df-lim 6177 df-suc 6178 df-iota 6297 df-fun 6341 df-fn 6342 df-f 6343 df-f1 6344 df-fo 6345 df-f1o 6346 df-fv 6347 df-isom 6348 df-riota 7129 df-ov 7175 df-oprab 7176 df-mpo 7177 df-of 7427 df-om 7602 df-1st 7716 df-2nd 7717 df-supp 7859 df-wrecs 7978 df-recs 8039 df-rdg 8077 df-1o 8133 df-2o 8134 df-oadd 8137 df-omul 8138 df-er 8322 df-map 8441 df-pm 8442 df-ixp 8510 df-en 8558 df-dom 8559 df-sdom 8560 df-fin 8561 df-fsupp 8909 df-fi 8950 df-sup 8981 df-inf 8982 df-oi 9049 df-dju 9405 df-card 9443 df-acn 9446 df-pnf 10757 df-mnf 10758 df-xr 10759 df-ltxr 10760 df-le 10761 df-sub 10952 df-neg 10953 df-div 11378 df-nn 11719 df-2 11781 df-3 11782 df-4 11783 df-5 11784 df-6 11785 df-7 11786 df-8 11787 df-9 11788 df-n0 11979 df-xnn0 12051 df-z 12065 df-dec 12182 df-uz 12327 df-q 12433 df-rp 12475 df-xneg 12592 df-xadd 12593 df-xmul 12594 df-ioo 12827 df-icc 12830 df-fz 12984 df-fzo 13127 df-fl 13255 df-seq 13463 df-exp 13524 df-fac 13728 df-bc 13757 df-hash 13785 df-cj 14550 df-re 14551 df-im 14552 df-sqrt 14686 df-abs 14687 df-clim 14937 df-sum 15138 df-dvds 15702 df-struct 16590 df-ndx 16591 df-slot 16592 df-base 16594 df-sets 16595 df-ress 16596 df-plusg 16683 df-mulr 16684 df-starv 16685 df-sca 16686 df-vsca 16687 df-ip 16688 df-tset 16689 df-ple 16690 df-ds 16692 df-unif 16693 df-hom 16694 df-cco 16695 df-rest 16801 df-topn 16802 df-0g 16820 df-gsum 16821 df-topgen 16822 df-pt 16823 df-prds 16826 df-xrs 16880 df-qtop 16885 df-imas 16886 df-xps 16888 df-mre 16962 df-mrc 16963 df-acs 16965 df-ps 17928 df-tsr 17929 df-mgm 17970 df-sgrp 18019 df-mnd 18030 df-submnd 18075 df-mulg 18345 df-cntz 18567 df-cmn 19028 df-psmet 20211 df-xmet 20212 df-met 20213 df-bl 20214 df-mopn 20215 df-cnfld 20220 df-top 21647 df-topon 21664 df-topsp 21686 df-bases 21699 df-cld 21772 df-ntr 21773 df-cls 21774 df-lp 21889 df-cn 21980 df-cnp 21981 df-t1 22067 df-haus 22068 df-cmp 22140 df-tx 22315 df-hmeo 22508 df-hmph 22509 df-xms 23075 df-ms 23076 df-tms 23077 df-ii 23631

This theorem is referenced by: (None)

W3C validator