isgrpd

Description: Deduce a group from its properties. Unlike isgrpd2 , this one goes straight from the base properties rather than going through Mnd . N (negative) is normally dependent on x i.e. read it as N ( x ) . (Contributed by NM, 6-Jun-2013) (Revised by Mario Carneiro, 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$
	isgrpd.n	$⊢ (φ \land x \in B) \to N \in B$
	isgrpd.j	$⊢ (φ \land x \in B) \to N \underset{˙}{+} x = \underset{˙}{0}$
Assertion	isgrpd	$⊢ φ \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		isgrpd.n	$⊢ (φ \land x \in B) \to N \in B$
8		isgrpd.j	$⊢ (φ \land x \in B) \to N \underset{˙}{+} x = \underset{˙}{0}$
9		oveq1	$⊢ y = N \to y \underset{˙}{+} x = N \underset{˙}{+} x$
10	9	eqeq1d	$⊢ y = N \to (y \underset{˙}{+} x = \underset{˙}{0} \leftrightarrow N \underset{˙}{+} x = \underset{˙}{0})$
11	10	rspcev	$⊢ (N \in B \land N \underset{˙}{+} x = \underset{˙}{0}) \to \exists y \in B y \underset{˙}{+} x = \underset{˙}{0}$
12	7 8 11	syl2anc	$⊢ (φ \land x \in B) \to \exists y \in B y \underset{˙}{+} x = \underset{˙}{0}$
13	1 2 3 4 5 6 12	isgrpde	$⊢ φ \to G \in Grp$

Metamath Proof Explorer

Theorem isgrpd

Proof