# Metamath Proof Explorer

Description: The group operation of pi1 is a binary operation. (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}$

### 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 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)$
7 eqidd ${⊢}{\phi }\to {\mathrm{Base}}_{\left({J}{\Omega }_{1}{Y}\right)}={\mathrm{Base}}_{\left({J}{\Omega }_{1}{Y}\right)}$
8 fvexd ${⊢}{\phi }\to {\simeq }_{\mathrm{ph}}\left({J}\right)\in \mathrm{V}$
9 ovexd ${⊢}{\phi }\to {J}{\Omega }_{1}{Y}\in \mathrm{V}$
10 eqid ${⊢}{J}{\Omega }_{1}{Y}={J}{\Omega }_{1}{Y}$
11 2 a1i ${⊢}{\phi }\to {B}={\mathrm{Base}}_{{G}}$
12 1 3 4 10 11 7 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)$
13 12 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)}$
14 6 7 8 9 13 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)$
15 1 3 4 10 pi1val ${⊢}{\phi }\to {G}=\left({J}{\Omega }_{1}{Y}\right){/}_{𝑠}{\simeq }_{\mathrm{ph}}\left({J}\right)$
16 1 3 4 10 11 7 pi1buni ${⊢}{\phi }\to \bigcup {B}={\mathrm{Base}}_{\left({J}{\Omega }_{1}{Y}\right)}$
17 16 sqxpeqd ${⊢}{\phi }\to \bigcup {B}×\bigcup {B}={\mathrm{Base}}_{\left({J}{\Omega }_{1}{Y}\right)}×{\mathrm{Base}}_{\left({J}{\Omega }_{1}{Y}\right)}$
18 17 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)$
19 18 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)$
20 14 15 19 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)$
21 phtpcer ${⊢}{\simeq }_{\mathrm{ph}}\left({J}\right)\mathrm{Er}\left(\mathrm{II}\mathrm{Cn}{J}\right)$
22 21 a1i ${⊢}{\phi }\to {\simeq }_{\mathrm{ph}}\left({J}\right)\mathrm{Er}\left(\mathrm{II}\mathrm{Cn}{J}\right)$
23 12 simprd ${⊢}{\phi }\to {\mathrm{Base}}_{\left({J}{\Omega }_{1}{Y}\right)}\subseteq \mathrm{II}\mathrm{Cn}{J}$
24 16 23 eqsstrd ${⊢}{\phi }\to \bigcup {B}\subseteq \mathrm{II}\mathrm{Cn}{J}$
25 22 24 erinxp ${⊢}{\phi }\to \left({\simeq }_{\mathrm{ph}}\left({J}\right)\cap \left(\bigcup {B}×\bigcup {B}\right)\right)\mathrm{Er}\bigcup {B}$
26 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)$
27 eqid ${⊢}{+}_{\left({J}{\Omega }_{1}{Y}\right)}={+}_{\left({J}{\Omega }_{1}{Y}\right)}$
28 1 3 4 11 26 10 27 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)$
29 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)$
30 4 adantr ${⊢}\left({\phi }\wedge \left({c}\in \bigcup {B}\wedge {d}\in \bigcup {B}\right)\right)\to {Y}\in {X}$
31 10 29 30 om1plusg ${⊢}\left({\phi }\wedge \left({c}\in \bigcup {B}\wedge {d}\in \bigcup {B}\right)\right)\to {*}_{𝑝}\left({J}\right)={+}_{\left({J}{\Omega }_{1}{Y}\right)}$
32 31 oveqd ${⊢}\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 16 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)}$
34 simprl ${⊢}\left({\phi }\wedge \left({c}\in \bigcup {B}\wedge {d}\in \bigcup {B}\right)\right)\to {c}\in \bigcup {B}$
35 simprr ${⊢}\left({\phi }\wedge \left({c}\in \bigcup {B}\wedge {d}\in \bigcup {B}\right)\right)\to {d}\in \bigcup {B}$
36 10 29 30 33 34 35 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}$
37 32 36 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}$
38 20 16 25 9 28 37 27 5 qusaddf
39 1 3 4 11 26 pi1bas3 ${⊢}{\phi }\to {B}=\bigcup {B}/\left({\simeq }_{\mathrm{ph}}\left({J}\right)\cap \left(\bigcup {B}×\bigcup {B}\right)\right)$
40 39 sqxpeqd ${⊢}{\phi }\to {B}×{B}=\left(\bigcup {B}/\left({\simeq }_{\mathrm{ph}}\left({J}\right)\cap \left(\bigcup {B}×\bigcup {B}\right)\right)\right)×\left(\bigcup {B}/\left({\simeq }_{\mathrm{ph}}\left({J}\right)\cap \left(\bigcup {B}×\bigcup {B}\right)\right)\right)$
41 40 feq2d
42 38 41 mpbird
43 39 feq3d
44 42 43 mpbird