ismndd

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

	Ref	Expression
Hypotheses	ismndd.b	$⊢ φ \to B = {Base}_{G}$
	ismndd.p	$⊢ φ \to \underset{˙}{+} = +_{G}$
	ismndd.c	$⊢ (φ \land x \in B \land y \in B) \to x \underset{˙}{+} y \in B$
	ismndd.a	$⊢ (φ \land (x \in B \land y \in B \land z \in B)) \to (x \underset{˙}{+} y) \underset{˙}{+} z = x \underset{˙}{+} (y \underset{˙}{+} z)$
	ismndd.z	$⊢ φ \to \underset{˙}{0} \in B$
	ismndd.i	$⊢ (φ \land x \in B) \to \underset{˙}{0} \underset{˙}{+} x = x$
	ismndd.j	$⊢ (φ \land x \in B) \to x \underset{˙}{+} \underset{˙}{0} = x$
Assertion	ismndd	$⊢ φ \to G \in Mnd$

Proof

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

Metamath Proof Explorer

Theorem ismndd

Proof