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	$$⊢\phi \to B={\mathrm{Base}}_G$$
	isgrpd2.p	$$⊢\phi \to \underset{\dot{}}{+}={+}_G$$
	isgrpd2.z	$$⊢\phi \to \underset{\dot{}}{0}=0_G$$
	isgrpd2.g	$$⊢\phi \to G\in \mathrm{Mnd}$$
	isgrpd2e.n	$$⊢\left(\phi \wedge x\in B\right)\to \exists y\in By\underset{\dot{}}{+}x=\underset{\dot{}}{0}$$
Assertion	isgrpd2e	$$⊢\phi \to G\in \mathrm{Grp}$$

Proof

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