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	⊢ 𝑂 = ( 𝐽 Ω1 𝑌 )
	om1bas.j	⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
	om1bas.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑋 )
Assertion	om1plusg	⊢ ( 𝜑 → ( *𝑝 ‘ 𝐽 ) = ( +g ‘ 𝑂 ) )

Proof

Step	Hyp	Ref	Expression
1		om1bas.o	⊢ 𝑂 = ( 𝐽 Ω1 𝑌 )
2		om1bas.j	⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
3		om1bas.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑋 )
4		fvex	⊢ ( *𝑝 ‘ 𝐽 ) ∈ V
5		eqid	⊢ { ⟨ ( Base ‘ ndx ) , ( Base ‘ 𝑂 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( *𝑝 ‘ 𝐽 ) ⟩ , ⟨ ( TopSet ‘ ndx ) , ( 𝐽 ↑ko II ) ⟩ } = { ⟨ ( Base ‘ ndx ) , ( Base ‘ 𝑂 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( *𝑝 ‘ 𝐽 ) ⟩ , ⟨ ( TopSet ‘ ndx ) , ( 𝐽 ↑ko II ) ⟩ }
6	5	topgrpplusg	⊢ ( ( *𝑝 ‘ 𝐽 ) ∈ V → ( *𝑝 ‘ 𝐽 ) = ( +g ‘ { ⟨ ( Base ‘ ndx ) , ( Base ‘ 𝑂 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( *𝑝 ‘ 𝐽 ) ⟩ , ⟨ ( TopSet ‘ ndx ) , ( 𝐽 ↑ko II ) ⟩ } ) )
7	4 6	ax-mp	⊢ ( *𝑝 ‘ 𝐽 ) = ( +g ‘ { ⟨ ( Base ‘ ndx ) , ( Base ‘ 𝑂 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( *𝑝 ‘ 𝐽 ) ⟩ , ⟨ ( TopSet ‘ ndx ) , ( 𝐽 ↑ko II ) ⟩ } )
8		eqidd	⊢ ( 𝜑 → ( Base ‘ 𝑂 ) = ( Base ‘ 𝑂 ) )
9	1 2 3 8	om1bas	⊢ ( 𝜑 → ( Base ‘ 𝑂 ) = { 𝑓 ∈ ( II Cn 𝐽 ) ∣ ( ( 𝑓 ‘ 0 ) = 𝑌 ∧ ( 𝑓 ‘ 1 ) = 𝑌 ) } )
10		eqidd	⊢ ( 𝜑 → ( *𝑝 ‘ 𝐽 ) = ( *𝑝 ‘ 𝐽 ) )
11		eqidd	⊢ ( 𝜑 → ( 𝐽 ↑ko II ) = ( 𝐽 ↑ko II ) )
12	1 9 10 11 2 3	om1val	⊢ ( 𝜑 → 𝑂 = { ⟨ ( Base ‘ ndx ) , ( Base ‘ 𝑂 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( *𝑝 ‘ 𝐽 ) ⟩ , ⟨ ( TopSet ‘ ndx ) , ( 𝐽 ↑ko II ) ⟩ } )
13	12	fveq2d	⊢ ( 𝜑 → ( +g ‘ 𝑂 ) = ( +g ‘ { ⟨ ( Base ‘ ndx ) , ( Base ‘ 𝑂 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( *𝑝 ‘ 𝐽 ) ⟩ , ⟨ ( TopSet ‘ ndx ) , ( 𝐽 ↑ko II ) ⟩ } ) )
14	7 13	eqtr4id	⊢ ( 𝜑 → ( *𝑝 ‘ 𝐽 ) = ( +g ‘ 𝑂 ) )