Theorem grppropstr

Description: Generalize a specific 2-element group L to show that any set K with the same (relevant) properties is also a group. (Contributed by NM, 28-Oct-2012) (Revised by Mario Carneiro, 6-Jan-2015)

	Ref	Expression
Hypotheses	grppropstr.b	$$⊢{\mathrm{Base}}_K=B$$
	grppropstr.p	$$⊢{+}_K=\underset{\dot{}}{+}$$
	grppropstr.l	$$⊢L=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{+}⟩\right\}$$
Assertion	grppropstr	$$⊢K\in \mathrm{Grp}\leftrightarrow L\in \mathrm{Grp}$$

Proof

Step	Hyp	Ref	Expression
1		grppropstr.b	$$⊢{\mathrm{Base}}_K=B$$
2		grppropstr.p	$$⊢{+}_K=\underset{\dot{}}{+}$$
3		grppropstr.l	$$⊢L=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{+}⟩\right\}$$
4		fvex	$$⊢{\mathrm{Base}}_K\in \mathrm{V}$$
5	1 4	eqeltrri	$$⊢B\in \mathrm{V}$$
6	3	grpbase	$$⊢B\in \mathrm{V}\to B={\mathrm{Base}}_L$$
7	5 6	ax-mp	$$⊢B={\mathrm{Base}}_L$$
8	1 7	eqtri	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_L$$
9		fvex	$$⊢{+}_K\in \mathrm{V}$$
10	2 9	eqeltrri	$$⊢\underset{\dot{}}{+}\in \mathrm{V}$$
11	3	grpplusg	$$⊢\underset{\dot{}}{+}\in \mathrm{V}\to \underset{\dot{}}{+}={+}_L$$
12	10 11	ax-mp	$$⊢\underset{\dot{}}{+}={+}_L$$
13	2 12	eqtri	$$⊢{+}_K={+}_L$$
14	8 13	grpprop	$$⊢K\in \mathrm{Grp}\leftrightarrow L\in \mathrm{Grp}$$