cvmliftlem5

Description: Lemma for cvmlift . Definition of Q at a successor. This is a function defined on W as ` ``' ( T |`I ) o. G where I is the unique covering set of 2nd( TM ) that contains Q ( M - 1 ) evaluated at the last defined point, namely ( M - 1 ) / N (note that for M = 1 this is using the seed value Q ( 0 ) ( 0 ) = P ). (Contributed by Mario Carneiro, 15-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⟩\}⟩\}))$
	cvmliftlem5.3	$⊢ W = [\frac{M - 1}{N}, \frac{M}{N}]$
Assertion	cvmliftlem5	$⊢ (φ \land M \in ℕ) \to Q (M) = (z \in W ⟼ {({F ↾}_{(ι b \in 2^{nd} (T (M)) \| Q (M - 1) (\frac{M - 1}{N}) \in b)})}^{-1} (G (z)))$

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		cvmliftlem5.3	$⊢ W = [\frac{M - 1}{N}, \frac{M}{N}]$
14		0z	$⊢ 0 \in ℤ$
15		simpr	$⊢ (φ \land M \in ℕ) \to M \in ℕ$
16		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
17		1e0p1	$⊢ 1 = 0 + 1$
18	17	fveq2i	$⊢ ℤ_{\geq 1} = ℤ_{\geq (0 + 1)}$
19	16 18	eqtri	$⊢ ℕ = ℤ_{\geq (0 + 1)}$
20	15 19	eleqtrdi	$⊢ (φ \land M \in ℕ) \to M \in ℤ_{\geq (0 + 1)}$
21		seqm1	$⊢ (0 \in ℤ \land M \in ℤ_{\geq (0 + 1)}) \to 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⟩\}⟩\})) (M) = 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⟩\}⟩\})) (M - 1) (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⟩\}⟩\}) (M)$
22	14 20 21	sylancr	$⊢ (φ \land M \in ℕ) \to 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⟩\}⟩\})) (M) = 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⟩\}⟩\})) (M - 1) (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⟩\}⟩\}) (M)$
23	12	fveq1i	$⊢ Q (M) = 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⟩\}⟩\})) (M)$
24	12	fveq1i	$⊢ Q (M - 1) = 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⟩\}⟩\})) (M - 1)$
25	24	oveq1i	$⊢ Q (M - 1) (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⟩\}⟩\}) (M) = 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⟩\}⟩\})) (M - 1) (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⟩\}⟩\}) (M)$
26	22 23 25	3eqtr4g	$⊢ (φ \land M \in ℕ) \to Q (M) = Q (M - 1) (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⟩\}⟩\}) (M)$
27		0nnn	$⊢ \neg 0 \in ℕ$
28		disjsn	$⊢ ℕ \cap \{0\} = \emptyset \leftrightarrow \neg 0 \in ℕ$
29	27 28	mpbir	$⊢ ℕ \cap \{0\} = \emptyset$
30		fnresi	$⊢ ({I ↾}_{ℕ}) Fn ℕ$
31		c0ex	$⊢ 0 \in V$
32		snex	$⊢ \{⟨0, P⟩\} \in V$
33	31 32	fnsn	$⊢ \{⟨0, \{⟨0, P⟩\}⟩\} Fn \{0\}$
34		fvun1	$⊢ (({I ↾}_{ℕ}) Fn ℕ \land \{⟨0, \{⟨0, P⟩\}⟩\} Fn \{0\} \land (ℕ \cap \{0\} = \emptyset \land M \in ℕ)) \to (({I ↾}_{ℕ}) \cup \{⟨0, \{⟨0, P⟩\}⟩\}) (M) = ({I ↾}_{ℕ}) (M)$
35	30 33 34	mp3an12	$⊢ (ℕ \cap \{0\} = \emptyset \land M \in ℕ) \to (({I ↾}_{ℕ}) \cup \{⟨0, \{⟨0, P⟩\}⟩\}) (M) = ({I ↾}_{ℕ}) (M)$
36	29 15 35	sylancr	$⊢ (φ \land M \in ℕ) \to (({I ↾}_{ℕ}) \cup \{⟨0, \{⟨0, P⟩\}⟩\}) (M) = ({I ↾}_{ℕ}) (M)$
37		fvresi	$⊢ M \in ℕ \to ({I ↾}_{ℕ}) (M) = M$
38	37	adantl	$⊢ (φ \land M \in ℕ) \to ({I ↾}_{ℕ}) (M) = M$
39	36 38	eqtrd	$⊢ (φ \land M \in ℕ) \to (({I ↾}_{ℕ}) \cup \{⟨0, \{⟨0, P⟩\}⟩\}) (M) = M$
40	39	oveq2d	$⊢ (φ \land M \in ℕ) \to Q (M - 1) (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⟩\}⟩\}) (M) = Q (M - 1) (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)))) M$
41		fvexd	$⊢ φ \to Q (M - 1) \in V$
42		simpr	$⊢ (x = Q (M - 1) \land m = M) \to m = M$
43	42	oveq1d	$⊢ (x = Q (M - 1) \land m = M) \to m - 1 = M - 1$
44	43	oveq1d	$⊢ (x = Q (M - 1) \land m = M) \to \frac{m - 1}{N} = \frac{M - 1}{N}$
45	42	oveq1d	$⊢ (x = Q (M - 1) \land m = M) \to \frac{m}{N} = \frac{M}{N}$
46	44 45	oveq12d	$⊢ (x = Q (M - 1) \land m = M) \to [\frac{m - 1}{N}, \frac{m}{N}] = [\frac{M - 1}{N}, \frac{M}{N}]$
47	46 13	eqtr4di	$⊢ (x = Q (M - 1) \land m = M) \to [\frac{m - 1}{N}, \frac{m}{N}] = W$
48	42	fveq2d	$⊢ (x = Q (M - 1) \land m = M) \to T (m) = T (M)$
49	48	fveq2d	$⊢ (x = Q (M - 1) \land m = M) \to 2^{nd} (T (m)) = 2^{nd} (T (M))$
50		simpl	$⊢ (x = Q (M - 1) \land m = M) \to x = Q (M - 1)$
51	50 44	fveq12d	$⊢ (x = Q (M - 1) \land m = M) \to x (\frac{m - 1}{N}) = Q (M - 1) (\frac{M - 1}{N})$
52	51	eleq1d	$⊢ (x = Q (M - 1) \land m = M) \to (x (\frac{m - 1}{N}) \in b \leftrightarrow Q (M - 1) (\frac{M - 1}{N}) \in b)$
53	49 52	riotaeqbidv	$⊢ (x = Q (M - 1) \land m = M) \to (ι b \in 2^{nd} (T (m)) \| x (\frac{m - 1}{N}) \in b) = (ι b \in 2^{nd} (T (M)) \| Q (M - 1) (\frac{M - 1}{N}) \in b)$
54	53	reseq2d	$⊢ (x = Q (M - 1) \land m = M) \to {F ↾}_{(ι b \in 2^{nd} (T (m)) \| x (\frac{m - 1}{N}) \in b)} = {F ↾}_{(ι b \in 2^{nd} (T (M)) \| Q (M - 1) (\frac{M - 1}{N}) \in b)}$
55	54	cnveqd	$⊢ (x = Q (M - 1) \land m = M) \to {({F ↾}_{(ι b \in 2^{nd} (T (m)) \| x (\frac{m - 1}{N}) \in b)})}^{-1} = {({F ↾}_{(ι b \in 2^{nd} (T (M)) \| Q (M - 1) (\frac{M - 1}{N}) \in b)})}^{-1}$
56	55	fveq1d	$⊢ (x = Q (M - 1) \land m = M) \to {({F ↾}_{(ι b \in 2^{nd} (T (m)) \| x (\frac{m - 1}{N}) \in b)})}^{-1} (G (z)) = {({F ↾}_{(ι b \in 2^{nd} (T (M)) \| Q (M - 1) (\frac{M - 1}{N}) \in b)})}^{-1} (G (z))$
57	47 56	mpteq12dv	$⊢ (x = Q (M - 1) \land m = M) \to (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))) = (z \in W ⟼ {({F ↾}_{(ι b \in 2^{nd} (T (M)) \| Q (M - 1) (\frac{M - 1}{N}) \in b)})}^{-1} (G (z)))$
58		eqid	$⊢ (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)))) = (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))))$
59		ovex	$⊢ [\frac{M - 1}{N}, \frac{M}{N}] \in V$
60	13 59	eqeltri	$⊢ W \in V$
61	60	mptex	$⊢ (z \in W ⟼ {({F ↾}_{(ι b \in 2^{nd} (T (M)) \| Q (M - 1) (\frac{M - 1}{N}) \in b)})}^{-1} (G (z))) \in V$
62	57 58 61	ovmpoa	$⊢ (Q (M - 1) \in V \land M \in ℕ) \to Q (M - 1) (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)))) M = (z \in W ⟼ {({F ↾}_{(ι b \in 2^{nd} (T (M)) \| Q (M - 1) (\frac{M - 1}{N}) \in b)})}^{-1} (G (z)))$
63	41 62	sylan	$⊢ (φ \land M \in ℕ) \to Q (M - 1) (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)))) M = (z \in W ⟼ {({F ↾}_{(ι b \in 2^{nd} (T (M)) \| Q (M - 1) (\frac{M - 1}{N}) \in b)})}^{-1} (G (z)))$
64	26 40 63	3eqtrd	$⊢ (φ \land M \in ℕ) \to Q (M) = (z \in W ⟼ {({F ↾}_{(ι b \in 2^{nd} (T (M)) \| Q (M - 1) (\frac{M - 1}{N}) \in b)})}^{-1} (G (z)))$

Metamath Proof Explorer

Theorem cvmliftlem5

Proof