mndpropd - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > mndpropd		Structured version Visualization version Unicode version

Theorem mndpropd 17316

Description: If two structures have the same base set, and the values of their group (addition) operations are equal for all pairs of elements of the base set, one is a monoid iff the other one is. (Contributed by Mario Carneiro, 6-Jan-2015.)

**Hypotheses**
Ref	Expression
mndpropd.1
mndpropd.2
mndpropd.3	$/\$ $/\$

**Assertion**
Ref	Expression
mndpropd

Distinct variable groups:

Proof of Theorem mndpropd Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		simplr 792	. . . . . 6 $/\$ $/\$ $/\$
2		simprl 794	. . . . . . 7 $/\$ $/\$ $/\$
3		mndpropd.1	. . . . . . . 8
4	3	ad2antrr 762	. . . . . . 7 $/\$ $/\$ $/\$
5	2, 4	eleqtrd 2703	. . . . . 6 $/\$ $/\$ $/\$
6		simprr 796	. . . . . . 7 $/\$ $/\$ $/\$
7	6, 4	eleqtrd 2703	. . . . . 6 $/\$ $/\$ $/\$
8		eqid 2622	. . . . . . 7
9		eqid 2622	. . . . . . 7
10	8, 9	mndcl 17301	. . . . . 6 $/\$ $/\$
11	1, 5, 7, 10	syl3anc 1326	. . . . 5 $/\$ $/\$ $/\$
12	11, 4	eleqtrrd 2704	. . . 4 $/\$ $/\$ $/\$
13	12	ralrimivva 2971	. . 3 $/\$
14	13	ex 450	. 2
15		simplr 792	. . . . . 6 $/\$ $/\$ $/\$
16		simprl 794	. . . . . . 7 $/\$ $/\$ $/\$
17		mndpropd.2	. . . . . . . 8
18	17	ad2antrr 762	. . . . . . 7 $/\$ $/\$ $/\$
19	16, 18	eleqtrd 2703	. . . . . 6 $/\$ $/\$ $/\$
20		simprr 796	. . . . . . 7 $/\$ $/\$ $/\$
21	20, 18	eleqtrd 2703	. . . . . 6 $/\$ $/\$ $/\$
22		eqid 2622	. . . . . . 7
23		eqid 2622	. . . . . . 7
24	22, 23	mndcl 17301	. . . . . 6 $/\$ $/\$
25	15, 19, 21, 24	syl3anc 1326	. . . . 5 $/\$ $/\$ $/\$
26		mndpropd.3	. . . . . 6 $/\$ $/\$
27	26	adantlr 751	. . . . 5 $/\$ $/\$ $/\$
28	25, 27, 18	3eltr4d 2716	. . . 4 $/\$ $/\$ $/\$
29	28	ralrimivva 2971	. . 3 $/\$
30	29	ex 450	. 2
31	26	oveqrspc2v 6673	. . . . . . . . . 10 $/\$ $/\$
32	31	adantlr 751	. . . . . . . . 9 $/\$ $/\$ $/\$
33	32	eleq1d 2686	. . . . . . . 8 $/\$ $/\$ $/\$
34		simplll 798	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
35		simplrl 800	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
36		simplrr 801	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
37		simpllr 799	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
38		ovrspc2v 6672	. . . . . . . . . . . . 13 $/\$ $/\$
39	35, 36, 37, 38	syl21anc 1325	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
40		simpr 477	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
41	26	oveqrspc2v 6673	. . . . . . . . . . . 12 $/\$ $/\$
42	34, 39, 40, 41	syl12anc 1324	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
43	34, 35, 36, 31	syl12anc 1324	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
44	43	oveq1d 6665	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
45	42, 44	eqtrd 2656	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
46		ovrspc2v 6672	. . . . . . . . . . . . 13 $/\$ $/\$
47	36, 40, 37, 46	syl21anc 1325	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
48	26	oveqrspc2v 6673	. . . . . . . . . . . 12 $/\$ $/\$
49	34, 35, 47, 48	syl12anc 1324	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
50	26	oveqrspc2v 6673	. . . . . . . . . . . . 13 $/\$ $/\$
51	34, 36, 40, 50	syl12anc 1324	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
52	51	oveq2d 6666	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
53	49, 52	eqtrd 2656	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
54	45, 53	eqeq12d 2637	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
55	54	ralbidva 2985	. . . . . . . 8 $/\$ $/\$ $/\$
56	33, 55	anbi12d 747	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
57	56	2ralbidva 2988	. . . . . 6 $/\$ $/\$ $/\$
58	3	adantr 481	. . . . . . 7 $/\$
59	58	eleq2d 2687	. . . . . . . . 9 $/\$
60	58	raleqdv 3144	. . . . . . . . 9 $/\$
61	59, 60	anbi12d 747	. . . . . . . 8 $/\$ $/\$ $/\$
62	58, 61	raleqbidv 3152	. . . . . . 7 $/\$ $/\$ $/\$
63	58, 62	raleqbidv 3152	. . . . . 6 $/\$ $/\$ $/\$
64	17	adantr 481	. . . . . . 7 $/\$
65	64	eleq2d 2687	. . . . . . . . 9 $/\$
66	64	raleqdv 3144	. . . . . . . . 9 $/\$
67	65, 66	anbi12d 747	. . . . . . . 8 $/\$ $/\$ $/\$
68	64, 67	raleqbidv 3152	. . . . . . 7 $/\$ $/\$ $/\$
69	64, 68	raleqbidv 3152	. . . . . 6 $/\$ $/\$ $/\$
70	57, 63, 69	3bitr3d 298	. . . . 5 $/\$ $/\$ $/\$
71		simplll 798	. . . . . . . . . . 11 $/\$ $/\$ $/\$
72		simplr 792	. . . . . . . . . . 11 $/\$ $/\$ $/\$
73		simpr 477	. . . . . . . . . . 11 $/\$ $/\$ $/\$
74	26	oveqrspc2v 6673	. . . . . . . . . . 11 $/\$ $/\$
75	71, 72, 73, 74	syl12anc 1324	. . . . . . . . . 10 $/\$ $/\$ $/\$
76	75	eqeq1d 2624	. . . . . . . . 9 $/\$ $/\$ $/\$
77	26	oveqrspc2v 6673	. . . . . . . . . . 11 $/\$ $/\$
78	71, 73, 72, 77	syl12anc 1324	. . . . . . . . . 10 $/\$ $/\$ $/\$
79	78	eqeq1d 2624	. . . . . . . . 9 $/\$ $/\$ $/\$
80	76, 79	anbi12d 747	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
81	80	ralbidva 2985	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
82	81	rexbidva 3049	. . . . . 6 $/\$ $/\$ $/\$
83	58	raleqdv 3144	. . . . . . 7 $/\$ $/\$ $/\$
84	58, 83	rexeqbidv 3153	. . . . . 6 $/\$ $/\$ $/\$
85	64	raleqdv 3144	. . . . . . 7 $/\$ $/\$ $/\$
86	64, 85	rexeqbidv 3153	. . . . . 6 $/\$ $/\$ $/\$
87	82, 84, 86	3bitr3d 298	. . . . 5 $/\$ $/\$ $/\$
88	70, 87	anbi12d 747	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
89	8, 9	ismnd 17297	. . . 4 $/\$ $/\$ $/\$
90	22, 23	ismnd 17297	. . . 4 $/\$ $/\$ $/\$
91	88, 89, 90	3bitr4g 303	. . 3 $/\$
92	91	ex 450	. 2
93	14, 30, 92	pm5.21ndd 369	1

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 196 $/\$ wa 384

wceq 1483

wcel 1990

wral 2912

wrex 2913

cfv 5888 (class class class)co 6650

cbs 15857

cplusg 15941

cmnd 17294

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-nul 4789 ax-pow 4843

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-ral 2917 df-rex 2918 df-rab 2921 df-v 3202 df-sbc 3436 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-nul 3916 df-if 4087 df-sn 4178 df-pr 4180 df-op 4184 df-uni 4437 df-br 4654 df-iota 5851 df-fv 5896 df-ov 6653 df-mgm 17242 df-sgrp 17284 df-mnd 17295

This theorem is referenced by: mndprop 17317 mhmpropd 17341 grppropd 17437 oppgmndb 17785 cmnpropd 18202 ringpropd 18582 prdsringd 18612

W3C validator