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

Metamath Proof Explorer

Theorem isgrpix

Description: Properties that determine a group. Read N as N ( x ) . Note: This theorem has hard-coded structure indices for demonstration purposes. It is not intended for general use. (New usage is discouraged.) (Contributed by NM, 4-Sep-2011)

		Ref	Expression
	Hypotheses	isgrpix.a	$⊢ B \in V$
		isgrpix.b	$⊢ \underset{˙}{+} \in V$
		isgrpix.g	$⊢ G = \{⟨1, B⟩, ⟨2, \underset{˙}{+}⟩\}$
		isgrpix.2	$⊢ (x \in B \land y \in B) \to x \underset{˙}{+} y \in B$
		isgrpix.3	$⊢ (x \in B \land y \in B \land z \in B) \to (x \underset{˙}{+} y) \underset{˙}{+} z = x \underset{˙}{+} (y \underset{˙}{+} z)$
		isgrpix.z	$⊢ \underset{˙}{0} \in B$
		isgrpix.5	$⊢ x \in B \to \underset{˙}{0} \underset{˙}{+} x = x$
		isgrpix.6	$⊢ x \in B \to N \in B$
		isgrpix.7	$⊢ x \in B \to N \underset{˙}{+} x = \underset{˙}{0}$
	Assertion	isgrpix	$⊢ G \in Grp$

Proof

Step	Hyp	Ref	Expression
1		isgrpix.a	$⊢ B \in V$
2		isgrpix.b	$⊢ \underset{˙}{+} \in V$
3		isgrpix.g	$⊢ G = \{⟨1, B⟩, ⟨2, \underset{˙}{+}⟩\}$
4		isgrpix.2	$⊢ (x \in B \land y \in B) \to x \underset{˙}{+} y \in B$
5		isgrpix.3	$⊢ (x \in B \land y \in B \land z \in B) \to (x \underset{˙}{+} y) \underset{˙}{+} z = x \underset{˙}{+} (y \underset{˙}{+} z)$
6		isgrpix.z	$⊢ \underset{˙}{0} \in B$
7		isgrpix.5	$⊢ x \in B \to \underset{˙}{0} \underset{˙}{+} x = x$
8		isgrpix.6	$⊢ x \in B \to N \in B$
9		isgrpix.7	$⊢ x \in B \to N \underset{˙}{+} x = \underset{˙}{0}$
10	1 2 3	grpbasex	$⊢ B = {Base}_{G}$
11	1 2 3	grpplusgx	$⊢ \underset{˙}{+} = +_{G}$
12	10 11 4 5 6 7 8 9	isgrpi	$⊢ G \in Grp$