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

Proof

Step	Hyp	Ref	Expression
1		isgrpi.b	$$⊢B={\mathrm{Base}}_G$$
2		isgrpi.p	$$⊢\underset{\dot{}}{+}={+}_G$$
3		isgrpi.c	$$⊢\left(x\in B\wedge y\in B\right)\to x\underset{\dot{}}{+}y\in B$$
4		isgrpi.a	$$⊢\left(x\in B\wedge y\in B\wedge z\in B\right)\to \left(x\underset{\dot{}}{+}y\right)\underset{\dot{}}{+}z=x\underset{\dot{}}{+}\left(y\underset{\dot{}}{+}z\right)$$
5		isgrpi.z	$$⊢\underset{\dot{}}{0}\in B$$
6		isgrpi.i	$$⊢x\in B\to \underset{\dot{}}{0}\underset{\dot{}}{+}x=x$$
7		isgrpi.n	$$⊢x\in B\to N\in B$$
8		isgrpi.j	$$⊢x\in B\to N\underset{\dot{}}{+}x=\underset{\dot{}}{0}$$
9	1	a1i	$$⊢\top \to B={\mathrm{Base}}_G$$
10	2	a1i	$$⊢\top \to \underset{\dot{}}{+}={+}_G$$
11	3	3adant1	$$⊢\left(\top \wedge x\in B\wedge y\in B\right)\to x\underset{\dot{}}{+}y\in B$$
12	4	adantl	$$⊢\left(\top \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)$$
13	5	a1i	$$⊢\top \to \underset{\dot{}}{0}\in B$$
14	6	adantl	$$⊢\left(\top \wedge x\in B\right)\to \underset{\dot{}}{0}\underset{\dot{}}{+}x=x$$
15	7	adantl	$$⊢\left(\top \wedge x\in B\right)\to N\in B$$
16	8	adantl	$$⊢\left(\top \wedge x\in B\right)\to N\underset{\dot{}}{+}x=\underset{\dot{}}{0}$$
17	9 10 11 12 13 14 15 16	isgrpd	$$⊢\top \to G\in \mathrm{Grp}$$
18	17	mptru	$$⊢G\in \mathrm{Grp}$$