Theorem pi1cpbl

Description: The group operation, loop concatenation, is compatible with homotopy equivalence. (Contributed by Mario Carneiro, 10-Jul-2015)

	Ref	Expression
Hypotheses	pi1val.g	⊢ 𝐺 = ( 𝐽 π1 𝑌 )
	pi1val.1	⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
	pi1val.2	⊢ ( 𝜑 → 𝑌 ∈ 𝑋 )
	pi1bas2.b	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐺 ) )
	pi1bas3.r	⊢ 𝑅 = ( ( ≃ph ‘ 𝐽 ) ∩ ( ∪ 𝐵 × ∪ 𝐵 ) )
	pi1cpbl.o	⊢ 𝑂 = ( 𝐽 Ω1 𝑌 )
	pi1cpbl.a	⊢ + = ( +g ‘ 𝑂 )
Assertion	pi1cpbl	⊢ ( 𝜑 → ( ( 𝑀 𝑅 𝑁 ∧ 𝑃 𝑅 𝑄 ) → ( 𝑀 + 𝑃 ) 𝑅 ( 𝑁 + 𝑄 ) ) )

Proof

Step	Hyp	Ref	Expression
1		pi1val.g	⊢ 𝐺 = ( 𝐽 π1 𝑌 )
2		pi1val.1	⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
3		pi1val.2	⊢ ( 𝜑 → 𝑌 ∈ 𝑋 )
4		pi1bas2.b	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐺 ) )
5		pi1bas3.r	⊢ 𝑅 = ( ( ≃ph ‘ 𝐽 ) ∩ ( ∪ 𝐵 × ∪ 𝐵 ) )
6		pi1cpbl.o	⊢ 𝑂 = ( 𝐽 Ω1 𝑌 )
7		pi1cpbl.a	⊢ + = ( +g ‘ 𝑂 )
8	2	adantr	⊢ ( ( 𝜑 ∧ ( 𝑀 𝑅 𝑁 ∧ 𝑃 𝑅 𝑄 ) ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
9	3	adantr	⊢ ( ( 𝜑 ∧ ( 𝑀 𝑅 𝑁 ∧ 𝑃 𝑅 𝑄 ) ) → 𝑌 ∈ 𝑋 )
10	4	adantr	⊢ ( ( 𝜑 ∧ ( 𝑀 𝑅 𝑁 ∧ 𝑃 𝑅 𝑄 ) ) → 𝐵 = ( Base ‘ 𝐺 ) )
11		eqidd	⊢ ( ( 𝜑 ∧ ( 𝑀 𝑅 𝑁 ∧ 𝑃 𝑅 𝑄 ) ) → ( Base ‘ 𝑂 ) = ( Base ‘ 𝑂 ) )
12	1 8 9 6 10 11	pi1buni	⊢ ( ( 𝜑 ∧ ( 𝑀 𝑅 𝑁 ∧ 𝑃 𝑅 𝑄 ) ) → ∪ 𝐵 = ( Base ‘ 𝑂 ) )
13		simprl	⊢ ( ( 𝜑 ∧ ( 𝑀 𝑅 𝑁 ∧ 𝑃 𝑅 𝑄 ) ) → 𝑀 𝑅 𝑁 )
14	5	breqi	⊢ ( 𝑀 𝑅 𝑁 ↔ 𝑀 ( ( ≃ph ‘ 𝐽 ) ∩ ( ∪ 𝐵 × ∪ 𝐵 ) ) 𝑁 )
15		brinxp2	⊢ ( 𝑀 ( ( ≃ph ‘ 𝐽 ) ∩ ( ∪ 𝐵 × ∪ 𝐵 ) ) 𝑁 ↔ ( ( 𝑀 ∈ ∪ 𝐵 ∧ 𝑁 ∈ ∪ 𝐵 ) ∧ 𝑀 ( ≃ph ‘ 𝐽 ) 𝑁 ) )
16	14 15	bitri	⊢ ( 𝑀 𝑅 𝑁 ↔ ( ( 𝑀 ∈ ∪ 𝐵 ∧ 𝑁 ∈ ∪ 𝐵 ) ∧ 𝑀 ( ≃ph ‘ 𝐽 ) 𝑁 ) )
17	13 16	sylib	⊢ ( ( 𝜑 ∧ ( 𝑀 𝑅 𝑁 ∧ 𝑃 𝑅 𝑄 ) ) → ( ( 𝑀 ∈ ∪ 𝐵 ∧ 𝑁 ∈ ∪ 𝐵 ) ∧ 𝑀 ( ≃ph ‘ 𝐽 ) 𝑁 ) )
18	17	simplld	⊢ ( ( 𝜑 ∧ ( 𝑀 𝑅 𝑁 ∧ 𝑃 𝑅 𝑄 ) ) → 𝑀 ∈ ∪ 𝐵 )
19		simprr	⊢ ( ( 𝜑 ∧ ( 𝑀 𝑅 𝑁 ∧ 𝑃 𝑅 𝑄 ) ) → 𝑃 𝑅 𝑄 )
20	5	breqi	⊢ ( 𝑃 𝑅 𝑄 ↔ 𝑃 ( ( ≃ph ‘ 𝐽 ) ∩ ( ∪ 𝐵 × ∪ 𝐵 ) ) 𝑄 )
21		brinxp2	⊢ ( 𝑃 ( ( ≃ph ‘ 𝐽 ) ∩ ( ∪ 𝐵 × ∪ 𝐵 ) ) 𝑄 ↔ ( ( 𝑃 ∈ ∪ 𝐵 ∧ 𝑄 ∈ ∪ 𝐵 ) ∧ 𝑃 ( ≃ph ‘ 𝐽 ) 𝑄 ) )
22	20 21	bitri	⊢ ( 𝑃 𝑅 𝑄 ↔ ( ( 𝑃 ∈ ∪ 𝐵 ∧ 𝑄 ∈ ∪ 𝐵 ) ∧ 𝑃 ( ≃ph ‘ 𝐽 ) 𝑄 ) )
23	19 22	sylib	⊢ ( ( 𝜑 ∧ ( 𝑀 𝑅 𝑁 ∧ 𝑃 𝑅 𝑄 ) ) → ( ( 𝑃 ∈ ∪ 𝐵 ∧ 𝑄 ∈ ∪ 𝐵 ) ∧ 𝑃 ( ≃ph ‘ 𝐽 ) 𝑄 ) )
24	23	simplld	⊢ ( ( 𝜑 ∧ ( 𝑀 𝑅 𝑁 ∧ 𝑃 𝑅 𝑄 ) ) → 𝑃 ∈ ∪ 𝐵 )
25	6 8 9 12 18 24	om1addcl	⊢ ( ( 𝜑 ∧ ( 𝑀 𝑅 𝑁 ∧ 𝑃 𝑅 𝑄 ) ) → ( 𝑀 ( *𝑝 ‘ 𝐽 ) 𝑃 ) ∈ ∪ 𝐵 )
26	17	simplrd	⊢ ( ( 𝜑 ∧ ( 𝑀 𝑅 𝑁 ∧ 𝑃 𝑅 𝑄 ) ) → 𝑁 ∈ ∪ 𝐵 )
27	23	simplrd	⊢ ( ( 𝜑 ∧ ( 𝑀 𝑅 𝑁 ∧ 𝑃 𝑅 𝑄 ) ) → 𝑄 ∈ ∪ 𝐵 )
28	6 8 9 12 26 27	om1addcl	⊢ ( ( 𝜑 ∧ ( 𝑀 𝑅 𝑁 ∧ 𝑃 𝑅 𝑄 ) ) → ( 𝑁 ( *𝑝 ‘ 𝐽 ) 𝑄 ) ∈ ∪ 𝐵 )
29	1 8 9 10	pi1eluni	⊢ ( ( 𝜑 ∧ ( 𝑀 𝑅 𝑁 ∧ 𝑃 𝑅 𝑄 ) ) → ( 𝑀 ∈ ∪ 𝐵 ↔ ( 𝑀 ∈ ( II Cn 𝐽 ) ∧ ( 𝑀 ‘ 0 ) = 𝑌 ∧ ( 𝑀 ‘ 1 ) = 𝑌 ) ) )
30	18 29	mpbid	⊢ ( ( 𝜑 ∧ ( 𝑀 𝑅 𝑁 ∧ 𝑃 𝑅 𝑄 ) ) → ( 𝑀 ∈ ( II Cn 𝐽 ) ∧ ( 𝑀 ‘ 0 ) = 𝑌 ∧ ( 𝑀 ‘ 1 ) = 𝑌 ) )
31	30	simp3d	⊢ ( ( 𝜑 ∧ ( 𝑀 𝑅 𝑁 ∧ 𝑃 𝑅 𝑄 ) ) → ( 𝑀 ‘ 1 ) = 𝑌 )
32	1 8 9 10	pi1eluni	⊢ ( ( 𝜑 ∧ ( 𝑀 𝑅 𝑁 ∧ 𝑃 𝑅 𝑄 ) ) → ( 𝑃 ∈ ∪ 𝐵 ↔ ( 𝑃 ∈ ( II Cn 𝐽 ) ∧ ( 𝑃 ‘ 0 ) = 𝑌 ∧ ( 𝑃 ‘ 1 ) = 𝑌 ) ) )
33	24 32	mpbid	⊢ ( ( 𝜑 ∧ ( 𝑀 𝑅 𝑁 ∧ 𝑃 𝑅 𝑄 ) ) → ( 𝑃 ∈ ( II Cn 𝐽 ) ∧ ( 𝑃 ‘ 0 ) = 𝑌 ∧ ( 𝑃 ‘ 1 ) = 𝑌 ) )
34	33	simp2d	⊢ ( ( 𝜑 ∧ ( 𝑀 𝑅 𝑁 ∧ 𝑃 𝑅 𝑄 ) ) → ( 𝑃 ‘ 0 ) = 𝑌 )
35	31 34	eqtr4d	⊢ ( ( 𝜑 ∧ ( 𝑀 𝑅 𝑁 ∧ 𝑃 𝑅 𝑄 ) ) → ( 𝑀 ‘ 1 ) = ( 𝑃 ‘ 0 ) )
36	17	simprd	⊢ ( ( 𝜑 ∧ ( 𝑀 𝑅 𝑁 ∧ 𝑃 𝑅 𝑄 ) ) → 𝑀 ( ≃ph ‘ 𝐽 ) 𝑁 )
37	23	simprd	⊢ ( ( 𝜑 ∧ ( 𝑀 𝑅 𝑁 ∧ 𝑃 𝑅 𝑄 ) ) → 𝑃 ( ≃ph ‘ 𝐽 ) 𝑄 )
38	35 36 37	pcohtpy	⊢ ( ( 𝜑 ∧ ( 𝑀 𝑅 𝑁 ∧ 𝑃 𝑅 𝑄 ) ) → ( 𝑀 ( *𝑝 ‘ 𝐽 ) 𝑃 ) ( ≃ph ‘ 𝐽 ) ( 𝑁 ( *𝑝 ‘ 𝐽 ) 𝑄 ) )
39	5	breqi	⊢ ( ( 𝑀 ( *𝑝 ‘ 𝐽 ) 𝑃 ) 𝑅 ( 𝑁 ( *𝑝 ‘ 𝐽 ) 𝑄 ) ↔ ( 𝑀 ( *𝑝 ‘ 𝐽 ) 𝑃 ) ( ( ≃ph ‘ 𝐽 ) ∩ ( ∪ 𝐵 × ∪ 𝐵 ) ) ( 𝑁 ( *𝑝 ‘ 𝐽 ) 𝑄 ) )
40		brinxp2	⊢ ( ( 𝑀 ( *𝑝 ‘ 𝐽 ) 𝑃 ) ( ( ≃ph ‘ 𝐽 ) ∩ ( ∪ 𝐵 × ∪ 𝐵 ) ) ( 𝑁 ( *𝑝 ‘ 𝐽 ) 𝑄 ) ↔ ( ( ( 𝑀 ( *𝑝 ‘ 𝐽 ) 𝑃 ) ∈ ∪ 𝐵 ∧ ( 𝑁 ( *𝑝 ‘ 𝐽 ) 𝑄 ) ∈ ∪ 𝐵 ) ∧ ( 𝑀 ( *𝑝 ‘ 𝐽 ) 𝑃 ) ( ≃ph ‘ 𝐽 ) ( 𝑁 ( *𝑝 ‘ 𝐽 ) 𝑄 ) ) )
41	39 40	bitri	⊢ ( ( 𝑀 ( *𝑝 ‘ 𝐽 ) 𝑃 ) 𝑅 ( 𝑁 ( *𝑝 ‘ 𝐽 ) 𝑄 ) ↔ ( ( ( 𝑀 ( *𝑝 ‘ 𝐽 ) 𝑃 ) ∈ ∪ 𝐵 ∧ ( 𝑁 ( *𝑝 ‘ 𝐽 ) 𝑄 ) ∈ ∪ 𝐵 ) ∧ ( 𝑀 ( *𝑝 ‘ 𝐽 ) 𝑃 ) ( ≃ph ‘ 𝐽 ) ( 𝑁 ( *𝑝 ‘ 𝐽 ) 𝑄 ) ) )
42	25 28 38 41	syl21anbrc	⊢ ( ( 𝜑 ∧ ( 𝑀 𝑅 𝑁 ∧ 𝑃 𝑅 𝑄 ) ) → ( 𝑀 ( *𝑝 ‘ 𝐽 ) 𝑃 ) 𝑅 ( 𝑁 ( *𝑝 ‘ 𝐽 ) 𝑄 ) )
43	6 8 9	om1plusg	⊢ ( ( 𝜑 ∧ ( 𝑀 𝑅 𝑁 ∧ 𝑃 𝑅 𝑄 ) ) → ( *𝑝 ‘ 𝐽 ) = ( +g ‘ 𝑂 ) )
44	43 7	eqtr4di	⊢ ( ( 𝜑 ∧ ( 𝑀 𝑅 𝑁 ∧ 𝑃 𝑅 𝑄 ) ) → ( *𝑝 ‘ 𝐽 ) = + )
45	44	oveqd	⊢ ( ( 𝜑 ∧ ( 𝑀 𝑅 𝑁 ∧ 𝑃 𝑅 𝑄 ) ) → ( 𝑀 ( *𝑝 ‘ 𝐽 ) 𝑃 ) = ( 𝑀 + 𝑃 ) )
46	44	oveqd	⊢ ( ( 𝜑 ∧ ( 𝑀 𝑅 𝑁 ∧ 𝑃 𝑅 𝑄 ) ) → ( 𝑁 ( *𝑝 ‘ 𝐽 ) 𝑄 ) = ( 𝑁 + 𝑄 ) )
47	42 45 46	3brtr3d	⊢ ( ( 𝜑 ∧ ( 𝑀 𝑅 𝑁 ∧ 𝑃 𝑅 𝑄 ) ) → ( 𝑀 + 𝑃 ) 𝑅 ( 𝑁 + 𝑄 ) )
48	47	ex	⊢ ( 𝜑 → ( ( 𝑀 𝑅 𝑁 ∧ 𝑃 𝑅 𝑄 ) → ( 𝑀 + 𝑃 ) 𝑅 ( 𝑁 + 𝑄 ) ) )