Metamath Proof Explorer

Theorem pi1cpbl

Description: The group operation, loop concatenation, is compatible with homotopy equivalence. (Contributed by Mario Carneiro, 10-Jul-2015)

Ref Expression
Hypotheses pi1val.g 
|- G = ( J pi1 Y )
pi1val.1 
|- ( ph -> J e. ( TopOn ` X ) )
pi1val.2 
|- ( ph -> Y e. X )
pi1bas2.b 
|- ( ph -> B = ( Base ` G ) )
pi1bas3.r 
|- R = ( ( ~=ph ` J ) i^i ( U. B X. U. B ) )
pi1cpbl.o 
|- O = ( J Om1 Y )
pi1cpbl.a 
|- .+ = ( +g ` O )
Assertion pi1cpbl 
|- ( ph -> ( ( M R N /\ P R Q ) -> ( M .+ P ) R ( N .+ Q ) ) )

Proof

Step Hyp Ref Expression
1 pi1val.g 
 |-  G = ( J pi1 Y )
2 pi1val.1 
 |-  ( ph -> J e. ( TopOn ` X ) )
3 pi1val.2 
 |-  ( ph -> Y e. X )
4 pi1bas2.b 
 |-  ( ph -> B = ( Base ` G ) )
5 pi1bas3.r 
 |-  R = ( ( ~=ph ` J ) i^i ( U. B X. U. B ) )
6 pi1cpbl.o 
 |-  O = ( J Om1 Y )
7 pi1cpbl.a 
 |-  .+ = ( +g ` O )
8 2 adantr 
 |-  ( ( ph /\ ( M R N /\ P R Q ) ) -> J e. ( TopOn ` X ) )
9 3 adantr 
 |-  ( ( ph /\ ( M R N /\ P R Q ) ) -> Y e. X )
10 4 adantr 
 |-  ( ( ph /\ ( M R N /\ P R Q ) ) -> B = ( Base ` G ) )
11 eqidd 
 |-  ( ( ph /\ ( M R N /\ P R Q ) ) -> ( Base ` O ) = ( Base ` O ) )
12 1 8 9 6 10 11 pi1buni 
 |-  ( ( ph /\ ( M R N /\ P R Q ) ) -> U. B = ( Base ` O ) )
13 simprl 
 |-  ( ( ph /\ ( M R N /\ P R Q ) ) -> M R N )
14 5 breqi 
 |-  ( M R N <-> M ( ( ~=ph ` J ) i^i ( U. B X. U. B ) ) N )
15 brinxp2 
 |-  ( M ( ( ~=ph ` J ) i^i ( U. B X. U. B ) ) N <-> ( ( M e. U. B /\ N e. U. B ) /\ M ( ~=ph ` J ) N ) )
16 14 15 bitri 
 |-  ( M R N <-> ( ( M e. U. B /\ N e. U. B ) /\ M ( ~=ph ` J ) N ) )
17 13 16 sylib 
 |-  ( ( ph /\ ( M R N /\ P R Q ) ) -> ( ( M e. U. B /\ N e. U. B ) /\ M ( ~=ph ` J ) N ) )
18 17 simplld 
 |-  ( ( ph /\ ( M R N /\ P R Q ) ) -> M e. U. B )
19 simprr 
 |-  ( ( ph /\ ( M R N /\ P R Q ) ) -> P R Q )
20 5 breqi 
 |-  ( P R Q <-> P ( ( ~=ph ` J ) i^i ( U. B X. U. B ) ) Q )
21 brinxp2 
 |-  ( P ( ( ~=ph ` J ) i^i ( U. B X. U. B ) ) Q <-> ( ( P e. U. B /\ Q e. U. B ) /\ P ( ~=ph ` J ) Q ) )
22 20 21 bitri 
 |-  ( P R Q <-> ( ( P e. U. B /\ Q e. U. B ) /\ P ( ~=ph ` J ) Q ) )
23 19 22 sylib 
 |-  ( ( ph /\ ( M R N /\ P R Q ) ) -> ( ( P e. U. B /\ Q e. U. B ) /\ P ( ~=ph ` J ) Q ) )
24 23 simplld 
 |-  ( ( ph /\ ( M R N /\ P R Q ) ) -> P e. U. B )
25 6 8 9 12 18 24 om1addcl 
 |-  ( ( ph /\ ( M R N /\ P R Q ) ) -> ( M ( *p ` J ) P ) e. U. B )
26 17 simplrd 
 |-  ( ( ph /\ ( M R N /\ P R Q ) ) -> N e. U. B )
27 23 simplrd 
 |-  ( ( ph /\ ( M R N /\ P R Q ) ) -> Q e. U. B )
28 6 8 9 12 26 27 om1addcl 
 |-  ( ( ph /\ ( M R N /\ P R Q ) ) -> ( N ( *p ` J ) Q ) e. U. B )
29 1 8 9 10 pi1eluni 
 |-  ( ( ph /\ ( M R N /\ P R Q ) ) -> ( M e. U. B <-> ( M e. ( II Cn J ) /\ ( M ` 0 ) = Y /\ ( M ` 1 ) = Y ) ) )
30 18 29 mpbid 
 |-  ( ( ph /\ ( M R N /\ P R Q ) ) -> ( M e. ( II Cn J ) /\ ( M ` 0 ) = Y /\ ( M ` 1 ) = Y ) )
31 30 simp3d 
 |-  ( ( ph /\ ( M R N /\ P R Q ) ) -> ( M ` 1 ) = Y )
32 1 8 9 10 pi1eluni 
 |-  ( ( ph /\ ( M R N /\ P R Q ) ) -> ( P e. U. B <-> ( P e. ( II Cn J ) /\ ( P ` 0 ) = Y /\ ( P ` 1 ) = Y ) ) )
33 24 32 mpbid 
 |-  ( ( ph /\ ( M R N /\ P R Q ) ) -> ( P e. ( II Cn J ) /\ ( P ` 0 ) = Y /\ ( P ` 1 ) = Y ) )
34 33 simp2d 
 |-  ( ( ph /\ ( M R N /\ P R Q ) ) -> ( P ` 0 ) = Y )
35 31 34 eqtr4d 
 |-  ( ( ph /\ ( M R N /\ P R Q ) ) -> ( M ` 1 ) = ( P ` 0 ) )
36 17 simprd 
 |-  ( ( ph /\ ( M R N /\ P R Q ) ) -> M ( ~=ph ` J ) N )
37 23 simprd 
 |-  ( ( ph /\ ( M R N /\ P R Q ) ) -> P ( ~=ph ` J ) Q )
38 35 36 37 pcohtpy 
 |-  ( ( ph /\ ( M R N /\ P R Q ) ) -> ( M ( *p ` J ) P ) ( ~=ph ` J ) ( N ( *p ` J ) Q ) )
39 5 breqi 
 |-  ( ( M ( *p ` J ) P ) R ( N ( *p ` J ) Q ) <-> ( M ( *p ` J ) P ) ( ( ~=ph ` J ) i^i ( U. B X. U. B ) ) ( N ( *p ` J ) Q ) )
40 brinxp2 
 |-  ( ( M ( *p ` J ) P ) ( ( ~=ph ` J ) i^i ( U. B X. U. B ) ) ( N ( *p ` J ) Q ) <-> ( ( ( M ( *p ` J ) P ) e. U. B /\ ( N ( *p ` J ) Q ) e. U. B ) /\ ( M ( *p ` J ) P ) ( ~=ph ` J ) ( N ( *p ` J ) Q ) ) )
41 39 40 bitri 
 |-  ( ( M ( *p ` J ) P ) R ( N ( *p ` J ) Q ) <-> ( ( ( M ( *p ` J ) P ) e. U. B /\ ( N ( *p ` J ) Q ) e. U. B ) /\ ( M ( *p ` J ) P ) ( ~=ph ` J ) ( N ( *p ` J ) Q ) ) )
42 25 28 38 41 syl21anbrc 
 |-  ( ( ph /\ ( M R N /\ P R Q ) ) -> ( M ( *p ` J ) P ) R ( N ( *p ` J ) Q ) )
43 6 8 9 om1plusg 
 |-  ( ( ph /\ ( M R N /\ P R Q ) ) -> ( *p ` J ) = ( +g ` O ) )
44 43 7 eqtr4di 
 |-  ( ( ph /\ ( M R N /\ P R Q ) ) -> ( *p ` J ) = .+ )
45 44 oveqd 
 |-  ( ( ph /\ ( M R N /\ P R Q ) ) -> ( M ( *p ` J ) P ) = ( M .+ P ) )
46 44 oveqd 
 |-  ( ( ph /\ ( M R N /\ P R Q ) ) -> ( N ( *p ` J ) Q ) = ( N .+ Q ) )
47 42 45 46 3brtr3d 
 |-  ( ( ph /\ ( M R N /\ P R Q ) ) -> ( M .+ P ) R ( N .+ Q ) )
48 47 ex 
 |-  ( ph -> ( ( M R N /\ P R Q ) -> ( M .+ P ) R ( N .+ Q ) ) )