# IsarMathLib

## Proofs by humans, for humans, formally verified by Isabelle/ZF proof assistant

theory Field_ZF imports Ring_ZF
begin

This theory covers basic facts about fields.

### Definition and basic properties

In this section we define what is a field and list the basic properties of fields.

Field is a notrivial commutative ring such that all non-zero elements have an inverse. We define the notion of being a field as a statement about three sets. The first set, denoted K is the carrier of the field. The second set, denoted A represents the additive operation on K (recall that in ZF set theory functions are sets). The third set M represents the multiplicative operation on K.

Definition

$$\text{IsAfield}(K,A,M) \equiv$$ $$( \text{IsAring}(K,A,M) \wedge (M \text{ is commutative on } K) \wedge$$ $$\text{ TheNeutralElement}(K,A) \neq \text{ TheNeutralElement}(K,M) \wedge$$ $$(\forall a\in K.\ a\neq \text{ TheNeutralElement}(K,A)\longrightarrow$$ $$(\exists b\in K.\ M\langle a,b\rangle = \text{ TheNeutralElement}(K,M))))$$

The field0 context extends the ring0 context adding field-related assumptions and notation related to the multiplicative inverse.

Locale field0 = ring0 K A M +

assumes mult_commute: $$M \text{ is commutative on } K$$

assumes not_triv: $$0 \neq 1$$

assumes inv_exists: $$\forall a\in K.\ a\neq 0 \longrightarrow (\exists b\in K.\ a\cdot b = 1 )$$

defines $$K_0 \equiv K-\{ 0 \}$$

defines $$a^{-1} \equiv \text{GroupInv}(K_0,\text{restrict}(M,K_0\times K_0))(a)$$

The next lemma assures us that we are talking fields in the field0 context.

lemma (in field0) Field_ZF_1_L1:

shows $$\text{IsAfield}(K,A,M)$$ using ringAssum, mult_commute, not_triv, inv_exists, IsAfield_def

We can use theorems proven in the field0 context whenever we talk about a field.

lemma field_field0:

assumes $$\text{IsAfield}(K,A,M)$$

shows $$field0(K,A,M)$$ using assms, IsAfield_def, field0_axioms.intro, ring0_def, field0_def

Let's have an explicit statement that the multiplication in fields is commutative.

lemma (in field0) field_mult_comm:

assumes $$a\in K$$, $$b\in K$$

shows $$a\cdot b = b\cdot a$$ using mult_commute, assms, IsCommutative_def

Fields do not have zero divisors.

lemma (in field0) field_has_no_zero_divs:

shows $$\text{HasNoZeroDivs}(K,A,M)$$proof
{
fix $$a$$ $$b$$
assume A1: $$a\in K$$, $$b\in K$$ and A2: $$a\cdot b = 0$$ and A3: $$b\neq 0$$
from inv_exists, A1, A3 obtain $$c$$ where I: $$c\in K$$ and II: $$b\cdot c = 1$$
from A2 have $$a\cdot b\cdot c = 0 \cdot c$$
with A1, I have $$a\cdot (b\cdot c) = 0$$ using Ring_ZF_1_L11, Ring_ZF_1_L6
with A1, II have $$a= 0$$ using Ring_ZF_1_L3
}
then have $$\forall a\in K.\ \forall b\in K.\ a\cdot b = 0 \longrightarrow a= 0 \vee b= 0$$
then show $$thesis$$ using HasNoZeroDivs_def
qed

$$K_0$$ (the set of nonzero field elements is closed with respect to multiplication.

lemma (in field0) Field_ZF_1_L2:

shows $$K_0 \text{ is closed under } M$$ using Ring_ZF_1_L4, field_has_no_zero_divs, Ring_ZF_1_L12, IsOpClosed_def

Any nonzero element has a right inverse that is nonzero.

lemma (in field0) Field_ZF_1_L3:

assumes A1: $$a\in K_0$$

shows $$\exists b\in K_0.\ a\cdot b = 1$$proof
from inv_exists, A1 obtain $$b$$ where $$b\in K$$ and $$a\cdot b = 1$$
with not_triv, A1 show $$\exists b\in K_0.\ a\cdot b = 1$$ using Ring_ZF_1_L6
qed

If we remove zero, the field with multiplication becomes a group and we can use all theorems proven in group0 context.

theorem (in field0) Field_ZF_1_L4:

shows $$\text{IsAgroup}(K_0,\text{restrict}(M,K_0\times K_0))$$, $$group0(K_0,\text{restrict}(M,K_0\times K_0))$$, $$1 = \text{ TheNeutralElement}(K_0,\text{restrict}(M,K_0\times K_0))$$proof
let $$f = \text{restrict}(M,K_0\times K_0)$$
have $$M \text{ is associative on } K$$, $$K_0 \subseteq K$$, $$K_0 \text{ is closed under } M$$ using Field_ZF_1_L1, IsAfield_def, IsAring_def, IsAgroup_def, IsAmonoid_def, Field_ZF_1_L2
then have $$f \text{ is associative on } K_0$$ using func_ZF_4_L3
moreover
from not_triv have I: $$1 \in K_0 \wedge (\forall a\in K_0.\ f\langle 1 ,a\rangle = a \wedge f\langle a,1 \rangle = a)$$ using Ring_ZF_1_L2, Ring_ZF_1_L3
then have $$\exists n\in K_0.\ \forall a\in K_0.\ f\langle n,a\rangle = a \wedge f\langle a,n\rangle = a$$
ultimately have II: $$\text{IsAmonoid}(K_0,f)$$ using IsAmonoid_def
then have $$monoid0(K_0,f)$$ using monoid0_def
moreover
note I
ultimately show $$1 = \text{ TheNeutralElement}(K_0,f)$$ by (rule group0_1_L4 )
then have $$\forall a\in K_0.\ \exists b\in K_0.\ f\langle a,b\rangle = \text{ TheNeutralElement}(K_0,f)$$ using Field_ZF_1_L3
with II show $$\text{IsAgroup}(K_0,f)$$ by (rule definition_of_group )
then show $$group0(K_0,f)$$ using group0_def
qed

The inverse of a nonzero field element is nonzero.

lemma (in field0) Field_ZF_1_L5:

assumes A1: $$a\in K$$, $$a\neq 0$$

shows $$a^{-1} \in K_0$$, $$(a^{-1})^2 \in K_0$$, $$a^{-1} \in K$$, $$a^{-1} \neq 0$$proof
from A1 have $$a \in K_0$$
then show $$a^{-1} \in K_0$$ using Field_ZF_1_L4, inverse_in_group
then show $$(a^{-1})^2 \in K_0$$, $$a^{-1} \in K$$, $$a^{-1} \neq 0$$ using Field_ZF_1_L2, IsOpClosed_def
qed

The inverse is really the inverse.

lemma (in field0) Field_ZF_1_L6:

assumes A1: $$a\in K$$, $$a\neq 0$$

shows $$a\cdot a^{-1} = 1$$, $$a^{-1}\cdot a = 1$$proof
let $$f = \text{restrict}(M,K_0\times K_0)$$
from A1 have $$group0(K_0,f)$$, $$a \in K_0$$ using Field_ZF_1_L4
then have $$f\langle a, \text{GroupInv}(K_0, f)(a)\rangle = \text{ TheNeutralElement}(K_0,f) \wedge$$ $$f\langle \text{GroupInv}(K_0,f)(a),a\rangle = \text{ TheNeutralElement}(K_0, f)$$ by (rule group0_2_L6 )
with A1 show $$a\cdot a^{-1} = 1$$, $$a^{-1}\cdot a = 1$$ using Field_ZF_1_L5, Field_ZF_1_L4
qed

A lemma with two field elements and cancelling.

lemma (in field0) Field_ZF_1_L7:

assumes $$a\in K$$, $$b\in K$$, $$b\neq 0$$

shows $$a\cdot b\cdot b^{-1} = a$$, $$a\cdot b^{-1}\cdot b = a$$ using assms, Field_ZF_1_L5, Ring_ZF_1_L11, Field_ZF_1_L6, Ring_ZF_1_L3

### Equations and identities

This section deals with more specialized identities that are true in fields.

$$a/(a^2) = 1/a$$ .

lemma (in field0) Field_ZF_2_L1:

assumes A1: $$a\in K$$, $$a\neq 0$$

shows $$a\cdot (a^{-1})^2 = a^{-1}$$proof
have $$a\cdot (a^{-1})^2 = a\cdot (a^{-1}\cdot a^{-1})$$
also
from A1 have $$\ldots = (a\cdot a^{-1})\cdot a^{-1}$$ using Field_ZF_1_L5, Ring_ZF_1_L11
also
from A1 have $$\ldots = a^{-1}$$ using Field_ZF_1_L6, Field_ZF_1_L5, Ring_ZF_1_L3
finally show $$a\cdot (a^{-1})^2 = a^{-1}$$
qed

If we multiply two different numbers by a nonzero number, the results will be different.

lemma (in field0) Field_ZF_2_L2:

assumes $$a\in K$$, $$b\in K$$, $$c\in K$$, $$a\neq b$$, $$c\neq 0$$

shows $$a\cdot c^{-1} \neq b\cdot c^{-1}$$ using assms, field_has_no_zero_divs, Field_ZF_1_L5, Ring_ZF_1_L12B

We can put a nonzero factor on the other side of non-identity (is this the best way to call it?) changing it to the inverse.

lemma (in field0) Field_ZF_2_L3:

assumes A1: $$a\in K$$, $$b\in K$$, $$b\neq 0$$, $$c\in K$$ and A2: $$a\cdot b \neq c$$

shows $$a \neq c\cdot b^{-1}$$proof
from A1, A2 have $$a\cdot b\cdot b^{-1} \neq c\cdot b^{-1}$$ using Ring_ZF_1_L4, Field_ZF_2_L2
with A1 show $$a \neq c\cdot b^{-1}$$ using Field_ZF_1_L7
qed

If if the inverse of $$b$$ is different than $$a$$, then the inverse of $$a$$ is different than $$b$$.

lemma (in field0) Field_ZF_2_L4:

assumes $$a\in K$$, $$a\neq 0$$ and $$b^{-1} \neq a$$

shows $$a^{-1} \neq b$$ using assms, Field_ZF_1_L4, group0_2_L11B

An identity with two field elements, one and an inverse.

lemma (in field0) Field_ZF_2_L5:

assumes $$a\in K$$, $$b\in K$$, $$b\neq 0$$

shows $$(1 + a\cdot b)\cdot b^{-1} = a + b^{-1}$$ using assms, Ring_ZF_1_L4, Field_ZF_1_L5, Ring_ZF_1_L2, ring_oper_distr, Field_ZF_1_L7, Ring_ZF_1_L3

An identity with three field elements, inverse and cancelling.

lemma (in field0) Field_ZF_2_L6:

assumes A1: $$a\in K$$, $$b\in K$$, $$b\neq 0$$, $$c\in K$$

shows $$a\cdot b\cdot (c\cdot b^{-1}) = a\cdot c$$proof
from A1 have T: $$a\cdot b \in K$$, $$b^{-1} \in K$$ using Ring_ZF_1_L4, Field_ZF_1_L5
with mult_commute, A1 have $$a\cdot b\cdot (c\cdot b^{-1}) = a\cdot b\cdot (b^{-1}\cdot c)$$ using IsCommutative_def
moreover
from A1, T have $$a\cdot b \in K$$, $$b^{-1} \in K$$, $$c\in K$$
then have $$a\cdot b\cdot b^{-1}\cdot c = a\cdot b\cdot (b^{-1}\cdot c)$$ by (rule Ring_ZF_1_L11 )
ultimately have $$a\cdot b\cdot (c\cdot b^{-1}) = a\cdot b\cdot b^{-1}\cdot c$$
with A1 show $$a\cdot b\cdot (c\cdot b^{-1}) = a\cdot c$$ using Field_ZF_1_L7
qed

### 1/0=0

In ZF if $$f: X\rightarrow Y$$ and $$x\notin X$$ we have $$f(x)=\emptyset$$. Since $$\emptyset$$ (the empty set) in ZF is the same as zero of natural numbers we can claim that $$1/0=0$$ in certain sense. In this section we prove a theorem that makes makes it explicit.

The next locale extends the field0 locale to introduce notation for division operation.

Locale fieldd = field0 +

defines $$division \equiv \{\langle p,\text{fst}(p)\cdot \text{snd}(p)^{-1}\rangle .\ p\in K\times K_0\}$$

defines $$x / y \equiv division\langle x,y\rangle$$

Division is a function on $$K\times K_0$$ with values in $$K$$.

lemma (in fieldd) div_fun:

shows $$division: K\times K_0 \rightarrow K$$proof
have $$\forall p \in K\times K_0.\ \text{fst}(p)\cdot \text{snd}(p)^{-1} \in K$$proof
fix $$p$$
assume $$p \in K\times K_0$$
hence $$\text{fst}(p) \in K$$ and $$\text{snd}(p) \in K_0$$
then show $$\text{fst}(p)\cdot \text{snd}(p)^{-1} \in K$$ using Ring_ZF_1_L4, Field_ZF_1_L5
qed
then have $$\{\langle p,\text{fst}(p)\cdot \text{snd}(p)^{-1}\rangle .\ p\in K\times K_0\}: K\times K_0 \rightarrow K$$ by (rule ZF_fun_from_total )
thus $$thesis$$
qed

So, really $$1/0=0$$. The essential lemma is apply_0 from standard Isabelle's func.thy.

theorem (in fieldd) one_over_zero:

shows $$1 / 0 = 0$$proof
have $$domain(division) = K\times K_0$$ using div_fun, func1_1_L1
hence $$\langle 1 , 0 \rangle \notin domain(division)$$
then show $$thesis$$ using apply_0
qed
end
Definition of IsAfield: $$\text{IsAfield}(K,A,M) \equiv$$ $$( \text{IsAring}(K,A,M) \wedge (M \text{ is commutative on } K) \wedge$$ $$\text{ TheNeutralElement}(K,A) \neq \text{ TheNeutralElement}(K,M) \wedge$$ $$(\forall a\in K.\ a\neq \text{ TheNeutralElement}(K,A)\longrightarrow$$ $$(\exists b\in K.\ M\langle a,b\rangle = \text{ TheNeutralElement}(K,M))))$$
Definition of IsCommutative: $$f \text{ is commutative on } G \equiv \forall x\in G.\ \forall y\in G.\ f\langle x,y\rangle = f\langle y,x\rangle$$
lemma (in ring0) Ring_ZF_1_L11:

assumes $$a\in R$$, $$b\in R$$, $$c\in R$$

shows $$a + b + c = a + (b + c)$$, $$a\cdot b\cdot c = a\cdot (b\cdot c)$$
lemma (in ring0) Ring_ZF_1_L6:

assumes $$x\in R$$

shows $$0 \cdot x = 0$$, $$x\cdot 0 = 0$$
lemma (in ring0) Ring_ZF_1_L3:

assumes $$a\in R$$

shows $$( - a) \in R$$, $$( - ( - a)) = a$$, $$a + 0 = a$$, $$0 + a = a$$, $$a\cdot 1 = a$$, $$1 \cdot a = a$$, $$a - a = 0$$, $$a - 0 = a$$, $$2 \cdot a = a + a$$, $$( - a) + a = 0$$
Definition of HasNoZeroDivs: $$\text{HasNoZeroDivs}(R,A,M) \equiv (\forall a\in R.\ \forall b\in R.\$$ $$M\langle a,b\rangle = \text{ TheNeutralElement}(R,A) \longrightarrow$$ $$a = \text{ TheNeutralElement}(R,A) \vee b = \text{ TheNeutralElement}(R,A))$$
lemma (in ring0) Ring_ZF_1_L4:

assumes $$a\in R$$, $$b\in R$$

shows $$a + b \in R$$, $$a - b \in R$$, $$a\cdot b \in R$$, $$a + b = b + a$$
lemma (in field0) field_has_no_zero_divs: shows $$\text{HasNoZeroDivs}(K,A,M)$$
lemma (in ring0) Ring_ZF_1_L12:

assumes $$\text{HasNoZeroDivs}(R,A,M)$$ and $$a\in R$$, $$a\neq 0$$, $$b\in R$$, $$b\neq 0$$

shows $$a\cdot b\neq 0$$
Definition of IsOpClosed: $$A \text{ is closed under } f \equiv \forall x\in A.\ \forall y\in A.\ f\langle x,y\rangle \in A$$
lemma (in field0) Field_ZF_1_L1: shows $$\text{IsAfield}(K,A,M)$$
Definition of IsAring: $$\text{IsAring}(R,A,M) \equiv \text{IsAgroup}(R,A) \wedge (A \text{ is commutative on } R) \wedge$$ $$\text{IsAmonoid}(R,M) \wedge \text{IsDistributive}(R,A,M)$$
Definition of IsAgroup: $$\text{IsAgroup}(G,f) \equiv$$ $$( \text{IsAmonoid}(G,f) \wedge (\forall g\in G.\ \exists b\in G.\ f\langle g,b\rangle = \text{ TheNeutralElement}(G,f)))$$
Definition of IsAmonoid: $$\text{IsAmonoid}(G,f) \equiv$$ $$f \text{ is associative on } G \wedge$$ $$(\exists e\in G.\ (\forall g\in G.\ ( (f(\langle e,g\rangle ) = g) \wedge (f(\langle g,e\rangle ) = g))))$$
lemma (in field0) Field_ZF_1_L2: shows $$K_0 \text{ is closed under } M$$
lemma func_ZF_4_L3:

assumes $$f \text{ is associative on } X$$ and $$A\subseteq X$$ and $$A \text{ is closed under } f$$

shows $$\text{restrict}(f,A\times A) \text{ is associative on } A$$
lemma (in ring0) Ring_ZF_1_L2: shows $$0 \in R$$, $$1 \in R$$, $$( - 0 ) = 0$$
lemma (in monoid0) group0_1_L4:

assumes $$e \in G \wedge (\forall g\in G.\ e \oplus g = g \wedge g \oplus e = g)$$

shows $$e = \text{ TheNeutralElement}(G,f)$$
lemma (in field0) Field_ZF_1_L3:

assumes $$a\in K_0$$

shows $$\exists b\in K_0.\ a\cdot b = 1$$
lemma definition_of_group:

assumes $$\text{IsAmonoid}(G,f)$$ and $$\forall g\in G.\ \exists b\in G.\ f\langle g,b\rangle = \text{ TheNeutralElement}(G,f)$$

shows $$\text{IsAgroup}(G,f)$$
theorem (in field0) Field_ZF_1_L4: shows $$\text{IsAgroup}(K_0,\text{restrict}(M,K_0\times K_0))$$, $$group0(K_0,\text{restrict}(M,K_0\times K_0))$$, $$1 = \text{ TheNeutralElement}(K_0,\text{restrict}(M,K_0\times K_0))$$
lemma (in group0) inverse_in_group:

assumes $$x\in G$$

shows $$x^{-1}\in G$$
lemma (in group0) group0_2_L6:

assumes $$x\in G$$

shows $$x\cdot x^{-1} = 1 \wedge x^{-1}\cdot x = 1$$
lemma (in field0) Field_ZF_1_L5:

assumes $$a\in K$$, $$a\neq 0$$

shows $$a^{-1} \in K_0$$, $$(a^{-1})^2 \in K_0$$, $$a^{-1} \in K$$, $$a^{-1} \neq 0$$
lemma (in field0) Field_ZF_1_L6:

assumes $$a\in K$$, $$a\neq 0$$

shows $$a\cdot a^{-1} = 1$$, $$a^{-1}\cdot a = 1$$
lemma (in ring0) Ring_ZF_1_L12B:

assumes $$\text{HasNoZeroDivs}(R,A,M)$$, $$a\in R$$, $$b\in R$$, $$c\in R$$, $$a\neq b$$, $$c\neq 0$$

shows $$a\cdot c \neq b\cdot c$$
lemma (in field0) Field_ZF_2_L2:

assumes $$a\in K$$, $$b\in K$$, $$c\in K$$, $$a\neq b$$, $$c\neq 0$$

shows $$a\cdot c^{-1} \neq b\cdot c^{-1}$$
lemma (in field0) Field_ZF_1_L7:

assumes $$a\in K$$, $$b\in K$$, $$b\neq 0$$

shows $$a\cdot b\cdot b^{-1} = a$$, $$a\cdot b^{-1}\cdot b = a$$
lemma (in group0) group0_2_L11B:

assumes $$a\in G$$ and $$b^{-1} \neq a$$

shows $$a^{-1} \neq b$$
lemma (in ring0) ring_oper_distr:

assumes $$a\in R$$, $$b\in R$$, $$c\in R$$

shows $$a\cdot (b + c) = a\cdot b + a\cdot c$$, $$(b + c)\cdot a = b\cdot a + c\cdot a$$
lemma ZF_fun_from_total:

assumes $$\forall x\in X.\ b(x) \in Y$$

shows $$\{\langle x,b(x)\rangle .\ x\in X\} : X\rightarrow Y$$
lemma (in fieldd) div_fun: shows $$division: K\times K_0 \rightarrow K$$
lemma func1_1_L1:

assumes $$f:A\rightarrow C$$

shows $$domain(f) = A$$