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{\Omega }_{1}Y$$
	om1bas.j	$$⊢\phi \to J\in \mathrm{TopOn}\left(X\right)$$
	om1bas.y	$$⊢\phi \to Y\in X$$
Assertion	om1plusg	$$⊢\phi \to {*}_{𝑝}\left(J\right)={+}_O$$

Proof

Step	Hyp	Ref	Expression
1		om1bas.o	$$⊢O=J{\Omega }_{1}Y$$
2		om1bas.j	$$⊢\phi \to J\in \mathrm{TopOn}\left(X\right)$$
3		om1bas.y	$$⊢\phi \to Y\in X$$
4		fvex	$$⊢{*}_{𝑝}\left(J\right)\in \mathrm{V}$$
5		eqid	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{\mathrm{Base}}_O⟩,⟨{+}_{\mathrm{ndx}},{*}_{𝑝}\left(J\right)⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),J{^}_{\mathrm{ko}}\mathrm{II}⟩\right\}=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{\mathrm{Base}}_O⟩,⟨{+}_{\mathrm{ndx}},{*}_{𝑝}\left(J\right)⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),J{^}_{\mathrm{ko}}\mathrm{II}⟩\right\}$$
6	5	topgrpplusg	$$⊢{*}_{𝑝}\left(J\right)\in \mathrm{V}\to {*}_{𝑝}\left(J\right)={+}_{\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{\mathrm{Base}}_O⟩,⟨{+}_{\mathrm{ndx}},{*}_{𝑝}\left(J\right)⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),J{^}_{\mathrm{ko}}\mathrm{II}⟩\right\}}$$
7	4 6	ax-mp	$$⊢{*}_{𝑝}\left(J\right)={+}_{\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{\mathrm{Base}}_O⟩,⟨{+}_{\mathrm{ndx}},{*}_{𝑝}\left(J\right)⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),J{^}_{\mathrm{ko}}\mathrm{II}⟩\right\}}$$
8		eqidd	$$⊢\phi \to {\mathrm{Base}}_O={\mathrm{Base}}_O$$
9	1 2 3 8	om1bas	$$⊢\phi \to {\mathrm{Base}}_O=\left\{f\in \left(\mathrm{II}\mathrm{Cn}J\right)|\left(f\left(0\right)=Y\wedge f\left(1\right)=Y\right)\right\}$$
10		eqidd	$$⊢\phi \to {*}_{𝑝}\left(J\right)={*}_{𝑝}\left(J\right)$$
11		eqidd	$$⊢\phi \to J{^}_{\mathrm{ko}}\mathrm{II}=J{^}_{\mathrm{ko}}\mathrm{II}$$
12	1 9 10 11 2 3	om1val	$$⊢\phi \to O=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{\mathrm{Base}}_O⟩,⟨{+}_{\mathrm{ndx}},{*}_{𝑝}\left(J\right)⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),J{^}_{\mathrm{ko}}\mathrm{II}⟩\right\}$$
13	12	fveq2d	$$⊢\phi \to {+}_O={+}_{\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{\mathrm{Base}}_O⟩,⟨{+}_{\mathrm{ndx}},{*}_{𝑝}\left(J\right)⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),J{^}_{\mathrm{ko}}\mathrm{II}⟩\right\}}$$
14	7 13	eqtr4id	$$⊢\phi \to {*}_{𝑝}\left(J\right)={+}_O$$