isgrpi

Description: Properties that determine a group. N (negative) is normally dependent on x i.e. read it as N ( x ) . (Contributed by NM, 3-Sep-2011)

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

Step	Hyp	Ref	Expression
1		isgrpi.b	$⊢ B = {Base}_{G}$
2		isgrpi.p	$⊢ \underset{˙}{+} = +_{G}$
3		isgrpi.c	$⊢ (x \in B \land y \in B) \to x \underset{˙}{+} y \in B$
4		isgrpi.a	$⊢ (x \in B \land y \in B \land z \in B) \to (x \underset{˙}{+} y) \underset{˙}{+} z = x \underset{˙}{+} (y \underset{˙}{+} z)$
5		isgrpi.z	$⊢ \underset{˙}{0} \in B$
6		isgrpi.i	$⊢ x \in B \to \underset{˙}{0} \underset{˙}{+} x = x$
7		isgrpi.n	$⊢ x \in B \to N \in B$
8		isgrpi.j	$⊢ x \in B \to N \underset{˙}{+} x = \underset{˙}{0}$
9	1	a1i	$⊢ ⊤ \to B = {Base}_{G}$
10	2	a1i	$⊢ ⊤ \to \underset{˙}{+} = +_{G}$
11	3	3adant1	$⊢ (⊤ \land x \in B \land y \in B) \to x \underset{˙}{+} y \in B$
12	4	adantl	$⊢ (⊤ \land (x \in B \land y \in B \land z \in B)) \to (x \underset{˙}{+} y) \underset{˙}{+} z = x \underset{˙}{+} (y \underset{˙}{+} z)$
13	5	a1i	$⊢ ⊤ \to \underset{˙}{0} \in B$
14	6	adantl	$⊢ (⊤ \land x \in B) \to \underset{˙}{0} \underset{˙}{+} x = x$
15	7	adantl	$⊢ (⊤ \land x \in B) \to N \in B$
16	8	adantl	$⊢ (⊤ \land x \in B) \to N \underset{˙}{+} x = \underset{˙}{0}$
17	9 10 11 12 13 14 15 16	isgrpd	$⊢ ⊤ \to G \in Grp$
18	17	mptru	$⊢ G \in Grp$

Metamath Proof Explorer