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	|- O = ( J Om1 Y )
	om1bas.j	|- ( ph -> J e. ( TopOn ` X ) )
	om1bas.y	|- ( ph -> Y e. X )
	om1bas.b	|- ( ph -> B = ( Base ` O ) )
	om1addcl.h	|- ( ph -> H e. B )
	om1addcl.k	|- ( ph -> K e. B )
Assertion	om1addcl	|- ( ph -> ( H ( *p ` J ) K ) e. B )

Proof

Step	Hyp	Ref	Expression
1		om1bas.o	|- O = ( J Om1 Y )
2		om1bas.j	|- ( ph -> J e. ( TopOn ` X ) )
3		om1bas.y	|- ( ph -> Y e. X )
4		om1bas.b	|- ( ph -> B = ( Base ` O ) )
5		om1addcl.h	|- ( ph -> H e. B )
6		om1addcl.k	|- ( ph -> K e. B )
7	1 2 3 4	om1elbas	|- ( ph -> ( H e. B <-> ( H e. ( II Cn J ) /\ ( H ` 0 ) = Y /\ ( H ` 1 ) = Y ) ) )
8	5 7	mpbid	|- ( ph -> ( H e. ( II Cn J ) /\ ( H ` 0 ) = Y /\ ( H ` 1 ) = Y ) )
9	8	simp1d	|- ( ph -> H e. ( II Cn J ) )
10	1 2 3 4	om1elbas	|- ( ph -> ( K e. B <-> ( K e. ( II Cn J ) /\ ( K ` 0 ) = Y /\ ( K ` 1 ) = Y ) ) )
11	6 10	mpbid	|- ( ph -> ( K e. ( II Cn J ) /\ ( K ` 0 ) = Y /\ ( K ` 1 ) = Y ) )
12	11	simp1d	|- ( ph -> K e. ( II Cn J ) )
13	8	simp3d	|- ( ph -> ( H ` 1 ) = Y )
14	11	simp2d	|- ( ph -> ( K ` 0 ) = Y )
15	13 14	eqtr4d	|- ( ph -> ( H ` 1 ) = ( K ` 0 ) )
16	9 12 15	pcocn	|- ( ph -> ( H ( *p ` J ) K ) e. ( II Cn J ) )
17	9 12	pco0	|- ( ph -> ( ( H ( *p ` J ) K ) ` 0 ) = ( H ` 0 ) )
18	8	simp2d	|- ( ph -> ( H ` 0 ) = Y )
19	17 18	eqtrd	|- ( ph -> ( ( H ( *p ` J ) K ) ` 0 ) = Y )
20	9 12	pco1	|- ( ph -> ( ( H ( *p ` J ) K ) ` 1 ) = ( K ` 1 ) )
21	11	simp3d	|- ( ph -> ( K ` 1 ) = Y )
22	20 21	eqtrd	|- ( ph -> ( ( H ( *p ` J ) K ) ` 1 ) = Y )
23	1 2 3 4	om1elbas	|- ( ph -> ( ( H ( *p ` J ) K ) e. B <-> ( ( H ( *p ` J ) K ) e. ( II Cn J ) /\ ( ( H ( *p ` J ) K ) ` 0 ) = Y /\ ( ( H ( *p ` J ) K ) ` 1 ) = Y ) ) )
24	16 19 22 23	mpbir3and	|- ( ph -> ( H ( *p ` J ) K ) e. B )