cvmliftlem13

Description: Lemma for cvmlift . The initial value of K is P because Q ( 1 ) is a subset of K which takes value P at 0 . (Contributed by Mario Carneiro, 16-Feb-2015)

	Ref	Expression
Hypotheses	cvmliftlem.1	$⊢ S = (k \in J ⟼ \{s \in (𝒫 C ∖ \{\emptyset\}) \| (⋃ s = F^{-1} [k] \land \forall u \in s (\forall v \in (s ∖ \{u\}) u \cap v = \emptyset \land {F ↾}_{u} \in ((C ↾_{𝑡} u) Homeo (J ↾_{𝑡} k))))\})$
	cvmliftlem.b	$⊢ B = ⋃ C$
	cvmliftlem.x	$⊢ X = ⋃ J$
	cvmliftlem.f	$⊢ φ \to F \in (C CovMap J)$
	cvmliftlem.g	$⊢ φ \to G \in (II Cn J)$
	cvmliftlem.p	$⊢ φ \to P \in B$
	cvmliftlem.e	$⊢ φ \to F (P) = G (0)$
	cvmliftlem.n	$⊢ φ \to N \in ℕ$
	cvmliftlem.t	$⊢ φ \to T : (1 \dots N) ⟶ ⋃_{j \in J} (\{j\} \times S (j))$
	cvmliftlem.a	$⊢ φ \to \forall k \in (1 \dots N) G [[\frac{k - 1}{N}, \frac{k}{N}]] \subseteq 1^{st} (T (k))$
	cvmliftlem.l	$⊢ L = topGen (ran (.))$
	cvmliftlem.q	$⊢ Q = seq 0 ((x \in V, m \in ℕ ⟼ (z \in [\frac{m - 1}{N}, \frac{m}{N}] ⟼ {({F ↾}_{(ι b \in 2^{nd} (T (m)) \| x (\frac{m - 1}{N}) \in b)})}^{-1} (G (z)))), (({I ↾}_{ℕ}) \cup \{⟨0, \{⟨0, P⟩\}⟩\}))$
	cvmliftlem.k	$⊢ K = ⋃_{k = 1}^{N} Q (k)$
Assertion	cvmliftlem13	$⊢ φ \to K (0) = P$

Proof

Step	Hyp	Ref	Expression
1		cvmliftlem.1	$⊢ S = (k \in J ⟼ \{s \in (𝒫 C ∖ \{\emptyset\}) \| (⋃ s = F^{-1} [k] \land \forall u \in s (\forall v \in (s ∖ \{u\}) u \cap v = \emptyset \land {F ↾}_{u} \in ((C ↾_{𝑡} u) Homeo (J ↾_{𝑡} k))))\})$
2		cvmliftlem.b	$⊢ B = ⋃ C$
3		cvmliftlem.x	$⊢ X = ⋃ J$
4		cvmliftlem.f	$⊢ φ \to F \in (C CovMap J)$
5		cvmliftlem.g	$⊢ φ \to G \in (II Cn J)$
6		cvmliftlem.p	$⊢ φ \to P \in B$
7		cvmliftlem.e	$⊢ φ \to F (P) = G (0)$
8		cvmliftlem.n	$⊢ φ \to N \in ℕ$
9		cvmliftlem.t	$⊢ φ \to T : (1 \dots N) ⟶ ⋃_{j \in J} (\{j\} \times S (j))$
10		cvmliftlem.a	$⊢ φ \to \forall k \in (1 \dots N) G [[\frac{k - 1}{N}, \frac{k}{N}]] \subseteq 1^{st} (T (k))$
11		cvmliftlem.l	$⊢ L = topGen (ran (.))$
12		cvmliftlem.q	$⊢ Q = seq 0 ((x \in V, m \in ℕ ⟼ (z \in [\frac{m - 1}{N}, \frac{m}{N}] ⟼ {({F ↾}_{(ι b \in 2^{nd} (T (m)) \| x (\frac{m - 1}{N}) \in b)})}^{-1} (G (z)))), (({I ↾}_{ℕ}) \cup \{⟨0, \{⟨0, P⟩\}⟩\}))$
13		cvmliftlem.k	$⊢ K = ⋃_{k = 1}^{N} Q (k)$
14	1 2 3 4 5 6 7 8 9 10 11 12 13	cvmliftlem11	$⊢ φ \to (K \in (II Cn C) \land F \circ K = G)$
15	14	simpld	$⊢ φ \to K \in (II Cn C)$
16		iiuni	$⊢ [0, 1] = ⋃ II$
17	16 2	cnf	$⊢ K \in (II Cn C) \to K : [0, 1] ⟶ B$
18	15 17	syl	$⊢ φ \to K : [0, 1] ⟶ B$
19	18	ffund	$⊢ φ \to Fun K$
20		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
21	8 20	eleqtrdi	$⊢ φ \to N \in ℤ_{\geq 1}$
22		eluzfz1	$⊢ N \in ℤ_{\geq 1} \to 1 \in (1 \dots N)$
23	21 22	syl	$⊢ φ \to 1 \in (1 \dots N)$
24		fveq2	$⊢ k = 1 \to Q (k) = Q (1)$
25	24	ssiun2s	$⊢ 1 \in (1 \dots N) \to Q (1) \subseteq ⋃_{k = 1}^{N} Q (k)$
26	23 25	syl	$⊢ φ \to Q (1) \subseteq ⋃_{k = 1}^{N} Q (k)$
27	26 13	sseqtrrdi	$⊢ φ \to Q (1) \subseteq K$
28		0xr	$⊢ 0 \in ℝ^{*}$
29	28	a1i	$⊢ φ \to 0 \in ℝ^{*}$
30	8	nnrecred	$⊢ φ \to \frac{1}{N} \in ℝ$
31	30	rexrd	$⊢ φ \to \frac{1}{N} \in ℝ^{*}$
32		1red	$⊢ φ \to 1 \in ℝ$
33		0le1	$⊢ 0 \leq 1$
34	33	a1i	$⊢ φ \to 0 \leq 1$
35	8	nnred	$⊢ φ \to N \in ℝ$
36	8	nngt0d	$⊢ φ \to 0 < N$
37		divge0	$⊢ ((1 \in ℝ \land 0 \leq 1) \land (N \in ℝ \land 0 < N)) \to 0 \leq \frac{1}{N}$
38	32 34 35 36 37	syl22anc	$⊢ φ \to 0 \leq \frac{1}{N}$
39		lbicc2	$⊢ (0 \in ℝ^{} \land \frac{1}{N} \in ℝ^{} \land 0 \leq \frac{1}{N}) \to 0 \in [0, \frac{1}{N}]$
40	29 31 38 39	syl3anc	$⊢ φ \to 0 \in [0, \frac{1}{N}]$
41		1m1e0	$⊢ 1 - 1 = 0$
42	41	oveq1i	$⊢ \frac{1 - 1}{N} = \frac{0}{N}$
43	8	nncnd	$⊢ φ \to N \in ℂ$
44	8	nnne0d	$⊢ φ \to N \neq 0$
45	43 44	div0d	$⊢ φ \to \frac{0}{N} = 0$
46	42 45	syl5eq	$⊢ φ \to \frac{1 - 1}{N} = 0$
47	46	oveq1d	$⊢ φ \to [\frac{1 - 1}{N}, \frac{1}{N}] = [0, \frac{1}{N}]$
48	40 47	eleqtrrd	$⊢ φ \to 0 \in [\frac{1 - 1}{N}, \frac{1}{N}]$
49		eqid	$⊢ [\frac{1 - 1}{N}, \frac{1}{N}] = [\frac{1 - 1}{N}, \frac{1}{N}]$
50		simpr	$⊢ (φ \land 1 \in (1 \dots N)) \to 1 \in (1 \dots N)$
51	1 2 3 4 5 6 7 8 9 10 11 12 49	cvmliftlem7	$⊢ (φ \land 1 \in (1 \dots N)) \to Q (1 - 1) (\frac{1 - 1}{N}) \in F^{-1} [\{G (\frac{1 - 1}{N})\}]$
52	1 2 3 4 5 6 7 8 9 10 11 12 49 50 51	cvmliftlem6	$⊢ (φ \land 1 \in (1 \dots N)) \to (Q (1) : [\frac{1 - 1}{N}, \frac{1}{N}] ⟶ B \land F \circ Q (1) = {G ↾}_{[\frac{1 - 1}{N}, \frac{1}{N}]})$
53	23 52	mpdan	$⊢ φ \to (Q (1) : [\frac{1 - 1}{N}, \frac{1}{N}] ⟶ B \land F \circ Q (1) = {G ↾}_{[\frac{1 - 1}{N}, \frac{1}{N}]})$
54	53	simpld	$⊢ φ \to Q (1) : [\frac{1 - 1}{N}, \frac{1}{N}] ⟶ B$
55	54	fdmd	$⊢ φ \to dom Q (1) = [\frac{1 - 1}{N}, \frac{1}{N}]$
56	48 55	eleqtrrd	$⊢ φ \to 0 \in dom Q (1)$
57		funssfv	$⊢ (Fun K \land Q (1) \subseteq K \land 0 \in dom Q (1)) \to K (0) = Q (1) (0)$
58	19 27 56 57	syl3anc	$⊢ φ \to K (0) = Q (1) (0)$
59	1 2 3 4 5 6 7 8 9 10 11 12	cvmliftlem9	$⊢ (φ \land 1 \in (1 \dots N)) \to Q (1) (\frac{1 - 1}{N}) = Q (1 - 1) (\frac{1 - 1}{N})$
60	23 59	mpdan	$⊢ φ \to Q (1) (\frac{1 - 1}{N}) = Q (1 - 1) (\frac{1 - 1}{N})$
61	46	fveq2d	$⊢ φ \to Q (1) (\frac{1 - 1}{N}) = Q (1) (0)$
62	41	fveq2i	$⊢ Q (1 - 1) = Q (0)$
63	1 2 3 4 5 6 7 8 9 10 11 12	cvmliftlem4	$⊢ Q (0) = \{⟨0, P⟩\}$
64	62 63	eqtri	$⊢ Q (1 - 1) = \{⟨0, P⟩\}$
65	64	a1i	$⊢ φ \to Q (1 - 1) = \{⟨0, P⟩\}$
66	65 46	fveq12d	$⊢ φ \to Q (1 - 1) (\frac{1 - 1}{N}) = \{⟨0, P⟩\} (0)$
67	60 61 66	3eqtr3d	$⊢ φ \to Q (1) (0) = \{⟨0, P⟩\} (0)$
68		0nn0	$⊢ 0 \in ℕ_{0}$
69		fvsng	$⊢ (0 \in ℕ_{0} \land P \in B) \to \{⟨0, P⟩\} (0) = P$
70	68 6 69	sylancr	$⊢ φ \to \{⟨0, P⟩\} (0) = P$
71	58 67 70	3eqtrd	$⊢ φ \to K (0) = P$

Metamath Proof Explorer

Theorem cvmliftlem13

Proof