GROUPS - definition and basic properties

Definition A.G.1
(G,o,e) is a group if and only if the following conditions hold.

A.G.A0    e:-G
A.G.A1    /\(x,y:-G) xoy:-G
A.G.A2    /\(x:-G) eox = x
A.G.A3    /\(x:-G)\/(y:-G) yox = e
A.G.A4    /\(x,y,z:-G) (xoy)oz = xo(yoz)

Theorem A.G.2
If (G,o,e) is a group, x:-G and xox=x then x=e.

Proof
By A.G.A1 we have y:-G such that yox=e. 
Since xox = x we get yo(xox) = yox.
By A.G.A4 we have (yox)ox = yox.
Thus eox = e and by A.G.A2 we get x = e. 

Theorem A.G.3
If (G,o,e) is a group, x,y:-G and yox = e then xoy = e.

Proof
Follow the calculations below.
(xoy)o(xoy) = xo(yox)oy = xoeoy = xo(eoy) = xoy.
Now by Theorem A.G.2 we have xoy = e.

Theorem A.G.4
If (G,o,e) is a group and x:-G then xoe = x.

Proof
By A.G.A1 we have y:-G such that yox = e.
By Theorem A.G.3 xoy = e.
Now, follow the calculations below.
xoe = xo(yox) = (xoy)ox = eox = x.
Thus xoe = x.

Theorem A.G.5
If (G,o,e) is a group, a:-G and /\(x:-G) aox = x then a = e.

Proof
By assumption we get aoa = a and by Theorem A.G.2 a = e.   

Theorem A.G.6
If (G,o,e) is a group, a:-G and /\(x:-G) xoa = x then a = e.

Proof
By assumption we get aoa = a and by Theorem A.G.2 a = e.

Theorem A.G.7
If (G,o,e) is a group, x:-G, y1,y2:-G and y1ox = y2ox = e then y1 = y2.

Proof
Follow the calculations below.
y1 = y1oe = y1o(xoy2) = (y1ox)oy2 = eoy2 = y2. Thus y1 = y2.

Definition A.G.8
Let (G,o,e) be a group and x,y:-G.
We define that y is the inverse of x if and only if yox = e.