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	⊢ 𝐺 = ( 𝐽 π1 𝑌 )
	elpi1.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
	elpi1.1	⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
	elpi1.2	⊢ ( 𝜑 → 𝑌 ∈ 𝑋 )
	pi1addf.p	⊢ + = ( +g ‘ 𝐺 )
Assertion	pi1addf	⊢ ( 𝜑 → + : ( 𝐵 × 𝐵 ) ⟶ 𝐵 )

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		eqidd	⊢ ( 𝜑 → ( ( 𝐽 Ω1 𝑌 ) /s ( ≃ph ‘ 𝐽 ) ) = ( ( 𝐽 Ω1 𝑌 ) /s ( ≃ph ‘ 𝐽 ) ) )
7		eqidd	⊢ ( 𝜑 → ( Base ‘ ( 𝐽 Ω1 𝑌 ) ) = ( Base ‘ ( 𝐽 Ω1 𝑌 ) ) )
8		fvexd	⊢ ( 𝜑 → ( ≃ph ‘ 𝐽 ) ∈ V )
9		ovexd	⊢ ( 𝜑 → ( 𝐽 Ω1 𝑌 ) ∈ V )
10		eqid	⊢ ( 𝐽 Ω1 𝑌 ) = ( 𝐽 Ω1 𝑌 )
11	2	a1i	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐺 ) )
12	1 3 4 10 11 7	pi1blem	⊢ ( 𝜑 → ( ( ( ≃ph ‘ 𝐽 ) “ ( Base ‘ ( 𝐽 Ω1 𝑌 ) ) ) ⊆ ( Base ‘ ( 𝐽 Ω1 𝑌 ) ) ∧ ( Base ‘ ( 𝐽 Ω1 𝑌 ) ) ⊆ ( II Cn 𝐽 ) ) )
13	12	simpld	⊢ ( 𝜑 → ( ( ≃ph ‘ 𝐽 ) “ ( Base ‘ ( 𝐽 Ω1 𝑌 ) ) ) ⊆ ( Base ‘ ( 𝐽 Ω1 𝑌 ) ) )
14	6 7 8 9 13	qusin	⊢ ( 𝜑 → ( ( 𝐽 Ω1 𝑌 ) /s ( ≃ph ‘ 𝐽 ) ) = ( ( 𝐽 Ω1 𝑌 ) /s ( ( ≃ph ‘ 𝐽 ) ∩ ( ( Base ‘ ( 𝐽 Ω1 𝑌 ) ) × ( Base ‘ ( 𝐽 Ω1 𝑌 ) ) ) ) ) )
15	1 3 4 10	pi1val	⊢ ( 𝜑 → 𝐺 = ( ( 𝐽 Ω1 𝑌 ) /s ( ≃ph ‘ 𝐽 ) ) )
16	1 3 4 10 11 7	pi1buni	⊢ ( 𝜑 → ∪ 𝐵 = ( Base ‘ ( 𝐽 Ω1 𝑌 ) ) )
17	16	sqxpeqd	⊢ ( 𝜑 → ( ∪ 𝐵 × ∪ 𝐵 ) = ( ( Base ‘ ( 𝐽 Ω1 𝑌 ) ) × ( Base ‘ ( 𝐽 Ω1 𝑌 ) ) ) )
18	17	ineq2d	⊢ ( 𝜑 → ( ( ≃ph ‘ 𝐽 ) ∩ ( ∪ 𝐵 × ∪ 𝐵 ) ) = ( ( ≃ph ‘ 𝐽 ) ∩ ( ( Base ‘ ( 𝐽 Ω1 𝑌 ) ) × ( Base ‘ ( 𝐽 Ω1 𝑌 ) ) ) ) )
19	18	oveq2d	⊢ ( 𝜑 → ( ( 𝐽 Ω1 𝑌 ) /s ( ( ≃ph ‘ 𝐽 ) ∩ ( ∪ 𝐵 × ∪ 𝐵 ) ) ) = ( ( 𝐽 Ω1 𝑌 ) /s ( ( ≃ph ‘ 𝐽 ) ∩ ( ( Base ‘ ( 𝐽 Ω1 𝑌 ) ) × ( Base ‘ ( 𝐽 Ω1 𝑌 ) ) ) ) ) )
20	14 15 19	3eqtr4d	⊢ ( 𝜑 → 𝐺 = ( ( 𝐽 Ω1 𝑌 ) /s ( ( ≃ph ‘ 𝐽 ) ∩ ( ∪ 𝐵 × ∪ 𝐵 ) ) ) )
21		phtpcer	⊢ ( ≃ph ‘ 𝐽 ) Er ( II Cn 𝐽 )
22	21	a1i	⊢ ( 𝜑 → ( ≃ph ‘ 𝐽 ) Er ( II Cn 𝐽 ) )
23	12	simprd	⊢ ( 𝜑 → ( Base ‘ ( 𝐽 Ω1 𝑌 ) ) ⊆ ( II Cn 𝐽 ) )
24	16 23	eqsstrd	⊢ ( 𝜑 → ∪ 𝐵 ⊆ ( II Cn 𝐽 ) )
25	22 24	erinxp	⊢ ( 𝜑 → ( ( ≃ph ‘ 𝐽 ) ∩ ( ∪ 𝐵 × ∪ 𝐵 ) ) Er ∪ 𝐵 )
26		eqid	⊢ ( ( ≃ph ‘ 𝐽 ) ∩ ( ∪ 𝐵 × ∪ 𝐵 ) ) = ( ( ≃ph ‘ 𝐽 ) ∩ ( ∪ 𝐵 × ∪ 𝐵 ) )
27		eqid	⊢ ( +g ‘ ( 𝐽 Ω1 𝑌 ) ) = ( +g ‘ ( 𝐽 Ω1 𝑌 ) )
28	1 3 4 11 26 10 27	pi1cpbl	⊢ ( 𝜑 → ( ( 𝑎 ( ( ≃ph ‘ 𝐽 ) ∩ ( ∪ 𝐵 × ∪ 𝐵 ) ) 𝑐 ∧ 𝑏 ( ( ≃ph ‘ 𝐽 ) ∩ ( ∪ 𝐵 × ∪ 𝐵 ) ) 𝑑 ) → ( 𝑎 ( +g ‘ ( 𝐽 Ω1 𝑌 ) ) 𝑏 ) ( ( ≃ph ‘ 𝐽 ) ∩ ( ∪ 𝐵 × ∪ 𝐵 ) ) ( 𝑐 ( +g ‘ ( 𝐽 Ω1 𝑌 ) ) 𝑑 ) ) )
29	3	adantr	⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ∪ 𝐵 ∧ 𝑑 ∈ ∪ 𝐵 ) ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
30	4	adantr	⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ∪ 𝐵 ∧ 𝑑 ∈ ∪ 𝐵 ) ) → 𝑌 ∈ 𝑋 )
31	10 29 30	om1plusg	⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ∪ 𝐵 ∧ 𝑑 ∈ ∪ 𝐵 ) ) → ( *𝑝 ‘ 𝐽 ) = ( +g ‘ ( 𝐽 Ω1 𝑌 ) ) )
32	31	oveqd	⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ∪ 𝐵 ∧ 𝑑 ∈ ∪ 𝐵 ) ) → ( 𝑐 ( *𝑝 ‘ 𝐽 ) 𝑑 ) = ( 𝑐 ( +g ‘ ( 𝐽 Ω1 𝑌 ) ) 𝑑 ) )
33	16	adantr	⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ∪ 𝐵 ∧ 𝑑 ∈ ∪ 𝐵 ) ) → ∪ 𝐵 = ( Base ‘ ( 𝐽 Ω1 𝑌 ) ) )
34		simprl	⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ∪ 𝐵 ∧ 𝑑 ∈ ∪ 𝐵 ) ) → 𝑐 ∈ ∪ 𝐵 )
35		simprr	⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ∪ 𝐵 ∧ 𝑑 ∈ ∪ 𝐵 ) ) → 𝑑 ∈ ∪ 𝐵 )
36	10 29 30 33 34 35	om1addcl	⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ∪ 𝐵 ∧ 𝑑 ∈ ∪ 𝐵 ) ) → ( 𝑐 ( *𝑝 ‘ 𝐽 ) 𝑑 ) ∈ ∪ 𝐵 )
37	32 36	eqeltrrd	⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ∪ 𝐵 ∧ 𝑑 ∈ ∪ 𝐵 ) ) → ( 𝑐 ( +g ‘ ( 𝐽 Ω1 𝑌 ) ) 𝑑 ) ∈ ∪ 𝐵 )
38	20 16 25 9 28 37 27 5	qusaddf	⊢ ( 𝜑 → + : ( ( ∪ 𝐵 / ( ( ≃ph ‘ 𝐽 ) ∩ ( ∪ 𝐵 × ∪ 𝐵 ) ) ) × ( ∪ 𝐵 / ( ( ≃ph ‘ 𝐽 ) ∩ ( ∪ 𝐵 × ∪ 𝐵 ) ) ) ) ⟶ ( ∪ 𝐵 / ( ( ≃ph ‘ 𝐽 ) ∩ ( ∪ 𝐵 × ∪ 𝐵 ) ) ) )
39	1 3 4 11 26	pi1bas3	⊢ ( 𝜑 → 𝐵 = ( ∪ 𝐵 / ( ( ≃ph ‘ 𝐽 ) ∩ ( ∪ 𝐵 × ∪ 𝐵 ) ) ) )
40	39	sqxpeqd	⊢ ( 𝜑 → ( 𝐵 × 𝐵 ) = ( ( ∪ 𝐵 / ( ( ≃ph ‘ 𝐽 ) ∩ ( ∪ 𝐵 × ∪ 𝐵 ) ) ) × ( ∪ 𝐵 / ( ( ≃ph ‘ 𝐽 ) ∩ ( ∪ 𝐵 × ∪ 𝐵 ) ) ) ) )
41	40	feq2d	⊢ ( 𝜑 → ( + : ( 𝐵 × 𝐵 ) ⟶ ( ∪ 𝐵 / ( ( ≃ph ‘ 𝐽 ) ∩ ( ∪ 𝐵 × ∪ 𝐵 ) ) ) ↔ + : ( ( ∪ 𝐵 / ( ( ≃ph ‘ 𝐽 ) ∩ ( ∪ 𝐵 × ∪ 𝐵 ) ) ) × ( ∪ 𝐵 / ( ( ≃ph ‘ 𝐽 ) ∩ ( ∪ 𝐵 × ∪ 𝐵 ) ) ) ) ⟶ ( ∪ 𝐵 / ( ( ≃ph ‘ 𝐽 ) ∩ ( ∪ 𝐵 × ∪ 𝐵 ) ) ) ) )
42	38 41	mpbird	⊢ ( 𝜑 → + : ( 𝐵 × 𝐵 ) ⟶ ( ∪ 𝐵 / ( ( ≃ph ‘ 𝐽 ) ∩ ( ∪ 𝐵 × ∪ 𝐵 ) ) ) )
43	39	feq3d	⊢ ( 𝜑 → ( + : ( 𝐵 × 𝐵 ) ⟶ 𝐵 ↔ + : ( 𝐵 × 𝐵 ) ⟶ ( ∪ 𝐵 / ( ( ≃ph ‘ 𝐽 ) ∩ ( ∪ 𝐵 × ∪ 𝐵 ) ) ) ) )
44	42 43	mpbird	⊢ ( 𝜑 → + : ( 𝐵 × 𝐵 ) ⟶ 𝐵 )