Theorem 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	$$⊢\phi \to B={\mathrm{Base}}_G$$
	isgrpd.p	$$⊢\phi \to \underset{\dot{}}{+}={+}_G$$
	isgrpd.c	$$⊢\left(\phi \wedge x\in B\wedge y\in B\right)\to x\underset{\dot{}}{+}y\in B$$
	isgrpd.a	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\wedge z\in B\right)\right)\to \left(x\underset{\dot{}}{+}y\right)\underset{\dot{}}{+}z=x\underset{\dot{}}{+}\left(y\underset{\dot{}}{+}z\right)$$
	isgrpd.z	$$⊢\phi \to \underset{\dot{}}{0}\in B$$
	isgrpd.i	$$⊢\left(\phi \wedge x\in B\right)\to \underset{\dot{}}{0}\underset{\dot{}}{+}x=x$$
	isgrpd.n	$$⊢\left(\phi \wedge x\in B\right)\to N\in B$$
	isgrpd.j	$$⊢\left(\phi \wedge x\in B\right)\to N\underset{\dot{}}{+}x=\underset{\dot{}}{0}$$
Assertion	isgrpd	$$⊢\phi \to G\in \mathrm{Grp}$$

Proof

Step	Hyp	Ref	Expression
1		isgrpd.b	$$⊢\phi \to B={\mathrm{Base}}_G$$
2		isgrpd.p	$$⊢\phi \to \underset{\dot{}}{+}={+}_G$$
3		isgrpd.c	$$⊢\left(\phi \wedge x\in B\wedge y\in B\right)\to x\underset{\dot{}}{+}y\in B$$
4		isgrpd.a	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\wedge z\in B\right)\right)\to \left(x\underset{\dot{}}{+}y\right)\underset{\dot{}}{+}z=x\underset{\dot{}}{+}\left(y\underset{\dot{}}{+}z\right)$$
5		isgrpd.z	$$⊢\phi \to \underset{\dot{}}{0}\in B$$
6		isgrpd.i	$$⊢\left(\phi \wedge x\in B\right)\to \underset{\dot{}}{0}\underset{\dot{}}{+}x=x$$
7		isgrpd.n	$$⊢\left(\phi \wedge x\in B\right)\to N\in B$$
8		isgrpd.j	$$⊢\left(\phi \wedge x\in B\right)\to N\underset{\dot{}}{+}x=\underset{\dot{}}{0}$$
9		oveq1	$$⊢y=N\to y\underset{\dot{}}{+}x=N\underset{\dot{}}{+}x$$
10	9	eqeq1d	$$⊢y=N\to \left(y\underset{\dot{}}{+}x=\underset{\dot{}}{0}\leftrightarrow N\underset{\dot{}}{+}x=\underset{\dot{}}{0}\right)$$
11	10	rspcev	$$⊢\left(N\in B\wedge N\underset{\dot{}}{+}x=\underset{\dot{}}{0}\right)\to \exists y\in By\underset{\dot{}}{+}x=\underset{\dot{}}{0}$$
12	7 8 11	syl2anc	$$⊢\left(\phi \wedge x\in B\right)\to \exists y\in By\underset{\dot{}}{+}x=\underset{\dot{}}{0}$$
13	1 2 3 4 5 6 12	isgrpde	$$⊢\phi \to G\in \mathrm{Grp}$$