mndpropd

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)

	Ref	Expression
Hypotheses	mndpropd.1	$⊢ φ \to B = {Base}_{K}$
	mndpropd.2	$⊢ φ \to B = {Base}_{L}$
	mndpropd.3	$⊢ (φ \land (x \in B \land y \in B)) \to x +_{K} y = x +_{L} y$
Assertion	mndpropd	$⊢ φ \to (K \in Mnd \leftrightarrow L \in Mnd)$

Proof

Step	Hyp	Ref	Expression
1		mndpropd.1	$⊢ φ \to B = {Base}_{K}$
2		mndpropd.2	$⊢ φ \to B = {Base}_{L}$
3		mndpropd.3	$⊢ (φ \land (x \in B \land y \in B)) \to x +_{K} y = x +_{L} y$
4		simplr	$⊢ ((φ \land K \in Mnd) \land (x \in B \land y \in B)) \to K \in Mnd$
5		simprl	$⊢ ((φ \land K \in Mnd) \land (x \in B \land y \in B)) \to x \in B$
6	1	ad2antrr	$⊢ ((φ \land K \in Mnd) \land (x \in B \land y \in B)) \to B = {Base}_{K}$
7	5 6	eleqtrd	$⊢ ((φ \land K \in Mnd) \land (x \in B \land y \in B)) \to x \in {Base}_{K}$
8		simprr	$⊢ ((φ \land K \in Mnd) \land (x \in B \land y \in B)) \to y \in B$
9	8 6	eleqtrd	$⊢ ((φ \land K \in Mnd) \land (x \in B \land y \in B)) \to y \in {Base}_{K}$
10		eqid	$⊢ {Base}_{K} = {Base}_{K}$
11		eqid	$⊢ +_{K} = +_{K}$
12	10 11	mndcl	$⊢ (K \in Mnd \land x \in {Base}_{K} \land y \in {Base}_{K}) \to x +_{K} y \in {Base}_{K}$
13	4 7 9 12	syl3anc	$⊢ ((φ \land K \in Mnd) \land (x \in B \land y \in B)) \to x +_{K} y \in {Base}_{K}$
14	13 6	eleqtrrd	$⊢ ((φ \land K \in Mnd) \land (x \in B \land y \in B)) \to x +_{K} y \in B$
15	14	ralrimivva	$⊢ (φ \land K \in Mnd) \to \forall x \in B \forall y \in B x +_{K} y \in B$
16	15	ex	$⊢ φ \to (K \in Mnd \to \forall x \in B \forall y \in B x +_{K} y \in B)$
17		simplr	$⊢ ((φ \land L \in Mnd) \land (x \in B \land y \in B)) \to L \in Mnd$
18		simprl	$⊢ ((φ \land L \in Mnd) \land (x \in B \land y \in B)) \to x \in B$
19	2	ad2antrr	$⊢ ((φ \land L \in Mnd) \land (x \in B \land y \in B)) \to B = {Base}_{L}$
20	18 19	eleqtrd	$⊢ ((φ \land L \in Mnd) \land (x \in B \land y \in B)) \to x \in {Base}_{L}$
21		simprr	$⊢ ((φ \land L \in Mnd) \land (x \in B \land y \in B)) \to y \in B$
22	21 19	eleqtrd	$⊢ ((φ \land L \in Mnd) \land (x \in B \land y \in B)) \to y \in {Base}_{L}$
23		eqid	$⊢ {Base}_{L} = {Base}_{L}$
24		eqid	$⊢ +_{L} = +_{L}$
25	23 24	mndcl	$⊢ (L \in Mnd \land x \in {Base}_{L} \land y \in {Base}_{L}) \to x +_{L} y \in {Base}_{L}$
26	17 20 22 25	syl3anc	$⊢ ((φ \land L \in Mnd) \land (x \in B \land y \in B)) \to x +_{L} y \in {Base}_{L}$
27	3	adantlr	$⊢ ((φ \land L \in Mnd) \land (x \in B \land y \in B)) \to x +_{K} y = x +_{L} y$
28	26 27 19	3eltr4d	$⊢ ((φ \land L \in Mnd) \land (x \in B \land y \in B)) \to x +_{K} y \in B$
29	28	ralrimivva	$⊢ (φ \land L \in Mnd) \to \forall x \in B \forall y \in B x +_{K} y \in B$
30	29	ex	$⊢ φ \to (L \in Mnd \to \forall x \in B \forall y \in B x +_{K} y \in B)$
31	3	oveqrspc2v	$⊢ (φ \land (u \in B \land v \in B)) \to u +_{K} v = u +_{L} v$
32	31	adantlr	$⊢ ((φ \land \forall x \in B \forall y \in B x +_{K} y \in B) \land (u \in B \land v \in B)) \to u +_{K} v = u +_{L} v$
33	32	eleq1d	$⊢ ((φ \land \forall x \in B \forall y \in B x +_{K} y \in B) \land (u \in B \land v \in B)) \to (u +_{K} v \in B \leftrightarrow u +_{L} v \in B)$
34		simplll	$⊢ (((φ \land \forall x \in B \forall y \in B x +_{K} y \in B) \land (u \in B \land v \in B)) \land w \in B) \to φ$
35		simplrl	$⊢ (((φ \land \forall x \in B \forall y \in B x +_{K} y \in B) \land (u \in B \land v \in B)) \land w \in B) \to u \in B$
36		simplrr	$⊢ (((φ \land \forall x \in B \forall y \in B x +_{K} y \in B) \land (u \in B \land v \in B)) \land w \in B) \to v \in B$
37		simpllr	$⊢ (((φ \land \forall x \in B \forall y \in B x +_{K} y \in B) \land (u \in B \land v \in B)) \land w \in B) \to \forall x \in B \forall y \in B x +_{K} y \in B$
38		ovrspc2v	$⊢ ((u \in B \land v \in B) \land \forall x \in B \forall y \in B x +_{K} y \in B) \to u +_{K} v \in B$
39	35 36 37 38	syl21anc	$⊢ (((φ \land \forall x \in B \forall y \in B x +_{K} y \in B) \land (u \in B \land v \in B)) \land w \in B) \to u +_{K} v \in B$
40		simpr	$⊢ (((φ \land \forall x \in B \forall y \in B x +_{K} y \in B) \land (u \in B \land v \in B)) \land w \in B) \to w \in B$
41	3	oveqrspc2v	$⊢ (φ \land (u +_{K} v \in B \land w \in B)) \to (u +_{K} v) +_{K} w = (u +_{K} v) +_{L} w$
42	34 39 40 41	syl12anc	$⊢ (((φ \land \forall x \in B \forall y \in B x +_{K} y \in B) \land (u \in B \land v \in B)) \land w \in B) \to (u +_{K} v) +_{K} w = (u +_{K} v) +_{L} w$
43	34 35 36 31	syl12anc	$⊢ (((φ \land \forall x \in B \forall y \in B x +_{K} y \in B) \land (u \in B \land v \in B)) \land w \in B) \to u +_{K} v = u +_{L} v$
44	43	oveq1d	$⊢ (((φ \land \forall x \in B \forall y \in B x +_{K} y \in B) \land (u \in B \land v \in B)) \land w \in B) \to (u +_{K} v) +_{L} w = (u +_{L} v) +_{L} w$
45	42 44	eqtrd	$⊢ (((φ \land \forall x \in B \forall y \in B x +_{K} y \in B) \land (u \in B \land v \in B)) \land w \in B) \to (u +_{K} v) +_{K} w = (u +_{L} v) +_{L} w$
46		ovrspc2v	$⊢ ((v \in B \land w \in B) \land \forall x \in B \forall y \in B x +_{K} y \in B) \to v +_{K} w \in B$
47	36 40 37 46	syl21anc	$⊢ (((φ \land \forall x \in B \forall y \in B x +_{K} y \in B) \land (u \in B \land v \in B)) \land w \in B) \to v +_{K} w \in B$
48	3	oveqrspc2v	$⊢ (φ \land (u \in B \land v +_{K} w \in B)) \to u +_{K} (v +_{K} w) = u +_{L} (v +_{K} w)$
49	34 35 47 48	syl12anc	$⊢ (((φ \land \forall x \in B \forall y \in B x +_{K} y \in B) \land (u \in B \land v \in B)) \land w \in B) \to u +_{K} (v +_{K} w) = u +_{L} (v +_{K} w)$
50	3	oveqrspc2v	$⊢ (φ \land (v \in B \land w \in B)) \to v +_{K} w = v +_{L} w$
51	34 36 40 50	syl12anc	$⊢ (((φ \land \forall x \in B \forall y \in B x +_{K} y \in B) \land (u \in B \land v \in B)) \land w \in B) \to v +_{K} w = v +_{L} w$
52	51	oveq2d	$⊢ (((φ \land \forall x \in B \forall y \in B x +_{K} y \in B) \land (u \in B \land v \in B)) \land w \in B) \to u +_{L} (v +_{K} w) = u +_{L} (v +_{L} w)$
53	49 52	eqtrd	$⊢ (((φ \land \forall x \in B \forall y \in B x +_{K} y \in B) \land (u \in B \land v \in B)) \land w \in B) \to u +_{K} (v +_{K} w) = u +_{L} (v +_{L} w)$
54	45 53	eqeq12d	$⊢ (((φ \land \forall x \in B \forall y \in B x +_{K} y \in B) \land (u \in B \land v \in B)) \land w \in B) \to ((u +_{K} v) +_{K} w = u +_{K} (v +_{K} w) \leftrightarrow (u +_{L} v) +_{L} w = u +_{L} (v +_{L} w))$
55	54	ralbidva	$⊢ ((φ \land \forall x \in B \forall y \in B x +_{K} y \in B) \land (u \in B \land v \in B)) \to (\forall w \in B (u +_{K} v) +_{K} w = u +_{K} (v +_{K} w) \leftrightarrow \forall w \in B (u +_{L} v) +_{L} w = u +_{L} (v +_{L} w))$
56	33 55	anbi12d	$⊢ ((φ \land \forall x \in B \forall y \in B x +_{K} y \in B) \land (u \in B \land v \in B)) \to ((u +_{K} v \in B \land \forall w \in B (u +_{K} v) +_{K} w = u +_{K} (v +_{K} w)) \leftrightarrow (u +_{L} v \in B \land \forall w \in B (u +_{L} v) +_{L} w = u +_{L} (v +_{L} w)))$
57	56	2ralbidva	$⊢ (φ \land \forall x \in B \forall y \in B x +_{K} y \in B) \to (\forall u \in B \forall v \in B (u +_{K} v \in B \land \forall w \in B (u +_{K} v) +_{K} w = u +_{K} (v +_{K} w)) \leftrightarrow \forall u \in B \forall v \in B (u +_{L} v \in B \land \forall w \in B (u +_{L} v) +_{L} w = u +_{L} (v +_{L} w)))$
58	1	adantr	$⊢ (φ \land \forall x \in B \forall y \in B x +_{K} y \in B) \to B = {Base}_{K}$
59	58	eleq2d	$⊢ (φ \land \forall x \in B \forall y \in B x +_{K} y \in B) \to (u +_{K} v \in B \leftrightarrow u +_{K} v \in {Base}_{K})$
60	58	raleqdv	$⊢ (φ \land \forall x \in B \forall y \in B x +_{K} y \in B) \to (\forall w \in B (u +_{K} v) +_{K} w = u +_{K} (v +_{K} w) \leftrightarrow \forall w \in {Base}_{K} (u +_{K} v) +_{K} w = u +_{K} (v +_{K} w))$
61	59 60	anbi12d	$⊢ (φ \land \forall x \in B \forall y \in B x +_{K} y \in B) \to ((u +_{K} v \in B \land \forall w \in B (u +_{K} v) +_{K} w = u +_{K} (v +_{K} w)) \leftrightarrow (u +_{K} v \in {Base}_{K} \land \forall w \in {Base}_{K} (u +_{K} v) +_{K} w = u +_{K} (v +_{K} w)))$
62	58 61	raleqbidv	$⊢ (φ \land \forall x \in B \forall y \in B x +_{K} y \in B) \to (\forall v \in B (u +_{K} v \in B \land \forall w \in B (u +_{K} v) +_{K} w = u +_{K} (v +_{K} w)) \leftrightarrow \forall v \in {Base}_{K} (u +_{K} v \in {Base}_{K} \land \forall w \in {Base}_{K} (u +_{K} v) +_{K} w = u +_{K} (v +_{K} w)))$
63	58 62	raleqbidv	$⊢ (φ \land \forall x \in B \forall y \in B x +_{K} y \in B) \to (\forall u \in B \forall v \in B (u +_{K} v \in B \land \forall w \in B (u +_{K} v) +_{K} w = u +_{K} (v +_{K} w)) \leftrightarrow \forall u \in {Base}_{K} \forall v \in {Base}_{K} (u +_{K} v \in {Base}_{K} \land \forall w \in {Base}_{K} (u +_{K} v) +_{K} w = u +_{K} (v +_{K} w)))$
64	2	adantr	$⊢ (φ \land \forall x \in B \forall y \in B x +_{K} y \in B) \to B = {Base}_{L}$
65	64	eleq2d	$⊢ (φ \land \forall x \in B \forall y \in B x +_{K} y \in B) \to (u +_{L} v \in B \leftrightarrow u +_{L} v \in {Base}_{L})$
66	64	raleqdv	$⊢ (φ \land \forall x \in B \forall y \in B x +_{K} y \in B) \to (\forall w \in B (u +_{L} v) +_{L} w = u +_{L} (v +_{L} w) \leftrightarrow \forall w \in {Base}_{L} (u +_{L} v) +_{L} w = u +_{L} (v +_{L} w))$
67	65 66	anbi12d	$⊢ (φ \land \forall x \in B \forall y \in B x +_{K} y \in B) \to ((u +_{L} v \in B \land \forall w \in B (u +_{L} v) +_{L} w = u +_{L} (v +_{L} w)) \leftrightarrow (u +_{L} v \in {Base}_{L} \land \forall w \in {Base}_{L} (u +_{L} v) +_{L} w = u +_{L} (v +_{L} w)))$
68	64 67	raleqbidv	$⊢ (φ \land \forall x \in B \forall y \in B x +_{K} y \in B) \to (\forall v \in B (u +_{L} v \in B \land \forall w \in B (u +_{L} v) +_{L} w = u +_{L} (v +_{L} w)) \leftrightarrow \forall v \in {Base}_{L} (u +_{L} v \in {Base}_{L} \land \forall w \in {Base}_{L} (u +_{L} v) +_{L} w = u +_{L} (v +_{L} w)))$
69	64 68	raleqbidv	$⊢ (φ \land \forall x \in B \forall y \in B x +_{K} y \in B) \to (\forall u \in B \forall v \in B (u +_{L} v \in B \land \forall w \in B (u +_{L} v) +_{L} w = u +_{L} (v +_{L} w)) \leftrightarrow \forall u \in {Base}_{L} \forall v \in {Base}_{L} (u +_{L} v \in {Base}_{L} \land \forall w \in {Base}_{L} (u +_{L} v) +_{L} w = u +_{L} (v +_{L} w)))$
70	57 63 69	3bitr3d	$⊢ (φ \land \forall x \in B \forall y \in B x +_{K} y \in B) \to (\forall u \in {Base}_{K} \forall v \in {Base}_{K} (u +_{K} v \in {Base}_{K} \land \forall w \in {Base}_{K} (u +_{K} v) +_{K} w = u +_{K} (v +_{K} w)) \leftrightarrow \forall u \in {Base}_{L} \forall v \in {Base}_{L} (u +_{L} v \in {Base}_{L} \land \forall w \in {Base}_{L} (u +_{L} v) +_{L} w = u +_{L} (v +_{L} w)))$
71		simplll	$⊢ (((φ \land \forall x \in B \forall y \in B x +_{K} y \in B) \land s \in B) \land u \in B) \to φ$
72		simplr	$⊢ (((φ \land \forall x \in B \forall y \in B x +_{K} y \in B) \land s \in B) \land u \in B) \to s \in B$
73		simpr	$⊢ (((φ \land \forall x \in B \forall y \in B x +_{K} y \in B) \land s \in B) \land u \in B) \to u \in B$
74	3	oveqrspc2v	$⊢ (φ \land (s \in B \land u \in B)) \to s +_{K} u = s +_{L} u$
75	71 72 73 74	syl12anc	$⊢ (((φ \land \forall x \in B \forall y \in B x +_{K} y \in B) \land s \in B) \land u \in B) \to s +_{K} u = s +_{L} u$
76	75	eqeq1d	$⊢ (((φ \land \forall x \in B \forall y \in B x +_{K} y \in B) \land s \in B) \land u \in B) \to (s +_{K} u = u \leftrightarrow s +_{L} u = u)$
77	3	oveqrspc2v	$⊢ (φ \land (u \in B \land s \in B)) \to u +_{K} s = u +_{L} s$
78	71 73 72 77	syl12anc	$⊢ (((φ \land \forall x \in B \forall y \in B x +_{K} y \in B) \land s \in B) \land u \in B) \to u +_{K} s = u +_{L} s$
79	78	eqeq1d	$⊢ (((φ \land \forall x \in B \forall y \in B x +_{K} y \in B) \land s \in B) \land u \in B) \to (u +_{K} s = u \leftrightarrow u +_{L} s = u)$
80	76 79	anbi12d	$⊢ (((φ \land \forall x \in B \forall y \in B x +_{K} y \in B) \land s \in B) \land u \in B) \to ((s +_{K} u = u \land u +_{K} s = u) \leftrightarrow (s +_{L} u = u \land u +_{L} s = u))$
81	80	ralbidva	$⊢ ((φ \land \forall x \in B \forall y \in B x +_{K} y \in B) \land s \in B) \to (\forall u \in B (s +_{K} u = u \land u +_{K} s = u) \leftrightarrow \forall u \in B (s +_{L} u = u \land u +_{L} s = u))$
82	81	rexbidva	$⊢ (φ \land \forall x \in B \forall y \in B x +_{K} y \in B) \to (\exists s \in B \forall u \in B (s +_{K} u = u \land u +_{K} s = u) \leftrightarrow \exists s \in B \forall u \in B (s +_{L} u = u \land u +_{L} s = u))$
83	58	raleqdv	$⊢ (φ \land \forall x \in B \forall y \in B x +_{K} y \in B) \to (\forall u \in B (s +_{K} u = u \land u +_{K} s = u) \leftrightarrow \forall u \in {Base}_{K} (s +_{K} u = u \land u +_{K} s = u))$
84	58 83	rexeqbidv	$⊢ (φ \land \forall x \in B \forall y \in B x +_{K} y \in B) \to (\exists s \in B \forall u \in B (s +_{K} u = u \land u +_{K} s = u) \leftrightarrow \exists s \in {Base}_{K} \forall u \in {Base}_{K} (s +_{K} u = u \land u +_{K} s = u))$
85	64	raleqdv	$⊢ (φ \land \forall x \in B \forall y \in B x +_{K} y \in B) \to (\forall u \in B (s +_{L} u = u \land u +_{L} s = u) \leftrightarrow \forall u \in {Base}_{L} (s +_{L} u = u \land u +_{L} s = u))$
86	64 85	rexeqbidv	$⊢ (φ \land \forall x \in B \forall y \in B x +_{K} y \in B) \to (\exists s \in B \forall u \in B (s +_{L} u = u \land u +_{L} s = u) \leftrightarrow \exists s \in {Base}_{L} \forall u \in {Base}_{L} (s +_{L} u = u \land u +_{L} s = u))$
87	82 84 86	3bitr3d	$⊢ (φ \land \forall x \in B \forall y \in B x +_{K} y \in B) \to (\exists s \in {Base}_{K} \forall u \in {Base}_{K} (s +_{K} u = u \land u +_{K} s = u) \leftrightarrow \exists s \in {Base}_{L} \forall u \in {Base}_{L} (s +_{L} u = u \land u +_{L} s = u))$
88	70 87	anbi12d	$⊢ (φ \land \forall x \in B \forall y \in B x +_{K} y \in B) \to ((\forall u \in {Base}_{K} \forall v \in {Base}_{K} (u +_{K} v \in {Base}_{K} \land \forall w \in {Base}_{K} (u +_{K} v) +_{K} w = u +_{K} (v +_{K} w)) \land \exists s \in {Base}_{K} \forall u \in {Base}_{K} (s +_{K} u = u \land u +_{K} s = u)) \leftrightarrow (\forall u \in {Base}_{L} \forall v \in {Base}_{L} (u +_{L} v \in {Base}_{L} \land \forall w \in {Base}_{L} (u +_{L} v) +_{L} w = u +_{L} (v +_{L} w)) \land \exists s \in {Base}_{L} \forall u \in {Base}_{L} (s +_{L} u = u \land u +_{L} s = u)))$
89	10 11	ismnd	$⊢ K \in Mnd \leftrightarrow (\forall u \in {Base}_{K} \forall v \in {Base}_{K} (u +_{K} v \in {Base}_{K} \land \forall w \in {Base}_{K} (u +_{K} v) +_{K} w = u +_{K} (v +_{K} w)) \land \exists s \in {Base}_{K} \forall u \in {Base}_{K} (s +_{K} u = u \land u +_{K} s = u))$
90	23 24	ismnd	$⊢ L \in Mnd \leftrightarrow (\forall u \in {Base}_{L} \forall v \in {Base}_{L} (u +_{L} v \in {Base}_{L} \land \forall w \in {Base}_{L} (u +_{L} v) +_{L} w = u +_{L} (v +_{L} w)) \land \exists s \in {Base}_{L} \forall u \in {Base}_{L} (s +_{L} u = u \land u +_{L} s = u))$
91	88 89 90	3bitr4g	$⊢ (φ \land \forall x \in B \forall y \in B x +_{K} y \in B) \to (K \in Mnd \leftrightarrow L \in Mnd)$
92	91	ex	$⊢ φ \to (\forall x \in B \forall y \in B x +_{K} y \in B \to (K \in Mnd \leftrightarrow L \in Mnd))$
93	16 30 92	pm5.21ndd	$⊢ φ \to (K \in Mnd \leftrightarrow L \in Mnd)$

Metamath Proof Explorer

Theorem mndpropd

Proof