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

Metamath Proof Explorer

Theorem isgrpd2e

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

		Ref	Expression
	Hypotheses	isgrpd2.b	$⊢ φ \to B = {Base}_{G}$
		isgrpd2.p	$⊢ φ \to \underset{˙}{+} = +_{G}$
		isgrpd2.z	$⊢ φ \to \underset{˙}{0} = 0_{G}$
		isgrpd2.g	$⊢ φ \to G \in Mnd$
		isgrpd2e.n	$⊢ (φ \land x \in B) \to \exists y \in B y \underset{˙}{+} x = \underset{˙}{0}$
	Assertion	isgrpd2e	$⊢ φ \to G \in Grp$

Proof

Step	Hyp	Ref	Expression
1		isgrpd2.b	$⊢ φ \to B = {Base}_{G}$
2		isgrpd2.p	$⊢ φ \to \underset{˙}{+} = +_{G}$
3		isgrpd2.z	$⊢ φ \to \underset{˙}{0} = 0_{G}$
4		isgrpd2.g	$⊢ φ \to G \in Mnd$
5		isgrpd2e.n	$⊢ (φ \land x \in B) \to \exists y \in B y \underset{˙}{+} x = \underset{˙}{0}$
6	5	ralrimiva	$⊢ φ \to \forall x \in B \exists y \in B y \underset{˙}{+} x = \underset{˙}{0}$
7	2	oveqd	$⊢ φ \to y \underset{˙}{+} x = y +_{G} x$
8	7 3	eqeq12d	$⊢ φ \to (y \underset{˙}{+} x = \underset{˙}{0} \leftrightarrow y +_{G} x = 0_{G})$
9	1 8	rexeqbidv	$⊢ φ \to (\exists y \in B y \underset{˙}{+} x = \underset{˙}{0} \leftrightarrow \exists y \in {Base}_{G} y +_{G} x = 0_{G})$
10	1 9	raleqbidv	$⊢ φ \to (\forall x \in B \exists y \in B y \underset{˙}{+} x = \underset{˙}{0} \leftrightarrow \forall x \in {Base}_{G} \exists y \in {Base}_{G} y +_{G} x = 0_{G})$
11	6 10	mpbid	$⊢ φ \to \forall x \in {Base}_{G} \exists y \in {Base}_{G} y +_{G} x = 0_{G}$
12		eqid	$⊢ {Base}_{G} = {Base}_{G}$
13		eqid	$⊢ +_{G} = +_{G}$
14		eqid	$⊢ 0_{G} = 0_{G}$
15	12 13 14	isgrp	$⊢ G \in Grp \leftrightarrow (G \in Mnd \land \forall x \in {Base}_{G} \exists y \in {Base}_{G} y +_{G} x = 0_{G})$
16	4 11 15	sylanbrc	$⊢ φ \to G \in Grp$