Theorem ismndd

Description: Deduce a monoid from its properties. (Contributed by Mario Carneiro, 6-Jan-2015)

	Ref	Expression
Hypotheses	ismndd.b	$$⊢\phi \to B={\mathrm{Base}}_G$$
	ismndd.p	$$⊢\phi \to \underset{\dot{}}{+}={+}_G$$
	ismndd.c	$$⊢\left(\phi \wedge x\in B\wedge y\in B\right)\to x\underset{\dot{}}{+}y\in B$$
	ismndd.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)$$
	ismndd.z	$$⊢\phi \to \underset{\dot{}}{0}\in B$$
	ismndd.i	$$⊢\left(\phi \wedge x\in B\right)\to \underset{\dot{}}{0}\underset{\dot{}}{+}x=x$$
	ismndd.j	$$⊢\left(\phi \wedge x\in B\right)\to x\underset{\dot{}}{+}\underset{\dot{}}{0}=x$$
Assertion	ismndd	$$⊢\phi \to G\in \mathrm{Mnd}$$

Proof

Step	Hyp	Ref	Expression
1		ismndd.b	$$⊢\phi \to B={\mathrm{Base}}_G$$
2		ismndd.p	$$⊢\phi \to \underset{\dot{}}{+}={+}_G$$
3		ismndd.c	$$⊢\left(\phi \wedge x\in B\wedge y\in B\right)\to x\underset{\dot{}}{+}y\in B$$
4		ismndd.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		ismndd.z	$$⊢\phi \to \underset{\dot{}}{0}\in B$$
6		ismndd.i	$$⊢\left(\phi \wedge x\in B\right)\to \underset{\dot{}}{0}\underset{\dot{}}{+}x=x$$
7		ismndd.j	$$⊢\left(\phi \wedge x\in B\right)\to x\underset{\dot{}}{+}\underset{\dot{}}{0}=x$$
8	3	3expb	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to x\underset{\dot{}}{+}y\in B$$
9		simpll	$$⊢\left(\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\wedge z\in B\right)\to \phi$$
10		simplrl	$$⊢\left(\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\wedge z\in B\right)\to x\in B$$
11		simplrr	$$⊢\left(\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\wedge z\in B\right)\to y\in B$$
12		simpr	$$⊢\left(\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\wedge z\in B\right)\to z\in B$$
13	9 10 11 12 4	syl13anc	$$⊢\left(\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\wedge z\in B\right)\to \left(x\underset{\dot{}}{+}y\right)\underset{\dot{}}{+}z=x\underset{\dot{}}{+}\left(y\underset{\dot{}}{+}z\right)$$
14	13	ralrimiva	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to \forall z\in B\left(x\underset{\dot{}}{+}y\right)\underset{\dot{}}{+}z=x\underset{\dot{}}{+}\left(y\underset{\dot{}}{+}z\right)$$
15	8 14	jca	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to \left(x\underset{\dot{}}{+}y\in B\wedge \forall z\in B\left(x\underset{\dot{}}{+}y\right)\underset{\dot{}}{+}z=x\underset{\dot{}}{+}\left(y\underset{\dot{}}{+}z\right)\right)$$
16	15	ralrimivva	$$⊢\phi \to \forall x\in B\forall y\in B\left(x\underset{\dot{}}{+}y\in B\wedge \forall z\in B\left(x\underset{\dot{}}{+}y\right)\underset{\dot{}}{+}z=x\underset{\dot{}}{+}\left(y\underset{\dot{}}{+}z\right)\right)$$
17	2	oveqd	$$⊢\phi \to x\underset{\dot{}}{+}y=x{+}_{G}y$$
18	17 1	eleq12d	$$⊢\phi \to \left(x\underset{\dot{}}{+}y\in B\leftrightarrow x{+}_{G}y\in {\mathrm{Base}}_G\right)$$
19		eqidd	$$⊢\phi \to z=z$$
20	2 17 19	oveq123d	$$⊢\phi \to \left(x\underset{\dot{}}{+}y\right)\underset{\dot{}}{+}z=\left(x{+}_{G}y\right){+}_{G}z$$
21		eqidd	$$⊢\phi \to x=x$$
22	2	oveqd	$$⊢\phi \to y\underset{\dot{}}{+}z=y{+}_{G}z$$
23	2 21 22	oveq123d	$$⊢\phi \to x\underset{\dot{}}{+}\left(y\underset{\dot{}}{+}z\right)=x{+}_G\left(y{+}_{G}z\right)$$
24	20 23	eqeq12d	$$⊢\phi \to \left(\left(x\underset{\dot{}}{+}y\right)\underset{\dot{}}{+}z=x\underset{\dot{}}{+}\left(y\underset{\dot{}}{+}z\right)\leftrightarrow \left(x{+}_{G}y\right){+}_{G}z=x{+}_G\left(y{+}_{G}z\right)\right)$$
25	1 24	raleqbidv	$$⊢\phi \to \left(\forall z\in B\left(x\underset{\dot{}}{+}y\right)\underset{\dot{}}{+}z=x\underset{\dot{}}{+}\left(y\underset{\dot{}}{+}z\right)\leftrightarrow \forall z\in {\mathrm{Base}}_G\left(x{+}_{G}y\right){+}_{G}z=x{+}_G\left(y{+}_{G}z\right)\right)$$
26	18 25	anbi12d	$$⊢\phi \to \left(\left(x\underset{\dot{}}{+}y\in B\wedge \forall z\in B\left(x\underset{\dot{}}{+}y\right)\underset{\dot{}}{+}z=x\underset{\dot{}}{+}\left(y\underset{\dot{}}{+}z\right)\right)\leftrightarrow \left(x{+}_{G}y\in {\mathrm{Base}}_G\wedge \forall z\in {\mathrm{Base}}_G\left(x{+}_{G}y\right){+}_{G}z=x{+}_G\left(y{+}_{G}z\right)\right)\right)$$
27	1 26	raleqbidv	$$⊢\phi \to \left(\forall y\in B\left(x\underset{\dot{}}{+}y\in B\wedge \forall z\in B\left(x\underset{\dot{}}{+}y\right)\underset{\dot{}}{+}z=x\underset{\dot{}}{+}\left(y\underset{\dot{}}{+}z\right)\right)\leftrightarrow \forall y\in {\mathrm{Base}}_G\left(x{+}_{G}y\in {\mathrm{Base}}_G\wedge \forall z\in {\mathrm{Base}}_G\left(x{+}_{G}y\right){+}_{G}z=x{+}_G\left(y{+}_{G}z\right)\right)\right)$$
28	1 27	raleqbidv	$$⊢\phi \to \left(\forall x\in B\forall y\in B\left(x\underset{\dot{}}{+}y\in B\wedge \forall z\in B\left(x\underset{\dot{}}{+}y\right)\underset{\dot{}}{+}z=x\underset{\dot{}}{+}\left(y\underset{\dot{}}{+}z\right)\right)\leftrightarrow \forall x\in {\mathrm{Base}}_G\forall y\in {\mathrm{Base}}_G\left(x{+}_{G}y\in {\mathrm{Base}}_G\wedge \forall z\in {\mathrm{Base}}_G\left(x{+}_{G}y\right){+}_{G}z=x{+}_G\left(y{+}_{G}z\right)\right)\right)$$
29	16 28	mpbid	$$⊢\phi \to \forall x\in {\mathrm{Base}}_G\forall y\in {\mathrm{Base}}_G\left(x{+}_{G}y\in {\mathrm{Base}}_G\wedge \forall z\in {\mathrm{Base}}_G\left(x{+}_{G}y\right){+}_{G}z=x{+}_G\left(y{+}_{G}z\right)\right)$$
30	5 1	eleqtrd	$$⊢\phi \to \underset{\dot{}}{0}\in {\mathrm{Base}}_G$$
31	1	eleq2d	$$⊢\phi \to \left(x\in B\leftrightarrow x\in {\mathrm{Base}}_G\right)$$
32	31	biimpar	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_G\right)\to x\in B$$
33	2	adantr	$$⊢\left(\phi \wedge x\in B\right)\to \underset{\dot{}}{+}={+}_G$$
34	33	oveqd	$$⊢\left(\phi \wedge x\in B\right)\to \underset{\dot{}}{0}\underset{\dot{}}{+}x=\underset{\dot{}}{0}{+}_{G}x$$
35	34 6	eqtr3d	$$⊢\left(\phi \wedge x\in B\right)\to \underset{\dot{}}{0}{+}_{G}x=x$$
36	33	oveqd	$$⊢\left(\phi \wedge x\in B\right)\to x\underset{\dot{}}{+}\underset{\dot{}}{0}=x{+}_G\underset{\dot{}}{0}$$
37	36 7	eqtr3d	$$⊢\left(\phi \wedge x\in B\right)\to x{+}_G\underset{\dot{}}{0}=x$$
38	35 37	jca	$$⊢\left(\phi \wedge x\in B\right)\to \left(\underset{\dot{}}{0}{+}_{G}x=x\wedge x{+}_G\underset{\dot{}}{0}=x\right)$$
39	32 38	syldan	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_G\right)\to \left(\underset{\dot{}}{0}{+}_{G}x=x\wedge x{+}_G\underset{\dot{}}{0}=x\right)$$
40	39	ralrimiva	$$⊢\phi \to \forall x\in {\mathrm{Base}}_G\left(\underset{\dot{}}{0}{+}_{G}x=x\wedge x{+}_G\underset{\dot{}}{0}=x\right)$$
41		oveq1	$$⊢u=\underset{\dot{}}{0}\to u{+}_{G}x=\underset{\dot{}}{0}{+}_{G}x$$
42	41	eqeq1d	$$⊢u=\underset{\dot{}}{0}\to \left(u{+}_{G}x=x\leftrightarrow \underset{\dot{}}{0}{+}_{G}x=x\right)$$
43	42	ovanraleqv	$$⊢u=\underset{\dot{}}{0}\to \left(\forall x\in {\mathrm{Base}}_G\left(u{+}_{G}x=x\wedge x{+}_{G}u=x\right)\leftrightarrow \forall x\in {\mathrm{Base}}_G\left(\underset{\dot{}}{0}{+}_{G}x=x\wedge x{+}_G\underset{\dot{}}{0}=x\right)\right)$$
44	43	rspcev	$$⊢\left(\underset{\dot{}}{0}\in {\mathrm{Base}}_G\wedge \forall x\in {\mathrm{Base}}_G\left(\underset{\dot{}}{0}{+}_{G}x=x\wedge x{+}_G\underset{\dot{}}{0}=x\right)\right)\to \exists u\in {\mathrm{Base}}_G\forall x\in {\mathrm{Base}}_G\left(u{+}_{G}x=x\wedge x{+}_{G}u=x\right)$$
45	30 40 44	syl2anc	$$⊢\phi \to \exists u\in {\mathrm{Base}}_G\forall x\in {\mathrm{Base}}_G\left(u{+}_{G}x=x\wedge x{+}_{G}u=x\right)$$
46		eqid	$$⊢{\mathrm{Base}}_G={\mathrm{Base}}_G$$
47		eqid	$$⊢{+}_G={+}_G$$
48	46 47	ismnd	$$⊢G\in \mathrm{Mnd}\leftrightarrow \left(\forall x\in {\mathrm{Base}}_G\forall y\in {\mathrm{Base}}_G\left(x{+}_{G}y\in {\mathrm{Base}}_G\wedge \forall z\in {\mathrm{Base}}_G\left(x{+}_{G}y\right){+}_{G}z=x{+}_G\left(y{+}_{G}z\right)\right)\wedge \exists u\in {\mathrm{Base}}_G\forall x\in {\mathrm{Base}}_G\left(u{+}_{G}x=x\wedge x{+}_{G}u=x\right)\right)$$
49	29 45 48	sylanbrc	$$⊢\phi \to G\in \mathrm{Mnd}$$