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 37614

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 8923	. . . . . . . 8 ⊢ (𝑥 ∈ ((0[,]1) ↑_m (1...𝑁)) → 𝑥 Fn (1...𝑁))
5	4, 2	eleq2s 2862	. . . . . . 7 ⊢ (𝑥 ∈ 𝐼 → 𝑥 Fn (1...𝑁))
6	5	adantl 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑥 Fn (1...𝑁))
7		broucube.1	. . . . . . . . 9 ⊢ (𝜑 → 𝐹 ∈ ((𝑅 ↾_t 𝐼) Cn (𝑅 ↾_t 𝐼)))
8		ovex 7481	. . . . . . . . . . . . 13 ⊢ (1...𝑁) ∈ V
9		retopon 24805	. . . . . . . . . . . . 13 ⊢ (topGen‘ran (,)) ∈ (TopOn‘ℝ)
10	3	pttoponconst 23626	. . . . . . . . . . . . 13 ⊢ (((1...𝑁) ∈ V ∧ (topGen‘ran (,)) ∈ (TopOn‘ℝ)) → 𝑅 ∈ (TopOn‘(ℝ ↑_m (1...𝑁))))
11	8, 9, 10	mp2an 691	. . . . . . . . . . . 12 ⊢ 𝑅 ∈ (TopOn‘(ℝ ↑_m (1...𝑁)))
12		reex 11275	. . . . . . . . . . . . . 14 ⊢ ℝ ∈ V
13		unitssre 13559	. . . . . . . . . . . . . 14 ⊢ (0[,]1) ⊆ ℝ
14		mapss 8947	. . . . . . . . . . . . . 14 ⊢ ((ℝ ∈ V ∧ (0[,]1) ⊆ ℝ) → ((0[,]1) ↑_m (1...𝑁)) ⊆ (ℝ ↑_m (1...𝑁)))
15	12, 13, 14	mp2an 691	. . . . . . . . . . . . 13 ⊢ ((0[,]1) ↑_m (1...𝑁)) ⊆ (ℝ ↑_m (1...𝑁))
16	2, 15	eqsstri 4043	. . . . . . . . . . . 12 ⊢ 𝐼 ⊆ (ℝ ↑_m (1...𝑁))
17		resttopon 23190	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ (TopOn‘(ℝ ↑_m (1...𝑁))) ∧ 𝐼 ⊆ (ℝ ↑_m (1...𝑁))) → (𝑅 ↾_t 𝐼) ∈ (TopOn‘𝐼))
18	11, 16, 17	mp2an 691	. . . . . . . . . . 11 ⊢ (𝑅 ↾_t 𝐼) ∈ (TopOn‘𝐼)
19	18	toponunii 22943	. . . . . . . . . 10 ⊢ 𝐼 = ∪ (𝑅 ↾_t 𝐼)
20	19, 19	cnf 23275	. . . . . . . . 9 ⊢ (𝐹 ∈ ((𝑅 ↾_t 𝐼) Cn (𝑅 ↾_t 𝐼)) → 𝐹:𝐼⟶𝐼)
21	7, 20	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝐹:𝐼⟶𝐼)
22	21	ffvelcdmda 7118	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝐹‘𝑥) ∈ 𝐼)
23		elmapfn 8923	. . . . . . . 8 ⊢ ((𝐹‘𝑥) ∈ ((0[,]1) ↑_m (1...𝑁)) → (𝐹‘𝑥) Fn (1...𝑁))
24	23, 2	eleq2s 2862	. . . . . . 7 ⊢ ((𝐹‘𝑥) ∈ 𝐼 → (𝐹‘𝑥) Fn (1...𝑁))
25	22, 24	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝐹‘𝑥) Fn (1...𝑁))
26		ovexd 7483	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (1...𝑁) ∈ V)
27		inidm 4248	. . . . . 6 ⊢ ((1...𝑁) ∩ (1...𝑁)) = (1...𝑁)
28		eqidd 2741	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → (𝑥‘𝑛) = (𝑥‘𝑛))
29		eqidd 2741	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → ((𝐹‘𝑥)‘𝑛) = ((𝐹‘𝑥)‘𝑛))
30	6, 25, 26, 26, 27, 28, 29	offval 7723	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑥 ∘_f − (𝐹‘𝑥)) = (𝑛 ∈ (1...𝑁) ↦ ((𝑥‘𝑛) − ((𝐹‘𝑥)‘𝑛))))
31	30	mpteq2dva 5266	. . . 4 ⊢ (𝜑 → (𝑥 ∈ 𝐼 ↦ (𝑥 ∘_f − (𝐹‘𝑥))) = (𝑥 ∈ 𝐼 ↦ (𝑛 ∈ (1...𝑁) ↦ ((𝑥‘𝑛) − ((𝐹‘𝑥)‘𝑛)))))
32	18	a1i 11	. . . . 5 ⊢ (𝜑 → (𝑅 ↾_t 𝐼) ∈ (TopOn‘𝐼))
33		ovexd 7483	. . . . 5 ⊢ (𝜑 → (1...𝑁) ∈ V)
34		retop 24803	. . . . . . 7 ⊢ (topGen‘ran (,)) ∈ Top
35	34	fconst6 6811	. . . . . 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 2740	. . . . . . . . . . . 12 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
39	38	cnfldtop 24825	. . . . . . . . . . 11 ⊢ (TopOpen‘ℂ_fld) ∈ Top
40		cnrest2r 23316	. . . . . . . . . . 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 6066	. . . . . . . . . . . . 13 ⊢ (𝐼 ⊆ (ℝ ↑_m (1...𝑁)) → ((𝑥 ∈ (ℝ ↑_m (1...𝑁)) ↦ (𝑥‘𝑛)) ↾ 𝐼) = (𝑥 ∈ 𝐼 ↦ (𝑥‘𝑛)))
43	16, 42	ax-mp 5	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ (ℝ ↑_m (1...𝑁)) ↦ (𝑥‘𝑛)) ↾ 𝐼) = (𝑥 ∈ 𝐼 ↦ (𝑥‘𝑛))
44	11	toponunii 22943	. . . . . . . . . . . . . . 15 ⊢ (ℝ ↑_m (1...𝑁)) = ∪ 𝑅
45	44, 3	ptpjcn 23640	. . . . . . . . . . . . . 14 ⊢ (((1...𝑁) ∈ V ∧ ((1...𝑁) × {(topGen‘ran (,))}):(1...𝑁)⟶Top ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ (ℝ ↑_m (1...𝑁)) ↦ (𝑥‘𝑛)) ∈ (𝑅 Cn (((1...𝑁) × {(topGen‘ran (,))})‘𝑛)))
46	8, 35, 45	mp3an12 1451	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ (1...𝑁) → (𝑥 ∈ (ℝ ↑_m (1...𝑁)) ↦ (𝑥‘𝑛)) ∈ (𝑅 Cn (((1...𝑁) × {(topGen‘ran (,))})‘𝑛)))
47	44	cnrest 23314	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ (ℝ ↑_m (1...𝑁)) ↦ (𝑥‘𝑛)) ∈ (𝑅 Cn (((1...𝑁) × {(topGen‘ran (,))})‘𝑛)) ∧ 𝐼 ⊆ (ℝ ↑_m (1...𝑁))) → ((𝑥 ∈ (ℝ ↑_m (1...𝑁)) ↦ (𝑥‘𝑛)) ↾ 𝐼) ∈ ((𝑅 ↾_t 𝐼) Cn (((1...𝑁) × {(topGen‘ran (,))})‘𝑛)))
48	46, 16, 47	sylancl 585	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ (1...𝑁) → ((𝑥 ∈ (ℝ ↑_m (1...𝑁)) ↦ (𝑥‘𝑛)) ↾ 𝐼) ∈ ((𝑅 ↾_t 𝐼) Cn (((1...𝑁) × {(topGen‘ran (,))})‘𝑛)))
49	43, 48	eqeltrrid 2849	. . . . . . . . . . 11 ⊢ (𝑛 ∈ (1...𝑁) → (𝑥 ∈ 𝐼 ↦ (𝑥‘𝑛)) ∈ ((𝑅 ↾_t 𝐼) Cn (((1...𝑁) × {(topGen‘ran (,))})‘𝑛)))
50		fvex 6933	. . . . . . . . . . . . . 14 ⊢ (topGen‘ran (,)) ∈ V
51	50	fvconst2 7241	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ (1...𝑁) → (((1...𝑁) × {(topGen‘ran (,))})‘𝑛) = (topGen‘ran (,)))
52	38	tgioo2 24844	. . . . . . . . . . . . 13 ⊢ (topGen‘ran (,)) = ((TopOpen‘ℂ_fld) ↾_t ℝ)
53	51, 52	eqtrdi 2796	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ (1...𝑁) → (((1...𝑁) × {(topGen‘ran (,))})‘𝑛) = ((TopOpen‘ℂ_fld) ↾_t ℝ))
54	53	oveq2d 7464	. . . . . . . . . . 11 ⊢ (𝑛 ∈ (1...𝑁) → ((𝑅 ↾_t 𝐼) Cn (((1...𝑁) × {(topGen‘ran (,))})‘𝑛)) = ((𝑅 ↾_t 𝐼) Cn ((TopOpen‘ℂ_fld) ↾_t ℝ)))
55	49, 54	eleqtrd 2846	. . . . . . . . . 10 ⊢ (𝑛 ∈ (1...𝑁) → (𝑥 ∈ 𝐼 ↦ (𝑥‘𝑛)) ∈ ((𝑅 ↾_t 𝐼) Cn ((TopOpen‘ℂ_fld) ↾_t ℝ)))
56	41, 55	sselid 4006	. . . . . . . . 9 ⊢ (𝑛 ∈ (1...𝑁) → (𝑥 ∈ 𝐼 ↦ (𝑥‘𝑛)) ∈ ((𝑅 ↾_t 𝐼) Cn (TopOpen‘ℂ_fld)))
57	56	adantl 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐼 ↦ (𝑥‘𝑛)) ∈ ((𝑅 ↾_t 𝐼) Cn (TopOpen‘ℂ_fld)))
58	21	feqmptd 6990	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐼 ↦ (𝐹‘𝑥)))
59	58, 7	eqeltrrd 2845	. . . . . . . . . 10 ⊢ (𝜑 → (𝑥 ∈ 𝐼 ↦ (𝐹‘𝑥)) ∈ ((𝑅 ↾_t 𝐼) Cn (𝑅 ↾_t 𝐼)))
60	59	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐼 ↦ (𝐹‘𝑥)) ∈ ((𝑅 ↾_t 𝐼) Cn (𝑅 ↾_t 𝐼)))
61		fveq1 6919	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑧 → (𝑥‘𝑛) = (𝑧‘𝑛))
62	61	cbvmptv 5279	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝐼 ↦ (𝑥‘𝑛)) = (𝑧 ∈ 𝐼 ↦ (𝑧‘𝑛))
63	62, 57	eqeltrrid 2849	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑧 ∈ 𝐼 ↦ (𝑧‘𝑛)) ∈ ((𝑅 ↾_t 𝐼) Cn (TopOpen‘ℂ_fld)))
64		fveq1 6919	. . . . . . . . 9 ⊢ (𝑧 = (𝐹‘𝑥) → (𝑧‘𝑛) = ((𝐹‘𝑥)‘𝑛))
65	37, 60, 37, 63, 64	cnmpt11 23692	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐼 ↦ ((𝐹‘𝑥)‘𝑛)) ∈ ((𝑅 ↾_t 𝐼) Cn (TopOpen‘ℂ_fld)))
66	38	subcn 24907	. . . . . . . . 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 23695	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐼 ↦ ((𝑥‘𝑛) − ((𝐹‘𝑥)‘𝑛))) ∈ ((𝑅 ↾_t 𝐼) Cn (TopOpen‘ℂ_fld)))
69		elmapi 8907	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ((0[,]1) ↑_m (1...𝑁)) → 𝑥:(1...𝑁)⟶(0[,]1))
70	69, 2	eleq2s 2862	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ 𝐼 → 𝑥:(1...𝑁)⟶(0[,]1))
71	70	ffvelcdmda 7118	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ 𝐼 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥‘𝑛) ∈ (0[,]1))
72	13, 71	sselid 4006	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ 𝐼 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥‘𝑛) ∈ ℝ)
73	72	adantll 713	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → (𝑥‘𝑛) ∈ ℝ)
74		elmapi 8907	. . . . . . . . . . . . . . 15 ⊢ ((𝐹‘𝑥) ∈ ((0[,]1) ↑_m (1...𝑁)) → (𝐹‘𝑥):(1...𝑁)⟶(0[,]1))
75	74, 2	eleq2s 2862	. . . . . . . . . . . . . 14 ⊢ ((𝐹‘𝑥) ∈ 𝐼 → (𝐹‘𝑥):(1...𝑁)⟶(0[,]1))
76	22, 75	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝐹‘𝑥):(1...𝑁)⟶(0[,]1))
77	76	ffvelcdmda 7118	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → ((𝐹‘𝑥)‘𝑛) ∈ (0[,]1))
78	13, 77	sselid 4006	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → ((𝐹‘𝑥)‘𝑛) ∈ ℝ)
79	73, 78	resubcld 11718	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑥‘𝑛) − ((𝐹‘𝑥)‘𝑛)) ∈ ℝ)
80	79	an32s 651	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐼) → ((𝑥‘𝑛) − ((𝐹‘𝑥)‘𝑛)) ∈ ℝ)
81	80	fmpttd 7149	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐼 ↦ ((𝑥‘𝑛) − ((𝐹‘𝑥)‘𝑛))):𝐼⟶ℝ)
82		frn 6754	. . . . . . . 8 ⊢ ((𝑥 ∈ 𝐼 ↦ ((𝑥‘𝑛) − ((𝐹‘𝑥)‘𝑛))):𝐼⟶ℝ → ran (𝑥 ∈ 𝐼 ↦ ((𝑥‘𝑛) − ((𝐹‘𝑥)‘𝑛))) ⊆ ℝ)
83	38	cnfldtopon 24824	. . . . . . . . 9 ⊢ (TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ)
84		ax-resscn 11241	. . . . . . . . 9 ⊢ ℝ ⊆ ℂ
85		cnrest2 23315	. . . . . . . . 9 ⊢ (((TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ) ∧ ran (𝑥 ∈ 𝐼 ↦ ((𝑥‘𝑛) − ((𝐹‘𝑥)‘𝑛))) ⊆ ℝ ∧ ℝ ⊆ ℂ) → ((𝑥 ∈ 𝐼 ↦ ((𝑥‘𝑛) − ((𝐹‘𝑥)‘𝑛))) ∈ ((𝑅 ↾_t 𝐼) Cn (TopOpen‘ℂ_fld)) ↔ (𝑥 ∈ 𝐼 ↦ ((𝑥‘𝑛) − ((𝐹‘𝑥)‘𝑛))) ∈ ((𝑅 ↾_t 𝐼) Cn ((TopOpen‘ℂ_fld) ↾_t ℝ))))
86	83, 84, 85	mp3an13 1452	. . . . . . . 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 2847	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐼 ↦ ((𝑥‘𝑛) − ((𝐹‘𝑥)‘𝑛))) ∈ ((𝑅 ↾_t 𝐼) Cn (((1...𝑁) × {(topGen‘ran (,))})‘𝑛)))
91	3, 32, 33, 36, 90	ptcn 23656	. . . 4 ⊢ (𝜑 → (𝑥 ∈ 𝐼 ↦ (𝑛 ∈ (1...𝑁) ↦ ((𝑥‘𝑛) − ((𝐹‘𝑥)‘𝑛)))) ∈ ((𝑅 ↾_t 𝐼) Cn 𝑅))
92	31, 91	eqeltrd 2844	. . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐼 ↦ (𝑥 ∘_f − (𝐹‘𝑥))) ∈ ((𝑅 ↾_t 𝐼) Cn 𝑅))
93		simpr2 1195	. . . . . 6 ⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧 ∈ 𝐼 ∧ (𝑧‘𝑛) = 0)) → 𝑧 ∈ 𝐼)
94		id 22	. . . . . . . . 9 ⊢ (𝑥 = 𝑧 → 𝑥 = 𝑧)
95		fveq2 6920	. . . . . . . . 9 ⊢ (𝑥 = 𝑧 → (𝐹‘𝑥) = (𝐹‘𝑧))
96	94, 95	oveq12d 7466	. . . . . . . 8 ⊢ (𝑥 = 𝑧 → (𝑥 ∘_f − (𝐹‘𝑥)) = (𝑧 ∘_f − (𝐹‘𝑧)))
97		eqid 2740	. . . . . . . 8 ⊢ (𝑥 ∈ 𝐼 ↦ (𝑥 ∘_f − (𝐹‘𝑥))) = (𝑥 ∈ 𝐼 ↦ (𝑥 ∘_f − (𝐹‘𝑥)))
98		ovex 7481	. . . . . . . 8 ⊢ (𝑧 ∘_f − (𝐹‘𝑧)) ∈ V
99	96, 97, 98	fvmpt 7029	. . . . . . 7 ⊢ (𝑧 ∈ 𝐼 → ((𝑥 ∈ 𝐼 ↦ (𝑥 ∘_f − (𝐹‘𝑥)))‘𝑧) = (𝑧 ∘_f − (𝐹‘𝑧)))
100	99	fveq1d 6922	. . . . . 6 ⊢ (𝑧 ∈ 𝐼 → (((𝑥 ∈ 𝐼 ↦ (𝑥 ∘_f − (𝐹‘𝑥)))‘𝑧)‘𝑛) = ((𝑧 ∘_f − (𝐹‘𝑧))‘𝑛))
101	93, 100	syl 17	. . . . 5 ⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧 ∈ 𝐼 ∧ (𝑧‘𝑛) = 0)) → (((𝑥 ∈ 𝐼 ↦ (𝑥 ∘_f − (𝐹‘𝑥)))‘𝑧)‘𝑛) = ((𝑧 ∘_f − (𝐹‘𝑧))‘𝑛))
102		elmapfn 8923	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ ((0[,]1) ↑_m (1...𝑁)) → 𝑧 Fn (1...𝑁))
103	102, 2	eleq2s 2862	. . . . . . . . . . 11 ⊢ (𝑧 ∈ 𝐼 → 𝑧 Fn (1...𝑁))
104	103	adantl 481	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑧‘𝑛) = 0) ∧ 𝑧 ∈ 𝐼) → 𝑧 Fn (1...𝑁))
105	21	ffvelcdmda 7118	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐼) → (𝐹‘𝑧) ∈ 𝐼)
106		elmapfn 8923	. . . . . . . . . . . . 13 ⊢ ((𝐹‘𝑧) ∈ ((0[,]1) ↑_m (1...𝑁)) → (𝐹‘𝑧) Fn (1...𝑁))
107	106, 2	eleq2s 2862	. . . . . . . . . . . 12 ⊢ ((𝐹‘𝑧) ∈ 𝐼 → (𝐹‘𝑧) Fn (1...𝑁))
108	105, 107	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐼) → (𝐹‘𝑧) Fn (1...𝑁))
109	108	adantlr 714	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑧‘𝑛) = 0) ∧ 𝑧 ∈ 𝐼) → (𝐹‘𝑧) Fn (1...𝑁))
110		ovexd 7483	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑧‘𝑛) = 0) ∧ 𝑧 ∈ 𝐼) → (1...𝑁) ∈ V)
111		simpllr 775	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑧‘𝑛) = 0) ∧ 𝑧 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → (𝑧‘𝑛) = 0)
112		eqidd 2741	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑧‘𝑛) = 0) ∧ 𝑧 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → ((𝐹‘𝑧)‘𝑛) = ((𝐹‘𝑧)‘𝑛))
113	104, 109, 110, 110, 27, 111, 112	ofval 7725	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑧‘𝑛) = 0) ∧ 𝑧 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑧 ∘_f − (𝐹‘𝑧))‘𝑛) = (0 − ((𝐹‘𝑧)‘𝑛)))
114		df-neg 11523	. . . . . . . . 9 ⊢ -((𝐹‘𝑧)‘𝑛) = (0 − ((𝐹‘𝑧)‘𝑛))
115	113, 114	eqtr4di 2798	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑧‘𝑛) = 0) ∧ 𝑧 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑧 ∘_f − (𝐹‘𝑧))‘𝑛) = -((𝐹‘𝑧)‘𝑛))
116	115	exp41 434	. . . . . . 7 ⊢ (𝜑 → ((𝑧‘𝑛) = 0 → (𝑧 ∈ 𝐼 → (𝑛 ∈ (1...𝑁) → ((𝑧 ∘_f − (𝐹‘𝑧))‘𝑛) = -((𝐹‘𝑧)‘𝑛)))))
117	116	com24 95	. . . . . 6 ⊢ (𝜑 → (𝑛 ∈ (1...𝑁) → (𝑧 ∈ 𝐼 → ((𝑧‘𝑛) = 0 → ((𝑧 ∘_f − (𝐹‘𝑧))‘𝑛) = -((𝐹‘𝑧)‘𝑛)))))
118	117	3imp2 1349	. . . . 5 ⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧 ∈ 𝐼 ∧ (𝑧‘𝑛) = 0)) → ((𝑧 ∘_f − (𝐹‘𝑧))‘𝑛) = -((𝐹‘𝑧)‘𝑛))
119	101, 118	eqtrd 2780	. . . 4 ⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧 ∈ 𝐼 ∧ (𝑧‘𝑛) = 0)) → (((𝑥 ∈ 𝐼 ↦ (𝑥 ∘_f − (𝐹‘𝑥)))‘𝑧)‘𝑛) = -((𝐹‘𝑧)‘𝑛))
120		elmapi 8907	. . . . . . . . . . . 12 ⊢ ((𝐹‘𝑧) ∈ ((0[,]1) ↑_m (1...𝑁)) → (𝐹‘𝑧):(1...𝑁)⟶(0[,]1))
121	120, 2	eleq2s 2862	. . . . . . . . . . 11 ⊢ ((𝐹‘𝑧) ∈ 𝐼 → (𝐹‘𝑧):(1...𝑁)⟶(0[,]1))
122	105, 121	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐼) → (𝐹‘𝑧):(1...𝑁)⟶(0[,]1))
123	122	ffvelcdmda 7118	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → ((𝐹‘𝑧)‘𝑛) ∈ (0[,]1))
124		0xr 11337	. . . . . . . . . 10 ⊢ 0 ∈ ℝ^*
125		1xr 11349	. . . . . . . . . 10 ⊢ 1 ∈ ℝ^*
126		iccgelb 13463	. . . . . . . . . 10 ⊢ ((0 ∈ ℝ^* ∧ 1 ∈ ℝ^* ∧ ((𝐹‘𝑧)‘𝑛) ∈ (0[,]1)) → 0 ≤ ((𝐹‘𝑧)‘𝑛))
127	124, 125, 126	mp3an12 1451	. . . . . . . . 9 ⊢ (((𝐹‘𝑧)‘𝑛) ∈ (0[,]1) → 0 ≤ ((𝐹‘𝑧)‘𝑛))
128	123, 127	syl 17	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → 0 ≤ ((𝐹‘𝑧)‘𝑛))
129	13, 123	sselid 4006	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → ((𝐹‘𝑧)‘𝑛) ∈ ℝ)
130	129	le0neg2d 11862	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → (0 ≤ ((𝐹‘𝑧)‘𝑛) ↔ -((𝐹‘𝑧)‘𝑛) ≤ 0))
131	128, 130	mpbid 232	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → -((𝐹‘𝑧)‘𝑛) ≤ 0)
132	131	an32s 651	. . . . . 6 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑧 ∈ 𝐼) → -((𝐹‘𝑧)‘𝑛) ≤ 0)
133	132	anasss 466	. . . . 5 ⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧 ∈ 𝐼)) → -((𝐹‘𝑧)‘𝑛) ≤ 0)
134	133	3adantr3 1171	. . . 4 ⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧 ∈ 𝐼 ∧ (𝑧‘𝑛) = 0)) → -((𝐹‘𝑧)‘𝑛) ≤ 0)
135	119, 134	eqbrtrd 5188	. . 3 ⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧 ∈ 𝐼 ∧ (𝑧‘𝑛) = 0)) → (((𝑥 ∈ 𝐼 ↦ (𝑥 ∘_f − (𝐹‘𝑥)))‘𝑧)‘𝑛) ≤ 0)
136		iccleub 13462	. . . . . . . . . 10 ⊢ ((0 ∈ ℝ^* ∧ 1 ∈ ℝ^* ∧ ((𝐹‘𝑧)‘𝑛) ∈ (0[,]1)) → ((𝐹‘𝑧)‘𝑛) ≤ 1)
137	124, 125, 136	mp3an12 1451	. . . . . . . . 9 ⊢ (((𝐹‘𝑧)‘𝑛) ∈ (0[,]1) → ((𝐹‘𝑧)‘𝑛) ≤ 1)
138	123, 137	syl 17	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → ((𝐹‘𝑧)‘𝑛) ≤ 1)
139		1red 11291	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → 1 ∈ ℝ)
140	139, 129	subge0d 11880	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → (0 ≤ (1 − ((𝐹‘𝑧)‘𝑛)) ↔ ((𝐹‘𝑧)‘𝑛) ≤ 1))
141	138, 140	mpbird 257	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → 0 ≤ (1 − ((𝐹‘𝑧)‘𝑛)))
142	141	an32s 651	. . . . . 6 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑧 ∈ 𝐼) → 0 ≤ (1 − ((𝐹‘𝑧)‘𝑛)))
143	142	anasss 466	. . . . 5 ⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧 ∈ 𝐼)) → 0 ≤ (1 − ((𝐹‘𝑧)‘𝑛)))
144	143	3adantr3 1171	. . . 4 ⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧 ∈ 𝐼 ∧ (𝑧‘𝑛) = 1)) → 0 ≤ (1 − ((𝐹‘𝑧)‘𝑛)))
145		simpr2 1195	. . . . . 6 ⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧 ∈ 𝐼 ∧ (𝑧‘𝑛) = 1)) → 𝑧 ∈ 𝐼)
146	145, 100	syl 17	. . . . 5 ⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧 ∈ 𝐼 ∧ (𝑧‘𝑛) = 1)) → (((𝑥 ∈ 𝐼 ↦ (𝑥 ∘_f − (𝐹‘𝑥)))‘𝑧)‘𝑛) = ((𝑧 ∘_f − (𝐹‘𝑧))‘𝑛))
147	103	adantl 481	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑧‘𝑛) = 1) ∧ 𝑧 ∈ 𝐼) → 𝑧 Fn (1...𝑁))
148	108	adantlr 714	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑧‘𝑛) = 1) ∧ 𝑧 ∈ 𝐼) → (𝐹‘𝑧) Fn (1...𝑁))
149		ovexd 7483	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑧‘𝑛) = 1) ∧ 𝑧 ∈ 𝐼) → (1...𝑁) ∈ V)
150		simpllr 775	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑧‘𝑛) = 1) ∧ 𝑧 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → (𝑧‘𝑛) = 1)
151		eqidd 2741	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑧‘𝑛) = 1) ∧ 𝑧 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → ((𝐹‘𝑧)‘𝑛) = ((𝐹‘𝑧)‘𝑛))
152	147, 148, 149, 149, 27, 150, 151	ofval 7725	. . . . . . . 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 1349	. . . . 5 ⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧 ∈ 𝐼 ∧ (𝑧‘𝑛) = 1)) → ((𝑧 ∘_f − (𝐹‘𝑧))‘𝑛) = (1 − ((𝐹‘𝑧)‘𝑛)))
156	146, 155	eqtrd 2780	. . . 4 ⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧 ∈ 𝐼 ∧ (𝑧‘𝑛) = 1)) → (((𝑥 ∈ 𝐼 ↦ (𝑥 ∘_f − (𝐹‘𝑥)))‘𝑧)‘𝑛) = (1 − ((𝐹‘𝑧)‘𝑛)))
157	144, 156	breqtrrd 5194	. . 3 ⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧 ∈ 𝐼 ∧ (𝑧‘𝑛) = 1)) → 0 ≤ (((𝑥 ∈ 𝐼 ↦ (𝑥 ∘_f − (𝐹‘𝑥)))‘𝑧)‘𝑛))
158	1, 2, 3, 92, 135, 157	poimir 37613	. 2 ⊢ (𝜑 → ∃𝑐 ∈ 𝐼 ((𝑥 ∈ 𝐼 ↦ (𝑥 ∘_f − (𝐹‘𝑥)))‘𝑐) = ((1...𝑁) × {0}))
159		id 22	. . . . . . . 8 ⊢ (𝑥 = 𝑐 → 𝑥 = 𝑐)
160		fveq2 6920	. . . . . . . 8 ⊢ (𝑥 = 𝑐 → (𝐹‘𝑥) = (𝐹‘𝑐))
161	159, 160	oveq12d 7466	. . . . . . 7 ⊢ (𝑥 = 𝑐 → (𝑥 ∘_f − (𝐹‘𝑥)) = (𝑐 ∘_f − (𝐹‘𝑐)))
162		ovex 7481	. . . . . . 7 ⊢ (𝑐 ∘_f − (𝐹‘𝑐)) ∈ V
163	161, 97, 162	fvmpt 7029	. . . . . 6 ⊢ (𝑐 ∈ 𝐼 → ((𝑥 ∈ 𝐼 ↦ (𝑥 ∘_f − (𝐹‘𝑥)))‘𝑐) = (𝑐 ∘_f − (𝐹‘𝑐)))
164	163	adantl 481	. . . . 5 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐼) → ((𝑥 ∈ 𝐼 ↦ (𝑥 ∘_f − (𝐹‘𝑥)))‘𝑐) = (𝑐 ∘_f − (𝐹‘𝑐)))
165	164	eqeq1d 2742	. . . 4 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐼) → (((𝑥 ∈ 𝐼 ↦ (𝑥 ∘_f − (𝐹‘𝑥)))‘𝑐) = ((1...𝑁) × {0}) ↔ (𝑐 ∘_f − (𝐹‘𝑐)) = ((1...𝑁) × {0})))
166		elmapfn 8923	. . . . . . . . . . 11 ⊢ (𝑐 ∈ ((0[,]1) ↑_m (1...𝑁)) → 𝑐 Fn (1...𝑁))
167	166, 2	eleq2s 2862	. . . . . . . . . 10 ⊢ (𝑐 ∈ 𝐼 → 𝑐 Fn (1...𝑁))
168	167	adantl 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐼) → 𝑐 Fn (1...𝑁))
169	21	ffvelcdmda 7118	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐼) → (𝐹‘𝑐) ∈ 𝐼)
170		elmapfn 8923	. . . . . . . . . . 11 ⊢ ((𝐹‘𝑐) ∈ ((0[,]1) ↑_m (1...𝑁)) → (𝐹‘𝑐) Fn (1...𝑁))
171	170, 2	eleq2s 2862	. . . . . . . . . 10 ⊢ ((𝐹‘𝑐) ∈ 𝐼 → (𝐹‘𝑐) Fn (1...𝑁))
172	169, 171	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐼) → (𝐹‘𝑐) Fn (1...𝑁))
173		ovexd 7483	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐼) → (1...𝑁) ∈ V)
174		eqidd 2741	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → (𝑐‘𝑛) = (𝑐‘𝑛))
175		eqidd 2741	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → ((𝐹‘𝑐)‘𝑛) = ((𝐹‘𝑐)‘𝑛))
176	168, 172, 173, 173, 27, 174, 175	ofval 7725	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑐 ∘_f − (𝐹‘𝑐))‘𝑛) = ((𝑐‘𝑛) − ((𝐹‘𝑐)‘𝑛)))
177		c0ex 11284	. . . . . . . . . 10 ⊢ 0 ∈ V
178	177	fvconst2 7241	. . . . . . . . 9 ⊢ (𝑛 ∈ (1...𝑁) → (((1...𝑁) × {0})‘𝑛) = 0)
179	178	adantl 481	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → (((1...𝑁) × {0})‘𝑛) = 0)
180	176, 179	eqeq12d 2756	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → (((𝑐 ∘_f − (𝐹‘𝑐))‘𝑛) = (((1...𝑁) × {0})‘𝑛) ↔ ((𝑐‘𝑛) − ((𝐹‘𝑐)‘𝑛)) = 0))
181	13, 84	sstri 4018	. . . . . . . . . 10 ⊢ (0[,]1) ⊆ ℂ
182		elmapi 8907	. . . . . . . . . . . 12 ⊢ (𝑐 ∈ ((0[,]1) ↑_m (1...𝑁)) → 𝑐:(1...𝑁)⟶(0[,]1))
183	182, 2	eleq2s 2862	. . . . . . . . . . 11 ⊢ (𝑐 ∈ 𝐼 → 𝑐:(1...𝑁)⟶(0[,]1))
184	183	ffvelcdmda 7118	. . . . . . . . . 10 ⊢ ((𝑐 ∈ 𝐼 ∧ 𝑛 ∈ (1...𝑁)) → (𝑐‘𝑛) ∈ (0[,]1))
185	181, 184	sselid 4006	. . . . . . . . 9 ⊢ ((𝑐 ∈ 𝐼 ∧ 𝑛 ∈ (1...𝑁)) → (𝑐‘𝑛) ∈ ℂ)
186	185	adantll 713	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → (𝑐‘𝑛) ∈ ℂ)
187		elmapi 8907	. . . . . . . . . . . 12 ⊢ ((𝐹‘𝑐) ∈ ((0[,]1) ↑_m (1...𝑁)) → (𝐹‘𝑐):(1...𝑁)⟶(0[,]1))
188	187, 2	eleq2s 2862	. . . . . . . . . . 11 ⊢ ((𝐹‘𝑐) ∈ 𝐼 → (𝐹‘𝑐):(1...𝑁)⟶(0[,]1))
189	169, 188	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐼) → (𝐹‘𝑐):(1...𝑁)⟶(0[,]1))
190	189	ffvelcdmda 7118	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → ((𝐹‘𝑐)‘𝑛) ∈ (0[,]1))
191	181, 190	sselid 4006	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → ((𝐹‘𝑐)‘𝑛) ∈ ℂ)
192	186, 191	subeq0ad 11657	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → (((𝑐‘𝑛) − ((𝐹‘𝑐)‘𝑛)) = 0 ↔ (𝑐‘𝑛) = ((𝐹‘𝑐)‘𝑛)))
193	180, 192	bitrd 279	. . . . . 6 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → (((𝑐 ∘_f − (𝐹‘𝑐))‘𝑛) = (((1...𝑁) × {0})‘𝑛) ↔ (𝑐‘𝑛) = ((𝐹‘𝑐)‘𝑛)))
194	193	ralbidva 3182	. . . . 5 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐼) → (∀𝑛 ∈ (1...𝑁)((𝑐 ∘_f − (𝐹‘𝑐))‘𝑛) = (((1...𝑁) × {0})‘𝑛) ↔ ∀𝑛 ∈ (1...𝑁)(𝑐‘𝑛) = ((𝐹‘𝑐)‘𝑛)))
195	168, 172, 173, 173, 27	offn 7727	. . . . . 6 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐼) → (𝑐 ∘_f − (𝐹‘𝑐)) Fn (1...𝑁))
196		fnconstg 6809	. . . . . . 7 ⊢ (0 ∈ V → ((1...𝑁) × {0}) Fn (1...𝑁))
197	177, 196	ax-mp 5	. . . . . 6 ⊢ ((1...𝑁) × {0}) Fn (1...𝑁)
198		eqfnfv 7064	. . . . . 6 ⊢ (((𝑐 ∘_f − (𝐹‘𝑐)) Fn (1...𝑁) ∧ ((1...𝑁) × {0}) Fn (1...𝑁)) → ((𝑐 ∘_f − (𝐹‘𝑐)) = ((1...𝑁) × {0}) ↔ ∀𝑛 ∈ (1...𝑁)((𝑐 ∘_f − (𝐹‘𝑐))‘𝑛) = (((1...𝑁) × {0})‘𝑛)))
199	195, 197, 198	sylancl 585	. . . . 5 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐼) → ((𝑐 ∘_f − (𝐹‘𝑐)) = ((1...𝑁) × {0}) ↔ ∀𝑛 ∈ (1...𝑁)((𝑐 ∘_f − (𝐹‘𝑐))‘𝑛) = (((1...𝑁) × {0})‘𝑛)))
200		eqfnfv 7064	. . . . . 6 ⊢ ((𝑐 Fn (1...𝑁) ∧ (𝐹‘𝑐) Fn (1...𝑁)) → (𝑐 = (𝐹‘𝑐) ↔ ∀𝑛 ∈ (1...𝑁)(𝑐‘𝑛) = ((𝐹‘𝑐)‘𝑛)))
201	168, 172, 200	syl2anc 583	. . . . 5 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐼) → (𝑐 = (𝐹‘𝑐) ↔ ∀𝑛 ∈ (1...𝑁)(𝑐‘𝑛) = ((𝐹‘𝑐)‘𝑛)))
202	194, 199, 201	3bitr4d 311	. . . 4 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐼) → ((𝑐 ∘_f − (𝐹‘𝑐)) = ((1...𝑁) × {0}) ↔ 𝑐 = (𝐹‘𝑐)))
203	165, 202	bitrd 279	. . 3 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐼) → (((𝑥 ∈ 𝐼 ↦ (𝑥 ∘_f − (𝐹‘𝑥)))‘𝑐) = ((1...𝑁) × {0}) ↔ 𝑐 = (𝐹‘𝑐)))
204	203	rexbidva 3183	. 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 1087 = wceq 1537 ∈ wcel 2108 ∀wral 3067 ∃wrex 3076 Vcvv 3488 ⊆ wss 3976 {csn 4648 class class class wbr 5166 ↦ cmpt 5249 × cxp 5698 ran crn 5701 ↾ cres 5702 Fn wfn 6568 ⟶wf 6569 ‘cfv 6573 (class class class)co 7448 ∘_f cof 7712 ↑_m cmap 8884 ℂcc 11182 ℝcr 11183 0cc0 11184 1c1 11185 ℝ^*cxr 11323 ≤ cle 11325 − cmin 11520 -cneg 11521 ℕcn 12293 (,)cioo 13407 [,]cicc 13410 ...cfz 13567 ↾_t crest 17480 TopOpenctopn 17481 topGenctg 17497 ∏_tcpt 17498 ℂ_fldccnfld 21387 Topctop 22920 TopOnctopon 22937 Cn ccn 23253 ×_t ctx 23589

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1793 ax-4 1807 ax-5 1909 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2158 ax-12 2178 ax-ext 2711 ax-rep 5303 ax-sep 5317 ax-nul 5324 ax-pow 5383 ax-pr 5447 ax-un 7770 ax-inf2 9710 ax-cnex 11240 ax-resscn 11241 ax-1cn 11242 ax-icn 11243 ax-addcl 11244 ax-addrcl 11245 ax-mulcl 11246 ax-mulrcl 11247 ax-mulcom 11248 ax-addass 11249 ax-mulass 11250 ax-distr 11251 ax-i2m1 11252 ax-1ne0 11253 ax-1rid 11254 ax-rnegex 11255 ax-rrecex 11256 ax-cnre 11257 ax-pre-lttri 11258 ax-pre-lttrn 11259 ax-pre-ltadd 11260 ax-pre-mulgt0 11261 ax-pre-sup 11262

This theorem depends on definitions: df-bi 207 df-an 396 df-or 847 df-3or 1088 df-3an 1089 df-tru 1540 df-fal 1550 df-ex 1778 df-nf 1782 df-sb 2065 df-mo 2543 df-eu 2572 df-clab 2718 df-cleq 2732 df-clel 2819 df-nfc 2895 df-ne 2947 df-nel 3053 df-ral 3068 df-rex 3077 df-rmo 3388 df-reu 3389 df-rab 3444 df-v 3490 df-sbc 3805 df-csb 3922 df-dif 3979 df-un 3981 df-in 3983 df-ss 3993 df-pss 3996 df-nul 4353 df-if 4549 df-pw 4624 df-sn 4649 df-pr 4651 df-tp 4653 df-op 4655 df-uni 4932 df-int 4971 df-iun 5017 df-iin 5018 df-disj 5134 df-br 5167 df-opab 5229 df-mpt 5250 df-tr 5284 df-id 5593 df-eprel 5599 df-po 5607 df-so 5608 df-fr 5652 df-se 5653 df-we 5654 df-xp 5706 df-rel 5707 df-cnv 5708 df-co 5709 df-dm 5710 df-rn 5711 df-res 5712 df-ima 5713 df-pred 6332 df-ord 6398 df-on 6399 df-lim 6400 df-suc 6401 df-iota 6525 df-fun 6575 df-fn 6576 df-f 6577 df-f1 6578 df-fo 6579 df-f1o 6580 df-fv 6581 df-isom 6582 df-riota 7404 df-ov 7451 df-oprab 7452 df-mpo 7453 df-of 7714 df-om 7904 df-1st 8030 df-2nd 8031 df-supp 8202 df-frecs 8322 df-wrecs 8353 df-recs 8427 df-rdg 8466 df-1o 8522 df-2o 8523 df-oadd 8526 df-omul 8527 df-er 8763 df-map 8886 df-pm 8887 df-ixp 8956 df-en 9004 df-dom 9005 df-sdom 9006 df-fin 9007 df-fsupp 9432 df-fi 9480 df-sup 9511 df-inf 9512 df-oi 9579 df-dju 9970 df-card 10008 df-acn 10011 df-pnf 11326 df-mnf 11327 df-xr 11328 df-ltxr 11329 df-le 11330 df-sub 11522 df-neg 11523 df-div 11948 df-nn 12294 df-2 12356 df-3 12357 df-4 12358 df-5 12359 df-6 12360 df-7 12361 df-8 12362 df-9 12363 df-n0 12554 df-xnn0 12626 df-z 12640 df-dec 12759 df-uz 12904 df-q 13014 df-rp 13058 df-xneg 13175 df-xadd 13176 df-xmul 13177 df-ioo 13411 df-icc 13414 df-fz 13568 df-fzo 13712 df-fl 13843 df-seq 14053 df-exp 14113 df-fac 14323 df-bc 14352 df-hash 14380 df-cj 15148 df-re 15149 df-im 15150 df-sqrt 15284 df-abs 15285 df-clim 15534 df-sum 15735 df-dvds 16303 df-struct 17194 df-sets 17211 df-slot 17229 df-ndx 17241 df-base 17259 df-ress 17288 df-plusg 17324 df-mulr 17325 df-starv 17326 df-sca 17327 df-vsca 17328 df-ip 17329 df-tset 17330 df-ple 17331 df-ds 17333 df-unif 17334 df-hom 17335 df-cco 17336 df-rest 17482 df-topn 17483 df-0g 17501 df-gsum 17502 df-topgen 17503 df-pt 17504 df-prds 17507 df-xrs 17562 df-qtop 17567 df-imas 17568 df-xps 17570 df-mre 17644 df-mrc 17645 df-acs 17647 df-ps 18636 df-tsr 18637 df-mgm 18678 df-sgrp 18757 df-mnd 18773 df-submnd 18819 df-mulg 19108 df-cntz 19357 df-cmn 19824 df-psmet 21379 df-xmet 21380 df-met 21381 df-bl 21382 df-mopn 21383 df-cnfld 21388 df-top 22921 df-topon 22938 df-topsp 22960 df-bases 22974 df-cld 23048 df-ntr 23049 df-cls 23050 df-lp 23165 df-cn 23256 df-cnp 23257 df-t1 23343 df-haus 23344 df-cmp 23416 df-tx 23591 df-hmeo 23784 df-hmph 23785 df-xms 24351 df-ms 24352 df-tms 24353 df-ii 24922

This theorem is referenced by: (None)

W3C validator