broucube

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)

	Ref	Expression
Hypotheses	poimir.0	$⊢ φ \to N \in ℕ$
	poimir.i	$⊢ I = {[0, 1]}^{(1 \dots N)}$
	poimir.r	$⊢ R = \prod_{𝑡} ((1 \dots N) \times \{topGen (ran (.))\})$
	broucube.1	$⊢ φ \to F \in ((R ↾_{𝑡} I) Cn (R ↾_{𝑡} I))$
Assertion	broucube	$⊢ φ \to \exists c \in I c = F (c)$

Proof

Step	Hyp	Ref	Expression
1		poimir.0	$⊢ φ \to N \in ℕ$
2		poimir.i	$⊢ I = {[0, 1]}^{(1 \dots N)}$
3		poimir.r	$⊢ R = \prod_{𝑡} ((1 \dots N) \times \{topGen (ran (.))\})$
4		broucube.1	$⊢ φ \to F \in ((R ↾_{𝑡} I) Cn (R ↾_{𝑡} I))$
5		elmapfn	$⊢ x \in ({[0, 1]}^{(1 \dots N)}) \to x Fn (1 \dots N)$
6	5 2	eleq2s	$⊢ x \in I \to x Fn (1 \dots N)$
7	6	adantl	$⊢ (φ \land x \in I) \to x Fn (1 \dots N)$
8		ovex	$⊢ (1 \dots N) \in V$
9		retopon	$⊢ topGen (ran (.)) \in TopOn (ℝ)$
10	3	pttoponconst	$⊢ ((1 \dots N) \in V \land topGen (ran (.)) \in TopOn (ℝ)) \to R \in TopOn (ℝ^{(1 \dots N)})$
11	8 9 10	mp2an	$⊢ R \in TopOn (ℝ^{(1 \dots N)})$
12		reex	$⊢ ℝ \in V$
13		unitssre	$⊢ [0, 1] \subseteq ℝ$
14		mapss	$⊢ (ℝ \in V \land [0, 1] \subseteq ℝ) \to {[0, 1]}^{(1 \dots N)} \subseteq ℝ^{(1 \dots N)}$
15	12 13 14	mp2an	$⊢ {[0, 1]}^{(1 \dots N)} \subseteq ℝ^{(1 \dots N)}$
16	2 15	eqsstri	$⊢ I \subseteq ℝ^{(1 \dots N)}$
17		resttopon	$⊢ (R \in TopOn (ℝ^{(1 \dots N)}) \land I \subseteq ℝ^{(1 \dots N)}) \to R ↾_{𝑡} I \in TopOn (I)$
18	11 16 17	mp2an	$⊢ R ↾_{𝑡} I \in TopOn (I)$
19	18	toponunii	$⊢ I = ⋃ (R ↾_{𝑡} I)$
20	19 19	cnf	$⊢ F \in ((R ↾_{𝑡} I) Cn (R ↾_{𝑡} I)) \to F : I ⟶ I$
21	4 20	syl	$⊢ φ \to F : I ⟶ I$
22	21	ffvelrnda	$⊢ (φ \land x \in I) \to F (x) \in I$
23		elmapfn	$⊢ F (x) \in ({[0, 1]}^{(1 \dots N)}) \to F (x) Fn (1 \dots N)$
24	23 2	eleq2s	$⊢ F (x) \in I \to F (x) Fn (1 \dots N)$
25	22 24	syl	$⊢ (φ \land x \in I) \to F (x) Fn (1 \dots N)$
26		ovexd	$⊢ (φ \land x \in I) \to (1 \dots N) \in V$
27		inidm	$⊢ (1 \dots N) \cap (1 \dots N) = (1 \dots N)$
28		eqidd	$⊢ ((φ \land x \in I) \land n \in (1 \dots N)) \to x (n) = x (n)$
29		eqidd	$⊢ ((φ \land x \in I) \land n \in (1 \dots N)) \to F (x) (n) = F (x) (n)$
30	7 25 26 26 27 28 29	offval	$⊢ (φ \land x \in I) \to x -_{f} F (x) = (n \in (1 \dots N) ⟼ x (n) - F (x) (n))$
31	30	mpteq2dva	$⊢ φ \to (x \in I ⟼ x -_{f} F (x)) = (x \in I ⟼ (n \in (1 \dots N) ⟼ x (n) - F (x) (n)))$
32	18	a1i	$⊢ φ \to R ↾_{𝑡} I \in TopOn (I)$
33		ovexd	$⊢ φ \to (1 \dots N) \in V$
34		retop	$⊢ topGen (ran (.)) \in Top$
35	34	fconst6	$⊢ ((1 \dots N) \times \{topGen (ran (.))\}) : (1 \dots N) ⟶ Top$
36	35	a1i	$⊢ φ \to ((1 \dots N) \times \{topGen (ran (.))\}) : (1 \dots N) ⟶ Top$
37	18	a1i	$⊢ (φ \land n \in (1 \dots N)) \to R ↾_{𝑡} I \in TopOn (I)$
38		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
39	38	cnfldtop	$⊢ TopOpen (ℂ_{fld}) \in Top$
40		cnrest2r	$⊢ TopOpen (ℂ_{fld}) \in Top \to (R ↾_{𝑡} I) Cn (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ) \subseteq (R ↾_{𝑡} I) Cn TopOpen (ℂ_{fld})$
41	39 40	ax-mp	$⊢ (R ↾_{𝑡} I) Cn (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ) \subseteq (R ↾_{𝑡} I) Cn TopOpen (ℂ_{fld})$
42		resmpt	$⊢ I \subseteq ℝ^{(1 \dots N)} \to {(x \in (ℝ^{(1 \dots N)}) ⟼ x (n)) ↾}_{I} = (x \in I ⟼ x (n))$
43	16 42	ax-mp	$⊢ {(x \in (ℝ^{(1 \dots N)}) ⟼ x (n)) ↾}_{I} = (x \in I ⟼ x (n))$
44	11	toponunii	$⊢ ℝ^{(1 \dots N)} = ⋃ R$
45	44 3	ptpjcn	$⊢ ((1 \dots N) \in V \land ((1 \dots N) \times \{topGen (ran (.))\}) : (1 \dots N) ⟶ Top \land n \in (1 \dots N)) \to (x \in (ℝ^{(1 \dots N)}) ⟼ x (n)) \in (R Cn ((1 \dots N) \times \{topGen (ran (.))\}) (n))$
46	8 35 45	mp3an12	$⊢ n \in (1 \dots N) \to (x \in (ℝ^{(1 \dots N)}) ⟼ x (n)) \in (R Cn ((1 \dots N) \times \{topGen (ran (.))\}) (n))$
47	44	cnrest	$⊢ ((x \in (ℝ^{(1 \dots N)}) ⟼ x (n)) \in (R Cn ((1 \dots N) \times \{topGen (ran (.))\}) (n)) \land I \subseteq ℝ^{(1 \dots N)}) \to {(x \in (ℝ^{(1 \dots N)}) ⟼ x (n)) ↾}_{I} \in ((R ↾_{𝑡} I) Cn ((1 \dots N) \times \{topGen (ran (.))\}) (n))$
48	46 16 47	sylancl	$⊢ n \in (1 \dots N) \to {(x \in (ℝ^{(1 \dots N)}) ⟼ x (n)) ↾}_{I} \in ((R ↾_{𝑡} I) Cn ((1 \dots N) \times \{topGen (ran (.))\}) (n))$
49	43 48	eqeltrrid	$⊢ n \in (1 \dots N) \to (x \in I ⟼ x (n)) \in ((R ↾_{𝑡} I) Cn ((1 \dots N) \times \{topGen (ran (.))\}) (n))$
50		fvex	$⊢ topGen (ran (.)) \in V$
51	50	fvconst2	$⊢ n \in (1 \dots N) \to ((1 \dots N) \times \{topGen (ran (.))\}) (n) = topGen (ran (.))$
52	38	tgioo2	$⊢ topGen (ran (.)) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ$
53	51 52	eqtrdi	$⊢ n \in (1 \dots N) \to ((1 \dots N) \times \{topGen (ran (.))\}) (n) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ$
54	53	oveq2d	$⊢ n \in (1 \dots N) \to (R ↾_{𝑡} I) Cn ((1 \dots N) \times \{topGen (ran (.))\}) (n) = (R ↾_{𝑡} I) Cn (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ)$
55	49 54	eleqtrd	$⊢ n \in (1 \dots N) \to (x \in I ⟼ x (n)) \in ((R ↾_{𝑡} I) Cn (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ))$
56	41 55	sselid	$⊢ n \in (1 \dots N) \to (x \in I ⟼ x (n)) \in ((R ↾_{𝑡} I) Cn TopOpen (ℂ_{fld}))$
57	56	adantl	$⊢ (φ \land n \in (1 \dots N)) \to (x \in I ⟼ x (n)) \in ((R ↾_{𝑡} I) Cn TopOpen (ℂ_{fld}))$
58	21	feqmptd	$⊢ φ \to F = (x \in I ⟼ F (x))$
59	58 4	eqeltrrd	$⊢ φ \to (x \in I ⟼ F (x)) \in ((R ↾_{𝑡} I) Cn (R ↾_{𝑡} I))$
60	59	adantr	$⊢ (φ \land n \in (1 \dots N)) \to (x \in I ⟼ F (x)) \in ((R ↾_{𝑡} I) Cn (R ↾_{𝑡} I))$
61		fveq1	$⊢ x = z \to x (n) = z (n)$
62	61	cbvmptv	$⊢ (x \in I ⟼ x (n)) = (z \in I ⟼ z (n))$
63	62 57	eqeltrrid	$⊢ (φ \land n \in (1 \dots N)) \to (z \in I ⟼ z (n)) \in ((R ↾_{𝑡} I) Cn TopOpen (ℂ_{fld}))$
64		fveq1	$⊢ z = F (x) \to z (n) = F (x) (n)$
65	37 60 37 63 64	cnmpt11	$⊢ (φ \land n \in (1 \dots N)) \to (x \in I ⟼ F (x) (n)) \in ((R ↾_{𝑡} I) Cn TopOpen (ℂ_{fld}))$
66	38	subcn	$⊢ - \in ((TopOpen (ℂ_{fld}) \times_{t} TopOpen (ℂ_{fld})) Cn TopOpen (ℂ_{fld}))$
67	66	a1i	$⊢ (φ \land n \in (1 \dots N)) \to - \in ((TopOpen (ℂ_{fld}) \times_{t} TopOpen (ℂ_{fld})) Cn TopOpen (ℂ_{fld}))$
68	37 57 65 67	cnmpt12f	$⊢ (φ \land n \in (1 \dots N)) \to (x \in I ⟼ x (n) - F (x) (n)) \in ((R ↾_{𝑡} I) Cn TopOpen (ℂ_{fld}))$
69		elmapi	$⊢ x \in ({[0, 1]}^{(1 \dots N)}) \to x : (1 \dots N) ⟶ [0, 1]$
70	69 2	eleq2s	$⊢ x \in I \to x : (1 \dots N) ⟶ [0, 1]$
71	70	ffvelrnda	$⊢ (x \in I \land n \in (1 \dots N)) \to x (n) \in [0, 1]$
72	13 71	sselid	$⊢ (x \in I \land n \in (1 \dots N)) \to x (n) \in ℝ$
73	72	adantll	$⊢ ((φ \land x \in I) \land n \in (1 \dots N)) \to x (n) \in ℝ$
74		elmapi	$⊢ F (x) \in ({[0, 1]}^{(1 \dots N)}) \to F (x) : (1 \dots N) ⟶ [0, 1]$
75	74 2	eleq2s	$⊢ F (x) \in I \to F (x) : (1 \dots N) ⟶ [0, 1]$
76	22 75	syl	$⊢ (φ \land x \in I) \to F (x) : (1 \dots N) ⟶ [0, 1]$
77	76	ffvelrnda	$⊢ ((φ \land x \in I) \land n \in (1 \dots N)) \to F (x) (n) \in [0, 1]$
78	13 77	sselid	$⊢ ((φ \land x \in I) \land n \in (1 \dots N)) \to F (x) (n) \in ℝ$
79	73 78	resubcld	$⊢ ((φ \land x \in I) \land n \in (1 \dots N)) \to x (n) - F (x) (n) \in ℝ$
80	79	an32s	$⊢ ((φ \land n \in (1 \dots N)) \land x \in I) \to x (n) - F (x) (n) \in ℝ$
81	80	fmpttd	$⊢ (φ \land n \in (1 \dots N)) \to (x \in I ⟼ x (n) - F (x) (n)) : I ⟶ ℝ$
82		frn	$⊢ (x \in I ⟼ x (n) - F (x) (n)) : I ⟶ ℝ \to ran (x \in I ⟼ x (n) - F (x) (n)) \subseteq ℝ$
83	38	cnfldtopon	$⊢ TopOpen (ℂ_{fld}) \in TopOn (ℂ)$
84		ax-resscn	$⊢ ℝ \subseteq ℂ$
85		cnrest2	$⊢ (TopOpen (ℂ_{fld}) \in TopOn (ℂ) \land ran (x \in I ⟼ x (n) - F (x) (n)) \subseteq ℝ \land ℝ \subseteq ℂ) \to ((x \in I ⟼ x (n) - F (x) (n)) \in ((R ↾_{𝑡} I) Cn TopOpen (ℂ_{fld})) \leftrightarrow (x \in I ⟼ x (n) - F (x) (n)) \in ((R ↾_{𝑡} I) Cn (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ)))$
86	83 84 85	mp3an13	$⊢ ran (x \in I ⟼ x (n) - F (x) (n)) \subseteq ℝ \to ((x \in I ⟼ x (n) - F (x) (n)) \in ((R ↾_{𝑡} I) Cn TopOpen (ℂ_{fld})) \leftrightarrow (x \in I ⟼ x (n) - F (x) (n)) \in ((R ↾_{𝑡} I) Cn (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ)))$
87	81 82 86	3syl	$⊢ (φ \land n \in (1 \dots N)) \to ((x \in I ⟼ x (n) - F (x) (n)) \in ((R ↾_{𝑡} I) Cn TopOpen (ℂ_{fld})) \leftrightarrow (x \in I ⟼ x (n) - F (x) (n)) \in ((R ↾_{𝑡} I) Cn (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ)))$
88	68 87	mpbid	$⊢ (φ \land n \in (1 \dots N)) \to (x \in I ⟼ x (n) - F (x) (n)) \in ((R ↾_{𝑡} I) Cn (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ))$
89	54	adantl	$⊢ (φ \land n \in (1 \dots N)) \to (R ↾_{𝑡} I) Cn ((1 \dots N) \times \{topGen (ran (.))\}) (n) = (R ↾_{𝑡} I) Cn (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ)$
90	88 89	eleqtrrd	$⊢ (φ \land n \in (1 \dots N)) \to (x \in I ⟼ x (n) - F (x) (n)) \in ((R ↾_{𝑡} I) Cn ((1 \dots N) \times \{topGen (ran (.))\}) (n))$
91	3 32 33 36 90	ptcn	$⊢ φ \to (x \in I ⟼ (n \in (1 \dots N) ⟼ x (n) - F (x) (n))) \in ((R ↾_{𝑡} I) Cn R)$
92	31 91	eqeltrd	$⊢ φ \to (x \in I ⟼ x -_{f} F (x)) \in ((R ↾_{𝑡} I) Cn R)$
93		simpr2	$⊢ (φ \land (n \in (1 \dots N) \land z \in I \land z (n) = 0)) \to z \in I$
94		id	$⊢ x = z \to x = z$
95		fveq2	$⊢ x = z \to F (x) = F (z)$
96	94 95	oveq12d	$⊢ x = z \to x -_{f} F (x) = z -_{f} F (z)$
97		eqid	$⊢ (x \in I ⟼ x -_{f} F (x)) = (x \in I ⟼ x -_{f} F (x))$
98		ovex	$⊢ z -_{f} F (z) \in V$
99	96 97 98	fvmpt	$⊢ z \in I \to (x \in I ⟼ x -_{f} F (x)) (z) = z -_{f} F (z)$
100	99	fveq1d	$⊢ z \in I \to (x \in I ⟼ x -_{f} F (x)) (z) (n) = (z -_{f} F (z)) (n)$
101	93 100	syl	$⊢ (φ \land (n \in (1 \dots N) \land z \in I \land z (n) = 0)) \to (x \in I ⟼ x -_{f} F (x)) (z) (n) = (z -_{f} F (z)) (n)$
102		elmapfn	$⊢ z \in ({[0, 1]}^{(1 \dots N)}) \to z Fn (1 \dots N)$
103	102 2	eleq2s	$⊢ z \in I \to z Fn (1 \dots N)$
104	103	adantl	$⊢ ((φ \land z (n) = 0) \land z \in I) \to z Fn (1 \dots N)$
105	21	ffvelrnda	$⊢ (φ \land z \in I) \to F (z) \in I$
106		elmapfn	$⊢ F (z) \in ({[0, 1]}^{(1 \dots N)}) \to F (z) Fn (1 \dots N)$
107	106 2	eleq2s	$⊢ F (z) \in I \to F (z) Fn (1 \dots N)$
108	105 107	syl	$⊢ (φ \land z \in I) \to F (z) Fn (1 \dots N)$
109	108	adantlr	$⊢ ((φ \land z (n) = 0) \land z \in I) \to F (z) Fn (1 \dots N)$
110		ovexd	$⊢ ((φ \land z (n) = 0) \land z \in I) \to (1 \dots N) \in V$
111		simpllr	$⊢ (((φ \land z (n) = 0) \land z \in I) \land n \in (1 \dots N)) \to z (n) = 0$
112		eqidd	$⊢ (((φ \land z (n) = 0) \land z \in I) \land n \in (1 \dots N)) \to F (z) (n) = F (z) (n)$
113	104 109 110 110 27 111 112	ofval	$⊢ (((φ \land z (n) = 0) \land z \in I) \land n \in (1 \dots N)) \to (z -_{f} F (z)) (n) = 0 - F (z) (n)$
114		df-neg	$⊢ - F (z) (n) = 0 - F (z) (n)$
115	113 114	eqtr4di	$⊢ (((φ \land z (n) = 0) \land z \in I) \land n \in (1 \dots N)) \to (z -_{f} F (z)) (n) = - F (z) (n)$
116	115	exp41	$⊢ φ \to (z (n) = 0 \to (z \in I \to (n \in (1 \dots N) \to (z -_{f} F (z)) (n) = - F (z) (n))))$
117	116	com24	$⊢ φ \to (n \in (1 \dots N) \to (z \in I \to (z (n) = 0 \to (z -_{f} F (z)) (n) = - F (z) (n))))$
118	117	3imp2	$⊢ (φ \land (n \in (1 \dots N) \land z \in I \land z (n) = 0)) \to (z -_{f} F (z)) (n) = - F (z) (n)$
119	101 118	eqtrd	$⊢ (φ \land (n \in (1 \dots N) \land z \in I \land z (n) = 0)) \to (x \in I ⟼ x -_{f} F (x)) (z) (n) = - F (z) (n)$
120		elmapi	$⊢ F (z) \in ({[0, 1]}^{(1 \dots N)}) \to F (z) : (1 \dots N) ⟶ [0, 1]$
121	120 2	eleq2s	$⊢ F (z) \in I \to F (z) : (1 \dots N) ⟶ [0, 1]$
122	105 121	syl	$⊢ (φ \land z \in I) \to F (z) : (1 \dots N) ⟶ [0, 1]$
123	122	ffvelrnda	$⊢ ((φ \land z \in I) \land n \in (1 \dots N)) \to F (z) (n) \in [0, 1]$
124		0xr	$⊢ 0 \in ℝ^{*}$
125		1xr	$⊢ 1 \in ℝ^{*}$
126		iccgelb	$⊢ (0 \in ℝ^{} \land 1 \in ℝ^{} \land F (z) (n) \in [0, 1]) \to 0 \leq F (z) (n)$
127	124 125 126	mp3an12	$⊢ F (z) (n) \in [0, 1] \to 0 \leq F (z) (n)$
128	123 127	syl	$⊢ ((φ \land z \in I) \land n \in (1 \dots N)) \to 0 \leq F (z) (n)$
129	13 123	sselid	$⊢ ((φ \land z \in I) \land n \in (1 \dots N)) \to F (z) (n) \in ℝ$
130	129	le0neg2d	$⊢ ((φ \land z \in I) \land n \in (1 \dots N)) \to (0 \leq F (z) (n) \leftrightarrow - F (z) (n) \leq 0)$
131	128 130	mpbid	$⊢ ((φ \land z \in I) \land n \in (1 \dots N)) \to - F (z) (n) \leq 0$
132	131	an32s	$⊢ ((φ \land n \in (1 \dots N)) \land z \in I) \to - F (z) (n) \leq 0$
133	132	anasss	$⊢ (φ \land (n \in (1 \dots N) \land z \in I)) \to - F (z) (n) \leq 0$
134	133	3adantr3	$⊢ (φ \land (n \in (1 \dots N) \land z \in I \land z (n) = 0)) \to - F (z) (n) \leq 0$
135	119 134	eqbrtrd	$⊢ (φ \land (n \in (1 \dots N) \land z \in I \land z (n) = 0)) \to (x \in I ⟼ x -_{f} F (x)) (z) (n) \leq 0$
136		iccleub	$⊢ (0 \in ℝ^{} \land 1 \in ℝ^{} \land F (z) (n) \in [0, 1]) \to F (z) (n) \leq 1$
137	124 125 136	mp3an12	$⊢ F (z) (n) \in [0, 1] \to F (z) (n) \leq 1$
138	123 137	syl	$⊢ ((φ \land z \in I) \land n \in (1 \dots N)) \to F (z) (n) \leq 1$
139		1red	$⊢ ((φ \land z \in I) \land n \in (1 \dots N)) \to 1 \in ℝ$
140	139 129	subge0d	$⊢ ((φ \land z \in I) \land n \in (1 \dots N)) \to (0 \leq 1 - F (z) (n) \leftrightarrow F (z) (n) \leq 1)$
141	138 140	mpbird	$⊢ ((φ \land z \in I) \land n \in (1 \dots N)) \to 0 \leq 1 - F (z) (n)$
142	141	an32s	$⊢ ((φ \land n \in (1 \dots N)) \land z \in I) \to 0 \leq 1 - F (z) (n)$
143	142	anasss	$⊢ (φ \land (n \in (1 \dots N) \land z \in I)) \to 0 \leq 1 - F (z) (n)$
144	143	3adantr3	$⊢ (φ \land (n \in (1 \dots N) \land z \in I \land z (n) = 1)) \to 0 \leq 1 - F (z) (n)$
145		simpr2	$⊢ (φ \land (n \in (1 \dots N) \land z \in I \land z (n) = 1)) \to z \in I$
146	145 100	syl	$⊢ (φ \land (n \in (1 \dots N) \land z \in I \land z (n) = 1)) \to (x \in I ⟼ x -_{f} F (x)) (z) (n) = (z -_{f} F (z)) (n)$
147	103	adantl	$⊢ ((φ \land z (n) = 1) \land z \in I) \to z Fn (1 \dots N)$
148	108	adantlr	$⊢ ((φ \land z (n) = 1) \land z \in I) \to F (z) Fn (1 \dots N)$
149		ovexd	$⊢ ((φ \land z (n) = 1) \land z \in I) \to (1 \dots N) \in V$
150		simpllr	$⊢ (((φ \land z (n) = 1) \land z \in I) \land n \in (1 \dots N)) \to z (n) = 1$
151		eqidd	$⊢ (((φ \land z (n) = 1) \land z \in I) \land n \in (1 \dots N)) \to F (z) (n) = F (z) (n)$
152	147 148 149 149 27 150 151	ofval	$⊢ (((φ \land z (n) = 1) \land z \in I) \land n \in (1 \dots N)) \to (z -_{f} F (z)) (n) = 1 - F (z) (n)$
153	152	exp41	$⊢ φ \to (z (n) = 1 \to (z \in I \to (n \in (1 \dots N) \to (z -_{f} F (z)) (n) = 1 - F (z) (n))))$
154	153	com24	$⊢ φ \to (n \in (1 \dots N) \to (z \in I \to (z (n) = 1 \to (z -_{f} F (z)) (n) = 1 - F (z) (n))))$
155	154	3imp2	$⊢ (φ \land (n \in (1 \dots N) \land z \in I \land z (n) = 1)) \to (z -_{f} F (z)) (n) = 1 - F (z) (n)$
156	146 155	eqtrd	$⊢ (φ \land (n \in (1 \dots N) \land z \in I \land z (n) = 1)) \to (x \in I ⟼ x -_{f} F (x)) (z) (n) = 1 - F (z) (n)$
157	144 156	breqtrrd	$⊢ (φ \land (n \in (1 \dots N) \land z \in I \land z (n) = 1)) \to 0 \leq (x \in I ⟼ x -_{f} F (x)) (z) (n)$
158	1 2 3 92 135 157	poimir	$⊢ φ \to \exists c \in I (x \in I ⟼ x -_{f} F (x)) (c) = (1 \dots N) \times \{0\}$
159		id	$⊢ x = c \to x = c$
160		fveq2	$⊢ x = c \to F (x) = F (c)$
161	159 160	oveq12d	$⊢ x = c \to x -_{f} F (x) = c -_{f} F (c)$
162		ovex	$⊢ c -_{f} F (c) \in V$
163	161 97 162	fvmpt	$⊢ c \in I \to (x \in I ⟼ x -_{f} F (x)) (c) = c -_{f} F (c)$
164	163	adantl	$⊢ (φ \land c \in I) \to (x \in I ⟼ x -_{f} F (x)) (c) = c -_{f} F (c)$
165	164	eqeq1d	$⊢ (φ \land c \in I) \to ((x \in I ⟼ x -_{f} F (x)) (c) = (1 \dots N) \times \{0\} \leftrightarrow c -_{f} F (c) = (1 \dots N) \times \{0\})$
166		elmapfn	$⊢ c \in ({[0, 1]}^{(1 \dots N)}) \to c Fn (1 \dots N)$
167	166 2	eleq2s	$⊢ c \in I \to c Fn (1 \dots N)$
168	167	adantl	$⊢ (φ \land c \in I) \to c Fn (1 \dots N)$
169	21	ffvelrnda	$⊢ (φ \land c \in I) \to F (c) \in I$
170		elmapfn	$⊢ F (c) \in ({[0, 1]}^{(1 \dots N)}) \to F (c) Fn (1 \dots N)$
171	170 2	eleq2s	$⊢ F (c) \in I \to F (c) Fn (1 \dots N)$
172	169 171	syl	$⊢ (φ \land c \in I) \to F (c) Fn (1 \dots N)$
173		ovexd	$⊢ (φ \land c \in I) \to (1 \dots N) \in V$
174		eqidd	$⊢ ((φ \land c \in I) \land n \in (1 \dots N)) \to c (n) = c (n)$
175		eqidd	$⊢ ((φ \land c \in I) \land n \in (1 \dots N)) \to F (c) (n) = F (c) (n)$
176	168 172 173 173 27 174 175	ofval	$⊢ ((φ \land c \in I) \land n \in (1 \dots N)) \to (c -_{f} F (c)) (n) = c (n) - F (c) (n)$
177		c0ex	$⊢ 0 \in V$
178	177	fvconst2	$⊢ n \in (1 \dots N) \to ((1 \dots N) \times \{0\}) (n) = 0$
179	178	adantl	$⊢ ((φ \land c \in I) \land n \in (1 \dots N)) \to ((1 \dots N) \times \{0\}) (n) = 0$
180	176 179	eqeq12d	$⊢ ((φ \land c \in I) \land n \in (1 \dots N)) \to ((c -_{f} F (c)) (n) = ((1 \dots N) \times \{0\}) (n) \leftrightarrow c (n) - F (c) (n) = 0)$
181	13 84	sstri	$⊢ [0, 1] \subseteq ℂ$
182		elmapi	$⊢ c \in ({[0, 1]}^{(1 \dots N)}) \to c : (1 \dots N) ⟶ [0, 1]$
183	182 2	eleq2s	$⊢ c \in I \to c : (1 \dots N) ⟶ [0, 1]$
184	183	ffvelrnda	$⊢ (c \in I \land n \in (1 \dots N)) \to c (n) \in [0, 1]$
185	181 184	sselid	$⊢ (c \in I \land n \in (1 \dots N)) \to c (n) \in ℂ$
186	185	adantll	$⊢ ((φ \land c \in I) \land n \in (1 \dots N)) \to c (n) \in ℂ$
187		elmapi	$⊢ F (c) \in ({[0, 1]}^{(1 \dots N)}) \to F (c) : (1 \dots N) ⟶ [0, 1]$
188	187 2	eleq2s	$⊢ F (c) \in I \to F (c) : (1 \dots N) ⟶ [0, 1]$
189	169 188	syl	$⊢ (φ \land c \in I) \to F (c) : (1 \dots N) ⟶ [0, 1]$
190	189	ffvelrnda	$⊢ ((φ \land c \in I) \land n \in (1 \dots N)) \to F (c) (n) \in [0, 1]$
191	181 190	sselid	$⊢ ((φ \land c \in I) \land n \in (1 \dots N)) \to F (c) (n) \in ℂ$
192	186 191	subeq0ad	$⊢ ((φ \land c \in I) \land n \in (1 \dots N)) \to (c (n) - F (c) (n) = 0 \leftrightarrow c (n) = F (c) (n))$
193	180 192	bitrd	$⊢ ((φ \land c \in I) \land n \in (1 \dots N)) \to ((c -_{f} F (c)) (n) = ((1 \dots N) \times \{0\}) (n) \leftrightarrow c (n) = F (c) (n))$
194	193	ralbidva	$⊢ (φ \land c \in I) \to (\forall n \in (1 \dots N) (c -_{f} F (c)) (n) = ((1 \dots N) \times \{0\}) (n) \leftrightarrow \forall n \in (1 \dots N) c (n) = F (c) (n))$
195	168 172 173 173 27	offn	$⊢ (φ \land c \in I) \to (c -_{f} F (c)) Fn (1 \dots N)$
196		fnconstg	$⊢ 0 \in V \to ((1 \dots N) \times \{0\}) Fn (1 \dots N)$
197	177 196	ax-mp	$⊢ ((1 \dots N) \times \{0\}) Fn (1 \dots N)$
198		eqfnfv	$⊢ ((c -_{f} F (c)) Fn (1 \dots N) \land ((1 \dots N) \times \{0\}) Fn (1 \dots N)) \to (c -_{f} F (c) = (1 \dots N) \times \{0\} \leftrightarrow \forall n \in (1 \dots N) (c -_{f} F (c)) (n) = ((1 \dots N) \times \{0\}) (n))$
199	195 197 198	sylancl	$⊢ (φ \land c \in I) \to (c -_{f} F (c) = (1 \dots N) \times \{0\} \leftrightarrow \forall n \in (1 \dots N) (c -_{f} F (c)) (n) = ((1 \dots N) \times \{0\}) (n))$
200		eqfnfv	$⊢ (c Fn (1 \dots N) \land F (c) Fn (1 \dots N)) \to (c = F (c) \leftrightarrow \forall n \in (1 \dots N) c (n) = F (c) (n))$
201	168 172 200	syl2anc	$⊢ (φ \land c \in I) \to (c = F (c) \leftrightarrow \forall n \in (1 \dots N) c (n) = F (c) (n))$
202	194 199 201	3bitr4d	$⊢ (φ \land c \in I) \to (c -_{f} F (c) = (1 \dots N) \times \{0\} \leftrightarrow c = F (c))$
203	165 202	bitrd	$⊢ (φ \land c \in I) \to ((x \in I ⟼ x -_{f} F (x)) (c) = (1 \dots N) \times \{0\} \leftrightarrow c = F (c))$
204	203	rexbidva	$⊢ φ \to (\exists c \in I (x \in I ⟼ x -_{f} F (x)) (c) = (1 \dots N) \times \{0\} \leftrightarrow \exists c \in I c = F (c))$
205	158 204	mpbid	$⊢ φ \to \exists c \in I c = F (c)$

Metamath Proof Explorer

Theorem broucube

Proof