sgrppropd

Description: If two structures are sets, 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 semigroup iff the other one is. (Contributed by AV, 15-Feb-2025)

	Ref	Expression
Hypotheses	sgrppropd.k	$⊢ φ \to K \in V$
	sgrppropd.l	$⊢ φ \to L \in W$
	sgrppropd.1	$⊢ φ \to B = {Base}_{K}$
	sgrppropd.2	$⊢ φ \to B = {Base}_{L}$
	sgrppropd.3	$⊢ (φ \land (x \in B \land y \in B)) \to x +_{K} y = x +_{L} y$
Assertion	sgrppropd	$⊢ φ \to (K \in Smgrp \leftrightarrow L \in Smgrp)$

Proof

Step	Hyp	Ref	Expression
1		sgrppropd.k	$⊢ φ \to K \in V$
2		sgrppropd.l	$⊢ φ \to L \in W$
3		sgrppropd.1	$⊢ φ \to B = {Base}_{K}$
4		sgrppropd.2	$⊢ φ \to B = {Base}_{L}$
5		sgrppropd.3	$⊢ (φ \land (x \in B \land y \in B)) \to x +_{K} y = x +_{L} y$
6		simplr	$⊢ ((φ \land K \in Smgrp) \land (x \in B \land y \in B)) \to K \in Smgrp$
7		simprl	$⊢ ((φ \land K \in Smgrp) \land (x \in B \land y \in B)) \to x \in B$
8	3	ad2antrr	$⊢ ((φ \land K \in Smgrp) \land (x \in B \land y \in B)) \to B = {Base}_{K}$
9	7 8	eleqtrd	$⊢ ((φ \land K \in Smgrp) \land (x \in B \land y \in B)) \to x \in {Base}_{K}$
10		simprr	$⊢ ((φ \land K \in Smgrp) \land (x \in B \land y \in B)) \to y \in B$
11	10 8	eleqtrd	$⊢ ((φ \land K \in Smgrp) \land (x \in B \land y \in B)) \to y \in {Base}_{K}$
12		eqid	$⊢ {Base}_{K} = {Base}_{K}$
13		eqid	$⊢ +_{K} = +_{K}$
14	12 13	sgrpcl	$⊢ (K \in Smgrp \land x \in {Base}_{K} \land y \in {Base}_{K}) \to x +_{K} y \in {Base}_{K}$
15	6 9 11 14	syl3anc	$⊢ ((φ \land K \in Smgrp) \land (x \in B \land y \in B)) \to x +_{K} y \in {Base}_{K}$
16	15 8	eleqtrrd	$⊢ ((φ \land K \in Smgrp) \land (x \in B \land y \in B)) \to x +_{K} y \in B$
17	16	ralrimivva	$⊢ (φ \land K \in Smgrp) \to \forall x \in B \forall y \in B x +_{K} y \in B$
18	17	ex	$⊢ φ \to (K \in Smgrp \to \forall x \in B \forall y \in B x +_{K} y \in B)$
19		simplr	$⊢ ((φ \land L \in Smgrp) \land (x \in B \land y \in B)) \to L \in Smgrp$
20		simprl	$⊢ ((φ \land L \in Smgrp) \land (x \in B \land y \in B)) \to x \in B$
21	4	ad2antrr	$⊢ ((φ \land L \in Smgrp) \land (x \in B \land y \in B)) \to B = {Base}_{L}$
22	20 21	eleqtrd	$⊢ ((φ \land L \in Smgrp) \land (x \in B \land y \in B)) \to x \in {Base}_{L}$
23		simprr	$⊢ ((φ \land L \in Smgrp) \land (x \in B \land y \in B)) \to y \in B$
24	23 21	eleqtrd	$⊢ ((φ \land L \in Smgrp) \land (x \in B \land y \in B)) \to y \in {Base}_{L}$
25		eqid	$⊢ {Base}_{L} = {Base}_{L}$
26		eqid	$⊢ +_{L} = +_{L}$
27	25 26	sgrpcl	$⊢ (L \in Smgrp \land x \in {Base}_{L} \land y \in {Base}_{L}) \to x +_{L} y \in {Base}_{L}$
28	19 22 24 27	syl3anc	$⊢ ((φ \land L \in Smgrp) \land (x \in B \land y \in B)) \to x +_{L} y \in {Base}_{L}$
29	5	adantlr	$⊢ ((φ \land L \in Smgrp) \land (x \in B \land y \in B)) \to x +_{K} y = x +_{L} y$
30	28 29 21	3eltr4d	$⊢ ((φ \land L \in Smgrp) \land (x \in B \land y \in B)) \to x +_{K} y \in B$
31	30	ralrimivva	$⊢ (φ \land L \in Smgrp) \to \forall x \in B \forall y \in B x +_{K} y \in B$
32	31	ex	$⊢ φ \to (L \in Smgrp \to \forall x \in B \forall y \in B x +_{K} y \in B)$
33	12 13	issgrpv	$⊢ K \in V \to (K \in Smgrp \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)))$
34	1 33	syl	$⊢ φ \to (K \in Smgrp \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)))$
35	34	adantr	$⊢ (φ \land \forall x \in B \forall y \in B x +_{K} y \in B) \to (K \in Smgrp \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)))$
36	5	oveqrspc2v	$⊢ (φ \land (u \in B \land v \in B)) \to u +_{K} v = u +_{L} v$
37	36	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$
38	37	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)$
39		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 φ$
40		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$
41		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$
42		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$
43		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$
44	40 41 42 43	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$
45		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$
46	5	oveqrspc2v	$⊢ (φ \land (u +_{K} v \in B \land w \in B)) \to (u +_{K} v) +_{K} w = (u +_{K} v) +_{L} w$
47	39 44 45 46	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$
48	39 40 41 36	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$
49	48	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$
50	47 49	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$
51		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$
52	41 45 42 51	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$
53	5	oveqrspc2v	$⊢ (φ \land (u \in B \land v +_{K} w \in B)) \to u +_{K} (v +_{K} w) = u +_{L} (v +_{K} w)$
54	39 40 52 53	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)$
55	5	oveqrspc2v	$⊢ (φ \land (v \in B \land w \in B)) \to v +_{K} w = v +_{L} w$
56	39 41 45 55	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$
57	56	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)$
58	54 57	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)$
59	50 58	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))$
60	59	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))$
61	38 60	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)))$
62	61	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)))$
63	3	adantr	$⊢ (φ \land \forall x \in B \forall y \in B x +_{K} y \in B) \to B = {Base}_{K}$
64	63	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})$
65	63	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))$
66	64 65	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)))$
67	63 66	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)))$
68	63 67	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)))$
69	4	adantr	$⊢ (φ \land \forall x \in B \forall y \in B x +_{K} y \in B) \to B = {Base}_{L}$
70	69	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})$
71	69	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))$
72	70 71	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)))$
73	69 72	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)))$
74	69 73	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)))$
75	62 68 74	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)))$
76	25 26	issgrpv	$⊢ L \in W \to (L \in Smgrp \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)))$
77	2 76	syl	$⊢ φ \to (L \in Smgrp \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)))$
78	77	bicomd	$⊢ φ \to (\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)) \leftrightarrow L \in Smgrp)$
79	78	adantr	$⊢ (φ \land \forall x \in B \forall y \in B x +_{K} y \in B) \to (\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)) \leftrightarrow L \in Smgrp)$
80	35 75 79	3bitrd	$⊢ (φ \land \forall x \in B \forall y \in B x +_{K} y \in B) \to (K \in Smgrp \leftrightarrow L \in Smgrp)$
81	80	ex	$⊢ φ \to (\forall x \in B \forall y \in B x +_{K} y \in B \to (K \in Smgrp \leftrightarrow L \in Smgrp))$
82	18 32 81	pm5.21ndd	$⊢ φ \to (K \in Smgrp \leftrightarrow L \in Smgrp)$

Metamath Proof Explorer

Theorem sgrppropd

Proof