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

Metamath Proof Explorer

Theorem isgrpde

Description: Deduce a group from its properties. In this version of isgrpd , we don't assume there is an expression for the inverse of x . (Contributed by NM, 6-Jan-2015)

		Ref	Expression
	Hypotheses	isgrpd.b	$⊢ φ \to B = {Base}_{G}$
		isgrpd.p	$⊢ φ \to \underset{˙}{+} = +_{G}$
		isgrpd.c	$⊢ (φ \land x \in B \land y \in B) \to x \underset{˙}{+} y \in B$
		isgrpd.a	$⊢ (φ \land (x \in B \land y \in B \land z \in B)) \to (x \underset{˙}{+} y) \underset{˙}{+} z = x \underset{˙}{+} (y \underset{˙}{+} z)$
		isgrpd.z	$⊢ φ \to \underset{˙}{0} \in B$
		isgrpd.i	$⊢ (φ \land x \in B) \to \underset{˙}{0} \underset{˙}{+} x = x$
		isgrpde.n	$⊢ (φ \land x \in B) \to \exists y \in B y \underset{˙}{+} x = \underset{˙}{0}$
	Assertion	isgrpde	$⊢ φ \to G \in Grp$

Proof

Step	Hyp	Ref	Expression
1		isgrpd.b	$⊢ φ \to B = {Base}_{G}$
2		isgrpd.p	$⊢ φ \to \underset{˙}{+} = +_{G}$
3		isgrpd.c	$⊢ (φ \land x \in B \land y \in B) \to x \underset{˙}{+} y \in B$
4		isgrpd.a	$⊢ (φ \land (x \in B \land y \in B \land z \in B)) \to (x \underset{˙}{+} y) \underset{˙}{+} z = x \underset{˙}{+} (y \underset{˙}{+} z)$
5		isgrpd.z	$⊢ φ \to \underset{˙}{0} \in B$
6		isgrpd.i	$⊢ (φ \land x \in B) \to \underset{˙}{0} \underset{˙}{+} x = x$
7		isgrpde.n	$⊢ (φ \land x \in B) \to \exists y \in B y \underset{˙}{+} x = \underset{˙}{0}$
8	3 5 6 4 7	grprida	$⊢ (φ \land x \in B) \to x \underset{˙}{+} \underset{˙}{0} = x$
9	1 2 5 6 8	grpidd	$⊢ φ \to \underset{˙}{0} = 0_{G}$
10	1 2 3 4 5 6 8	ismndd	$⊢ φ \to G \in Mnd$
11	1 2 9 10 7	isgrpd2e	$⊢ φ \to G \in Grp$