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 π_{1} Y$
	pi1val.1	$⊢ φ \to J \in TopOn (X)$
	pi1val.2	$⊢ φ \to Y \in X$
	pi1bas2.b	$⊢ φ \to B = {Base}_{G}$
	pi1bas3.r	$⊢ R = ≃_{ph} (J) \cap (⋃ B \times ⋃ B)$
	pi1cpbl.o	$⊢ O = J Ω_{1} Y$
	pi1cpbl.a	$⊢ \underset{˙}{+} = +_{O}$
Assertion	pi1cpbl	$⊢ φ \to ((M R N \land P R Q) \to (M \underset{˙}{+} P) R (N \underset{˙}{+} Q))$

Proof

Step	Hyp	Ref	Expression
1		pi1val.g	$⊢ G = J π_{1} Y$
2		pi1val.1	$⊢ φ \to J \in TopOn (X)$
3		pi1val.2	$⊢ φ \to Y \in X$
4		pi1bas2.b	$⊢ φ \to B = {Base}_{G}$
5		pi1bas3.r	$⊢ R = ≃_{ph} (J) \cap (⋃ B \times ⋃ B)$
6		pi1cpbl.o	$⊢ O = J Ω_{1} Y$
7		pi1cpbl.a	$⊢ \underset{˙}{+} = +_{O}$
8	2	adantr	$⊢ (φ \land (M R N \land P R Q)) \to J \in TopOn (X)$
9	3	adantr	$⊢ (φ \land (M R N \land P R Q)) \to Y \in X$
10	4	adantr	$⊢ (φ \land (M R N \land P R Q)) \to B = {Base}_{G}$
11		eqidd	$⊢ (φ \land (M R N \land P R Q)) \to {Base}_{O} = {Base}_{O}$
12	1 8 9 6 10 11	pi1buni	$⊢ (φ \land (M R N \land P R Q)) \to ⋃ B = {Base}_{O}$
13		simprl	$⊢ (φ \land (M R N \land P R Q)) \to M R N$
14	5	breqi	$⊢ M R N \leftrightarrow M (≃_{ph} (J) \cap (⋃ B \times ⋃ B)) N$
15		brinxp2	$⊢ M (≃_{ph} (J) \cap (⋃ B \times ⋃ B)) N \leftrightarrow ((M \in ⋃ B \land N \in ⋃ B) \land M ≃_{ph} (J) N)$
16	14 15	bitri	$⊢ M R N \leftrightarrow ((M \in ⋃ B \land N \in ⋃ B) \land M ≃_{ph} (J) N)$
17	13 16	sylib	$⊢ (φ \land (M R N \land P R Q)) \to ((M \in ⋃ B \land N \in ⋃ B) \land M ≃_{ph} (J) N)$
18	17	simplld	$⊢ (φ \land (M R N \land P R Q)) \to M \in ⋃ B$
19		simprr	$⊢ (φ \land (M R N \land P R Q)) \to P R Q$
20	5	breqi	$⊢ P R Q \leftrightarrow P (≃_{ph} (J) \cap (⋃ B \times ⋃ B)) Q$
21		brinxp2	$⊢ P (≃_{ph} (J) \cap (⋃ B \times ⋃ B)) Q \leftrightarrow ((P \in ⋃ B \land Q \in ⋃ B) \land P ≃_{ph} (J) Q)$
22	20 21	bitri	$⊢ P R Q \leftrightarrow ((P \in ⋃ B \land Q \in ⋃ B) \land P ≃_{ph} (J) Q)$
23	19 22	sylib	$⊢ (φ \land (M R N \land P R Q)) \to ((P \in ⋃ B \land Q \in ⋃ B) \land P ≃_{ph} (J) Q)$
24	23	simplld	$⊢ (φ \land (M R N \land P R Q)) \to P \in ⋃ B$
25	6 8 9 12 18 24	om1addcl	$⊢ (φ \land (M R N \land P R Q)) \to M *_{𝑝} (J) P \in ⋃ B$
26	17	simplrd	$⊢ (φ \land (M R N \land P R Q)) \to N \in ⋃ B$
27	23	simplrd	$⊢ (φ \land (M R N \land P R Q)) \to Q \in ⋃ B$
28	6 8 9 12 26 27	om1addcl	$⊢ (φ \land (M R N \land P R Q)) \to N *_{𝑝} (J) Q \in ⋃ B$
29	1 8 9 10	pi1eluni	$⊢ (φ \land (M R N \land P R Q)) \to (M \in ⋃ B \leftrightarrow (M \in (II Cn J) \land M (0) = Y \land M (1) = Y))$
30	18 29	mpbid	$⊢ (φ \land (M R N \land P R Q)) \to (M \in (II Cn J) \land M (0) = Y \land M (1) = Y)$
31	30	simp3d	$⊢ (φ \land (M R N \land P R Q)) \to M (1) = Y$
32	1 8 9 10	pi1eluni	$⊢ (φ \land (M R N \land P R Q)) \to (P \in ⋃ B \leftrightarrow (P \in (II Cn J) \land P (0) = Y \land P (1) = Y))$
33	24 32	mpbid	$⊢ (φ \land (M R N \land P R Q)) \to (P \in (II Cn J) \land P (0) = Y \land P (1) = Y)$
34	33	simp2d	$⊢ (φ \land (M R N \land P R Q)) \to P (0) = Y$
35	31 34	eqtr4d	$⊢ (φ \land (M R N \land P R Q)) \to M (1) = P (0)$
36	17	simprd	$⊢ (φ \land (M R N \land P R Q)) \to M ≃_{ph} (J) N$
37	23	simprd	$⊢ (φ \land (M R N \land P R Q)) \to P ≃_{ph} (J) Q$
38	35 36 37	pcohtpy	$⊢ (φ \land (M R N \land P R Q)) \to (M _{𝑝} (J) P) ≃_{ph} (J) (N _{𝑝} (J) Q)$
39	5	breqi	$⊢ (M _{𝑝} (J) P) R (N _{𝑝} (J) Q) \leftrightarrow (M _{𝑝} (J) P) (≃_{ph} (J) \cap (⋃ B \times ⋃ B)) (N _{𝑝} (J) Q)$
40		brinxp2	$⊢ (M _{𝑝} (J) P) (≃_{ph} (J) \cap (⋃ B \times ⋃ B)) (N _{𝑝} (J) Q) \leftrightarrow ((M _{𝑝} (J) P \in ⋃ B \land N _{𝑝} (J) Q \in ⋃ B) \land (M _{𝑝} (J) P) ≃_{ph} (J) (N _{𝑝} (J) Q))$
41	39 40	bitri	$⊢ (M _{𝑝} (J) P) R (N _{𝑝} (J) Q) \leftrightarrow ((M _{𝑝} (J) P \in ⋃ B \land N _{𝑝} (J) Q \in ⋃ B) \land (M _{𝑝} (J) P) ≃_{ph} (J) (N _{𝑝} (J) Q))$
42	25 28 38 41	syl21anbrc	$⊢ (φ \land (M R N \land P R Q)) \to (M _{𝑝} (J) P) R (N _{𝑝} (J) Q)$
43	6 8 9	om1plusg	$⊢ (φ \land (M R N \land P R Q)) \to *_{𝑝} (J) = +_{O}$
44	43 7	eqtr4di	$⊢ (φ \land (M R N \land P R Q)) \to *_{𝑝} (J) = \underset{˙}{+}$
45	44	oveqd	$⊢ (φ \land (M R N \land P R Q)) \to M *_{𝑝} (J) P = M \underset{˙}{+} P$
46	44	oveqd	$⊢ (φ \land (M R N \land P R Q)) \to N *_{𝑝} (J) Q = N \underset{˙}{+} Q$
47	42 45 46	3brtr3d	$⊢ (φ \land (M R N \land P R Q)) \to (M \underset{˙}{+} P) R (N \underset{˙}{+} Q)$
48	47	ex	$⊢ φ \to ((M R N \land P R Q) \to (M \underset{˙}{+} P) R (N \underset{˙}{+} Q))$

Metamath Proof Explorer

Theorem pi1cpbl

Proof