Theorem isgrp

Description: The predicate "is a group." (This theorem demonstrates the use of symbols as variable names, first proposed by FL in 2010.) (Contributed by NM, 17-Oct-2012) (Revised by Mario Carneiro, 6-Jan-2015)

	Ref	Expression
Hypotheses	isgrp.b	$$⊢B={\mathrm{Base}}_G$$
	isgrp.p	$$⊢\underset{\dot{}}{+}={+}_G$$
	isgrp.z	$$⊢\underset{\dot{}}{0}=0_G$$
Assertion	isgrp	$$⊢G\in \mathrm{Grp}\leftrightarrow \left(G\in \mathrm{Mnd}\wedge \forall a\in B\exists m\in Bm\underset{\dot{}}{+}a=\underset{\dot{}}{0}\right)$$

Proof

Step	Hyp	Ref	Expression
1		isgrp.b	$$⊢B={\mathrm{Base}}_G$$
2		isgrp.p	$$⊢\underset{\dot{}}{+}={+}_G$$
3		isgrp.z	$$⊢\underset{\dot{}}{0}=0_G$$
4		fveq2	$$⊢g=G\to {\mathrm{Base}}_g={\mathrm{Base}}_G$$
5	4 1	eqtr4di	$$⊢g=G\to {\mathrm{Base}}_g=B$$
6		fveq2	$$⊢g=G\to {+}_g={+}_G$$
7	6 2	eqtr4di	$$⊢g=G\to {+}_g=\underset{\dot{}}{+}$$
8	7	oveqd	$$⊢g=G\to m{+}_{g}a=m\underset{\dot{}}{+}a$$
9		fveq2	$$⊢g=G\to 0_g=0_G$$
10	9 3	eqtr4di	$$⊢g=G\to 0_g=\underset{\dot{}}{0}$$
11	8 10	eqeq12d	$$⊢g=G\to \left(m{+}_{g}a=0_g\leftrightarrow m\underset{\dot{}}{+}a=\underset{\dot{}}{0}\right)$$
12	5 11	rexeqbidv	$$⊢g=G\to \left(\exists m\in {\mathrm{Base}}_{g}m{+}_{g}a=0_g\leftrightarrow \exists m\in Bm\underset{\dot{}}{+}a=\underset{\dot{}}{0}\right)$$
13	5 12	raleqbidv	$$⊢g=G\to \left(\forall a\in {\mathrm{Base}}_g\exists m\in {\mathrm{Base}}_{g}m{+}_{g}a=0_g\leftrightarrow \forall a\in B\exists m\in Bm\underset{\dot{}}{+}a=\underset{\dot{}}{0}\right)$$
14		df-grp	$$⊢\mathrm{Grp}=\left\{g\in \mathrm{Mnd}|\forall a\in {\mathrm{Base}}_g\exists m\in {\mathrm{Base}}_{g}m{+}_{g}a=0_g\right\}$$
15	13 14	elrab2	$$⊢G\in \mathrm{Grp}\leftrightarrow \left(G\in \mathrm{Mnd}\wedge \forall a\in B\exists m\in Bm\underset{\dot{}}{+}a=\underset{\dot{}}{0}\right)$$