Theorem dfgrp3e

Description: Alternate definition of a group as a set with a closed, associative operation, for which solutions x and y of the equations ( a .+ x ) = b and ( x .+ a ) = b exist. Exercise 1 of Herstein p. 57. (Contributed by NM, 5-Dec-2006) (Revised by AV, 28-Aug-2021)

	Ref	Expression
Hypotheses	dfgrp3.b	$$⊢B={\mathrm{Base}}_G$$
	dfgrp3.p	$$⊢\underset{\dot{}}{+}={+}_G$$
Assertion	dfgrp3e	$$⊢G\in \mathrm{Grp}\leftrightarrow \left(B\ne \varnothing \wedge \forall x\in B\forall y\in B\left(x\underset{\dot{}}{+}y\in B\wedge \forall z\in B\left(x\underset{\dot{}}{+}y\right)\underset{\dot{}}{+}z=x\underset{\dot{}}{+}\left(y\underset{\dot{}}{+}z\right)\wedge \left(\exists l\in Bl\underset{\dot{}}{+}x=y\wedge \exists r\in Bx\underset{\dot{}}{+}r=y\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		dfgrp3.b	$$⊢B={\mathrm{Base}}_G$$
2		dfgrp3.p	$$⊢\underset{\dot{}}{+}={+}_G$$
3	1 2	dfgrp3	Could not format ( G e. Grp <-> ( G e. Smgrp /\ B =/= (/) /\ A. x e. B A. y e. B ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) ) : No typesetting found for |- ( G e. Grp <-> ( G e. Smgrp /\ B =/= (/) /\ A. x e. B A. y e. B ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) ) with typecode |-
4		simp2	Could not format ( ( G e. Smgrp /\ B =/= (/) /\ A. x e. B A. y e. B ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) -> B =/= (/) ) : No typesetting found for |- ( ( G e. Smgrp /\ B =/= (/) /\ A. x e. B A. y e. B ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) -> B =/= (/) ) with typecode |-
5		sgrpmgm	Could not format ( G e. Smgrp -> G e. Mgm ) : No typesetting found for |- ( G e. Smgrp -> G e. Mgm ) with typecode |-
6	5	adantr	Could not format ( ( G e. Smgrp /\ x e. B ) -> G e. Mgm ) : No typesetting found for |- ( ( G e. Smgrp /\ x e. B ) -> G e. Mgm ) with typecode |-
7	6	adantr	Could not format ( ( ( G e. Smgrp /\ x e. B ) /\ y e. B ) -> G e. Mgm ) : No typesetting found for |- ( ( ( G e. Smgrp /\ x e. B ) /\ y e. B ) -> G e. Mgm ) with typecode |-
8		simpr	Could not format ( ( G e. Smgrp /\ x e. B ) -> x e. B ) : No typesetting found for |- ( ( G e. Smgrp /\ x e. B ) -> x e. B ) with typecode |-
9	8	adantr	Could not format ( ( ( G e. Smgrp /\ x e. B ) /\ y e. B ) -> x e. B ) : No typesetting found for |- ( ( ( G e. Smgrp /\ x e. B ) /\ y e. B ) -> x e. B ) with typecode |-
10		simpr	Could not format ( ( ( G e. Smgrp /\ x e. B ) /\ y e. B ) -> y e. B ) : No typesetting found for |- ( ( ( G e. Smgrp /\ x e. B ) /\ y e. B ) -> y e. B ) with typecode |-
11	1 2	mgmcl	$$⊢\left(G\in \mathrm{Mgm}\wedge x\in B\wedge y\in B\right)\to x\underset{\dot{}}{+}y\in B$$
12	7 9 10 11	syl3anc	Could not format ( ( ( G e. Smgrp /\ x e. B ) /\ y e. B ) -> ( x .+ y ) e. B ) : No typesetting found for |- ( ( ( G e. Smgrp /\ x e. B ) /\ y e. B ) -> ( x .+ y ) e. B ) with typecode |-
13	12	adantr	Could not format ( ( ( ( G e. Smgrp /\ x e. B ) /\ y e. B ) /\ ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) -> ( x .+ y ) e. B ) : No typesetting found for |- ( ( ( ( G e. Smgrp /\ x e. B ) /\ y e. B ) /\ ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) -> ( x .+ y ) e. B ) with typecode |-
14	1 2	sgrpass	Could not format ( ( G e. Smgrp /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) ) : No typesetting found for |- ( ( G e. Smgrp /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) ) with typecode |-
15	14	3anassrs	Could not format ( ( ( ( G e. Smgrp /\ x e. B ) /\ y e. B ) /\ z e. B ) -> ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) ) : No typesetting found for |- ( ( ( ( G e. Smgrp /\ x e. B ) /\ y e. B ) /\ z e. B ) -> ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) ) with typecode |-
16	15	ralrimiva	Could not format ( ( ( G e. Smgrp /\ x e. B ) /\ y e. B ) -> A. z e. B ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) ) : No typesetting found for |- ( ( ( G e. Smgrp /\ x e. B ) /\ y e. B ) -> A. z e. B ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) ) with typecode |-
17	16	adantr	Could not format ( ( ( ( G e. Smgrp /\ x e. B ) /\ y e. B ) /\ ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) -> A. z e. B ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) ) : No typesetting found for |- ( ( ( ( G e. Smgrp /\ x e. B ) /\ y e. B ) /\ ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) -> A. z e. B ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) ) with typecode |-
18		simpr	Could not format ( ( ( ( G e. Smgrp /\ x e. B ) /\ y e. B ) /\ ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) -> ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) : No typesetting found for |- ( ( ( ( G e. Smgrp /\ x e. B ) /\ y e. B ) /\ ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) -> ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) with typecode |-
19	13 17 18	3jca	Could not format ( ( ( ( G e. Smgrp /\ x e. B ) /\ y e. B ) /\ ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) -> ( ( x .+ y ) e. B /\ A. z e. B ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) /\ ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) ) : No typesetting found for |- ( ( ( ( G e. Smgrp /\ x e. B ) /\ y e. B ) /\ ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) -> ( ( x .+ y ) e. B /\ A. z e. B ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) /\ ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) ) with typecode |-
20	19	ex	Could not format ( ( ( G e. Smgrp /\ x e. B ) /\ y e. B ) -> ( ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) -> ( ( x .+ y ) e. B /\ A. z e. B ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) /\ ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) ) ) : No typesetting found for |- ( ( ( G e. Smgrp /\ x e. B ) /\ y e. B ) -> ( ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) -> ( ( x .+ y ) e. B /\ A. z e. B ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) /\ ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) ) ) with typecode |-
21	20	ralimdva	Could not format ( ( G e. Smgrp /\ x e. B ) -> ( A. y e. B ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) -> A. y e. B ( ( x .+ y ) e. B /\ A. z e. B ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) /\ ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) ) ) : No typesetting found for |- ( ( G e. Smgrp /\ x e. B ) -> ( A. y e. B ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) -> A. y e. B ( ( x .+ y ) e. B /\ A. z e. B ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) /\ ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) ) ) with typecode |-
22	21	ralimdva	Could not format ( G e. Smgrp -> ( A. x e. B A. y e. B ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) -> A. x e. B A. y e. B ( ( x .+ y ) e. B /\ A. z e. B ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) /\ ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) ) ) : No typesetting found for |- ( G e. Smgrp -> ( A. x e. B A. y e. B ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) -> A. x e. B A. y e. B ( ( x .+ y ) e. B /\ A. z e. B ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) /\ ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) ) ) with typecode |-
23	22	a1d	Could not format ( G e. Smgrp -> ( B =/= (/) -> ( A. x e. B A. y e. B ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) -> A. x e. B A. y e. B ( ( x .+ y ) e. B /\ A. z e. B ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) /\ ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) ) ) ) : No typesetting found for |- ( G e. Smgrp -> ( B =/= (/) -> ( A. x e. B A. y e. B ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) -> A. x e. B A. y e. B ( ( x .+ y ) e. B /\ A. z e. B ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) /\ ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) ) ) ) with typecode |-
24	23	3imp	Could not format ( ( G e. Smgrp /\ B =/= (/) /\ A. x e. B A. y e. B ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) -> A. x e. B A. y e. B ( ( x .+ y ) e. B /\ A. z e. B ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) /\ ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) ) : No typesetting found for |- ( ( G e. Smgrp /\ B =/= (/) /\ A. x e. B A. y e. B ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) -> A. x e. B A. y e. B ( ( x .+ y ) e. B /\ A. z e. B ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) /\ ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) ) with typecode |-
25	4 24	jca	Could not format ( ( G e. Smgrp /\ B =/= (/) /\ A. x e. B A. y e. B ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) -> ( B =/= (/) /\ A. x e. B A. y e. B ( ( x .+ y ) e. B /\ A. z e. B ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) /\ ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) ) ) : No typesetting found for |- ( ( G e. Smgrp /\ B =/= (/) /\ A. x e. B A. y e. B ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) -> ( B =/= (/) /\ A. x e. B A. y e. B ( ( x .+ y ) e. B /\ A. z e. B ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) /\ ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) ) ) with typecode |-
26		n0	$$⊢B\ne \varnothing \leftrightarrow \exists aa\in B$$
27		3simpa	$$⊢\left(x\underset{\dot{}}{+}y\in B\wedge \forall z\in B\left(x\underset{\dot{}}{+}y\right)\underset{\dot{}}{+}z=x\underset{\dot{}}{+}\left(y\underset{\dot{}}{+}z\right)\wedge \left(\exists l\in Bl\underset{\dot{}}{+}x=y\wedge \exists r\in Bx\underset{\dot{}}{+}r=y\right)\right)\to \left(x\underset{\dot{}}{+}y\in B\wedge \forall z\in B\left(x\underset{\dot{}}{+}y\right)\underset{\dot{}}{+}z=x\underset{\dot{}}{+}\left(y\underset{\dot{}}{+}z\right)\right)$$
28	27	2ralimi	$$⊢\forall x\in B\forall y\in B\left(x\underset{\dot{}}{+}y\in B\wedge \forall z\in B\left(x\underset{\dot{}}{+}y\right)\underset{\dot{}}{+}z=x\underset{\dot{}}{+}\left(y\underset{\dot{}}{+}z\right)\wedge \left(\exists l\in Bl\underset{\dot{}}{+}x=y\wedge \exists r\in Bx\underset{\dot{}}{+}r=y\right)\right)\to \forall x\in B\forall y\in B\left(x\underset{\dot{}}{+}y\in B\wedge \forall z\in B\left(x\underset{\dot{}}{+}y\right)\underset{\dot{}}{+}z=x\underset{\dot{}}{+}\left(y\underset{\dot{}}{+}z\right)\right)$$
29	1 2	issgrpn0	Could not format ( a e. B -> ( G e. Smgrp <-> A. x e. B A. y e. B ( ( x .+ y ) e. B /\ A. z e. B ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) ) ) ) : No typesetting found for |- ( a e. B -> ( G e. Smgrp <-> A. x e. B A. y e. B ( ( x .+ y ) e. B /\ A. z e. B ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) ) ) ) with typecode |-
30	28 29	syl5ibr	Could not format ( a e. B -> ( A. x e. B A. y e. B ( ( x .+ y ) e. B /\ A. z e. B ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) /\ ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) -> G e. Smgrp ) ) : No typesetting found for |- ( a e. B -> ( A. x e. B A. y e. B ( ( x .+ y ) e. B /\ A. z e. B ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) /\ ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) -> G e. Smgrp ) ) with typecode |-
31	30	exlimiv	Could not format ( E. a a e. B -> ( A. x e. B A. y e. B ( ( x .+ y ) e. B /\ A. z e. B ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) /\ ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) -> G e. Smgrp ) ) : No typesetting found for |- ( E. a a e. B -> ( A. x e. B A. y e. B ( ( x .+ y ) e. B /\ A. z e. B ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) /\ ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) -> G e. Smgrp ) ) with typecode |-
32	26 31	sylbi	Could not format ( B =/= (/) -> ( A. x e. B A. y e. B ( ( x .+ y ) e. B /\ A. z e. B ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) /\ ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) -> G e. Smgrp ) ) : No typesetting found for |- ( B =/= (/) -> ( A. x e. B A. y e. B ( ( x .+ y ) e. B /\ A. z e. B ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) /\ ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) -> G e. Smgrp ) ) with typecode |-
33	32	imp	Could not format ( ( B =/= (/) /\ A. x e. B A. y e. B ( ( x .+ y ) e. B /\ A. z e. B ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) /\ ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) ) -> G e. Smgrp ) : No typesetting found for |- ( ( B =/= (/) /\ A. x e. B A. y e. B ( ( x .+ y ) e. B /\ A. z e. B ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) /\ ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) ) -> G e. Smgrp ) with typecode |-
34		simpl	$$⊢\left(B\ne \varnothing \wedge \forall x\in B\forall y\in B\left(x\underset{\dot{}}{+}y\in B\wedge \forall z\in B\left(x\underset{\dot{}}{+}y\right)\underset{\dot{}}{+}z=x\underset{\dot{}}{+}\left(y\underset{\dot{}}{+}z\right)\wedge \left(\exists l\in Bl\underset{\dot{}}{+}x=y\wedge \exists r\in Bx\underset{\dot{}}{+}r=y\right)\right)\right)\to B\ne \varnothing$$
35		simp3	$$⊢\left(x\underset{\dot{}}{+}y\in B\wedge \forall z\in B\left(x\underset{\dot{}}{+}y\right)\underset{\dot{}}{+}z=x\underset{\dot{}}{+}\left(y\underset{\dot{}}{+}z\right)\wedge \left(\exists l\in Bl\underset{\dot{}}{+}x=y\wedge \exists r\in Bx\underset{\dot{}}{+}r=y\right)\right)\to \left(\exists l\in Bl\underset{\dot{}}{+}x=y\wedge \exists r\in Bx\underset{\dot{}}{+}r=y\right)$$
36	35	2ralimi	$$⊢\forall x\in B\forall y\in B\left(x\underset{\dot{}}{+}y\in B\wedge \forall z\in B\left(x\underset{\dot{}}{+}y\right)\underset{\dot{}}{+}z=x\underset{\dot{}}{+}\left(y\underset{\dot{}}{+}z\right)\wedge \left(\exists l\in Bl\underset{\dot{}}{+}x=y\wedge \exists r\in Bx\underset{\dot{}}{+}r=y\right)\right)\to \forall x\in B\forall y\in B\left(\exists l\in Bl\underset{\dot{}}{+}x=y\wedge \exists r\in Bx\underset{\dot{}}{+}r=y\right)$$
37	36	adantl	$$⊢\left(B\ne \varnothing \wedge \forall x\in B\forall y\in B\left(x\underset{\dot{}}{+}y\in B\wedge \forall z\in B\left(x\underset{\dot{}}{+}y\right)\underset{\dot{}}{+}z=x\underset{\dot{}}{+}\left(y\underset{\dot{}}{+}z\right)\wedge \left(\exists l\in Bl\underset{\dot{}}{+}x=y\wedge \exists r\in Bx\underset{\dot{}}{+}r=y\right)\right)\right)\to \forall x\in B\forall y\in B\left(\exists l\in Bl\underset{\dot{}}{+}x=y\wedge \exists r\in Bx\underset{\dot{}}{+}r=y\right)$$
38	33 34 37	3jca	Could not format ( ( B =/= (/) /\ A. x e. B A. y e. B ( ( x .+ y ) e. B /\ A. z e. B ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) /\ ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) ) -> ( G e. Smgrp /\ B =/= (/) /\ A. x e. B A. y e. B ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) ) : No typesetting found for |- ( ( B =/= (/) /\ A. x e. B A. y e. B ( ( x .+ y ) e. B /\ A. z e. B ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) /\ ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) ) -> ( G e. Smgrp /\ B =/= (/) /\ A. x e. B A. y e. B ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) ) with typecode |-
39	25 38	impbii	Could not format ( ( G e. Smgrp /\ B =/= (/) /\ A. x e. B A. y e. B ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) <-> ( B =/= (/) /\ A. x e. B A. y e. B ( ( x .+ y ) e. B /\ A. z e. B ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) /\ ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) ) ) : No typesetting found for |- ( ( G e. Smgrp /\ B =/= (/) /\ A. x e. B A. y e. B ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) <-> ( B =/= (/) /\ A. x e. B A. y e. B ( ( x .+ y ) e. B /\ A. z e. B ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) /\ ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) ) ) with typecode |-
40	3 39	bitri	$$⊢G\in \mathrm{Grp}\leftrightarrow \left(B\ne \varnothing \wedge \forall x\in B\forall y\in B\left(x\underset{\dot{}}{+}y\in B\wedge \forall z\in B\left(x\underset{\dot{}}{+}y\right)\underset{\dot{}}{+}z=x\underset{\dot{}}{+}\left(y\underset{\dot{}}{+}z\right)\wedge \left(\exists l\in Bl\underset{\dot{}}{+}x=y\wedge \exists r\in Bx\underset{\dot{}}{+}r=y\right)\right)\right)$$