This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	$⊢ {Base}_{K} = B$
		grppropstr.p	$⊢ +_{K} = \underset{˙}{+}$
		grppropstr.l	$⊢ L = \{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, \underset{˙}{+}⟩\}$
	Assertion	grppropstr	$⊢ K \in Grp \leftrightarrow L \in Grp$

Proof

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