Theorem 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	⊢ 𝐺 = ( 𝐽 π1 𝑌 )
	elpi1.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
	elpi1.1	⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
	elpi1.2	⊢ ( 𝜑 → 𝑌 ∈ 𝑋 )
	pi1addf.p	⊢ + = ( +g ‘ 𝐺 )
	pi1addval.3	⊢ ( 𝜑 → 𝑀 ∈ ∪ 𝐵 )
	pi1addval.4	⊢ ( 𝜑 → 𝑁 ∈ ∪ 𝐵 )
Assertion	pi1addval	⊢ ( 𝜑 → ( [ 𝑀 ] ( ≃ph ‘ 𝐽 ) + [ 𝑁 ] ( ≃ph ‘ 𝐽 ) ) = [ ( 𝑀 ( *𝑝 ‘ 𝐽 ) 𝑁 ) ] ( ≃ph ‘ 𝐽 ) )

Proof

Step	Hyp	Ref	Expression
1		elpi1.g	⊢ 𝐺 = ( 𝐽 π1 𝑌 )
2		elpi1.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
3		elpi1.1	⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
4		elpi1.2	⊢ ( 𝜑 → 𝑌 ∈ 𝑋 )
5		pi1addf.p	⊢ + = ( +g ‘ 𝐺 )
6		pi1addval.3	⊢ ( 𝜑 → 𝑀 ∈ ∪ 𝐵 )
7		pi1addval.4	⊢ ( 𝜑 → 𝑁 ∈ ∪ 𝐵 )
8		eqidd	⊢ ( 𝜑 → ( ( 𝐽 Ω1 𝑌 ) /s ( ≃ph ‘ 𝐽 ) ) = ( ( 𝐽 Ω1 𝑌 ) /s ( ≃ph ‘ 𝐽 ) ) )
9		eqidd	⊢ ( 𝜑 → ( Base ‘ ( 𝐽 Ω1 𝑌 ) ) = ( Base ‘ ( 𝐽 Ω1 𝑌 ) ) )
10		fvexd	⊢ ( 𝜑 → ( ≃ph ‘ 𝐽 ) ∈ V )
11		ovexd	⊢ ( 𝜑 → ( 𝐽 Ω1 𝑌 ) ∈ V )
12		eqid	⊢ ( 𝐽 Ω1 𝑌 ) = ( 𝐽 Ω1 𝑌 )
13	2	a1i	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐺 ) )
14	1 3 4 12 13 9	pi1blem	⊢ ( 𝜑 → ( ( ( ≃ph ‘ 𝐽 ) “ ( Base ‘ ( 𝐽 Ω1 𝑌 ) ) ) ⊆ ( Base ‘ ( 𝐽 Ω1 𝑌 ) ) ∧ ( Base ‘ ( 𝐽 Ω1 𝑌 ) ) ⊆ ( II Cn 𝐽 ) ) )
15	14	simpld	⊢ ( 𝜑 → ( ( ≃ph ‘ 𝐽 ) “ ( Base ‘ ( 𝐽 Ω1 𝑌 ) ) ) ⊆ ( Base ‘ ( 𝐽 Ω1 𝑌 ) ) )
16	8 9 10 11 15	qusin	⊢ ( 𝜑 → ( ( 𝐽 Ω1 𝑌 ) /s ( ≃ph ‘ 𝐽 ) ) = ( ( 𝐽 Ω1 𝑌 ) /s ( ( ≃ph ‘ 𝐽 ) ∩ ( ( Base ‘ ( 𝐽 Ω1 𝑌 ) ) × ( Base ‘ ( 𝐽 Ω1 𝑌 ) ) ) ) ) )
17	1 3 4 12	pi1val	⊢ ( 𝜑 → 𝐺 = ( ( 𝐽 Ω1 𝑌 ) /s ( ≃ph ‘ 𝐽 ) ) )
18	1 3 4 12 13 9	pi1buni	⊢ ( 𝜑 → ∪ 𝐵 = ( Base ‘ ( 𝐽 Ω1 𝑌 ) ) )
19	18	sqxpeqd	⊢ ( 𝜑 → ( ∪ 𝐵 × ∪ 𝐵 ) = ( ( Base ‘ ( 𝐽 Ω1 𝑌 ) ) × ( Base ‘ ( 𝐽 Ω1 𝑌 ) ) ) )
20	19	ineq2d	⊢ ( 𝜑 → ( ( ≃ph ‘ 𝐽 ) ∩ ( ∪ 𝐵 × ∪ 𝐵 ) ) = ( ( ≃ph ‘ 𝐽 ) ∩ ( ( Base ‘ ( 𝐽 Ω1 𝑌 ) ) × ( Base ‘ ( 𝐽 Ω1 𝑌 ) ) ) ) )
21	20	oveq2d	⊢ ( 𝜑 → ( ( 𝐽 Ω1 𝑌 ) /s ( ( ≃ph ‘ 𝐽 ) ∩ ( ∪ 𝐵 × ∪ 𝐵 ) ) ) = ( ( 𝐽 Ω1 𝑌 ) /s ( ( ≃ph ‘ 𝐽 ) ∩ ( ( Base ‘ ( 𝐽 Ω1 𝑌 ) ) × ( Base ‘ ( 𝐽 Ω1 𝑌 ) ) ) ) ) )
22	16 17 21	3eqtr4d	⊢ ( 𝜑 → 𝐺 = ( ( 𝐽 Ω1 𝑌 ) /s ( ( ≃ph ‘ 𝐽 ) ∩ ( ∪ 𝐵 × ∪ 𝐵 ) ) ) )
23		phtpcer	⊢ ( ≃ph ‘ 𝐽 ) Er ( II Cn 𝐽 )
24	23	a1i	⊢ ( 𝜑 → ( ≃ph ‘ 𝐽 ) Er ( II Cn 𝐽 ) )
25	14	simprd	⊢ ( 𝜑 → ( Base ‘ ( 𝐽 Ω1 𝑌 ) ) ⊆ ( II Cn 𝐽 ) )
26	18 25	eqsstrd	⊢ ( 𝜑 → ∪ 𝐵 ⊆ ( II Cn 𝐽 ) )
27	24 26	erinxp	⊢ ( 𝜑 → ( ( ≃ph ‘ 𝐽 ) ∩ ( ∪ 𝐵 × ∪ 𝐵 ) ) Er ∪ 𝐵 )
28		eqid	⊢ ( ( ≃ph ‘ 𝐽 ) ∩ ( ∪ 𝐵 × ∪ 𝐵 ) ) = ( ( ≃ph ‘ 𝐽 ) ∩ ( ∪ 𝐵 × ∪ 𝐵 ) )
29		eqid	⊢ ( +g ‘ ( 𝐽 Ω1 𝑌 ) ) = ( +g ‘ ( 𝐽 Ω1 𝑌 ) )
30	1 3 4 13 28 12 29	pi1cpbl	⊢ ( 𝜑 → ( ( 𝑎 ( ( ≃ph ‘ 𝐽 ) ∩ ( ∪ 𝐵 × ∪ 𝐵 ) ) 𝑐 ∧ 𝑏 ( ( ≃ph ‘ 𝐽 ) ∩ ( ∪ 𝐵 × ∪ 𝐵 ) ) 𝑑 ) → ( 𝑎 ( +g ‘ ( 𝐽 Ω1 𝑌 ) ) 𝑏 ) ( ( ≃ph ‘ 𝐽 ) ∩ ( ∪ 𝐵 × ∪ 𝐵 ) ) ( 𝑐 ( +g ‘ ( 𝐽 Ω1 𝑌 ) ) 𝑑 ) ) )
31	12 3 4	om1plusg	⊢ ( 𝜑 → ( *𝑝 ‘ 𝐽 ) = ( +g ‘ ( 𝐽 Ω1 𝑌 ) ) )
32	31	oveqdr	⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ∪ 𝐵 ∧ 𝑑 ∈ ∪ 𝐵 ) ) → ( 𝑐 ( *𝑝 ‘ 𝐽 ) 𝑑 ) = ( 𝑐 ( +g ‘ ( 𝐽 Ω1 𝑌 ) ) 𝑑 ) )
33	3	adantr	⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ∪ 𝐵 ∧ 𝑑 ∈ ∪ 𝐵 ) ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
34	4	adantr	⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ∪ 𝐵 ∧ 𝑑 ∈ ∪ 𝐵 ) ) → 𝑌 ∈ 𝑋 )
35	18	adantr	⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ∪ 𝐵 ∧ 𝑑 ∈ ∪ 𝐵 ) ) → ∪ 𝐵 = ( Base ‘ ( 𝐽 Ω1 𝑌 ) ) )
36		simprl	⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ∪ 𝐵 ∧ 𝑑 ∈ ∪ 𝐵 ) ) → 𝑐 ∈ ∪ 𝐵 )
37		simprr	⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ∪ 𝐵 ∧ 𝑑 ∈ ∪ 𝐵 ) ) → 𝑑 ∈ ∪ 𝐵 )
38	12 33 34 35 36 37	om1addcl	⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ∪ 𝐵 ∧ 𝑑 ∈ ∪ 𝐵 ) ) → ( 𝑐 ( *𝑝 ‘ 𝐽 ) 𝑑 ) ∈ ∪ 𝐵 )
39	32 38	eqeltrrd	⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ∪ 𝐵 ∧ 𝑑 ∈ ∪ 𝐵 ) ) → ( 𝑐 ( +g ‘ ( 𝐽 Ω1 𝑌 ) ) 𝑑 ) ∈ ∪ 𝐵 )
40	22 18 27 11 30 39 29 5	qusaddval	⊢ ( ( 𝜑 ∧ 𝑀 ∈ ∪ 𝐵 ∧ 𝑁 ∈ ∪ 𝐵 ) → ( [ 𝑀 ] ( ( ≃ph ‘ 𝐽 ) ∩ ( ∪ 𝐵 × ∪ 𝐵 ) ) + [ 𝑁 ] ( ( ≃ph ‘ 𝐽 ) ∩ ( ∪ 𝐵 × ∪ 𝐵 ) ) ) = [ ( 𝑀 ( +g ‘ ( 𝐽 Ω1 𝑌 ) ) 𝑁 ) ] ( ( ≃ph ‘ 𝐽 ) ∩ ( ∪ 𝐵 × ∪ 𝐵 ) ) )
41	6 7 40	mpd3an23	⊢ ( 𝜑 → ( [ 𝑀 ] ( ( ≃ph ‘ 𝐽 ) ∩ ( ∪ 𝐵 × ∪ 𝐵 ) ) + [ 𝑁 ] ( ( ≃ph ‘ 𝐽 ) ∩ ( ∪ 𝐵 × ∪ 𝐵 ) ) ) = [ ( 𝑀 ( +g ‘ ( 𝐽 Ω1 𝑌 ) ) 𝑁 ) ] ( ( ≃ph ‘ 𝐽 ) ∩ ( ∪ 𝐵 × ∪ 𝐵 ) ) )
42	18	imaeq2d	⊢ ( 𝜑 → ( ( ≃ph ‘ 𝐽 ) “ ∪ 𝐵 ) = ( ( ≃ph ‘ 𝐽 ) “ ( Base ‘ ( 𝐽 Ω1 𝑌 ) ) ) )
43	15 42 18	3sstr4d	⊢ ( 𝜑 → ( ( ≃ph ‘ 𝐽 ) “ ∪ 𝐵 ) ⊆ ∪ 𝐵 )
44		ecinxp	⊢ ( ( ( ( ≃ph ‘ 𝐽 ) “ ∪ 𝐵 ) ⊆ ∪ 𝐵 ∧ 𝑀 ∈ ∪ 𝐵 ) → [ 𝑀 ] ( ≃ph ‘ 𝐽 ) = [ 𝑀 ] ( ( ≃ph ‘ 𝐽 ) ∩ ( ∪ 𝐵 × ∪ 𝐵 ) ) )
45	43 6 44	syl2anc	⊢ ( 𝜑 → [ 𝑀 ] ( ≃ph ‘ 𝐽 ) = [ 𝑀 ] ( ( ≃ph ‘ 𝐽 ) ∩ ( ∪ 𝐵 × ∪ 𝐵 ) ) )
46		ecinxp	⊢ ( ( ( ( ≃ph ‘ 𝐽 ) “ ∪ 𝐵 ) ⊆ ∪ 𝐵 ∧ 𝑁 ∈ ∪ 𝐵 ) → [ 𝑁 ] ( ≃ph ‘ 𝐽 ) = [ 𝑁 ] ( ( ≃ph ‘ 𝐽 ) ∩ ( ∪ 𝐵 × ∪ 𝐵 ) ) )
47	43 7 46	syl2anc	⊢ ( 𝜑 → [ 𝑁 ] ( ≃ph ‘ 𝐽 ) = [ 𝑁 ] ( ( ≃ph ‘ 𝐽 ) ∩ ( ∪ 𝐵 × ∪ 𝐵 ) ) )
48	45 47	oveq12d	⊢ ( 𝜑 → ( [ 𝑀 ] ( ≃ph ‘ 𝐽 ) + [ 𝑁 ] ( ≃ph ‘ 𝐽 ) ) = ( [ 𝑀 ] ( ( ≃ph ‘ 𝐽 ) ∩ ( ∪ 𝐵 × ∪ 𝐵 ) ) + [ 𝑁 ] ( ( ≃ph ‘ 𝐽 ) ∩ ( ∪ 𝐵 × ∪ 𝐵 ) ) ) )
49	12 3 4 18 6 7	om1addcl	⊢ ( 𝜑 → ( 𝑀 ( *𝑝 ‘ 𝐽 ) 𝑁 ) ∈ ∪ 𝐵 )
50		ecinxp	⊢ ( ( ( ( ≃ph ‘ 𝐽 ) “ ∪ 𝐵 ) ⊆ ∪ 𝐵 ∧ ( 𝑀 ( *𝑝 ‘ 𝐽 ) 𝑁 ) ∈ ∪ 𝐵 ) → [ ( 𝑀 ( *𝑝 ‘ 𝐽 ) 𝑁 ) ] ( ≃ph ‘ 𝐽 ) = [ ( 𝑀 ( *𝑝 ‘ 𝐽 ) 𝑁 ) ] ( ( ≃ph ‘ 𝐽 ) ∩ ( ∪ 𝐵 × ∪ 𝐵 ) ) )
51	43 49 50	syl2anc	⊢ ( 𝜑 → [ ( 𝑀 ( *𝑝 ‘ 𝐽 ) 𝑁 ) ] ( ≃ph ‘ 𝐽 ) = [ ( 𝑀 ( *𝑝 ‘ 𝐽 ) 𝑁 ) ] ( ( ≃ph ‘ 𝐽 ) ∩ ( ∪ 𝐵 × ∪ 𝐵 ) ) )
52	31	oveqd	⊢ ( 𝜑 → ( 𝑀 ( *𝑝 ‘ 𝐽 ) 𝑁 ) = ( 𝑀 ( +g ‘ ( 𝐽 Ω1 𝑌 ) ) 𝑁 ) )
53	52	eceq1d	⊢ ( 𝜑 → [ ( 𝑀 ( *𝑝 ‘ 𝐽 ) 𝑁 ) ] ( ( ≃ph ‘ 𝐽 ) ∩ ( ∪ 𝐵 × ∪ 𝐵 ) ) = [ ( 𝑀 ( +g ‘ ( 𝐽 Ω1 𝑌 ) ) 𝑁 ) ] ( ( ≃ph ‘ 𝐽 ) ∩ ( ∪ 𝐵 × ∪ 𝐵 ) ) )
54	51 53	eqtrd	⊢ ( 𝜑 → [ ( 𝑀 ( *𝑝 ‘ 𝐽 ) 𝑁 ) ] ( ≃ph ‘ 𝐽 ) = [ ( 𝑀 ( +g ‘ ( 𝐽 Ω1 𝑌 ) ) 𝑁 ) ] ( ( ≃ph ‘ 𝐽 ) ∩ ( ∪ 𝐵 × ∪ 𝐵 ) ) )
55	41 48 54	3eqtr4d	⊢ ( 𝜑 → ( [ 𝑀 ] ( ≃ph ‘ 𝐽 ) + [ 𝑁 ] ( ≃ph ‘ 𝐽 ) ) = [ ( 𝑀 ( *𝑝 ‘ 𝐽 ) 𝑁 ) ] ( ≃ph ‘ 𝐽 ) )