Theorem om1addcl

Description: Closure of the group operation of the loop space. (Contributed by Jeff Madsen, 11-Jun-2010) (Revised by Mario Carneiro, 5-Sep-2015)

	Ref	Expression
Hypotheses	om1bas.o	⊢ 𝑂 = ( 𝐽 Ω1 𝑌 )
	om1bas.j	⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
	om1bas.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑋 )
	om1bas.b	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝑂 ) )
	om1addcl.h	⊢ ( 𝜑 → 𝐻 ∈ 𝐵 )
	om1addcl.k	⊢ ( 𝜑 → 𝐾 ∈ 𝐵 )
Assertion	om1addcl	⊢ ( 𝜑 → ( 𝐻 ( *𝑝 ‘ 𝐽 ) 𝐾 ) ∈ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		om1bas.o	⊢ 𝑂 = ( 𝐽 Ω1 𝑌 )
2		om1bas.j	⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
3		om1bas.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑋 )
4		om1bas.b	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝑂 ) )
5		om1addcl.h	⊢ ( 𝜑 → 𝐻 ∈ 𝐵 )
6		om1addcl.k	⊢ ( 𝜑 → 𝐾 ∈ 𝐵 )
7	1 2 3 4	om1elbas	⊢ ( 𝜑 → ( 𝐻 ∈ 𝐵 ↔ ( 𝐻 ∈ ( II Cn 𝐽 ) ∧ ( 𝐻 ‘ 0 ) = 𝑌 ∧ ( 𝐻 ‘ 1 ) = 𝑌 ) ) )
8	5 7	mpbid	⊢ ( 𝜑 → ( 𝐻 ∈ ( II Cn 𝐽 ) ∧ ( 𝐻 ‘ 0 ) = 𝑌 ∧ ( 𝐻 ‘ 1 ) = 𝑌 ) )
9	8	simp1d	⊢ ( 𝜑 → 𝐻 ∈ ( II Cn 𝐽 ) )
10	1 2 3 4	om1elbas	⊢ ( 𝜑 → ( 𝐾 ∈ 𝐵 ↔ ( 𝐾 ∈ ( II Cn 𝐽 ) ∧ ( 𝐾 ‘ 0 ) = 𝑌 ∧ ( 𝐾 ‘ 1 ) = 𝑌 ) ) )
11	6 10	mpbid	⊢ ( 𝜑 → ( 𝐾 ∈ ( II Cn 𝐽 ) ∧ ( 𝐾 ‘ 0 ) = 𝑌 ∧ ( 𝐾 ‘ 1 ) = 𝑌 ) )
12	11	simp1d	⊢ ( 𝜑 → 𝐾 ∈ ( II Cn 𝐽 ) )
13	8	simp3d	⊢ ( 𝜑 → ( 𝐻 ‘ 1 ) = 𝑌 )
14	11	simp2d	⊢ ( 𝜑 → ( 𝐾 ‘ 0 ) = 𝑌 )
15	13 14	eqtr4d	⊢ ( 𝜑 → ( 𝐻 ‘ 1 ) = ( 𝐾 ‘ 0 ) )
16	9 12 15	pcocn	⊢ ( 𝜑 → ( 𝐻 ( *𝑝 ‘ 𝐽 ) 𝐾 ) ∈ ( II Cn 𝐽 ) )
17	9 12	pco0	⊢ ( 𝜑 → ( ( 𝐻 ( *𝑝 ‘ 𝐽 ) 𝐾 ) ‘ 0 ) = ( 𝐻 ‘ 0 ) )
18	8	simp2d	⊢ ( 𝜑 → ( 𝐻 ‘ 0 ) = 𝑌 )
19	17 18	eqtrd	⊢ ( 𝜑 → ( ( 𝐻 ( *𝑝 ‘ 𝐽 ) 𝐾 ) ‘ 0 ) = 𝑌 )
20	9 12	pco1	⊢ ( 𝜑 → ( ( 𝐻 ( *𝑝 ‘ 𝐽 ) 𝐾 ) ‘ 1 ) = ( 𝐾 ‘ 1 ) )
21	11	simp3d	⊢ ( 𝜑 → ( 𝐾 ‘ 1 ) = 𝑌 )
22	20 21	eqtrd	⊢ ( 𝜑 → ( ( 𝐻 ( *𝑝 ‘ 𝐽 ) 𝐾 ) ‘ 1 ) = 𝑌 )
23	1 2 3 4	om1elbas	⊢ ( 𝜑 → ( ( 𝐻 ( *𝑝 ‘ 𝐽 ) 𝐾 ) ∈ 𝐵 ↔ ( ( 𝐻 ( *𝑝 ‘ 𝐽 ) 𝐾 ) ∈ ( II Cn 𝐽 ) ∧ ( ( 𝐻 ( *𝑝 ‘ 𝐽 ) 𝐾 ) ‘ 0 ) = 𝑌 ∧ ( ( 𝐻 ( *𝑝 ‘ 𝐽 ) 𝐾 ) ‘ 1 ) = 𝑌 ) ) )
24	16 19 22 23	mpbir3and	⊢ ( 𝜑 → ( 𝐻 ( *𝑝 ‘ 𝐽 ) 𝐾 ) ∈ 𝐵 )