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 \mathrm{V}$$
	isgrpix.b	$$⊢\underset{\dot{}}{+}\in \mathrm{V}$$
	isgrpix.g	$$⊢G=\left\{⟨1,B⟩,⟨2,\underset{\dot{}}{+}⟩\right\}$$
	isgrpix.2	$$⊢\left(x\in B\wedge y\in B\right)\to x\underset{\dot{}}{+}y\in B$$
	isgrpix.3	$$⊢\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)$$
	isgrpix.z	$$⊢\underset{\dot{}}{0}\in B$$
	isgrpix.5	$$⊢x\in B\to \underset{\dot{}}{0}\underset{\dot{}}{+}x=x$$
	isgrpix.6	$$⊢x\in B\to N\in B$$
	isgrpix.7	$$⊢x\in B\to N\underset{\dot{}}{+}x=\underset{\dot{}}{0}$$
Assertion	isgrpix	$$⊢G\in \mathrm{Grp}$$

Proof

Step	Hyp	Ref	Expression
1		isgrpix.a	$$⊢B\in \mathrm{V}$$
2		isgrpix.b	$$⊢\underset{\dot{}}{+}\in \mathrm{V}$$
3		isgrpix.g	$$⊢G=\left\{⟨1,B⟩,⟨2,\underset{\dot{}}{+}⟩\right\}$$
4		isgrpix.2	$$⊢\left(x\in B\wedge y\in B\right)\to x\underset{\dot{}}{+}y\in B$$
5		isgrpix.3	$$⊢\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)$$
6		isgrpix.z	$$⊢\underset{\dot{}}{0}\in B$$
7		isgrpix.5	$$⊢x\in B\to \underset{\dot{}}{0}\underset{\dot{}}{+}x=x$$
8		isgrpix.6	$$⊢x\in B\to N\in B$$
9		isgrpix.7	$$⊢x\in B\to N\underset{\dot{}}{+}x=\underset{\dot{}}{0}$$
10	1 2 3	grpbasex	$$⊢B={\mathrm{Base}}_G$$
11	1 2 3	grpplusgx	$$⊢\underset{\dot{}}{+}={+}_G$$
12	10 11 4 5 6 7 8 9	isgrpi	$$⊢G\in \mathrm{Grp}$$