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 π_{1} Y$
	elpi1.b	$⊢ B = {Base}_{G}$
	elpi1.1	$⊢ φ \to J \in TopOn (X)$
	elpi1.2	$⊢ φ \to Y \in X$
	pi1addf.p	$⊢ \underset{˙}{+} = +_{G}$
	pi1addval.3	$⊢ φ \to M \in ⋃ B$
	pi1addval.4	$⊢ φ \to N \in ⋃ B$
Assertion	pi1addval	$⊢ φ \to [M] ≃_{ph} (J) \underset{˙}{+} [N] ≃_{ph} (J) = [(M *_{𝑝} (J) N)] ≃_{ph} (J)$

Proof

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

Metamath Proof Explorer

Theorem pi1addval

Proof