Metamath Proof Explorer

Theorem cvmliftpht

Description: If G and H are path-homotopic, then their lifts M and N are also path-homotopic. (Contributed by Mario Carneiro, 6-Jul-2015)

Ref Expression
Hypotheses cvmliftpht.b 
|- B = U. C
cvmliftpht.m 
|- M = ( iota_ f e. ( II Cn C ) ( ( F o. f ) = G /\ ( f ` 0 ) = P ) )
cvmliftpht.n 
|- N = ( iota_ f e. ( II Cn C ) ( ( F o. f ) = H /\ ( f ` 0 ) = P ) )
cvmliftpht.f 
|- ( ph -> F e. ( C CovMap J ) )
cvmliftpht.p 
|- ( ph -> P e. B )
cvmliftpht.e 
|- ( ph -> ( F ` P ) = ( G ` 0 ) )
cvmliftpht.g 
|- ( ph -> G ( ~=ph ` J ) H )
Assertion cvmliftpht 
|- ( ph -> M ( ~=ph ` C ) N )

Proof

Step Hyp Ref Expression
1 cvmliftpht.b 
 |-  B = U. C
2 cvmliftpht.m 
 |-  M = ( iota_ f e. ( II Cn C ) ( ( F o. f ) = G /\ ( f ` 0 ) = P ) )
3 cvmliftpht.n 
 |-  N = ( iota_ f e. ( II Cn C ) ( ( F o. f ) = H /\ ( f ` 0 ) = P ) )
4 cvmliftpht.f 
 |-  ( ph -> F e. ( C CovMap J ) )
5 cvmliftpht.p 
 |-  ( ph -> P e. B )
6 cvmliftpht.e 
 |-  ( ph -> ( F ` P ) = ( G ` 0 ) )
7 cvmliftpht.g 
 |-  ( ph -> G ( ~=ph ` J ) H )
8 isphtpc 
 |-  ( G ( ~=ph ` J ) H <-> ( G e. ( II Cn J ) /\ H e. ( II Cn J ) /\ ( G ( PHtpy ` J ) H ) =/= (/) ) )
9 7 8 sylib 
 |-  ( ph -> ( G e. ( II Cn J ) /\ H e. ( II Cn J ) /\ ( G ( PHtpy ` J ) H ) =/= (/) ) )
10 9 simp1d 
 |-  ( ph -> G e. ( II Cn J ) )
11 1 2 4 10 5 6 cvmliftiota 
 |-  ( ph -> ( M e. ( II Cn C ) /\ ( F o. M ) = G /\ ( M ` 0 ) = P ) )
12 11 simp1d 
 |-  ( ph -> M e. ( II Cn C ) )
13 9 simp2d 
 |-  ( ph -> H e. ( II Cn J ) )
14 phtpc01 
 |-  ( G ( ~=ph ` J ) H -> ( ( G ` 0 ) = ( H ` 0 ) /\ ( G ` 1 ) = ( H ` 1 ) ) )
15 7 14 syl 
 |-  ( ph -> ( ( G ` 0 ) = ( H ` 0 ) /\ ( G ` 1 ) = ( H ` 1 ) ) )
16 15 simpld 
 |-  ( ph -> ( G ` 0 ) = ( H ` 0 ) )
17 6 16 eqtrd 
 |-  ( ph -> ( F ` P ) = ( H ` 0 ) )
18 1 3 4 13 5 17 cvmliftiota 
 |-  ( ph -> ( N e. ( II Cn C ) /\ ( F o. N ) = H /\ ( N ` 0 ) = P ) )
19 18 simp1d 
 |-  ( ph -> N e. ( II Cn C ) )
20 9 simp3d 
 |-  ( ph -> ( G ( PHtpy ` J ) H ) =/= (/) )
21 n0 
 |-  ( ( G ( PHtpy ` J ) H ) =/= (/) <-> E. g g e. ( G ( PHtpy ` J ) H ) )
22 20 21 sylib 
 |-  ( ph -> E. g g e. ( G ( PHtpy ` J ) H ) )
23 4 adantr 
 |-  ( ( ph /\ g e. ( G ( PHtpy ` J ) H ) ) -> F e. ( C CovMap J ) )
24 10 13 phtpycn 
 |-  ( ph -> ( G ( PHtpy ` J ) H ) C_ ( ( II tX II ) Cn J ) )
25 24 sselda 
 |-  ( ( ph /\ g e. ( G ( PHtpy ` J ) H ) ) -> g e. ( ( II tX II ) Cn J ) )
26 5 adantr 
 |-  ( ( ph /\ g e. ( G ( PHtpy ` J ) H ) ) -> P e. B )
27 6 adantr 
 |-  ( ( ph /\ g e. ( G ( PHtpy ` J ) H ) ) -> ( F ` P ) = ( G ` 0 ) )
28 0elunit 
 |-  0 e. ( 0 [,] 1 )
29 10 adantr 
 |-  ( ( ph /\ g e. ( G ( PHtpy ` J ) H ) ) -> G e. ( II Cn J ) )
30 13 adantr 
 |-  ( ( ph /\ g e. ( G ( PHtpy ` J ) H ) ) -> H e. ( II Cn J ) )
31 simpr 
 |-  ( ( ph /\ g e. ( G ( PHtpy ` J ) H ) ) -> g e. ( G ( PHtpy ` J ) H ) )
32 29 30 31 phtpyi 
 |-  ( ( ( ph /\ g e. ( G ( PHtpy ` J ) H ) ) /\ 0 e. ( 0 [,] 1 ) ) -> ( ( 0 g 0 ) = ( G ` 0 ) /\ ( 1 g 0 ) = ( G ` 1 ) ) )
33 28 32 mpan2 
 |-  ( ( ph /\ g e. ( G ( PHtpy ` J ) H ) ) -> ( ( 0 g 0 ) = ( G ` 0 ) /\ ( 1 g 0 ) = ( G ` 1 ) ) )
34 33 simpld 
 |-  ( ( ph /\ g e. ( G ( PHtpy ` J ) H ) ) -> ( 0 g 0 ) = ( G ` 0 ) )
35 27 34 eqtr4d 
 |-  ( ( ph /\ g e. ( G ( PHtpy ` J ) H ) ) -> ( F ` P ) = ( 0 g 0 ) )
36 1 23 25 26 35 cvmlift2 
 |-  ( ( ph /\ g e. ( G ( PHtpy ` J ) H ) ) -> E! h e. ( ( II tX II ) Cn C ) ( ( F o. h ) = g /\ ( 0 h 0 ) = P ) )
37 reurex 
 |-  ( E! h e. ( ( II tX II ) Cn C ) ( ( F o. h ) = g /\ ( 0 h 0 ) = P ) -> E. h e. ( ( II tX II ) Cn C ) ( ( F o. h ) = g /\ ( 0 h 0 ) = P ) )
38 36 37 syl 
 |-  ( ( ph /\ g e. ( G ( PHtpy ` J ) H ) ) -> E. h e. ( ( II tX II ) Cn C ) ( ( F o. h ) = g /\ ( 0 h 0 ) = P ) )
39 4 ad2antrr 
 |-  ( ( ( ph /\ g e. ( G ( PHtpy ` J ) H ) ) /\ ( h e. ( ( II tX II ) Cn C ) /\ ( ( F o. h ) = g /\ ( 0 h 0 ) = P ) ) ) -> F e. ( C CovMap J ) )
40 5 ad2antrr 
 |-  ( ( ( ph /\ g e. ( G ( PHtpy ` J ) H ) ) /\ ( h e. ( ( II tX II ) Cn C ) /\ ( ( F o. h ) = g /\ ( 0 h 0 ) = P ) ) ) -> P e. B )
41 6 ad2antrr 
 |-  ( ( ( ph /\ g e. ( G ( PHtpy ` J ) H ) ) /\ ( h e. ( ( II tX II ) Cn C ) /\ ( ( F o. h ) = g /\ ( 0 h 0 ) = P ) ) ) -> ( F ` P ) = ( G ` 0 ) )
42 10 ad2antrr 
 |-  ( ( ( ph /\ g e. ( G ( PHtpy ` J ) H ) ) /\ ( h e. ( ( II tX II ) Cn C ) /\ ( ( F o. h ) = g /\ ( 0 h 0 ) = P ) ) ) -> G e. ( II Cn J ) )
43 13 ad2antrr 
 |-  ( ( ( ph /\ g e. ( G ( PHtpy ` J ) H ) ) /\ ( h e. ( ( II tX II ) Cn C ) /\ ( ( F o. h ) = g /\ ( 0 h 0 ) = P ) ) ) -> H e. ( II Cn J ) )
44 simplr 
 |-  ( ( ( ph /\ g e. ( G ( PHtpy ` J ) H ) ) /\ ( h e. ( ( II tX II ) Cn C ) /\ ( ( F o. h ) = g /\ ( 0 h 0 ) = P ) ) ) -> g e. ( G ( PHtpy ` J ) H ) )
45 simprl 
 |-  ( ( ( ph /\ g e. ( G ( PHtpy ` J ) H ) ) /\ ( h e. ( ( II tX II ) Cn C ) /\ ( ( F o. h ) = g /\ ( 0 h 0 ) = P ) ) ) -> h e. ( ( II tX II ) Cn C ) )
46 simprrl 
 |-  ( ( ( ph /\ g e. ( G ( PHtpy ` J ) H ) ) /\ ( h e. ( ( II tX II ) Cn C ) /\ ( ( F o. h ) = g /\ ( 0 h 0 ) = P ) ) ) -> ( F o. h ) = g )
47 simprrr 
 |-  ( ( ( ph /\ g e. ( G ( PHtpy ` J ) H ) ) /\ ( h e. ( ( II tX II ) Cn C ) /\ ( ( F o. h ) = g /\ ( 0 h 0 ) = P ) ) ) -> ( 0 h 0 ) = P )
48 1 2 3 39 40 41 42 43 44 45 46 47 cvmliftphtlem 
 |-  ( ( ( ph /\ g e. ( G ( PHtpy ` J ) H ) ) /\ ( h e. ( ( II tX II ) Cn C ) /\ ( ( F o. h ) = g /\ ( 0 h 0 ) = P ) ) ) -> h e. ( M ( PHtpy ` C ) N ) )
49 48 ne0d 
 |-  ( ( ( ph /\ g e. ( G ( PHtpy ` J ) H ) ) /\ ( h e. ( ( II tX II ) Cn C ) /\ ( ( F o. h ) = g /\ ( 0 h 0 ) = P ) ) ) -> ( M ( PHtpy ` C ) N ) =/= (/) )
50 38 49 rexlimddv 
 |-  ( ( ph /\ g e. ( G ( PHtpy ` J ) H ) ) -> ( M ( PHtpy ` C ) N ) =/= (/) )
51 22 50 exlimddv 
 |-  ( ph -> ( M ( PHtpy ` C ) N ) =/= (/) )
52 isphtpc 
 |-  ( M ( ~=ph ` C ) N <-> ( M e. ( II Cn C ) /\ N e. ( II Cn C ) /\ ( M ( PHtpy ` C ) N ) =/= (/) ) )
53 12 19 51 52 syl3anbrc 
 |-  ( ph -> M ( ~=ph ` C ) N )