Theorem pi1addf

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$$
	pi1addf.p	$$⊢\underset{\dot{}}{+}={+}_G$$
Assertion	pi1addf	$$⊢\phi \to \underset{\dot{}}{+}:B\times B⟶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$$
5		pi1addf.p	$$⊢\underset{\dot{}}{+}={+}_G$$
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)}\times {\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\times \bigcup B={\mathrm{Base}}_{\left(J{\Omega }_{1}Y\right)}\times {\mathrm{Base}}_{\left(J{\Omega }_{1}Y\right)}$$
18	17	ineq2d	$$⊢\phi \to {\simeq }_{\mathrm{ph}}\left(J\right)\cap \left(\bigcup B\times \bigcup B\right)={\simeq }_{\mathrm{ph}}\left(J\right)\cap \left({\mathrm{Base}}_{\left(J{\Omega }_{1}Y\right)}\times {\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\times \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)}\times {\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\times \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\times \bigcup B\right)\right)\mathrm{Er}\bigcup B$$
26		eqid	$$⊢{\simeq }_{\mathrm{ph}}\left(J\right)\cap \left(\bigcup B\times \bigcup B\right)={\simeq }_{\mathrm{ph}}\left(J\right)\cap \left(\bigcup B\times \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\times \bigcup B\right)\right)c\wedge b\left({\simeq }_{\mathrm{ph}}\left(J\right)\cap \left(\bigcup B\times \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\times \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	$$⊢\phi \to \underset{\dot{}}{+}:\left(\bigcup B/\left({\simeq }_{\mathrm{ph}}\left(J\right)\cap \left(\bigcup B\times \bigcup B\right)\right)\right)\times \left(\bigcup B/\left({\simeq }_{\mathrm{ph}}\left(J\right)\cap \left(\bigcup B\times \bigcup B\right)\right)\right)⟶\bigcup B/\left({\simeq }_{\mathrm{ph}}\left(J\right)\cap \left(\bigcup B\times \bigcup B\right)\right)$$
39	1 3 4 11 26	pi1bas3	$$⊢\phi \to B=\bigcup B/\left({\simeq }_{\mathrm{ph}}\left(J\right)\cap \left(\bigcup B\times \bigcup B\right)\right)$$
40	39	sqxpeqd	$$⊢\phi \to B\times B=\left(\bigcup B/\left({\simeq }_{\mathrm{ph}}\left(J\right)\cap \left(\bigcup B\times \bigcup B\right)\right)\right)\times \left(\bigcup B/\left({\simeq }_{\mathrm{ph}}\left(J\right)\cap \left(\bigcup B\times \bigcup B\right)\right)\right)$$
41	40	feq2d	$$⊢\phi \to \left(\underset{\dot{}}{+}:B\times B⟶\bigcup B/\left({\simeq }_{\mathrm{ph}}\left(J\right)\cap \left(\bigcup B\times \bigcup B\right)\right)\leftrightarrow \underset{\dot{}}{+}:\left(\bigcup B/\left({\simeq }_{\mathrm{ph}}\left(J\right)\cap \left(\bigcup B\times \bigcup B\right)\right)\right)\times \left(\bigcup B/\left({\simeq }_{\mathrm{ph}}\left(J\right)\cap \left(\bigcup B\times \bigcup B\right)\right)\right)⟶\bigcup B/\left({\simeq }_{\mathrm{ph}}\left(J\right)\cap \left(\bigcup B\times \bigcup B\right)\right)\right)$$
42	38 41	mpbird	$$⊢\phi \to \underset{\dot{}}{+}:B\times B⟶\bigcup B/\left({\simeq }_{\mathrm{ph}}\left(J\right)\cap \left(\bigcup B\times \bigcup B\right)\right)$$
43	39	feq3d	$$⊢\phi \to \left(\underset{\dot{}}{+}:B\times B⟶B\leftrightarrow \underset{\dot{}}{+}:B\times B⟶\bigcup B/\left({\simeq }_{\mathrm{ph}}\left(J\right)\cap \left(\bigcup B\times \bigcup B\right)\right)\right)$$
44	42 43	mpbird	$$⊢\phi \to \underset{\dot{}}{+}:B\times B⟶B$$