mndpropd - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > mndpropd		Unicode version

Theorem mndpropd 12676

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 525	. . . . . 6 $/\$ $/\$ $/\$
2		simprl 526	. . . . . . 7 $/\$ $/\$ $/\$
3		mndpropd.1	. . . . . . . 8
4	3	ad2antrr 485	. . . . . . 7 $/\$ $/\$ $/\$
5	2, 4	eleqtrd 2249	. . . . . 6 $/\$ $/\$ $/\$
6		simprr 527	. . . . . . 7 $/\$ $/\$ $/\$
7	6, 4	eleqtrd 2249	. . . . . 6 $/\$ $/\$ $/\$
8		eqid 2170	. . . . . . 7
9		eqid 2170	. . . . . . 7
10	8, 9	mndcl 12659	. . . . . 6 $/\$ $/\$
11	1, 5, 7, 10	syl3anc 1233	. . . . 5 $/\$ $/\$ $/\$
12	11, 4	eleqtrrd 2250	. . . 4 $/\$ $/\$ $/\$
13	12	ralrimivva 2552	. . 3 $/\$
14	13	ex 114	. 2
15		simplr 525	. . . . . 6 $/\$ $/\$ $/\$
16		simprl 526	. . . . . . 7 $/\$ $/\$ $/\$
17		mndpropd.2	. . . . . . . 8
18	17	ad2antrr 485	. . . . . . 7 $/\$ $/\$ $/\$
19	16, 18	eleqtrd 2249	. . . . . 6 $/\$ $/\$ $/\$
20		simprr 527	. . . . . . 7 $/\$ $/\$ $/\$
21	20, 18	eleqtrd 2249	. . . . . 6 $/\$ $/\$ $/\$
22		eqid 2170	. . . . . . 7
23		eqid 2170	. . . . . . 7
24	22, 23	mndcl 12659	. . . . . 6 $/\$ $/\$
25	15, 19, 21, 24	syl3anc 1233	. . . . 5 $/\$ $/\$ $/\$
26		mndpropd.3	. . . . . 6 $/\$ $/\$
27	26	adantlr 474	. . . . 5 $/\$ $/\$ $/\$
28	25, 27, 18	3eltr4d 2254	. . . 4 $/\$ $/\$ $/\$
29	28	ralrimivva 2552	. . 3 $/\$
30	29	ex 114	. 2
31	26	oveqrspc2v 5880	. . . . . . . . . 10 $/\$ $/\$
32	31	adantlr 474	. . . . . . . . 9 $/\$ $/\$ $/\$
33	32	eleq1d 2239	. . . . . . . 8 $/\$ $/\$ $/\$
34		simplll 528	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
35		simplrl 530	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
36		simplrr 531	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
37		simpllr 529	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
38		ovrspc2v 5879	. . . . . . . . . . . . 13 $/\$ $/\$
39	35, 36, 37, 38	syl21anc 1232	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
40		simpr 109	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
41	26	oveqrspc2v 5880	. . . . . . . . . . . 12 $/\$ $/\$
42	34, 39, 40, 41	syl12anc 1231	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
43	34, 35, 36, 31	syl12anc 1231	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
44	43	oveq1d 5868	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
45	42, 44	eqtrd 2203	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
46		ovrspc2v 5879	. . . . . . . . . . . . 13 $/\$ $/\$
47	36, 40, 37, 46	syl21anc 1232	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
48	26	oveqrspc2v 5880	. . . . . . . . . . . 12 $/\$ $/\$
49	34, 35, 47, 48	syl12anc 1231	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
50	26	oveqrspc2v 5880	. . . . . . . . . . . . 13 $/\$ $/\$
51	34, 36, 40, 50	syl12anc 1231	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
52	51	oveq2d 5869	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
53	49, 52	eqtrd 2203	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
54	45, 53	eqeq12d 2185	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
55	54	ralbidva 2466	. . . . . . . 8 $/\$ $/\$ $/\$
56	33, 55	anbi12d 470	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
57	56	2ralbidva 2492	. . . . . 6 $/\$ $/\$ $/\$
58	3	adantr 274	. . . . . . 7 $/\$
59	58	eleq2d 2240	. . . . . . . . 9 $/\$
60	58	raleqdv 2671	. . . . . . . . 9 $/\$
61	59, 60	anbi12d 470	. . . . . . . 8 $/\$ $/\$ $/\$
62	58, 61	raleqbidv 2677	. . . . . . 7 $/\$ $/\$ $/\$
63	58, 62	raleqbidv 2677	. . . . . 6 $/\$ $/\$ $/\$
64	17	adantr 274	. . . . . . 7 $/\$
65	64	eleq2d 2240	. . . . . . . . 9 $/\$
66	64	raleqdv 2671	. . . . . . . . 9 $/\$
67	65, 66	anbi12d 470	. . . . . . . 8 $/\$ $/\$ $/\$
68	64, 67	raleqbidv 2677	. . . . . . 7 $/\$ $/\$ $/\$
69	64, 68	raleqbidv 2677	. . . . . 6 $/\$ $/\$ $/\$
70	57, 63, 69	3bitr3d 217	. . . . 5 $/\$ $/\$ $/\$
71		simplll 528	. . . . . . . . . . 11 $/\$ $/\$ $/\$
72		simplr 525	. . . . . . . . . . 11 $/\$ $/\$ $/\$
73		simpr 109	. . . . . . . . . . 11 $/\$ $/\$ $/\$
74	26	oveqrspc2v 5880	. . . . . . . . . . 11 $/\$ $/\$
75	71, 72, 73, 74	syl12anc 1231	. . . . . . . . . 10 $/\$ $/\$ $/\$
76	75	eqeq1d 2179	. . . . . . . . 9 $/\$ $/\$ $/\$
77	26	oveqrspc2v 5880	. . . . . . . . . . 11 $/\$ $/\$
78	71, 73, 72, 77	syl12anc 1231	. . . . . . . . . 10 $/\$ $/\$ $/\$
79	78	eqeq1d 2179	. . . . . . . . 9 $/\$ $/\$ $/\$
80	76, 79	anbi12d 470	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
81	80	ralbidva 2466	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
82	81	rexbidva 2467	. . . . . 6 $/\$ $/\$ $/\$
83	58	raleqdv 2671	. . . . . . 7 $/\$ $/\$ $/\$
84	58, 83	rexeqbidv 2678	. . . . . 6 $/\$ $/\$ $/\$
85	64	raleqdv 2671	. . . . . . 7 $/\$ $/\$ $/\$
86	64, 85	rexeqbidv 2678	. . . . . 6 $/\$ $/\$ $/\$
87	82, 84, 86	3bitr3d 217	. . . . 5 $/\$ $/\$ $/\$
88	70, 87	anbi12d 470	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
89	8, 9	ismnd 12655	. . . 4 $/\$ $/\$ $/\$
90	22, 23	ismnd 12655	. . . 4 $/\$ $/\$ $/\$
91	88, 89, 90	3bitr4g 222	. . 3 $/\$
92	91	ex 114	. 2
93	14, 30, 92	pm5.21ndd 700	1

Colors of variables: wff set class

Syntax hints:

wi 4 $/\$ wa 103

wb 104

wceq 1348

wcel 2141

wral 2448

wrex 2449

cfv 5198 (class class class)co 5853

cbs 12416

cplusg 12480

cmnd 12652

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 704 ax-5 1440 ax-7 1441 ax-gen 1442 ax-ie1 1486 ax-ie2 1487 ax-8 1497 ax-10 1498 ax-11 1499 ax-i12 1500 ax-bndl 1502 ax-4 1503 ax-17 1519 ax-i9 1523 ax-ial 1527 ax-i5r 1528 ax-13 2143 ax-14 2144 ax-ext 2152 ax-sep 4107 ax-pow 4160 ax-pr 4194 ax-un 4418 ax-cnex 7865 ax-resscn 7866 ax-1re 7868 ax-addrcl 7871

This theorem depends on definitions: df-bi 116 df-3an 975 df-tru 1351 df-nf 1454 df-sb 1756 df-eu 2022 df-mo 2023 df-clab 2157 df-cleq 2163 df-clel 2166 df-nfc 2301 df-ral 2453 df-rex 2454 df-rab 2457 df-v 2732 df-sbc 2956 df-un 3125 df-in 3127 df-ss 3134 df-pw 3568 df-sn 3589 df-pr 3590 df-op 3592 df-uni 3797 df-int 3832 df-br 3990 df-opab 4051 df-mpt 4052 df-id 4278 df-xp 4617 df-rel 4618 df-cnv 4619 df-co 4620 df-dm 4621 df-rn 4622 df-res 4623 df-iota 5160 df-fun 5200 df-fn 5201 df-fv 5206 df-ov 5856 df-inn 8879 df-2 8937 df-ndx 12419 df-slot 12420 df-base 12422 df-plusg 12493 df-mgm 12610 df-sgrp 12643 df-mnd 12653

This theorem is referenced by: mndprop 12677 mhmpropd 12689 grppropd 12724

W3C validator