Theorem om1plusg

Description: The group operation (which isn't much more than a magma) of the loop space. (Contributed by Mario Carneiro, 11-Feb-2015)

	Ref	Expression
Hypotheses	om1bas.o	|- O = ( J Om1 Y )
	om1bas.j	|- ( ph -> J e. ( TopOn ` X ) )
	om1bas.y	|- ( ph -> Y e. X )
Assertion	om1plusg	|- ( ph -> ( *p ` J ) = ( +g ` O ) )

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		fvex	|- ( *p ` J ) e. _V
5		eqid	|- { <. ( Base ` ndx ) , ( Base ` O ) >. , <. ( +g ` ndx ) , ( *p ` J ) >. , <. ( TopSet ` ndx ) , ( J ^ko II ) >. } = { <. ( Base ` ndx ) , ( Base ` O ) >. , <. ( +g ` ndx ) , ( *p ` J ) >. , <. ( TopSet ` ndx ) , ( J ^ko II ) >. }
6	5	topgrpplusg	|- ( ( *p ` J ) e. _V -> ( *p ` J ) = ( +g ` { <. ( Base ` ndx ) , ( Base ` O ) >. , <. ( +g ` ndx ) , ( *p ` J ) >. , <. ( TopSet ` ndx ) , ( J ^ko II ) >. } ) )
7	4 6	ax-mp	|- ( *p ` J ) = ( +g ` { <. ( Base ` ndx ) , ( Base ` O ) >. , <. ( +g ` ndx ) , ( *p ` J ) >. , <. ( TopSet ` ndx ) , ( J ^ko II ) >. } )
8		eqidd	|- ( ph -> ( Base ` O ) = ( Base ` O ) )
9	1 2 3 8	om1bas	|- ( ph -> ( Base ` O ) = { f e. ( II Cn J ) | ( ( f ` 0 ) = Y /\ ( f ` 1 ) = Y ) } )
10		eqidd	|- ( ph -> ( *p ` J ) = ( *p ` J ) )
11		eqidd	|- ( ph -> ( J ^ko II ) = ( J ^ko II ) )
12	1 9 10 11 2 3	om1val	|- ( ph -> O = { <. ( Base ` ndx ) , ( Base ` O ) >. , <. ( +g ` ndx ) , ( *p ` J ) >. , <. ( TopSet ` ndx ) , ( J ^ko II ) >. } )
13	12	fveq2d	|- ( ph -> ( +g ` O ) = ( +g ` { <. ( Base ` ndx ) , ( Base ` O ) >. , <. ( +g ` ndx ) , ( *p ` J ) >. , <. ( TopSet ` ndx ) , ( J ^ko II ) >. } ) )
14	7 13	eqtr4id	|- ( ph -> ( *p ` J ) = ( +g ` O ) )