FIELDS - definition and basic properties

Definition A.F.1
(K,+,*,0,1) is a field if and only if the following conditions hold.

A.F.A1    (K,+,0) is a group.
A.F.A2    /\(x,y:-K) x+y = y+x
A.F.A3    /\(x,y:-K) x*y:-K
A.F.A4    (K\{0},*,1) is a group
A.F.A5    /\(x,y:-K) x*y = y*x
A.F.A6    /\(x,y,z):-K z*(x+y) = z*x+z*y

Theorem A.F.2
If (K,+,*,0,1) is a field and x:-K then x*0 = 0.

Proof
By A.F.A6 x*0 + x*0 = x*(0+0).
By A.F.A2 0+0 = 0.
Thus x*0 + x*0 = x*0. 
Now by A.F.A2 and Theorem A.G.2 x*0 = 0.

Definition A.F.3
Let (K,+,*,0,1) be a field and x,y:-K.
We define that y = -x if and only if y+x = 0. 

Remark A.F.4
Definition A.F.3 is correct because of Theorem A.G.7. 

Theorem A.F.5
If (K,+,*,0,1) is a field and x:-K then (-1)*x = -x.

Proof
Follow the calculations below.
(-1)*x+x = x*(-1)+x*1 = x*(-1+1) = x*0 = 0.
Thus by Definition A.F.3 (-1)*x = -x.

Definition A.F.6
Let (K,+,*,0,1) be a field and x,y:-K\{0}.
We define that y = x^(-1) if and only if y*x = 1. 

Remark A.F.7
Definition A.F.6 is correct because of Theorem A.G.7.

Theorem A.F.8
If (K,+,*,0,1) is a field, x,y:-K and x*y = 0 then x = 0 or y = 0.

Proof
Assume to the contrary that x != 0 and y != 0.
By A.F.A4 there exist  x^(-1) and y^(-1).
By Theorem A.F.2 ( (y^(-1))*(x^(-1)) )*x*y = 0.
By A.F.A4 ( (y^(-1))*(x^(-1)) )*x*y = (y^(-1))*y = 1. Thus 1 = 0.
But by A.F.A4 1:-K\{0}. Thus 1 != 0. Contradiction.
We have proved that x = 0 or y = 0.