Metamath Proof Explorer

Theorem pi1addval

Description: The concatenation of two path-homotopy classes in the fundamental group. (Contributed by Jeff Madsen, 11-Jun-2010) (Revised by Mario Carneiro, 10-Jul-2015)

Ref Expression
Hypotheses elpi1.g 
|- G = ( J pi1 Y )
elpi1.b 
|- B = ( Base ` G )
elpi1.1 
|- ( ph -> J e. ( TopOn ` X ) )
elpi1.2 
|- ( ph -> Y e. X )
pi1addf.p 
|- .+ = ( +g ` G )
pi1addval.3 
|- ( ph -> M e. U. B )
pi1addval.4 
|- ( ph -> N e. U. B )
Assertion pi1addval 
|- ( ph -> ( [ M ] ( ~=ph ` J ) .+ [ N ] ( ~=ph ` J ) ) = [ ( M ( *p ` J ) N ) ] ( ~=ph ` J ) )

Proof

Step Hyp Ref Expression
1 elpi1.g 
 |-  G = ( J pi1 Y )
2 elpi1.b 
 |-  B = ( Base ` G )
3 elpi1.1 
 |-  ( ph -> J e. ( TopOn ` X ) )
4 elpi1.2 
 |-  ( ph -> Y e. X )
5 pi1addf.p 
 |-  .+ = ( +g ` G )
6 pi1addval.3 
 |-  ( ph -> M e. U. B )
7 pi1addval.4 
 |-  ( ph -> N e. U. B )
8 eqidd 
 |-  ( ph -> ( ( J Om1 Y ) /s ( ~=ph ` J ) ) = ( ( J Om1 Y ) /s ( ~=ph ` J ) ) )
9 eqidd 
 |-  ( ph -> ( Base ` ( J Om1 Y ) ) = ( Base ` ( J Om1 Y ) ) )
10 fvexd 
 |-  ( ph -> ( ~=ph ` J ) e. _V )
11 ovexd 
 |-  ( ph -> ( J Om1 Y ) e. _V )
12 eqid 
 |-  ( J Om1 Y ) = ( J Om1 Y )
13 2 a1i 
 |-  ( ph -> B = ( Base ` G ) )
14 1 3 4 12 13 9 pi1blem 
 |-  ( ph -> ( ( ( ~=ph ` J ) " ( Base ` ( J Om1 Y ) ) ) C_ ( Base ` ( J Om1 Y ) ) /\ ( Base ` ( J Om1 Y ) ) C_ ( II Cn J ) ) )
15 14 simpld 
 |-  ( ph -> ( ( ~=ph ` J ) " ( Base ` ( J Om1 Y ) ) ) C_ ( Base ` ( J Om1 Y ) ) )
16 8 9 10 11 15 qusin 
 |-  ( ph -> ( ( J Om1 Y ) /s ( ~=ph ` J ) ) = ( ( J Om1 Y ) /s ( ( ~=ph ` J ) i^i ( ( Base ` ( J Om1 Y ) ) X. ( Base ` ( J Om1 Y ) ) ) ) ) )
17 1 3 4 12 pi1val 
 |-  ( ph -> G = ( ( J Om1 Y ) /s ( ~=ph ` J ) ) )
18 1 3 4 12 13 9 pi1buni 
 |-  ( ph -> U. B = ( Base ` ( J Om1 Y ) ) )
19 18 sqxpeqd 
 |-  ( ph -> ( U. B X. U. B ) = ( ( Base ` ( J Om1 Y ) ) X. ( Base ` ( J Om1 Y ) ) ) )
20 19 ineq2d 
 |-  ( ph -> ( ( ~=ph ` J ) i^i ( U. B X. U. B ) ) = ( ( ~=ph ` J ) i^i ( ( Base ` ( J Om1 Y ) ) X. ( Base ` ( J Om1 Y ) ) ) ) )
21 20 oveq2d 
 |-  ( ph -> ( ( J Om1 Y ) /s ( ( ~=ph ` J ) i^i ( U. B X. U. B ) ) ) = ( ( J Om1 Y ) /s ( ( ~=ph ` J ) i^i ( ( Base ` ( J Om1 Y ) ) X. ( Base ` ( J Om1 Y ) ) ) ) ) )
22 16 17 21 3eqtr4d 
 |-  ( ph -> G = ( ( J Om1 Y ) /s ( ( ~=ph ` J ) i^i ( U. B X. U. B ) ) ) )
23 phtpcer 
 |-  ( ~=ph ` J ) Er ( II Cn J )
24 23 a1i 
 |-  ( ph -> ( ~=ph ` J ) Er ( II Cn J ) )
25 14 simprd 
 |-  ( ph -> ( Base ` ( J Om1 Y ) ) C_ ( II Cn J ) )
26 18 25 eqsstrd 
 |-  ( ph -> U. B C_ ( II Cn J ) )
27 24 26 erinxp 
 |-  ( ph -> ( ( ~=ph ` J ) i^i ( U. B X. U. B ) ) Er U. B )
28 eqid 
 |-  ( ( ~=ph ` J ) i^i ( U. B X. U. B ) ) = ( ( ~=ph ` J ) i^i ( U. B X. U. B ) )
29 eqid 
 |-  ( +g ` ( J Om1 Y ) ) = ( +g ` ( J Om1 Y ) )
30 1 3 4 13 28 12 29 pi1cpbl 
 |-  ( ph -> ( ( a ( ( ~=ph ` J ) i^i ( U. B X. U. B ) ) c /\ b ( ( ~=ph ` J ) i^i ( U. B X. U. B ) ) d ) -> ( a ( +g ` ( J Om1 Y ) ) b ) ( ( ~=ph ` J ) i^i ( U. B X. U. B ) ) ( c ( +g ` ( J Om1 Y ) ) d ) ) )
31 12 3 4 om1plusg 
 |-  ( ph -> ( *p ` J ) = ( +g ` ( J Om1 Y ) ) )
32 31 oveqdr 
 |-  ( ( ph /\ ( c e. U. B /\ d e. U. B ) ) -> ( c ( *p ` J ) d ) = ( c ( +g ` ( J Om1 Y ) ) d ) )
33 3 adantr 
 |-  ( ( ph /\ ( c e. U. B /\ d e. U. B ) ) -> J e. ( TopOn ` X ) )
34 4 adantr 
 |-  ( ( ph /\ ( c e. U. B /\ d e. U. B ) ) -> Y e. X )
35 18 adantr 
 |-  ( ( ph /\ ( c e. U. B /\ d e. U. B ) ) -> U. B = ( Base ` ( J Om1 Y ) ) )
36 simprl 
 |-  ( ( ph /\ ( c e. U. B /\ d e. U. B ) ) -> c e. U. B )
37 simprr 
 |-  ( ( ph /\ ( c e. U. B /\ d e. U. B ) ) -> d e. U. B )
38 12 33 34 35 36 37 om1addcl 
 |-  ( ( ph /\ ( c e. U. B /\ d e. U. B ) ) -> ( c ( *p ` J ) d ) e. U. B )
39 32 38 eqeltrrd 
 |-  ( ( ph /\ ( c e. U. B /\ d e. U. B ) ) -> ( c ( +g ` ( J Om1 Y ) ) d ) e. U. B )
40 22 18 27 11 30 39 29 5 qusaddval 
 |-  ( ( ph /\ M e. U. B /\ N e. U. B ) -> ( [ M ] ( ( ~=ph ` J ) i^i ( U. B X. U. B ) ) .+ [ N ] ( ( ~=ph ` J ) i^i ( U. B X. U. B ) ) ) = [ ( M ( +g ` ( J Om1 Y ) ) N ) ] ( ( ~=ph ` J ) i^i ( U. B X. U. B ) ) )
41 6 7 40 mpd3an23 
 |-  ( ph -> ( [ M ] ( ( ~=ph ` J ) i^i ( U. B X. U. B ) ) .+ [ N ] ( ( ~=ph ` J ) i^i ( U. B X. U. B ) ) ) = [ ( M ( +g ` ( J Om1 Y ) ) N ) ] ( ( ~=ph ` J ) i^i ( U. B X. U. B ) ) )
42 18 imaeq2d 
 |-  ( ph -> ( ( ~=ph ` J ) " U. B ) = ( ( ~=ph ` J ) " ( Base ` ( J Om1 Y ) ) ) )
43 15 42 18 3sstr4d 
 |-  ( ph -> ( ( ~=ph ` J ) " U. B ) C_ U. B )
44 ecinxp 
 |-  ( ( ( ( ~=ph ` J ) " U. B ) C_ U. B /\ M e. U. B ) -> [ M ] ( ~=ph ` J ) = [ M ] ( ( ~=ph ` J ) i^i ( U. B X. U. B ) ) )
45 43 6 44 syl2anc 
 |-  ( ph -> [ M ] ( ~=ph ` J ) = [ M ] ( ( ~=ph ` J ) i^i ( U. B X. U. B ) ) )
46 ecinxp 
 |-  ( ( ( ( ~=ph ` J ) " U. B ) C_ U. B /\ N e. U. B ) -> [ N ] ( ~=ph ` J ) = [ N ] ( ( ~=ph ` J ) i^i ( U. B X. U. B ) ) )
47 43 7 46 syl2anc 
 |-  ( ph -> [ N ] ( ~=ph ` J ) = [ N ] ( ( ~=ph ` J ) i^i ( U. B X. U. B ) ) )
48 45 47 oveq12d 
 |-  ( ph -> ( [ M ] ( ~=ph ` J ) .+ [ N ] ( ~=ph ` J ) ) = ( [ M ] ( ( ~=ph ` J ) i^i ( U. B X. U. B ) ) .+ [ N ] ( ( ~=ph ` J ) i^i ( U. B X. U. B ) ) ) )
49 12 3 4 18 6 7 om1addcl 
 |-  ( ph -> ( M ( *p ` J ) N ) e. U. B )
50 ecinxp 
 |-  ( ( ( ( ~=ph ` J ) " U. B ) C_ U. B /\ ( M ( *p ` J ) N ) e. U. B ) -> [ ( M ( *p ` J ) N ) ] ( ~=ph ` J ) = [ ( M ( *p ` J ) N ) ] ( ( ~=ph ` J ) i^i ( U. B X. U. B ) ) )
51 43 49 50 syl2anc 
 |-  ( ph -> [ ( M ( *p ` J ) N ) ] ( ~=ph ` J ) = [ ( M ( *p ` J ) N ) ] ( ( ~=ph ` J ) i^i ( U. B X. U. B ) ) )
52 31 oveqd 
 |-  ( ph -> ( M ( *p ` J ) N ) = ( M ( +g ` ( J Om1 Y ) ) N ) )
53 52 eceq1d 
 |-  ( ph -> [ ( M ( *p ` J ) N ) ] ( ( ~=ph ` J ) i^i ( U. B X. U. B ) ) = [ ( M ( +g ` ( J Om1 Y ) ) N ) ] ( ( ~=ph ` J ) i^i ( U. B X. U. B ) ) )
54 51 53 eqtrd 
 |-  ( ph -> [ ( M ( *p ` J ) N ) ] ( ~=ph ` J ) = [ ( M ( +g ` ( J Om1 Y ) ) N ) ] ( ( ~=ph ` J ) i^i ( U. B X. U. B ) ) )
55 41 48 54 3eqtr4d 
 |-  ( ph -> ( [ M ] ( ~=ph ` J ) .+ [ N ] ( ~=ph ` J ) ) = [ ( M ( *p ` J ) N ) ] ( ~=ph ` J ) )