# Metamath Proof Explorer

## Theorem cvmlift2lem3

Description: Lemma for cvmlift2 . (Contributed by Mario Carneiro, 7-May-2015)

Ref Expression
Hypotheses cvmlift2.b ${⊢}{B}=\bigcup {C}$
cvmlift2.f ${⊢}{\phi }\to {F}\in \left({C}\mathrm{CovMap}{J}\right)$
cvmlift2.g ${⊢}{\phi }\to {G}\in \left(\left(\mathrm{II}{×}_{t}\mathrm{II}\right)\mathrm{Cn}{J}\right)$
cvmlift2.p ${⊢}{\phi }\to {P}\in {B}$
cvmlift2.i ${⊢}{\phi }\to {F}\left({P}\right)=0{G}0$
cvmlift2.h ${⊢}{H}=\left(\iota {f}\in \left(\mathrm{II}\mathrm{Cn}{C}\right)|\left({F}\circ {f}=\left({z}\in \left[0,1\right]⟼{z}{G}0\right)\wedge {f}\left(0\right)={P}\right)\right)$
cvmlift2lem3.1 ${⊢}{K}=\left(\iota {f}\in \left(\mathrm{II}\mathrm{Cn}{C}\right)|\left({F}\circ {f}=\left({z}\in \left[0,1\right]⟼{X}{G}{z}\right)\wedge {f}\left(0\right)={H}\left({X}\right)\right)\right)$
Assertion cvmlift2lem3 ${⊢}\left({\phi }\wedge {X}\in \left[0,1\right]\right)\to \left({K}\in \left(\mathrm{II}\mathrm{Cn}{C}\right)\wedge {F}\circ {K}=\left({z}\in \left[0,1\right]⟼{X}{G}{z}\right)\wedge {K}\left(0\right)={H}\left({X}\right)\right)$

### Proof

Step Hyp Ref Expression
1 cvmlift2.b ${⊢}{B}=\bigcup {C}$
2 cvmlift2.f ${⊢}{\phi }\to {F}\in \left({C}\mathrm{CovMap}{J}\right)$
3 cvmlift2.g ${⊢}{\phi }\to {G}\in \left(\left(\mathrm{II}{×}_{t}\mathrm{II}\right)\mathrm{Cn}{J}\right)$
4 cvmlift2.p ${⊢}{\phi }\to {P}\in {B}$
5 cvmlift2.i ${⊢}{\phi }\to {F}\left({P}\right)=0{G}0$
6 cvmlift2.h ${⊢}{H}=\left(\iota {f}\in \left(\mathrm{II}\mathrm{Cn}{C}\right)|\left({F}\circ {f}=\left({z}\in \left[0,1\right]⟼{z}{G}0\right)\wedge {f}\left(0\right)={P}\right)\right)$
7 cvmlift2lem3.1 ${⊢}{K}=\left(\iota {f}\in \left(\mathrm{II}\mathrm{Cn}{C}\right)|\left({F}\circ {f}=\left({z}\in \left[0,1\right]⟼{X}{G}{z}\right)\wedge {f}\left(0\right)={H}\left({X}\right)\right)\right)$
8 2 adantr ${⊢}\left({\phi }\wedge {X}\in \left[0,1\right]\right)\to {F}\in \left({C}\mathrm{CovMap}{J}\right)$
9 iitopon ${⊢}\mathrm{II}\in \mathrm{TopOn}\left(\left[0,1\right]\right)$
10 9 a1i ${⊢}\left({\phi }\wedge {X}\in \left[0,1\right]\right)\to \mathrm{II}\in \mathrm{TopOn}\left(\left[0,1\right]\right)$
11 simpr ${⊢}\left({\phi }\wedge {X}\in \left[0,1\right]\right)\to {X}\in \left[0,1\right]$
12 10 10 11 cnmptc ${⊢}\left({\phi }\wedge {X}\in \left[0,1\right]\right)\to \left({z}\in \left[0,1\right]⟼{X}\right)\in \left(\mathrm{II}\mathrm{Cn}\mathrm{II}\right)$
13 10 cnmptid ${⊢}\left({\phi }\wedge {X}\in \left[0,1\right]\right)\to \left({z}\in \left[0,1\right]⟼{z}\right)\in \left(\mathrm{II}\mathrm{Cn}\mathrm{II}\right)$
14 3 adantr ${⊢}\left({\phi }\wedge {X}\in \left[0,1\right]\right)\to {G}\in \left(\left(\mathrm{II}{×}_{t}\mathrm{II}\right)\mathrm{Cn}{J}\right)$
15 10 12 13 14 cnmpt12f ${⊢}\left({\phi }\wedge {X}\in \left[0,1\right]\right)\to \left({z}\in \left[0,1\right]⟼{X}{G}{z}\right)\in \left(\mathrm{II}\mathrm{Cn}{J}\right)$
16 1 2 3 4 5 6 cvmlift2lem2 ${⊢}{\phi }\to \left({H}\in \left(\mathrm{II}\mathrm{Cn}{C}\right)\wedge {F}\circ {H}=\left({z}\in \left[0,1\right]⟼{z}{G}0\right)\wedge {H}\left(0\right)={P}\right)$
17 16 simp1d ${⊢}{\phi }\to {H}\in \left(\mathrm{II}\mathrm{Cn}{C}\right)$
18 iiuni ${⊢}\left[0,1\right]=\bigcup \mathrm{II}$
19 18 1 cnf ${⊢}{H}\in \left(\mathrm{II}\mathrm{Cn}{C}\right)\to {H}:\left[0,1\right]⟶{B}$
20 17 19 syl ${⊢}{\phi }\to {H}:\left[0,1\right]⟶{B}$
21 20 ffvelrnda ${⊢}\left({\phi }\wedge {X}\in \left[0,1\right]\right)\to {H}\left({X}\right)\in {B}$
22 0elunit ${⊢}0\in \left[0,1\right]$
23 oveq2 ${⊢}{z}=0\to {X}{G}{z}={X}{G}0$
24 eqid ${⊢}\left({z}\in \left[0,1\right]⟼{X}{G}{z}\right)=\left({z}\in \left[0,1\right]⟼{X}{G}{z}\right)$
25 ovex ${⊢}{X}{G}0\in \mathrm{V}$
26 23 24 25 fvmpt ${⊢}0\in \left[0,1\right]\to \left({z}\in \left[0,1\right]⟼{X}{G}{z}\right)\left(0\right)={X}{G}0$
27 22 26 mp1i ${⊢}\left({\phi }\wedge {X}\in \left[0,1\right]\right)\to \left({z}\in \left[0,1\right]⟼{X}{G}{z}\right)\left(0\right)={X}{G}0$
28 16 simp2d ${⊢}{\phi }\to {F}\circ {H}=\left({z}\in \left[0,1\right]⟼{z}{G}0\right)$
29 28 fveq1d ${⊢}{\phi }\to \left({F}\circ {H}\right)\left({X}\right)=\left({z}\in \left[0,1\right]⟼{z}{G}0\right)\left({X}\right)$
30 oveq1 ${⊢}{z}={X}\to {z}{G}0={X}{G}0$
31 eqid ${⊢}\left({z}\in \left[0,1\right]⟼{z}{G}0\right)=\left({z}\in \left[0,1\right]⟼{z}{G}0\right)$
32 30 31 25 fvmpt ${⊢}{X}\in \left[0,1\right]\to \left({z}\in \left[0,1\right]⟼{z}{G}0\right)\left({X}\right)={X}{G}0$
33 29 32 sylan9eq ${⊢}\left({\phi }\wedge {X}\in \left[0,1\right]\right)\to \left({F}\circ {H}\right)\left({X}\right)={X}{G}0$
34 fvco3 ${⊢}\left({H}:\left[0,1\right]⟶{B}\wedge {X}\in \left[0,1\right]\right)\to \left({F}\circ {H}\right)\left({X}\right)={F}\left({H}\left({X}\right)\right)$
35 20 34 sylan ${⊢}\left({\phi }\wedge {X}\in \left[0,1\right]\right)\to \left({F}\circ {H}\right)\left({X}\right)={F}\left({H}\left({X}\right)\right)$
36 27 33 35 3eqtr2rd ${⊢}\left({\phi }\wedge {X}\in \left[0,1\right]\right)\to {F}\left({H}\left({X}\right)\right)=\left({z}\in \left[0,1\right]⟼{X}{G}{z}\right)\left(0\right)$
37 1 7 8 15 21 36 cvmliftiota ${⊢}\left({\phi }\wedge {X}\in \left[0,1\right]\right)\to \left({K}\in \left(\mathrm{II}\mathrm{Cn}{C}\right)\wedge {F}\circ {K}=\left({z}\in \left[0,1\right]⟼{X}{G}{z}\right)\wedge {K}\left(0\right)={H}\left({X}\right)\right)$