cvmliftlem11

	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	cvmliftlem11	$⊢ φ \to (K \in (II Cn C) \land F \circ K = G)$

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		biid	$⊢ ((n \in ℕ \land n + 1 \in (1 \dots N)) \land (⋃_{k = 1}^{n} Q (k) \in ((L ↾_{𝑡} [0, \frac{n}{N}]) Cn C) \land F \circ ⋃_{k = 1}^{n} Q (k) = {G ↾}_{[0, \frac{n}{N}]})) \leftrightarrow ((n \in ℕ \land n + 1 \in (1 \dots N)) \land (⋃_{k = 1}^{n} Q (k) \in ((L ↾_{𝑡} [0, \frac{n}{N}]) Cn C) \land F \circ ⋃_{k = 1}^{n} Q (k) = {G ↾}_{[0, \frac{n}{N}]}))$
15	1 2 3 4 5 6 7 8 9 10 11 12 13 14	cvmliftlem10	$⊢ φ \to (K \in ((L ↾_{𝑡} [0, \frac{N}{N}]) Cn C) \land F \circ K = {G ↾}_{[0, \frac{N}{N}]})$
16	15	simpld	$⊢ φ \to K \in ((L ↾_{𝑡} [0, \frac{N}{N}]) Cn C)$
17	11	a1i	$⊢ φ \to L = topGen (ran (.))$
18	8	nncnd	$⊢ φ \to N \in ℂ$
19	8	nnne0d	$⊢ φ \to N \neq 0$
20	18 19	dividd	$⊢ φ \to \frac{N}{N} = 1$
21	20	oveq2d	$⊢ φ \to [0, \frac{N}{N}] = [0, 1]$
22	17 21	oveq12d	$⊢ φ \to L ↾_{𝑡} [0, \frac{N}{N}] = topGen (ran (.)) ↾_{𝑡} [0, 1]$
23		dfii2	$⊢ II = topGen (ran (.)) ↾_{𝑡} [0, 1]$
24	22 23	eqtr4di	$⊢ φ \to L ↾_{𝑡} [0, \frac{N}{N}] = II$
25	24	oveq1d	$⊢ φ \to (L ↾_{𝑡} [0, \frac{N}{N}]) Cn C = II Cn C$
26	16 25	eleqtrd	$⊢ φ \to K \in (II Cn C)$
27	15	simprd	$⊢ φ \to F \circ K = {G ↾}_{[0, \frac{N}{N}]}$
28	21	reseq2d	$⊢ φ \to {G ↾}_{[0, \frac{N}{N}]} = {G ↾}_{[0, 1]}$
29		iiuni	$⊢ [0, 1] = ⋃ II$
30	29 3	cnf	$⊢ G \in (II Cn J) \to G : [0, 1] ⟶ X$
31		ffn	$⊢ G : [0, 1] ⟶ X \to G Fn [0, 1]$
32		fnresdm	$⊢ G Fn [0, 1] \to {G ↾}_{[0, 1]} = G$
33	5 30 31 32	4syl	$⊢ φ \to {G ↾}_{[0, 1]} = G$
34	27 28 33	3eqtrd	$⊢ φ \to F \circ K = G$
35	26 34	jca	$⊢ φ \to (K \in (II Cn C) \land F \circ K = G)$

Metamath Proof Explorer

Theorem cvmliftlem11

Proof