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 34925

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 8428	. . . . . . . 8 ⊢ (𝑥 ∈ ((0[,]1) ↑_m (1...𝑁)) → 𝑥 Fn (1...𝑁))
5	4, 2	eleq2s 2931	. . . . . . 7 ⊢ (𝑥 ∈ 𝐼 → 𝑥 Fn (1...𝑁))
6	5	adantl 484	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑥 Fn (1...𝑁))
7		broucube.1	. . . . . . . . 9 ⊢ (𝜑 → 𝐹 ∈ ((𝑅 ↾_t 𝐼) Cn (𝑅 ↾_t 𝐼)))
8		ovex 7188	. . . . . . . . . . . . 13 ⊢ (1...𝑁) ∈ V
9		retopon 23371	. . . . . . . . . . . . 13 ⊢ (topGen‘ran (,)) ∈ (TopOn‘ℝ)
10	3	pttoponconst 22204	. . . . . . . . . . . . 13 ⊢ (((1...𝑁) ∈ V ∧ (topGen‘ran (,)) ∈ (TopOn‘ℝ)) → 𝑅 ∈ (TopOn‘(ℝ ↑_m (1...𝑁))))
11	8, 9, 10	mp2an 690	. . . . . . . . . . . 12 ⊢ 𝑅 ∈ (TopOn‘(ℝ ↑_m (1...𝑁)))
12		reex 10627	. . . . . . . . . . . . . 14 ⊢ ℝ ∈ V
13		unitssre 12884	. . . . . . . . . . . . . 14 ⊢ (0[,]1) ⊆ ℝ
14		mapss 8452	. . . . . . . . . . . . . 14 ⊢ ((ℝ ∈ V ∧ (0[,]1) ⊆ ℝ) → ((0[,]1) ↑_m (1...𝑁)) ⊆ (ℝ ↑_m (1...𝑁)))
15	12, 13, 14	mp2an 690	. . . . . . . . . . . . 13 ⊢ ((0[,]1) ↑_m (1...𝑁)) ⊆ (ℝ ↑_m (1...𝑁))
16	2, 15	eqsstri 4000	. . . . . . . . . . . 12 ⊢ 𝐼 ⊆ (ℝ ↑_m (1...𝑁))
17		resttopon 21768	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ (TopOn‘(ℝ ↑_m (1...𝑁))) ∧ 𝐼 ⊆ (ℝ ↑_m (1...𝑁))) → (𝑅 ↾_t 𝐼) ∈ (TopOn‘𝐼))
18	11, 16, 17	mp2an 690	. . . . . . . . . . 11 ⊢ (𝑅 ↾_t 𝐼) ∈ (TopOn‘𝐼)
19	18	toponunii 21523	. . . . . . . . . 10 ⊢ 𝐼 = ∪ (𝑅 ↾_t 𝐼)
20	19, 19	cnf 21853	. . . . . . . . 9 ⊢ (𝐹 ∈ ((𝑅 ↾_t 𝐼) Cn (𝑅 ↾_t 𝐼)) → 𝐹:𝐼⟶𝐼)
21	7, 20	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝐹:𝐼⟶𝐼)
22	21	ffvelrnda 6850	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝐹‘𝑥) ∈ 𝐼)
23		elmapfn 8428	. . . . . . . 8 ⊢ ((𝐹‘𝑥) ∈ ((0[,]1) ↑_m (1...𝑁)) → (𝐹‘𝑥) Fn (1...𝑁))
24	23, 2	eleq2s 2931	. . . . . . 7 ⊢ ((𝐹‘𝑥) ∈ 𝐼 → (𝐹‘𝑥) Fn (1...𝑁))
25	22, 24	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝐹‘𝑥) Fn (1...𝑁))
26		ovexd 7190	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (1...𝑁) ∈ V)
27		inidm 4194	. . . . . 6 ⊢ ((1...𝑁) ∩ (1...𝑁)) = (1...𝑁)
28		eqidd 2822	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → (𝑥‘𝑛) = (𝑥‘𝑛))
29		eqidd 2822	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → ((𝐹‘𝑥)‘𝑛) = ((𝐹‘𝑥)‘𝑛))
30	6, 25, 26, 26, 27, 28, 29	offval 7415	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑥 ∘_f − (𝐹‘𝑥)) = (𝑛 ∈ (1...𝑁) ↦ ((𝑥‘𝑛) − ((𝐹‘𝑥)‘𝑛))))
31	30	mpteq2dva 5160	. . . 4 ⊢ (𝜑 → (𝑥 ∈ 𝐼 ↦ (𝑥 ∘_f − (𝐹‘𝑥))) = (𝑥 ∈ 𝐼 ↦ (𝑛 ∈ (1...𝑁) ↦ ((𝑥‘𝑛) − ((𝐹‘𝑥)‘𝑛)))))
32	18	a1i 11	. . . . 5 ⊢ (𝜑 → (𝑅 ↾_t 𝐼) ∈ (TopOn‘𝐼))
33		ovexd 7190	. . . . 5 ⊢ (𝜑 → (1...𝑁) ∈ V)
34		retop 23369	. . . . . . 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 2821	. . . . . . . . . . . 12 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
39	38	cnfldtop 23391	. . . . . . . . . . 11 ⊢ (TopOpen‘ℂ_fld) ∈ Top
40		cnrest2r 21894	. . . . . . . . . . 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 5904	. . . . . . . . . . . . 13 ⊢ (𝐼 ⊆ (ℝ ↑_m (1...𝑁)) → ((𝑥 ∈ (ℝ ↑_m (1...𝑁)) ↦ (𝑥‘𝑛)) ↾ 𝐼) = (𝑥 ∈ 𝐼 ↦ (𝑥‘𝑛)))
43	16, 42	ax-mp 5	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ (ℝ ↑_m (1...𝑁)) ↦ (𝑥‘𝑛)) ↾ 𝐼) = (𝑥 ∈ 𝐼 ↦ (𝑥‘𝑛))
44	11	toponunii 21523	. . . . . . . . . . . . . . 15 ⊢ (ℝ ↑_m (1...𝑁)) = ∪ 𝑅
45	44, 3	ptpjcn 22218	. . . . . . . . . . . . . 14 ⊢ (((1...𝑁) ∈ V ∧ ((1...𝑁) × {(topGen‘ran (,))}):(1...𝑁)⟶Top ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ (ℝ ↑_m (1...𝑁)) ↦ (𝑥‘𝑛)) ∈ (𝑅 Cn (((1...𝑁) × {(topGen‘ran (,))})‘𝑛)))
46	8, 35, 45	mp3an12 1447	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ (1...𝑁) → (𝑥 ∈ (ℝ ↑_m (1...𝑁)) ↦ (𝑥‘𝑛)) ∈ (𝑅 Cn (((1...𝑁) × {(topGen‘ran (,))})‘𝑛)))
47	44	cnrest 21892	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ (ℝ ↑_m (1...𝑁)) ↦ (𝑥‘𝑛)) ∈ (𝑅 Cn (((1...𝑁) × {(topGen‘ran (,))})‘𝑛)) ∧ 𝐼 ⊆ (ℝ ↑_m (1...𝑁))) → ((𝑥 ∈ (ℝ ↑_m (1...𝑁)) ↦ (𝑥‘𝑛)) ↾ 𝐼) ∈ ((𝑅 ↾_t 𝐼) Cn (((1...𝑁) × {(topGen‘ran (,))})‘𝑛)))
48	46, 16, 47	sylancl 588	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ (1...𝑁) → ((𝑥 ∈ (ℝ ↑_m (1...𝑁)) ↦ (𝑥‘𝑛)) ↾ 𝐼) ∈ ((𝑅 ↾_t 𝐼) Cn (((1...𝑁) × {(topGen‘ran (,))})‘𝑛)))
49	43, 48	eqeltrrid 2918	. . . . . . . . . . 11 ⊢ (𝑛 ∈ (1...𝑁) → (𝑥 ∈ 𝐼 ↦ (𝑥‘𝑛)) ∈ ((𝑅 ↾_t 𝐼) Cn (((1...𝑁) × {(topGen‘ran (,))})‘𝑛)))
50		fvex 6682	. . . . . . . . . . . . . 14 ⊢ (topGen‘ran (,)) ∈ V
51	50	fvconst2 6965	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ (1...𝑁) → (((1...𝑁) × {(topGen‘ran (,))})‘𝑛) = (topGen‘ran (,)))
52	38	tgioo2 23410	. . . . . . . . . . . . 13 ⊢ (topGen‘ran (,)) = ((TopOpen‘ℂ_fld) ↾_t ℝ)
53	51, 52	syl6eq 2872	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ (1...𝑁) → (((1...𝑁) × {(topGen‘ran (,))})‘𝑛) = ((TopOpen‘ℂ_fld) ↾_t ℝ))
54	53	oveq2d 7171	. . . . . . . . . . 11 ⊢ (𝑛 ∈ (1...𝑁) → ((𝑅 ↾_t 𝐼) Cn (((1...𝑁) × {(topGen‘ran (,))})‘𝑛)) = ((𝑅 ↾_t 𝐼) Cn ((TopOpen‘ℂ_fld) ↾_t ℝ)))
55	49, 54	eleqtrd 2915	. . . . . . . . . 10 ⊢ (𝑛 ∈ (1...𝑁) → (𝑥 ∈ 𝐼 ↦ (𝑥‘𝑛)) ∈ ((𝑅 ↾_t 𝐼) Cn ((TopOpen‘ℂ_fld) ↾_t ℝ)))
56	41, 55	sseldi 3964	. . . . . . . . 9 ⊢ (𝑛 ∈ (1...𝑁) → (𝑥 ∈ 𝐼 ↦ (𝑥‘𝑛)) ∈ ((𝑅 ↾_t 𝐼) Cn (TopOpen‘ℂ_fld)))
57	56	adantl 484	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐼 ↦ (𝑥‘𝑛)) ∈ ((𝑅 ↾_t 𝐼) Cn (TopOpen‘ℂ_fld)))
58	21	feqmptd 6732	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐼 ↦ (𝐹‘𝑥)))
59	58, 7	eqeltrrd 2914	. . . . . . . . . 10 ⊢ (𝜑 → (𝑥 ∈ 𝐼 ↦ (𝐹‘𝑥)) ∈ ((𝑅 ↾_t 𝐼) Cn (𝑅 ↾_t 𝐼)))
60	59	adantr 483	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐼 ↦ (𝐹‘𝑥)) ∈ ((𝑅 ↾_t 𝐼) Cn (𝑅 ↾_t 𝐼)))
61		fveq1 6668	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑧 → (𝑥‘𝑛) = (𝑧‘𝑛))
62	61	cbvmptv 5168	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝐼 ↦ (𝑥‘𝑛)) = (𝑧 ∈ 𝐼 ↦ (𝑧‘𝑛))
63	62, 57	eqeltrrid 2918	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑧 ∈ 𝐼 ↦ (𝑧‘𝑛)) ∈ ((𝑅 ↾_t 𝐼) Cn (TopOpen‘ℂ_fld)))
64		fveq1 6668	. . . . . . . . 9 ⊢ (𝑧 = (𝐹‘𝑥) → (𝑧‘𝑛) = ((𝐹‘𝑥)‘𝑛))
65	37, 60, 37, 63, 64	cnmpt11 22270	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐼 ↦ ((𝐹‘𝑥)‘𝑛)) ∈ ((𝑅 ↾_t 𝐼) Cn (TopOpen‘ℂ_fld)))
66	38	subcn 23473	. . . . . . . . 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 22273	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐼 ↦ ((𝑥‘𝑛) − ((𝐹‘𝑥)‘𝑛))) ∈ ((𝑅 ↾_t 𝐼) Cn (TopOpen‘ℂ_fld)))
69		elmapi 8427	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ((0[,]1) ↑_m (1...𝑁)) → 𝑥:(1...𝑁)⟶(0[,]1))
70	69, 2	eleq2s 2931	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ 𝐼 → 𝑥:(1...𝑁)⟶(0[,]1))
71	70	ffvelrnda 6850	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ 𝐼 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥‘𝑛) ∈ (0[,]1))
72	13, 71	sseldi 3964	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ 𝐼 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥‘𝑛) ∈ ℝ)
73	72	adantll 712	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → (𝑥‘𝑛) ∈ ℝ)
74		elmapi 8427	. . . . . . . . . . . . . . 15 ⊢ ((𝐹‘𝑥) ∈ ((0[,]1) ↑_m (1...𝑁)) → (𝐹‘𝑥):(1...𝑁)⟶(0[,]1))
75	74, 2	eleq2s 2931	. . . . . . . . . . . . . 14 ⊢ ((𝐹‘𝑥) ∈ 𝐼 → (𝐹‘𝑥):(1...𝑁)⟶(0[,]1))
76	22, 75	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝐹‘𝑥):(1...𝑁)⟶(0[,]1))
77	76	ffvelrnda 6850	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → ((𝐹‘𝑥)‘𝑛) ∈ (0[,]1))
78	13, 77	sseldi 3964	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → ((𝐹‘𝑥)‘𝑛) ∈ ℝ)
79	73, 78	resubcld 11067	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑥‘𝑛) − ((𝐹‘𝑥)‘𝑛)) ∈ ℝ)
80	79	an32s 650	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐼) → ((𝑥‘𝑛) − ((𝐹‘𝑥)‘𝑛)) ∈ ℝ)
81	80	fmpttd 6878	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐼 ↦ ((𝑥‘𝑛) − ((𝐹‘𝑥)‘𝑛))):𝐼⟶ℝ)
82		frn 6519	. . . . . . . 8 ⊢ ((𝑥 ∈ 𝐼 ↦ ((𝑥‘𝑛) − ((𝐹‘𝑥)‘𝑛))):𝐼⟶ℝ → ran (𝑥 ∈ 𝐼 ↦ ((𝑥‘𝑛) − ((𝐹‘𝑥)‘𝑛))) ⊆ ℝ)
83	38	cnfldtopon 23390	. . . . . . . . 9 ⊢ (TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ)
84		ax-resscn 10593	. . . . . . . . 9 ⊢ ℝ ⊆ ℂ
85		cnrest2 21893	. . . . . . . . 9 ⊢ (((TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ) ∧ ran (𝑥 ∈ 𝐼 ↦ ((𝑥‘𝑛) − ((𝐹‘𝑥)‘𝑛))) ⊆ ℝ ∧ ℝ ⊆ ℂ) → ((𝑥 ∈ 𝐼 ↦ ((𝑥‘𝑛) − ((𝐹‘𝑥)‘𝑛))) ∈ ((𝑅 ↾_t 𝐼) Cn (TopOpen‘ℂ_fld)) ↔ (𝑥 ∈ 𝐼 ↦ ((𝑥‘𝑛) − ((𝐹‘𝑥)‘𝑛))) ∈ ((𝑅 ↾_t 𝐼) Cn ((TopOpen‘ℂ_fld) ↾_t ℝ))))
86	83, 84, 85	mp3an13 1448	. . . . . . . 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 234	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐼 ↦ ((𝑥‘𝑛) − ((𝐹‘𝑥)‘𝑛))) ∈ ((𝑅 ↾_t 𝐼) Cn ((TopOpen‘ℂ_fld) ↾_t ℝ)))
89	54	adantl 484	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((𝑅 ↾_t 𝐼) Cn (((1...𝑁) × {(topGen‘ran (,))})‘𝑛)) = ((𝑅 ↾_t 𝐼) Cn ((TopOpen‘ℂ_fld) ↾_t ℝ)))
90	88, 89	eleqtrrd 2916	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐼 ↦ ((𝑥‘𝑛) − ((𝐹‘𝑥)‘𝑛))) ∈ ((𝑅 ↾_t 𝐼) Cn (((1...𝑁) × {(topGen‘ran (,))})‘𝑛)))
91	3, 32, 33, 36, 90	ptcn 22234	. . . 4 ⊢ (𝜑 → (𝑥 ∈ 𝐼 ↦ (𝑛 ∈ (1...𝑁) ↦ ((𝑥‘𝑛) − ((𝐹‘𝑥)‘𝑛)))) ∈ ((𝑅 ↾_t 𝐼) Cn 𝑅))
92	31, 91	eqeltrd 2913	. . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐼 ↦ (𝑥 ∘_f − (𝐹‘𝑥))) ∈ ((𝑅 ↾_t 𝐼) Cn 𝑅))
93		simpr2 1191	. . . . . 6 ⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧 ∈ 𝐼 ∧ (𝑧‘𝑛) = 0)) → 𝑧 ∈ 𝐼)
94		id 22	. . . . . . . . 9 ⊢ (𝑥 = 𝑧 → 𝑥 = 𝑧)
95		fveq2 6669	. . . . . . . . 9 ⊢ (𝑥 = 𝑧 → (𝐹‘𝑥) = (𝐹‘𝑧))
96	94, 95	oveq12d 7173	. . . . . . . 8 ⊢ (𝑥 = 𝑧 → (𝑥 ∘_f − (𝐹‘𝑥)) = (𝑧 ∘_f − (𝐹‘𝑧)))
97		eqid 2821	. . . . . . . 8 ⊢ (𝑥 ∈ 𝐼 ↦ (𝑥 ∘_f − (𝐹‘𝑥))) = (𝑥 ∈ 𝐼 ↦ (𝑥 ∘_f − (𝐹‘𝑥)))
98		ovex 7188	. . . . . . . 8 ⊢ (𝑧 ∘_f − (𝐹‘𝑧)) ∈ V
99	96, 97, 98	fvmpt 6767	. . . . . . 7 ⊢ (𝑧 ∈ 𝐼 → ((𝑥 ∈ 𝐼 ↦ (𝑥 ∘_f − (𝐹‘𝑥)))‘𝑧) = (𝑧 ∘_f − (𝐹‘𝑧)))
100	99	fveq1d 6671	. . . . . 6 ⊢ (𝑧 ∈ 𝐼 → (((𝑥 ∈ 𝐼 ↦ (𝑥 ∘_f − (𝐹‘𝑥)))‘𝑧)‘𝑛) = ((𝑧 ∘_f − (𝐹‘𝑧))‘𝑛))
101	93, 100	syl 17	. . . . 5 ⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧 ∈ 𝐼 ∧ (𝑧‘𝑛) = 0)) → (((𝑥 ∈ 𝐼 ↦ (𝑥 ∘_f − (𝐹‘𝑥)))‘𝑧)‘𝑛) = ((𝑧 ∘_f − (𝐹‘𝑧))‘𝑛))
102		elmapfn 8428	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ ((0[,]1) ↑_m (1...𝑁)) → 𝑧 Fn (1...𝑁))
103	102, 2	eleq2s 2931	. . . . . . . . . . 11 ⊢ (𝑧 ∈ 𝐼 → 𝑧 Fn (1...𝑁))
104	103	adantl 484	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑧‘𝑛) = 0) ∧ 𝑧 ∈ 𝐼) → 𝑧 Fn (1...𝑁))
105	21	ffvelrnda 6850	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐼) → (𝐹‘𝑧) ∈ 𝐼)
106		elmapfn 8428	. . . . . . . . . . . . 13 ⊢ ((𝐹‘𝑧) ∈ ((0[,]1) ↑_m (1...𝑁)) → (𝐹‘𝑧) Fn (1...𝑁))
107	106, 2	eleq2s 2931	. . . . . . . . . . . 12 ⊢ ((𝐹‘𝑧) ∈ 𝐼 → (𝐹‘𝑧) Fn (1...𝑁))
108	105, 107	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐼) → (𝐹‘𝑧) Fn (1...𝑁))
109	108	adantlr 713	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑧‘𝑛) = 0) ∧ 𝑧 ∈ 𝐼) → (𝐹‘𝑧) Fn (1...𝑁))
110		ovexd 7190	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑧‘𝑛) = 0) ∧ 𝑧 ∈ 𝐼) → (1...𝑁) ∈ V)
111		simpllr 774	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑧‘𝑛) = 0) ∧ 𝑧 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → (𝑧‘𝑛) = 0)
112		eqidd 2822	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑧‘𝑛) = 0) ∧ 𝑧 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → ((𝐹‘𝑧)‘𝑛) = ((𝐹‘𝑧)‘𝑛))
113	104, 109, 110, 110, 27, 111, 112	ofval 7417	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑧‘𝑛) = 0) ∧ 𝑧 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑧 ∘_f − (𝐹‘𝑧))‘𝑛) = (0 − ((𝐹‘𝑧)‘𝑛)))
114		df-neg 10872	. . . . . . . . 9 ⊢ -((𝐹‘𝑧)‘𝑛) = (0 − ((𝐹‘𝑧)‘𝑛))
115	113, 114	syl6eqr 2874	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑧‘𝑛) = 0) ∧ 𝑧 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑧 ∘_f − (𝐹‘𝑧))‘𝑛) = -((𝐹‘𝑧)‘𝑛))
116	115	exp41 437	. . . . . . 7 ⊢ (𝜑 → ((𝑧‘𝑛) = 0 → (𝑧 ∈ 𝐼 → (𝑛 ∈ (1...𝑁) → ((𝑧 ∘_f − (𝐹‘𝑧))‘𝑛) = -((𝐹‘𝑧)‘𝑛)))))
117	116	com24 95	. . . . . 6 ⊢ (𝜑 → (𝑛 ∈ (1...𝑁) → (𝑧 ∈ 𝐼 → ((𝑧‘𝑛) = 0 → ((𝑧 ∘_f − (𝐹‘𝑧))‘𝑛) = -((𝐹‘𝑧)‘𝑛)))))
118	117	3imp2 1345	. . . . 5 ⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧 ∈ 𝐼 ∧ (𝑧‘𝑛) = 0)) → ((𝑧 ∘_f − (𝐹‘𝑧))‘𝑛) = -((𝐹‘𝑧)‘𝑛))
119	101, 118	eqtrd 2856	. . . 4 ⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧 ∈ 𝐼 ∧ (𝑧‘𝑛) = 0)) → (((𝑥 ∈ 𝐼 ↦ (𝑥 ∘_f − (𝐹‘𝑥)))‘𝑧)‘𝑛) = -((𝐹‘𝑧)‘𝑛))
120		elmapi 8427	. . . . . . . . . . . 12 ⊢ ((𝐹‘𝑧) ∈ ((0[,]1) ↑_m (1...𝑁)) → (𝐹‘𝑧):(1...𝑁)⟶(0[,]1))
121	120, 2	eleq2s 2931	. . . . . . . . . . 11 ⊢ ((𝐹‘𝑧) ∈ 𝐼 → (𝐹‘𝑧):(1...𝑁)⟶(0[,]1))
122	105, 121	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐼) → (𝐹‘𝑧):(1...𝑁)⟶(0[,]1))
123	122	ffvelrnda 6850	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → ((𝐹‘𝑧)‘𝑛) ∈ (0[,]1))
124		0xr 10687	. . . . . . . . . 10 ⊢ 0 ∈ ℝ^*
125		1xr 10699	. . . . . . . . . 10 ⊢ 1 ∈ ℝ^*
126		iccgelb 12792	. . . . . . . . . 10 ⊢ ((0 ∈ ℝ^* ∧ 1 ∈ ℝ^* ∧ ((𝐹‘𝑧)‘𝑛) ∈ (0[,]1)) → 0 ≤ ((𝐹‘𝑧)‘𝑛))
127	124, 125, 126	mp3an12 1447	. . . . . . . . 9 ⊢ (((𝐹‘𝑧)‘𝑛) ∈ (0[,]1) → 0 ≤ ((𝐹‘𝑧)‘𝑛))
128	123, 127	syl 17	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → 0 ≤ ((𝐹‘𝑧)‘𝑛))
129	13, 123	sseldi 3964	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → ((𝐹‘𝑧)‘𝑛) ∈ ℝ)
130	129	le0neg2d 11211	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → (0 ≤ ((𝐹‘𝑧)‘𝑛) ↔ -((𝐹‘𝑧)‘𝑛) ≤ 0))
131	128, 130	mpbid 234	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → -((𝐹‘𝑧)‘𝑛) ≤ 0)
132	131	an32s 650	. . . . . 6 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑧 ∈ 𝐼) → -((𝐹‘𝑧)‘𝑛) ≤ 0)
133	132	anasss 469	. . . . 5 ⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧 ∈ 𝐼)) → -((𝐹‘𝑧)‘𝑛) ≤ 0)
134	133	3adantr3 1167	. . . 4 ⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧 ∈ 𝐼 ∧ (𝑧‘𝑛) = 0)) → -((𝐹‘𝑧)‘𝑛) ≤ 0)
135	119, 134	eqbrtrd 5087	. . 3 ⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧 ∈ 𝐼 ∧ (𝑧‘𝑛) = 0)) → (((𝑥 ∈ 𝐼 ↦ (𝑥 ∘_f − (𝐹‘𝑥)))‘𝑧)‘𝑛) ≤ 0)
136		iccleub 12791	. . . . . . . . . 10 ⊢ ((0 ∈ ℝ^* ∧ 1 ∈ ℝ^* ∧ ((𝐹‘𝑧)‘𝑛) ∈ (0[,]1)) → ((𝐹‘𝑧)‘𝑛) ≤ 1)
137	124, 125, 136	mp3an12 1447	. . . . . . . . 9 ⊢ (((𝐹‘𝑧)‘𝑛) ∈ (0[,]1) → ((𝐹‘𝑧)‘𝑛) ≤ 1)
138	123, 137	syl 17	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → ((𝐹‘𝑧)‘𝑛) ≤ 1)
139		1red 10641	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → 1 ∈ ℝ)
140	139, 129	subge0d 11229	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → (0 ≤ (1 − ((𝐹‘𝑧)‘𝑛)) ↔ ((𝐹‘𝑧)‘𝑛) ≤ 1))
141	138, 140	mpbird 259	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → 0 ≤ (1 − ((𝐹‘𝑧)‘𝑛)))
142	141	an32s 650	. . . . . 6 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑧 ∈ 𝐼) → 0 ≤ (1 − ((𝐹‘𝑧)‘𝑛)))
143	142	anasss 469	. . . . 5 ⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧 ∈ 𝐼)) → 0 ≤ (1 − ((𝐹‘𝑧)‘𝑛)))
144	143	3adantr3 1167	. . . 4 ⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧 ∈ 𝐼 ∧ (𝑧‘𝑛) = 1)) → 0 ≤ (1 − ((𝐹‘𝑧)‘𝑛)))
145		simpr2 1191	. . . . . 6 ⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧 ∈ 𝐼 ∧ (𝑧‘𝑛) = 1)) → 𝑧 ∈ 𝐼)
146	145, 100	syl 17	. . . . 5 ⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧 ∈ 𝐼 ∧ (𝑧‘𝑛) = 1)) → (((𝑥 ∈ 𝐼 ↦ (𝑥 ∘_f − (𝐹‘𝑥)))‘𝑧)‘𝑛) = ((𝑧 ∘_f − (𝐹‘𝑧))‘𝑛))
147	103	adantl 484	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑧‘𝑛) = 1) ∧ 𝑧 ∈ 𝐼) → 𝑧 Fn (1...𝑁))
148	108	adantlr 713	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑧‘𝑛) = 1) ∧ 𝑧 ∈ 𝐼) → (𝐹‘𝑧) Fn (1...𝑁))
149		ovexd 7190	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑧‘𝑛) = 1) ∧ 𝑧 ∈ 𝐼) → (1...𝑁) ∈ V)
150		simpllr 774	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑧‘𝑛) = 1) ∧ 𝑧 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → (𝑧‘𝑛) = 1)
151		eqidd 2822	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑧‘𝑛) = 1) ∧ 𝑧 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → ((𝐹‘𝑧)‘𝑛) = ((𝐹‘𝑧)‘𝑛))
152	147, 148, 149, 149, 27, 150, 151	ofval 7417	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑧‘𝑛) = 1) ∧ 𝑧 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑧 ∘_f − (𝐹‘𝑧))‘𝑛) = (1 − ((𝐹‘𝑧)‘𝑛)))
153	152	exp41 437	. . . . . . 7 ⊢ (𝜑 → ((𝑧‘𝑛) = 1 → (𝑧 ∈ 𝐼 → (𝑛 ∈ (1...𝑁) → ((𝑧 ∘_f − (𝐹‘𝑧))‘𝑛) = (1 − ((𝐹‘𝑧)‘𝑛))))))
154	153	com24 95	. . . . . 6 ⊢ (𝜑 → (𝑛 ∈ (1...𝑁) → (𝑧 ∈ 𝐼 → ((𝑧‘𝑛) = 1 → ((𝑧 ∘_f − (𝐹‘𝑧))‘𝑛) = (1 − ((𝐹‘𝑧)‘𝑛))))))
155	154	3imp2 1345	. . . . 5 ⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧 ∈ 𝐼 ∧ (𝑧‘𝑛) = 1)) → ((𝑧 ∘_f − (𝐹‘𝑧))‘𝑛) = (1 − ((𝐹‘𝑧)‘𝑛)))
156	146, 155	eqtrd 2856	. . . 4 ⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧 ∈ 𝐼 ∧ (𝑧‘𝑛) = 1)) → (((𝑥 ∈ 𝐼 ↦ (𝑥 ∘_f − (𝐹‘𝑥)))‘𝑧)‘𝑛) = (1 − ((𝐹‘𝑧)‘𝑛)))
157	144, 156	breqtrrd 5093	. . 3 ⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧 ∈ 𝐼 ∧ (𝑧‘𝑛) = 1)) → 0 ≤ (((𝑥 ∈ 𝐼 ↦ (𝑥 ∘_f − (𝐹‘𝑥)))‘𝑧)‘𝑛))
158	1, 2, 3, 92, 135, 157	poimir 34924	. 2 ⊢ (𝜑 → ∃𝑐 ∈ 𝐼 ((𝑥 ∈ 𝐼 ↦ (𝑥 ∘_f − (𝐹‘𝑥)))‘𝑐) = ((1...𝑁) × {0}))
159		id 22	. . . . . . . 8 ⊢ (𝑥 = 𝑐 → 𝑥 = 𝑐)
160		fveq2 6669	. . . . . . . 8 ⊢ (𝑥 = 𝑐 → (𝐹‘𝑥) = (𝐹‘𝑐))
161	159, 160	oveq12d 7173	. . . . . . 7 ⊢ (𝑥 = 𝑐 → (𝑥 ∘_f − (𝐹‘𝑥)) = (𝑐 ∘_f − (𝐹‘𝑐)))
162		ovex 7188	. . . . . . 7 ⊢ (𝑐 ∘_f − (𝐹‘𝑐)) ∈ V
163	161, 97, 162	fvmpt 6767	. . . . . 6 ⊢ (𝑐 ∈ 𝐼 → ((𝑥 ∈ 𝐼 ↦ (𝑥 ∘_f − (𝐹‘𝑥)))‘𝑐) = (𝑐 ∘_f − (𝐹‘𝑐)))
164	163	adantl 484	. . . . 5 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐼) → ((𝑥 ∈ 𝐼 ↦ (𝑥 ∘_f − (𝐹‘𝑥)))‘𝑐) = (𝑐 ∘_f − (𝐹‘𝑐)))
165	164	eqeq1d 2823	. . . 4 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐼) → (((𝑥 ∈ 𝐼 ↦ (𝑥 ∘_f − (𝐹‘𝑥)))‘𝑐) = ((1...𝑁) × {0}) ↔ (𝑐 ∘_f − (𝐹‘𝑐)) = ((1...𝑁) × {0})))
166		elmapfn 8428	. . . . . . . . . . 11 ⊢ (𝑐 ∈ ((0[,]1) ↑_m (1...𝑁)) → 𝑐 Fn (1...𝑁))
167	166, 2	eleq2s 2931	. . . . . . . . . 10 ⊢ (𝑐 ∈ 𝐼 → 𝑐 Fn (1...𝑁))
168	167	adantl 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐼) → 𝑐 Fn (1...𝑁))
169	21	ffvelrnda 6850	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐼) → (𝐹‘𝑐) ∈ 𝐼)
170		elmapfn 8428	. . . . . . . . . . 11 ⊢ ((𝐹‘𝑐) ∈ ((0[,]1) ↑_m (1...𝑁)) → (𝐹‘𝑐) Fn (1...𝑁))
171	170, 2	eleq2s 2931	. . . . . . . . . 10 ⊢ ((𝐹‘𝑐) ∈ 𝐼 → (𝐹‘𝑐) Fn (1...𝑁))
172	169, 171	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐼) → (𝐹‘𝑐) Fn (1...𝑁))
173		ovexd 7190	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐼) → (1...𝑁) ∈ V)
174		eqidd 2822	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → (𝑐‘𝑛) = (𝑐‘𝑛))
175		eqidd 2822	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → ((𝐹‘𝑐)‘𝑛) = ((𝐹‘𝑐)‘𝑛))
176	168, 172, 173, 173, 27, 174, 175	ofval 7417	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑐 ∘_f − (𝐹‘𝑐))‘𝑛) = ((𝑐‘𝑛) − ((𝐹‘𝑐)‘𝑛)))
177		c0ex 10634	. . . . . . . . . 10 ⊢ 0 ∈ V
178	177	fvconst2 6965	. . . . . . . . 9 ⊢ (𝑛 ∈ (1...𝑁) → (((1...𝑁) × {0})‘𝑛) = 0)
179	178	adantl 484	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → (((1...𝑁) × {0})‘𝑛) = 0)
180	176, 179	eqeq12d 2837	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → (((𝑐 ∘_f − (𝐹‘𝑐))‘𝑛) = (((1...𝑁) × {0})‘𝑛) ↔ ((𝑐‘𝑛) − ((𝐹‘𝑐)‘𝑛)) = 0))
181	13, 84	sstri 3975	. . . . . . . . . 10 ⊢ (0[,]1) ⊆ ℂ
182		elmapi 8427	. . . . . . . . . . . 12 ⊢ (𝑐 ∈ ((0[,]1) ↑_m (1...𝑁)) → 𝑐:(1...𝑁)⟶(0[,]1))
183	182, 2	eleq2s 2931	. . . . . . . . . . 11 ⊢ (𝑐 ∈ 𝐼 → 𝑐:(1...𝑁)⟶(0[,]1))
184	183	ffvelrnda 6850	. . . . . . . . . 10 ⊢ ((𝑐 ∈ 𝐼 ∧ 𝑛 ∈ (1...𝑁)) → (𝑐‘𝑛) ∈ (0[,]1))
185	181, 184	sseldi 3964	. . . . . . . . 9 ⊢ ((𝑐 ∈ 𝐼 ∧ 𝑛 ∈ (1...𝑁)) → (𝑐‘𝑛) ∈ ℂ)
186	185	adantll 712	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → (𝑐‘𝑛) ∈ ℂ)
187		elmapi 8427	. . . . . . . . . . . 12 ⊢ ((𝐹‘𝑐) ∈ ((0[,]1) ↑_m (1...𝑁)) → (𝐹‘𝑐):(1...𝑁)⟶(0[,]1))
188	187, 2	eleq2s 2931	. . . . . . . . . . 11 ⊢ ((𝐹‘𝑐) ∈ 𝐼 → (𝐹‘𝑐):(1...𝑁)⟶(0[,]1))
189	169, 188	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐼) → (𝐹‘𝑐):(1...𝑁)⟶(0[,]1))
190	189	ffvelrnda 6850	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → ((𝐹‘𝑐)‘𝑛) ∈ (0[,]1))
191	181, 190	sseldi 3964	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → ((𝐹‘𝑐)‘𝑛) ∈ ℂ)
192	186, 191	subeq0ad 11006	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → (((𝑐‘𝑛) − ((𝐹‘𝑐)‘𝑛)) = 0 ↔ (𝑐‘𝑛) = ((𝐹‘𝑐)‘𝑛)))
193	180, 192	bitrd 281	. . . . . 6 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → (((𝑐 ∘_f − (𝐹‘𝑐))‘𝑛) = (((1...𝑁) × {0})‘𝑛) ↔ (𝑐‘𝑛) = ((𝐹‘𝑐)‘𝑛)))
194	193	ralbidva 3196	. . . . 5 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐼) → (∀𝑛 ∈ (1...𝑁)((𝑐 ∘_f − (𝐹‘𝑐))‘𝑛) = (((1...𝑁) × {0})‘𝑛) ↔ ∀𝑛 ∈ (1...𝑁)(𝑐‘𝑛) = ((𝐹‘𝑐)‘𝑛)))
195	168, 172, 173, 173, 27	offn 7419	. . . . . 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 6801	. . . . . 6 ⊢ (((𝑐 ∘_f − (𝐹‘𝑐)) Fn (1...𝑁) ∧ ((1...𝑁) × {0}) Fn (1...𝑁)) → ((𝑐 ∘_f − (𝐹‘𝑐)) = ((1...𝑁) × {0}) ↔ ∀𝑛 ∈ (1...𝑁)((𝑐 ∘_f − (𝐹‘𝑐))‘𝑛) = (((1...𝑁) × {0})‘𝑛)))
199	195, 197, 198	sylancl 588	. . . . 5 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐼) → ((𝑐 ∘_f − (𝐹‘𝑐)) = ((1...𝑁) × {0}) ↔ ∀𝑛 ∈ (1...𝑁)((𝑐 ∘_f − (𝐹‘𝑐))‘𝑛) = (((1...𝑁) × {0})‘𝑛)))
200		eqfnfv 6801	. . . . . 6 ⊢ ((𝑐 Fn (1...𝑁) ∧ (𝐹‘𝑐) Fn (1...𝑁)) → (𝑐 = (𝐹‘𝑐) ↔ ∀𝑛 ∈ (1...𝑁)(𝑐‘𝑛) = ((𝐹‘𝑐)‘𝑛)))
201	168, 172, 200	syl2anc 586	. . . . 5 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐼) → (𝑐 = (𝐹‘𝑐) ↔ ∀𝑛 ∈ (1...𝑁)(𝑐‘𝑛) = ((𝐹‘𝑐)‘𝑛)))
202	194, 199, 201	3bitr4d 313	. . . 4 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐼) → ((𝑐 ∘_f − (𝐹‘𝑐)) = ((1...𝑁) × {0}) ↔ 𝑐 = (𝐹‘𝑐)))
203	165, 202	bitrd 281	. . 3 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐼) → (((𝑥 ∈ 𝐼 ↦ (𝑥 ∘_f − (𝐹‘𝑥)))‘𝑐) = ((1...𝑁) × {0}) ↔ 𝑐 = (𝐹‘𝑐)))
204	203	rexbidva 3296	. 2 ⊢ (𝜑 → (∃𝑐 ∈ 𝐼 ((𝑥 ∈ 𝐼 ↦ (𝑥 ∘_f − (𝐹‘𝑥)))‘𝑐) = ((1...𝑁) × {0}) ↔ ∃𝑐 ∈ 𝐼 𝑐 = (𝐹‘𝑐)))
205	158, 204	mpbid 234	1 ⊢ (𝜑 → ∃𝑐 ∈ 𝐼 𝑐 = (𝐹‘𝑐))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 208 ∧ wa 398 ∧ w3a 1083 = wceq 1533 ∈ wcel 2110 ∀wral 3138 ∃wrex 3139 Vcvv 3494 ⊆ wss 3935 {csn 4566 class class class wbr 5065 ↦ cmpt 5145 × cxp 5552 ran crn 5555 ↾ cres 5556 Fn wfn 6349 ⟶wf 6350 ‘cfv 6354 (class class class)co 7155 ∘_f cof 7406 ↑_m cmap 8405 ℂcc 10534 ℝcr 10535 0cc0 10536 1c1 10537 ℝ^*cxr 10673 ≤ cle 10675 − cmin 10869 -cneg 10870 ℕcn 11637 (,)cioo 12737 [,]cicc 12740 ...cfz 12891 ↾_t crest 16693 TopOpenctopn 16694 topGenctg 16710 ∏_tcpt 16711 ℂ_fldccnfld 20544 Topctop 21500 TopOnctopon 21517 Cn ccn 21831 ×_t ctx 22167

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2157 ax-12 2173 ax-ext 2793 ax-rep 5189 ax-sep 5202 ax-nul 5209 ax-pow 5265 ax-pr 5329 ax-un 7460 ax-inf2 9103 ax-cnex 10592 ax-resscn 10593 ax-1cn 10594 ax-icn 10595 ax-addcl 10596 ax-addrcl 10597 ax-mulcl 10598 ax-mulrcl 10599 ax-mulcom 10600 ax-addass 10601 ax-mulass 10602 ax-distr 10603 ax-i2m1 10604 ax-1ne0 10605 ax-1rid 10606 ax-rnegex 10607 ax-rrecex 10608 ax-cnre 10609 ax-pre-lttri 10610 ax-pre-lttrn 10611 ax-pre-ltadd 10612 ax-pre-mulgt0 10613 ax-pre-sup 10614

This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3or 1084 df-3an 1085 df-tru 1536 df-fal 1546 df-ex 1777 df-nf 1781 df-sb 2066 df-mo 2618 df-eu 2650 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ne 3017 df-nel 3124 df-ral 3143 df-rex 3144 df-reu 3145 df-rmo 3146 df-rab 3147 df-v 3496 df-sbc 3772 df-csb 3883 df-dif 3938 df-un 3940 df-in 3942 df-ss 3951 df-pss 3953 df-nul 4291 df-if 4467 df-pw 4540 df-sn 4567 df-pr 4569 df-tp 4571 df-op 4573 df-uni 4838 df-int 4876 df-iun 4920 df-iin 4921 df-disj 5031 df-br 5066 df-opab 5128 df-mpt 5146 df-tr 5172 df-id 5459 df-eprel 5464 df-po 5473 df-so 5474 df-fr 5513 df-se 5514 df-we 5515 df-xp 5560 df-rel 5561 df-cnv 5562 df-co 5563 df-dm 5564 df-rn 5565 df-res 5566 df-ima 5567 df-pred 6147 df-ord 6193 df-on 6194 df-lim 6195 df-suc 6196 df-iota 6313 df-fun 6356 df-fn 6357 df-f 6358 df-f1 6359 df-fo 6360 df-f1o 6361 df-fv 6362 df-isom 6363 df-riota 7113 df-ov 7158 df-oprab 7159 df-mpo 7160 df-of 7408 df-om 7580 df-1st 7688 df-2nd 7689 df-supp 7830 df-wrecs 7946 df-recs 8007 df-rdg 8045 df-1o 8101 df-2o 8102 df-oadd 8105 df-omul 8106 df-er 8288 df-map 8407 df-pm 8408 df-ixp 8461 df-en 8509 df-dom 8510 df-sdom 8511 df-fin 8512 df-fsupp 8833 df-fi 8874 df-sup 8905 df-inf 8906 df-oi 8973 df-dju 9329 df-card 9367 df-acn 9370 df-pnf 10676 df-mnf 10677 df-xr 10678 df-ltxr 10679 df-le 10680 df-sub 10871 df-neg 10872 df-div 11297 df-nn 11638 df-2 11699 df-3 11700 df-4 11701 df-5 11702 df-6 11703 df-7 11704 df-8 11705 df-9 11706 df-n0 11897 df-xnn0 11967 df-z 11981 df-dec 12098 df-uz 12243 df-q 12348 df-rp 12389 df-xneg 12506 df-xadd 12507 df-xmul 12508 df-ioo 12741 df-icc 12744 df-fz 12892 df-fzo 13033 df-fl 13161 df-seq 13369 df-exp 13429 df-fac 13633 df-bc 13662 df-hash 13690 df-cj 14457 df-re 14458 df-im 14459 df-sqrt 14593 df-abs 14594 df-clim 14844 df-sum 15042 df-dvds 15607 df-struct 16484 df-ndx 16485 df-slot 16486 df-base 16488 df-sets 16489 df-ress 16490 df-plusg 16577 df-mulr 16578 df-starv 16579 df-sca 16580 df-vsca 16581 df-ip 16582 df-tset 16583 df-ple 16584 df-ds 16586 df-unif 16587 df-hom 16588 df-cco 16589 df-rest 16695 df-topn 16696 df-0g 16714 df-gsum 16715 df-topgen 16716 df-pt 16717 df-prds 16720 df-xrs 16774 df-qtop 16779 df-imas 16780 df-xps 16782 df-mre 16856 df-mrc 16857 df-acs 16859 df-ps 17809 df-tsr 17810 df-mgm 17851 df-sgrp 17900 df-mnd 17911 df-submnd 17956 df-mulg 18224 df-cntz 18446 df-cmn 18907 df-psmet 20536 df-xmet 20537 df-met 20538 df-bl 20539 df-mopn 20540 df-cnfld 20545 df-top 21501 df-topon 21518 df-topsp 21540 df-bases 21553 df-cld 21626 df-ntr 21627 df-cls 21628 df-lp 21743 df-cn 21834 df-cnp 21835 df-t1 21921 df-haus 21922 df-cmp 21994 df-tx 22169 df-hmeo 22362 df-hmph 22363 df-xms 22929 df-ms 22930 df-tms 22931 df-ii 23484

This theorem is referenced by: (None)

W3C validator