# Metamath Proof Explorer

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}{\pi }_{1}{Y}$
elpi1.b ${⊢}{B}={\mathrm{Base}}_{{G}}$
elpi1.1 ${⊢}{\phi }\to {J}\in \mathrm{TopOn}\left({X}\right)$
elpi1.2 ${⊢}{\phi }\to {Y}\in {X}$
pi1addval.3 ${⊢}{\phi }\to {M}\in \bigcup {B}$
pi1addval.4 ${⊢}{\phi }\to {N}\in \bigcup {B}$

### Proof

Step Hyp Ref Expression
1 elpi1.g ${⊢}{G}={J}{\pi }_{1}{Y}$
2 elpi1.b ${⊢}{B}={\mathrm{Base}}_{{G}}$
3 elpi1.1 ${⊢}{\phi }\to {J}\in \mathrm{TopOn}\left({X}\right)$
4 elpi1.2 ${⊢}{\phi }\to {Y}\in {X}$
6 pi1addval.3 ${⊢}{\phi }\to {M}\in \bigcup {B}$
7 pi1addval.4 ${⊢}{\phi }\to {N}\in \bigcup {B}$
8 eqidd ${⊢}{\phi }\to \left({J}{\Omega }_{1}{Y}\right){/}_{𝑠}{\simeq }_{\mathrm{ph}}\left({J}\right)=\left({J}{\Omega }_{1}{Y}\right){/}_{𝑠}{\simeq }_{\mathrm{ph}}\left({J}\right)$
9 eqidd ${⊢}{\phi }\to {\mathrm{Base}}_{\left({J}{\Omega }_{1}{Y}\right)}={\mathrm{Base}}_{\left({J}{\Omega }_{1}{Y}\right)}$
10 fvexd ${⊢}{\phi }\to {\simeq }_{\mathrm{ph}}\left({J}\right)\in \mathrm{V}$
11 ovexd ${⊢}{\phi }\to {J}{\Omega }_{1}{Y}\in \mathrm{V}$
12 eqid ${⊢}{J}{\Omega }_{1}{Y}={J}{\Omega }_{1}{Y}$
13 2 a1i ${⊢}{\phi }\to {B}={\mathrm{Base}}_{{G}}$
14 1 3 4 12 13 9 pi1blem ${⊢}{\phi }\to \left({\simeq }_{\mathrm{ph}}\left({J}\right)\left[{\mathrm{Base}}_{\left({J}{\Omega }_{1}{Y}\right)}\right]\subseteq {\mathrm{Base}}_{\left({J}{\Omega }_{1}{Y}\right)}\wedge {\mathrm{Base}}_{\left({J}{\Omega }_{1}{Y}\right)}\subseteq \mathrm{II}\mathrm{Cn}{J}\right)$
15 14 simpld ${⊢}{\phi }\to {\simeq }_{\mathrm{ph}}\left({J}\right)\left[{\mathrm{Base}}_{\left({J}{\Omega }_{1}{Y}\right)}\right]\subseteq {\mathrm{Base}}_{\left({J}{\Omega }_{1}{Y}\right)}$
16 8 9 10 11 15 qusin ${⊢}{\phi }\to \left({J}{\Omega }_{1}{Y}\right){/}_{𝑠}{\simeq }_{\mathrm{ph}}\left({J}\right)=\left({J}{\Omega }_{1}{Y}\right){/}_{𝑠}\left({\simeq }_{\mathrm{ph}}\left({J}\right)\cap \left({\mathrm{Base}}_{\left({J}{\Omega }_{1}{Y}\right)}×{\mathrm{Base}}_{\left({J}{\Omega }_{1}{Y}\right)}\right)\right)$
17 1 3 4 12 pi1val ${⊢}{\phi }\to {G}=\left({J}{\Omega }_{1}{Y}\right){/}_{𝑠}{\simeq }_{\mathrm{ph}}\left({J}\right)$
18 1 3 4 12 13 9 pi1buni ${⊢}{\phi }\to \bigcup {B}={\mathrm{Base}}_{\left({J}{\Omega }_{1}{Y}\right)}$
19 18 sqxpeqd ${⊢}{\phi }\to \bigcup {B}×\bigcup {B}={\mathrm{Base}}_{\left({J}{\Omega }_{1}{Y}\right)}×{\mathrm{Base}}_{\left({J}{\Omega }_{1}{Y}\right)}$
20 19 ineq2d ${⊢}{\phi }\to {\simeq }_{\mathrm{ph}}\left({J}\right)\cap \left(\bigcup {B}×\bigcup {B}\right)={\simeq }_{\mathrm{ph}}\left({J}\right)\cap \left({\mathrm{Base}}_{\left({J}{\Omega }_{1}{Y}\right)}×{\mathrm{Base}}_{\left({J}{\Omega }_{1}{Y}\right)}\right)$
21 20 oveq2d ${⊢}{\phi }\to \left({J}{\Omega }_{1}{Y}\right){/}_{𝑠}\left({\simeq }_{\mathrm{ph}}\left({J}\right)\cap \left(\bigcup {B}×\bigcup {B}\right)\right)=\left({J}{\Omega }_{1}{Y}\right){/}_{𝑠}\left({\simeq }_{\mathrm{ph}}\left({J}\right)\cap \left({\mathrm{Base}}_{\left({J}{\Omega }_{1}{Y}\right)}×{\mathrm{Base}}_{\left({J}{\Omega }_{1}{Y}\right)}\right)\right)$
22 16 17 21 3eqtr4d ${⊢}{\phi }\to {G}=\left({J}{\Omega }_{1}{Y}\right){/}_{𝑠}\left({\simeq }_{\mathrm{ph}}\left({J}\right)\cap \left(\bigcup {B}×\bigcup {B}\right)\right)$
23 phtpcer ${⊢}{\simeq }_{\mathrm{ph}}\left({J}\right)\mathrm{Er}\left(\mathrm{II}\mathrm{Cn}{J}\right)$
24 23 a1i ${⊢}{\phi }\to {\simeq }_{\mathrm{ph}}\left({J}\right)\mathrm{Er}\left(\mathrm{II}\mathrm{Cn}{J}\right)$
25 14 simprd ${⊢}{\phi }\to {\mathrm{Base}}_{\left({J}{\Omega }_{1}{Y}\right)}\subseteq \mathrm{II}\mathrm{Cn}{J}$
26 18 25 eqsstrd ${⊢}{\phi }\to \bigcup {B}\subseteq \mathrm{II}\mathrm{Cn}{J}$
27 24 26 erinxp ${⊢}{\phi }\to \left({\simeq }_{\mathrm{ph}}\left({J}\right)\cap \left(\bigcup {B}×\bigcup {B}\right)\right)\mathrm{Er}\bigcup {B}$
28 eqid ${⊢}{\simeq }_{\mathrm{ph}}\left({J}\right)\cap \left(\bigcup {B}×\bigcup {B}\right)={\simeq }_{\mathrm{ph}}\left({J}\right)\cap \left(\bigcup {B}×\bigcup {B}\right)$
29 eqid ${⊢}{+}_{\left({J}{\Omega }_{1}{Y}\right)}={+}_{\left({J}{\Omega }_{1}{Y}\right)}$
30 1 3 4 13 28 12 29 pi1cpbl ${⊢}{\phi }\to \left(\left({a}\left({\simeq }_{\mathrm{ph}}\left({J}\right)\cap \left(\bigcup {B}×\bigcup {B}\right)\right){c}\wedge {b}\left({\simeq }_{\mathrm{ph}}\left({J}\right)\cap \left(\bigcup {B}×\bigcup {B}\right)\right){d}\right)\to \left({a}{+}_{\left({J}{\Omega }_{1}{Y}\right)}{b}\right)\left({\simeq }_{\mathrm{ph}}\left({J}\right)\cap \left(\bigcup {B}×\bigcup {B}\right)\right)\left({c}{+}_{\left({J}{\Omega }_{1}{Y}\right)}{d}\right)\right)$
31 12 3 4 om1plusg ${⊢}{\phi }\to {*}_{𝑝}\left({J}\right)={+}_{\left({J}{\Omega }_{1}{Y}\right)}$
32 31 oveqdr ${⊢}\left({\phi }\wedge \left({c}\in \bigcup {B}\wedge {d}\in \bigcup {B}\right)\right)\to {c}{*}_{𝑝}\left({J}\right){d}={c}{+}_{\left({J}{\Omega }_{1}{Y}\right)}{d}$
33 3 adantr ${⊢}\left({\phi }\wedge \left({c}\in \bigcup {B}\wedge {d}\in \bigcup {B}\right)\right)\to {J}\in \mathrm{TopOn}\left({X}\right)$
34 4 adantr ${⊢}\left({\phi }\wedge \left({c}\in \bigcup {B}\wedge {d}\in \bigcup {B}\right)\right)\to {Y}\in {X}$
35 18 adantr ${⊢}\left({\phi }\wedge \left({c}\in \bigcup {B}\wedge {d}\in \bigcup {B}\right)\right)\to \bigcup {B}={\mathrm{Base}}_{\left({J}{\Omega }_{1}{Y}\right)}$
36 simprl ${⊢}\left({\phi }\wedge \left({c}\in \bigcup {B}\wedge {d}\in \bigcup {B}\right)\right)\to {c}\in \bigcup {B}$
37 simprr ${⊢}\left({\phi }\wedge \left({c}\in \bigcup {B}\wedge {d}\in \bigcup {B}\right)\right)\to {d}\in \bigcup {B}$
38 12 33 34 35 36 37 om1addcl ${⊢}\left({\phi }\wedge \left({c}\in \bigcup {B}\wedge {d}\in \bigcup {B}\right)\right)\to {c}{*}_{𝑝}\left({J}\right){d}\in \bigcup {B}$
39 32 38 eqeltrrd ${⊢}\left({\phi }\wedge \left({c}\in \bigcup {B}\wedge {d}\in \bigcup {B}\right)\right)\to {c}{+}_{\left({J}{\Omega }_{1}{Y}\right)}{d}\in \bigcup {B}$
40 22 18 27 11 30 39 29 5 qusaddval
41 6 7 40 mpd3an23
42 18 imaeq2d ${⊢}{\phi }\to {\simeq }_{\mathrm{ph}}\left({J}\right)\left[\bigcup {B}\right]={\simeq }_{\mathrm{ph}}\left({J}\right)\left[{\mathrm{Base}}_{\left({J}{\Omega }_{1}{Y}\right)}\right]$
43 15 42 18 3sstr4d ${⊢}{\phi }\to {\simeq }_{\mathrm{ph}}\left({J}\right)\left[\bigcup {B}\right]\subseteq \bigcup {B}$
44 ecinxp ${⊢}\left({\simeq }_{\mathrm{ph}}\left({J}\right)\left[\bigcup {B}\right]\subseteq \bigcup {B}\wedge {M}\in \bigcup {B}\right)\to \left[{M}\right]{\simeq }_{\mathrm{ph}}\left({J}\right)=\left[{M}\right]\left({\simeq }_{\mathrm{ph}}\left({J}\right)\cap \left(\bigcup {B}×\bigcup {B}\right)\right)$
45 43 6 44 syl2anc ${⊢}{\phi }\to \left[{M}\right]{\simeq }_{\mathrm{ph}}\left({J}\right)=\left[{M}\right]\left({\simeq }_{\mathrm{ph}}\left({J}\right)\cap \left(\bigcup {B}×\bigcup {B}\right)\right)$
46 ecinxp ${⊢}\left({\simeq }_{\mathrm{ph}}\left({J}\right)\left[\bigcup {B}\right]\subseteq \bigcup {B}\wedge {N}\in \bigcup {B}\right)\to \left[{N}\right]{\simeq }_{\mathrm{ph}}\left({J}\right)=\left[{N}\right]\left({\simeq }_{\mathrm{ph}}\left({J}\right)\cap \left(\bigcup {B}×\bigcup {B}\right)\right)$
47 43 7 46 syl2anc ${⊢}{\phi }\to \left[{N}\right]{\simeq }_{\mathrm{ph}}\left({J}\right)=\left[{N}\right]\left({\simeq }_{\mathrm{ph}}\left({J}\right)\cap \left(\bigcup {B}×\bigcup {B}\right)\right)$
48 45 47 oveq12d
49 12 3 4 18 6 7 om1addcl ${⊢}{\phi }\to {M}{*}_{𝑝}\left({J}\right){N}\in \bigcup {B}$
50 ecinxp ${⊢}\left({\simeq }_{\mathrm{ph}}\left({J}\right)\left[\bigcup {B}\right]\subseteq \bigcup {B}\wedge {M}{*}_{𝑝}\left({J}\right){N}\in \bigcup {B}\right)\to \left[\left({M}{*}_{𝑝}\left({J}\right){N}\right)\right]{\simeq }_{\mathrm{ph}}\left({J}\right)=\left[\left({M}{*}_{𝑝}\left({J}\right){N}\right)\right]\left({\simeq }_{\mathrm{ph}}\left({J}\right)\cap \left(\bigcup {B}×\bigcup {B}\right)\right)$
51 43 49 50 syl2anc ${⊢}{\phi }\to \left[\left({M}{*}_{𝑝}\left({J}\right){N}\right)\right]{\simeq }_{\mathrm{ph}}\left({J}\right)=\left[\left({M}{*}_{𝑝}\left({J}\right){N}\right)\right]\left({\simeq }_{\mathrm{ph}}\left({J}\right)\cap \left(\bigcup {B}×\bigcup {B}\right)\right)$
52 31 oveqd ${⊢}{\phi }\to {M}{*}_{𝑝}\left({J}\right){N}={M}{+}_{\left({J}{\Omega }_{1}{Y}\right)}{N}$
53 52 eceq1d ${⊢}{\phi }\to \left[\left({M}{*}_{𝑝}\left({J}\right){N}\right)\right]\left({\simeq }_{\mathrm{ph}}\left({J}\right)\cap \left(\bigcup {B}×\bigcup {B}\right)\right)=\left[\left({M}{+}_{\left({J}{\Omega }_{1}{Y}\right)}{N}\right)\right]\left({\simeq }_{\mathrm{ph}}\left({J}\right)\cap \left(\bigcup {B}×\bigcup {B}\right)\right)$
54 51 53 eqtrd ${⊢}{\phi }\to \left[\left({M}{*}_{𝑝}\left({J}\right){N}\right)\right]{\simeq }_{\mathrm{ph}}\left({J}\right)=\left[\left({M}{+}_{\left({J}{\Omega }_{1}{Y}\right)}{N}\right)\right]\left({\simeq }_{\mathrm{ph}}\left({J}\right)\cap \left(\bigcup {B}×\bigcup {B}\right)\right)$
55 41 48 54 3eqtr4d