FORMALIZED MATHEMATICS Vol.2, No.2, March–April 1991 Université Catholique de Louvain

Metrics in Cartesian Product ^{1}

Stanisława Kanas Technical University of Rzeszów

Jan Stankiewicz Technical University of Rzeszów

Summary. A continuation of the paper [8]. It deals with the method of creation of the distance in the Cartesian product of metric spaces. The distance of two points belonging to the Cartesian product of metric spaces has been defined as the sum of distances of appriopriate coordinates (or projections) of these points. It is shown that the product of metric spaces with such a distance is a metric space.

MML Identifier: METRIC 3.

The articles [7], [12], [4], [5], [2], [6], [1], [9], [3], [8], [11], and [10] provide the notation and terminology for this paper. We follow the rules: X, Y will denote metric spaces, x_{1}, y_{1}, z_{1} will denote elements of the carrier of X, and x_{2}, y_{2}, z_{2} will denote elements of the carrier of Y. The scheme LambdaMCART concerns a non-empty set A, a non-empty set B, a non-empty set C, and a 4-ary functor F yielding an element of C and states that:

there exists a function f from [: [: A, B:], [: A, B:] :] into C such that for all elements x_{1}, y_{1} of A and for all elements x_{2}, y_{2} of B and for all elements x, y of [: A, B:] such that x = ⟨⟨x_{1}, x_{2}⟩⟩ and y = ⟨⟨y_{1}, y_{2}⟩⟩ holds f(⟨⟨x, y⟩⟩) = F(x_{1}, y_{1}, x_{2}, y_{2}) for all values of the parameters.

Let us consider X, Y. The functor ρ^{X×Y} yielding a function from [: [: the carrier of X, the carrier of Y :], [: the carrier of X, the carrier of Y :] :] into is defined by: (Def.1) for all elements x_{1}, y_{1} of the carrier of X and for all elements x_{2}, y_{2}

of the carrier of Y and for all elements x, y of [: the carrier of X, the carrier of Y :] such that x = ⟨⟨x_{1}, x_{2}⟩⟩ and y = ⟨⟨y_{1}, y_{2}⟩⟩ holds ρ^{X×Y} (x,

y) = ρ(x_{1}, y_{1}) + ρ(x_{2}, y_{2}).

The following proposition is true (1) Let X be a metric space. Let Y be a metric space. Let F be a function

1Supported by RPBP.III-24.B3

from [: [: the carrier of X, the carrier of Y :], [: the carrier of X, the carrier of Y :] :] into . Then F = ρ^{X×Y} if and only if for all elements x_{1}, y_{1} of the carrier of X and for all elements x_{2}, y_{2} of the carrier of Y and for all elements x, y of [: the carrier of X, the carrier of Y :] such that x = ⟨⟨x_{1}, x_{2}⟩⟩ and y = ⟨⟨y_{1}, y_{2}⟩⟩ holds F (x, y) = ρ(x_{1}, y_{1}) + ρ(x_{2}, y_{2}).

One can prove the following proposition

(2) For all elements a, b of such that a + b = 0 and 0 ≤ a and 0 ≤ b holds a = 0 and b = 0.

We now state four propositions:

(3) For every metric space M and for all elements a, b of the carrier of M holds ρ(a, b) = 0 if and only if a = b.

(5)^{2} For all elements x, y of [: the carrier of X, the carrier of Y :] such that

x = ⟨⟨x_{1}, x_{2}⟩⟩ and y = ⟨⟨y_{1}, y_{2}⟩⟩ holds ρ^{X×Y} (x, y) = 0 if and only if x = y.

(6) For all elements x, y of [: the carrier of X, the carrier of Y :] such that x = ⟨⟨x_{1}, x_{2}⟩⟩ and y = ⟨⟨y_{1}, y_{2}⟩⟩ holds ρ^{X×Y} (x, y) = ρ^{X×Y} (y, x).

(7) For all elements x, y, z of [: the carrier of X, the carrier of Y :] such that x = ⟨⟨x_{1}, x_{2}⟩⟩ and y = ⟨⟨y_{1}, y_{2}⟩⟩ and z = ⟨⟨z_{1}, z_{2}⟩⟩ holds ρ^{X×Y} (x, z) ≤ ρ^{X×Y} (x, y) + ρ^{X×Y} (y, z).

Let us consider X, Y, and let x, y be elements of [: the carrier of X, the carrier of Y :]. The functor ρ(x, y) yielding a real number is defined as follows: (Def.2) ρ(x, y) = ρ^{X×Y} (x, y).

We now state the proposition

(8) For all elements x, y of [: the carrier of X, the carrier of Y :] holds ρ(x, y) = ρ^{X×Y} (x, y).

Let X, Y be metric spaces. The functor [: X, Y :] yields a metric space and is defined as follows: (Def.3) [: X, Y :] = ⟨[: the carrier of X, the carrier of Y :], ρ^{X×Y} ⟩.

One can prove the following proposition

(9) For every metric space X and for every metric space Y holds ⟨[: the carrier of X, the carrier of Y :], ρ^{X×Y} ⟩ is a metric space.

In the sequel Z will denote a metric space and x_{3}, y_{3}, z_{3} will denote elements of the carrier of Z. The scheme LambdaMCART1 deals with a non-empty set A, a non-empty set B, a non-empty set C, a non-empty set D, and a 6-ary functor F yielding an element of D and states that:

there exists a function f from [: [: A, B, C:], [: A, B, C:] :] into D such that for all elements x_{1}, y_{1} of A and for all elements x_{2}, y_{2} of B and for all elements x_{3}, y_{3} of C and for all elements x, y of [: A, B, C:] such that x = ⟨⟨x_{1}, x_{2}, x_{3}⟩⟩ and y = ⟨⟨y_{1}, y_{2}, y_{3}⟩⟩ holds f(⟨⟨x, y⟩⟩) = F(x_{1}, y_{1}, x_{2}, y_{2}, x_{3}, y_{3}) for all values of the parameters.

2The proposition (4) was either repeated or obvious.

Let us consider X, Y, Z. The functor ρ^{X×Y ×Z} yielding a function from [: [: the carrier of X, the carrier of Y, the carrier of Z:], [: the carrier of X, the carrier of Y, the carrier of Z:] :] into is defined by: (Def.4) Let x_{1}, y_{1} be elements of the carrier of X. Let x_{2}, y_{2} be elements of

the carrier of Y. Then for all elements x_{3}, y_{3} of the carrier of Z and for all elements x, y of [: the carrier of X, the carrier of Y, the carrier of Z:] such that x = ⟨⟨x_{1}, x_{2}, x_{3}⟩⟩ and y = ⟨⟨y_{1}, y_{2}, y_{3}⟩⟩ holds ρ^{X×Y ×Z}(x,

y) = ρ(x_{1}, y_{1}) + ρ(x_{2}, y_{2}) + ρ(x_{3}, y_{3}).

Next we state four propositions:

(10) Let X be a metric space. Let Y be a metric space. Let Z be a metric space. Let F be a function from [: [: the carrier of X, the carrier of Y, the carrier of Z:], [: the carrier of X, the carrier of Y, the carrier of Z:] :] into . Then F = ρ^{X×Y ×Z} if and only if for all elements x_{1}, y_{1} of the carrier of X and for all elements x_{2}, y_{2} of the carrier of Y and for all elements x_{3}, y_{3} of the carrier of Z and for all elements x, y of [: the carrier of X, the carrier of Y, the carrier of Z:] such that x = ⟨⟨x_{1}, x_{2}, x_{3}⟩⟩ and y = ⟨⟨y_{1}, y_{2}, y_{3}⟩⟩ holds F (x, y) = ρ(x_{1}, y_{1}) + ρ(x_{2}, y_{2}) + ρ(x_{3}, y_{3}).

(12)^{3} For all elements x, y of [: the carrier of X, the carrier of Y, the carrier of Z:] such that x = ⟨⟨x_{1}, x_{2}, x_{3}⟩⟩ and y = ⟨⟨y_{1}, y_{2}, y_{3}⟩⟩ holds ρ^{X×Y ×Z}(x,

y) = 0 if and only if x = y.

(13) For all elements x, y of [: the carrier of X, the carrier of Y, the carrier of Z:] such that x = ⟨⟨x_{1}, x_{2}, x_{3}⟩⟩ and y = ⟨⟨y_{1}, y_{2}, y_{3}⟩⟩ holds ρ^{X×Y ×Z}(x,

y) = ρ^{X×Y ×Z}(y, x).

(14) Let x, y, z be elements of [: the carrier of X, the carrier of Y, the carrier of Z:]. Then if x = ⟨⟨x_{1}, x_{2}, x_{3}⟩⟩ and y = ⟨⟨y_{1}, y_{2}, y_{3}⟩⟩ and z = ⟨⟨z_{1}, z_{2}, z_{3}⟩⟩, then ρ^{X×Y ×Z}(x, z) ≤ ρ^{X×Y ×Z}(x, y) + ρ^{X×Y ×Z}(y, z).

Let X, Y, Z be metric spaces. The functor [: X, Y, Z:] yields a metric space and is defined by: (Def.5) [: X, Y, Z:] = ⟨[: the carrier of X, the carrier of Y, the carrier of

Z:], ρ^{X×Y ×Z}⟩.

Let us consider X, Y, Z, and let x, y be elements of [: the carrier of X, the carrier of Y, the carrier of Z:]. The functor ρ(x, y) yielding a real number is defined by: (Def.6) ρ(x, y) = ρ^{X×Y ×Z}(x, y).

The following propositions are true:

(15) For all elements x, y of [: the carrier of X, the carrier of Y, the carrier of Z:] holds ρ(x, y) = ρ^{X×Y ×Z}(x, y).

(16) For every metric space X and for every metric space Y and for every metric space Z holds ⟨[: the carrier of X, the carrier of Y, the carrier of Z:], ρ^{X×Y ×Z}⟩ is a metric space.

3The proposition (11) was either repeated or obvious.

In the sequel W is a metric space and x_{4}, y_{4}, z_{4} are elements of the carrier of W. The scheme LambdaMCART2 deals with a non-empty set A, a non-empty set B, a non-empty set C, a non-empty set D, a non-empty set E, and a 8-ary functor F yielding an element of E and states that:

there exists a function f from [: [: A, B, C, D:], [: A, B, C, D:] :] into E such that for all elements x_{1}, y_{1} of A and for all elements x_{2}, y_{2} of B and for all elements x_{3}, y_{3} of C and for all elements x_{4}, y_{4} of D and for all elements x, y of [: A, B, C, D:] such that x = ⟨⟨x_{1}, x_{2}, x_{3}, x_{4}⟩⟩ and y = ⟨⟨y_{1}, y_{2}, y_{3}, y_{4}⟩⟩ holds f(⟨⟨x, y⟩⟩) = F(x_{1}, y_{1}, x_{2}, y_{2}, x_{3}, y_{3}, x_{4}, y_{4}) for all values of the parameters.

Let us consider X, Y, Z, W. The functor ρ^{X×Y ×Z×W} yielding a function from [: [: the carrier of X, the carrier of Y, the carrier of Z, the carrier of W :], [: the carrier of X, the carrier of Y, the carrier of Z, the carrier of W :] :] into is defined as follows:

(Def.7) Let x_{1}, y_{1} be elements of the carrier of X. Let x_{2}, y_{2} be elements of the carrier of Y. Let x_{3}, y_{3} be elements of the carrier of Z. Let x_{4}, y_{4} be elements of the carrier of W. Then for all elements x, y of [: the carrier of X, the carrier of Y, the carrier of Z, the carrier of W :] such that x = ⟨⟨x_{1}, x_{2}, x_{3}, x_{4}⟩⟩ and y = ⟨⟨y_{1}, y_{2}, y_{3}, y_{4}⟩⟩ holds ρ^{X×Y ×Z×W} (x,

y) = ρ(x_{1}, y_{1}) + ρ(x_{2}, y_{2}) + (ρ(x_{3}, y_{3}) + ρ(x_{4}, y_{4})).

The following propositions are true:

(17) Let X be a metric space. Let Y be a metric space. Let Z be a metric space. Let W be a metric space. Let F be a function from [: [: the carrier of X, the carrier of Y, the carrier of Z, the carrier of W :], [: the carrier of X, the carrier of Y, the carrier of Z, the carrier of W :] :] into . Then F = ρ^{X×Y ×Z×W} if and only if for all elements x_{1}, y_{1} of the carrier of X and for all elements x_{2}, y_{2} of the carrier of Y and for all elements x_{3}, y_{3} of the carrier of Z and for all elements x_{4}, y_{4} of the carrier of W and for all elements x, y of [: the carrier of X, the carrier of Y, the carrier of Z, the carrier of W :] such that x = ⟨⟨x_{1}, x_{2}, x_{3}, x_{4}⟩⟩ and y = ⟨⟨y_{1}, y_{2}, y_{3}, y_{4}⟩⟩ holds F (x, y) = ρ(x_{1}, y_{1}) + ρ(x_{2}, y_{2}) + (ρ(x_{3}, y_{3}) + ρ(x_{4}, y_{4})).

(19)^{4} For all elements x, y of [: the carrier of X, the carrier of Y, the carrier of Z, the carrier of W :] such that x = ⟨⟨x_{1}, x_{2}, x_{3}, x_{4}⟩⟩ and y = ⟨⟨y_{1}, y_{2}, y_{3}, y_{4}⟩⟩ holds ρ^{X×Y ×Z×W} (x, y) = 0 if and only if x = y.

(20) For all elements x, y of [: the carrier of X, the carrier of Y, the carrier of Z, the carrier of W :] such that x = ⟨⟨x_{1}, x_{2}, x_{3}, x_{4}⟩⟩ and y = ⟨⟨y_{1}, y_{2}, y_{3}, y_{4}⟩⟩ holds ρ^{X×Y ×Z×W} (x, y) = ρ^{X×Y ×Z×W} (y, x).

(21) Let x, y, z be elements of [: the carrier of X, the carrier of Y, the carrier of Z, the carrier of W :]. Then if x = ⟨⟨x_{1}, x_{2}, x_{3}, x_{4}⟩⟩ and y = ⟨⟨y_{1}, y_{2}, y_{3}, y_{4}⟩⟩ and z = ⟨⟨z_{1}, z_{2}, z_{3}, z_{4}⟩⟩, then ρ^{X×Y ×Z×W} (x, z) ≤ ρ^{X×Y ×Z×W} (x, y) + ρ^{X×Y ×Z×W} (y, z).

4The proposition (18) was either repeated or obvious.

Metrics in Cartesian Product 197

Let X, Y, Z, W be metric spaces. The functor [: X, Y, Z, W :] yielding a metric space is defined as follows: (Def.8) [: X, Y, Z, W :] = ⟨[: the carrier of X, the carrier of Y, the carrier of Z,

the carrier of W :], ρ^{X×Y ×Z×W} ⟩. Let us consider X, Y, Z, W, and let x, y be elements of [: the carrier of X,

the carrier of Y, the carrier of Z, the carrier of W :]. The functor ρ(x, y) yields a real number and is defined by: (Def.9) ρ(x, y) = ρ^{X×Y ×Z×W} (x, y).

One can prove the following propositions:

(22) For all elements x, y of [: the carrier of X, the carrier of Y, the carrier of Z, the carrier of W :] holds ρ(x, y) = ρ^{X×Y ×Z×W} (x, y).

(23) For every metric space X and for every metric space Y and for every metric space Z and for every metric space W holds ⟨[: the carrier of X, the carrier of Y, the carrier of Z, the carrier of W :], ρ^{X×Y ×Z×W} ⟩ is a metric space.

References

[1] Grzegorz Bancerek. Curried and uncurried functions. Formalized Mathematics, 1(3):537–541, 1990.

[2] Czesław Byliński. Basic functions and operations on functions. Formalized Mathematics, 1(1):245–254, 1990.

[3] Czesław Byliński. Binary operations. Formalized Mathematics, 1(1):175–180, 1990.

[4] Czesław Byliński. Functions and their basic properties. Formalized Mathematics, 1(1):55–65, 1990.

[5] Czesław Byliński. Functions from a set to a set. Formalized Mathematics, 1(1):153–164, 1990.

[6] Czesław Byliński. The modification of a function by a function and the iteration of the composition of a function. Formalized Mathematics, 1(3):521–527, 1990.

[7] Krzysztof Hryniewiecki. Basic properties of real numbers. Formalized Mathematics, 1(1):35–40, 1990.

[8] Stanisława Kanas, Adam Lecko, and Mariusz Startek. Metric spaces. Formalized Mathematics, 1(3):607–610, 1990.

[9] Andrzej Trybulec. Binary operations applied to functions. Formalized Mathematics, 1(2):329–334, 1990.

[10] Andrzej Trybulec. Domains and their Cartesian products. Formalized Mathematics, 1(1):115–122, 1990.

[11] Andrzej Trybulec. Tuples, projections and Cartesian products. Formalized Mathematics, 1(1):97–105, 1990.

[12] Zinaida Trybulec and Halina Świe‘czkowska. Boolean properties of sets. Formalized Mathematics, 1(1):17–23, 1990.

198

Submetric Spaces - Part I ^{1}

Adam Lecko

Technical University of Rzeszów

Mariusz Startek Technical University of Rzeszów

Summary. Definitions of pseudometric space, nonsymmetric metric space, semimetric space and ultrametric space are introduced. We find some relations between these spaces and prove that every ultrametric space is a metric space. We define the relation is between. Moreover we introduce the notions of the open segment and the closed segment.

MML Identifier: SUB METR.

The terminology and notation used here are introduced in the following articles: [8], [2], [3], [1], [6], [4], [7], [9], and [5]. One can prove the following propositions:

(1) For all elements x, y of such that 0 ≤ x and 0 ≤ y holds max(x, y) ≤ x + y.

(2) For every metric space M and for all elements x, y of the carrier of M such that x ≠ y holds 0 < ρ(x, y).

(3) For every element x of {∅} holds x = ∅.

(4) For all elements x, y of {∅} such that x = y holds {[∅, ∅]} ↦ 0(x, y) = 0.

(5) For all elements x, y of {∅} such that x ≠ y holds 0 < {[∅, ∅]} ↦ 0(x, y).

(6) For all elements x, y of {∅} holds {[∅, ∅]} ↦ 0(x, y) = {[∅, ∅]} ↦ 0(y, x).

(7) For all elements x, y, z of {∅} holds {[∅, ∅]} ↦ 0(x, z) ≤ {[∅, ∅]} ↦ 0(x, y) + {[∅, ∅]} ↦ 0(y, z).

(8) For all elements x, y, z of {∅} holds {[∅, ∅]} ↦ 0(x, z) ≤ max({[∅, ∅]} ↦ 0(x, y), {[∅, ∅]} ↦ 0(y, z)).

A metric structure is called a pseudo metric space if: (Def.1) for all elements a, b, c of the carrier of it holds if a = b, then ρ(a, b) = 0

but ρ(a, b) = ρ(b, a) and ρ(a, c) ≤ ρ(a, b) + ρ(b, c). Next we state four propositions:

1Supported by RPBP-III.24.B3

(10)^{2} For every pseudo metric space M and for all elements a, b of the carrier

of M such that a = b holds ρ(a, b) = 0.

(11) For every pseudo metric space M and for all elements a, b of the carrier of M holds ρ(a, b) = ρ(b, a).

(12) For every pseudo metric space M and for all elements a, b, c of the carrier of M holds ρ(a, c) ≤ ρ(a, b) + ρ(b, c).

(13) For every pseudo metric space M and for all elements a, b of the carrier

of M holds 0 ≤ ρ(a, b). A metric structure is said to be a semi metric space if:

(Def.2) for all elements a, b of the carrier of it holds if a = b, then ρ(a, b) = 0 but if a ≠ b, then 0 < ρ(a, b) and ρ(a, b) = ρ(b, a).

One can prove the following four propositions: (15)^{3} For every semi metric space M and for all elements a, b of the carrier

of M such that a = b holds ρ(a, b) = 0.

(16) For every semi metric space M and for all elements a, b of the carrier of M such that a ≠ b holds 0 < ρ(a, b).

(17) For every semi metric space M and for all elements a, b of the carrier of M holds ρ(a, b) = ρ(b, a).

(18) For every semi metric space M and for all elements a, b of the carrier

of M holds 0 ≤ ρ(a, b). A metric structure is called a non-symmetric metric space if:

(Def.3) for all elements a, b, c of the carrier of it holds if a = b, then ρ(a, b) = 0 but if a ≠ b, then 0 < ρ(a, b) and ρ(a, c) ≤ ρ(a, b) + ρ(b, c).

One can prove the following four propositions: (20)^{4} For every non-symmetric metric space M and for all elements a, b of

the carrier of M such that a = b holds ρ(a, b) = 0.

(21) For every non-symmetric metric space M and for all elements a, b of the carrier of M such that a ≠ b holds 0 < ρ(a, b).

(22) For every non-symmetric metric space M and for all elements a, b, c of the carrier of M holds ρ(a, c) ≤ ρ(a, b) + ρ(b, c).

(23) For every non-symmetric metric space M and for all elements a, b of

the carrier of M holds 0 ≤ ρ(a, b). A metric structure is said to be a ultra metric space if:

(Def.4) for all elements a, b, c of the carrier of it holds if a = b, then ρ(a, b) = 0 but if a ≠ b, then 0 < ρ(a, b) and ρ(a, b) = ρ(b, a) and ρ(a, c) ≤ max(ρ(a, b), ρ(b, c)).

We now state a number of propositions:

2The proposition (9) was either repeated or obvious.

3The proposition (14) was either repeated or obvious.

4The proposition (19) was either repeated or obvious.

(25)^{5} For every ultra metric space M and for all elements a, b of the carrier

of M such that a = b holds ρ(a, b) = 0.

(26) For every ultra metric space M and for all elements a, b of the carrier of M such that a ≠ b holds 0 < ρ(a, b).

(27) For every ultra metric space M and for all elements a, b of the carrier of M holds ρ(a, b) = ρ(b, a).

(28) For every ultra metric space M and for all elements a, b, c of the carrier of M holds ρ(a, c) ≤ max(ρ(a, b), ρ(b, c)).

(29) For every ultra metric space M and for all elements a, b of the carrier of M holds 0 ≤ ρ(a, b).

(30) For every metric space M holds M is a pseudo metric space.

(31) For every metric space M holds M is a semi metric space.

(32) For every metric space M holds M is a non-symmetric metric space.

(33) For every ultra metric space M holds M is a metric space.

(34) For every ultra metric space M holds M is a pseudo metric space.

(35) For every ultra metric space M holds M is a semi metric space.

(36) For every ultra metric space M holds M is a non-symmetric metric

space. In the sequel x, y will be arbitrary. Let us consider x, y. Then {x, y} is a

non-empty set.

The function (2^{2} → 0) from [: {∅, {∅}}, {∅, {∅}}:] into is defined by: (Def.5) (2^{2} → 0) = [: {∅, {∅}}, {∅, {∅}}:] ⟼ 0.

Next we state several propositions:

(37) (2^{2} → 0) = [: {∅, {∅}}, {∅, {∅}}:] ⟼ 0.

(38) For every element x of {∅, {∅}} holds x = ∅ or x = {∅}.

(39) (i) ⟨⟨∅, ∅⟩⟩ ∈ [: {∅, {∅}}, {∅, {∅}}:], (ii) ⟨⟨∅, {∅}⟩⟩ ∈ [: {∅, {∅}}, {∅, {∅}}:], (iii) ⟨⟨{∅}, ∅⟩⟩ ∈ [: {∅, {∅}}, {∅, {∅}}:], (iv) ⟨⟨{∅}, {∅}⟩⟩ ∈ [: {∅, {∅}}, {∅, {∅}}:].

(40) For all elements x, y of {∅, {∅}} holds (2^{2} → 0)(x, y) = 0.

(41) For all elements x, y of {∅, {∅}} such that x = y holds (2^{2} → 0)(x, y) = 0.

(42) For all elements x, y of {∅, {∅}} holds (2^{2} → 0)(x, y) = (2^{2} → 0)(y, x).

(43) For all elements x, y, z of {∅, {∅}} holds (2^{2} → 0)(x, z) ≤ (2^{2} → 0)(x,

y) + (2^{2} → 0)(y, z). The pseudo metric space is defined as follows:

(Def.6) = ⟨{∅, {∅}}, (2^{2} → 0)⟩.

The following proposition is true

(44) = ⟨{∅, {∅}}, (2^{2} → 0)⟩.

5The proposition (24) was either repeated or obvious.

Let S be a metric space, and let p, q, r be elements of the carrier of S. We say that q is between p and r if and only if: (Def.7) p ≠ q and p ≠ r and q ≠ r and ρ(p, r) = ρ(p, q) + ρ(q, r).

Next we state three propositions: (47)^{6} For every metric space S and for all elements p, q, r of the carrier of S

such that q is between p and r holds q is between r and p.

(48) For every metric space S and for all elements p, q, r of the carrier of S such that q is between p and r holds p is not between q and r and r is not between p and q.

(49) For every metric space S and for all elements p, q, r, s of the carrier of S such that q is between p and r and r is between p and s holds q is between p and s and r is between q and s.

Let M be a metric space, and let p, r be elements of the carrier of M. The functor IntSeg(p, r) yielding a subset of the carrier of M is defined as follows: (Def.8) IntSeg(p, r) = {q : q is between p and r }, where q ranges over elements

of the carrier of M.

One can prove the following two propositions:

(50) For every metric space M and for all elements p, r of the carrier of M holds IntSeg(p, r) = {q : q is between p and r }, where q ranges over elements of the carrier of M.

(51) For every metric space M and for all elements p, r, x of the carrier of

M holds x ∈ IntSeg(p, r) if and only if x is between p and r. Let M be a metric space, and let p, r be elements of the carrier of M. The

functor ClSeg(p, r) yielding a subset of the carrier of M is defined by: (Def.9) ClSeg(p, r) = {q : q is between p and r } ∪ {p, r}, where q ranges over

elements of the carrier of M.

We now state three propositions:

(52) For every metric space M and for all elements p, r of the carrier of M holds ClSeg(p, r) = {q : q is between p and r } ∪ {p, r}, where q ranges over elements of the carrier of M.

(53) For every metric space M and for all elements p, r, x of the carrier of M holds x ∈ ClSeg(p, r) if and only if x is between p and r or x = p or x = r.

(54) For every metric space M and for all elements p, r of the carrier of M holds IntSeg(p, r) ⊆ ClSeg(p, r).

References

[1] Czesław Byliński. Binary operations. Formalized Mathematics, 1(1):175–180, 1990.

[2] Czesław Byliński. Functions and their basic properties. Formalized Mathematics, 1(1):55– 65, 1990.

6The propositions (45)–(46) were either repeated or obvious.

Submetric Spaces - Part I 203

[3] Czesław Byliński. Functions from a set to a set. Formalized Mathematics, 1(1):153–164, 1990.

[4] Krzysztof Hryniewiecki. Basic properties of real numbers. Formalized Mathematics, 1(1):35–40, 1990.

[5] Stanisława Kanas, Adam Lecko, and Mariusz Startek. Metric spaces. Formalized Mathematics, 1(3):607–610, 1990.

[6] Andrzej Trybulec. Binary operations applied to functions. Formalized Mathematics, 1(2):329–334, 1990.

[7] Andrzej Trybulec. Domains and their Cartesian products. Formalized Mathematics, 1(1):115–122, 1990.

[8] Andrzej Trybulec. Tarski Grothendieck set theory. Formalized Mathematics, 1(1):9–11, 1990.

[9] Andrzej Trybulec and Czesław Byliński. Some properties of real numbers. Formalized Mathematics, 1(3):445–449, 1990.

204

On Pseudometric Spaces ^{1}

Adam Lecko

Technical University of Rzeszów

Mariusz Startek Technical University of Rzeszów

Summary. We introduce the equivalence classes in a pseudometric space. Next we prove that the set of the equivalence classes forms the metric space with the special metric defined in the article.

MML Identifier: METRIC 2.

The terminology and notation used here have been introduced in the following articles: [9], [4], [13], [12], [10], [8], [2], [3], [1], [14], [7], [11], [5], and [6]. Let M be a metric structure, and let x, y be elements of the carrier of M. The predicate x ≈ y is defined by: (Def.1) ρ(x, y) = 0.

Let M be a metric structure, and let x be an element of the carrier of M. The functor x^{}yielding a subset of the carrier of M is defined as follows: (Def.2) x^{}= {y : x ≈ y}, where y ranges over elements of the carrier of M.

One can prove the following proposition

(2)^{2} For every M being a metric structure and for every element x of the carrier of M holds x^{}= {y : x ≈ y}, where y ranges over elements of the carrier of M.

Let M be a metric structure. A subset of the carrier of M is called a - equivalence class of M if: (Def.3) there exists an element x of the carrier of M such that it = x^{}.

Next we state a number of propositions:

(4)^{3} For every pseudo metric space M and for every element x of the carrier

of M holds x ≈ x.

(5) For every pseudo metric space M and for all elements x, y of the carrier of M such that x ≈ y holds y ≈ x.

1Supported by RPBP-III.24.B3

2The proposition (1) was either repeated or obvious.

3The proposition (3) was either repeated or obvious.

(6) For every pseudo metric space M and for all elements x, y, z of the carrier of M such that x ≈ y and y ≈ z holds x ≈ z.

(7) For every pseudo metric space M and for all elements x, y of the carrier of M holds y ∈ x^{}if and only if y ≈ x.

(8) For every pseudo metric space M and for all elements x, p, q of the carrier of M such that p ∈ x^{}and q ∈ x^{}holds p ≈ q.

(9) For every pseudo metric space M and for every element x of the carrier of M holds x ∈ x^{}.

(10) For every pseudo metric space M and for all elements x, y of the carrier of M holds x ∈ y^{}if and only if y ∈ x^{}.

(11) For every pseudo metric space M and for all elements p, x, y of the carrier of M such that p ∈ x^{}and x ≈ y holds p ∈ y^{}.

(12) For every pseudo metric space M and for all elements x, y of the carrier of M such that y ∈ x^{}holds x^{}= y^{}.

(13) For every pseudo metric space M and for all elements x, y of the carrier

of M holds x^{}= y^{}if and only if x ≈ y. The following propositions are true:

(14) For every pseudo metric space M and for all elements x, y of the carrier of M holds x^{}∩ y^{}≠ ∅ if and only if x ≈ y.

(15) For every pseudo metric space M and for every element x of the carrier of M holds x^{}is a non-empty set.

(16) For every pseudo metric space M and for every -equivalence class V of M holds V is a non-empty set.

(17) For every pseudo metric space M and for all elements x, p, q of the carrier of M such that p ∈ x^{}and q ∈ x^{}holds ρ(p, q) = 0.

(18) For every metric space M and for all elements x, y of the carrier of M holds x ≈ y if and only if x = y.

(19) For every metric space M and for all elements x, y of the carrier of M

holds y ∈ x^{}if and only if y = x. One can prove the following two propositions:

(20) For every metric space M and for every element x of the carrier of M holds x^{}= {x}.

(21) For every metric space M and for every subset V of the carrier of M holds V is a -equivalence class of M if and only if there exists an element x of the carrier of M such that V = {x}.

Let M be a metric structure. The functor M^{}yields a non-empty set and is defined by:

(Def.4) M^{}= {s : ⋁_{x} x^{}= s}, where s ranges over elements of 2^{the carrier of M}, and x ranges over elements of the carrier of M.

One can prove the following proposition (22) For every M being a metric structure holds M^{}= {s : ⋁_{x} x^{}= s},

where s ranges over elements of 2^{the carrier of M}, and x ranges over elements of the carrier of M.

In the sequel V is arbitrary. The following two propositions are true:

(23) For every M being a metric structure holds V ∈ M^{}if and only if there exists an element x of the carrier of M such that V = x^{}.

(24) For every M being a metric structure and for every element x of the carrier of M holds x^{}∈ M^{}.

We now state the proposition (26)^{4} For every M being a metric structure holds V ∈ M^{}if and only if V is

a -equivalence class of M.

We now state three propositions:

(27) For every metric space M and for every element x of the carrier of M holds {x} ∈ M^{}.

(28) For every metric space M holds V ∈ M^{}if and only if there exists an element x of the carrier of M such that V = {x}.

(29) For every pseudo metric space M and for all elements V, Q of M^{}and for all elements p_{1}, p_{2}, q_{1}, q_{2} of the carrier of M such that p_{1} ∈ V and q_{1} ∈ Q and p_{2} ∈ V and q_{2} ∈ Q holds ρ(p_{1}, q_{1}) = ρ(p_{2}, q_{2}).

Let M be a pseudo metric space, and let V, Q be elements of M^{}, and let v be an element of . We say that the distance between V and Q is v if and only if:

(Def.5) for all elements p, q of the carrier of M such that p ∈ V and q ∈ Q holds ρ(p, q) = v.

We now state two propositions: (31)^{5} For every pseudo metric space M and for all elements V, Q of M^{}and

for every element v of holds the distance between V and Q is v if and only if there exist elements p, q of the carrier of M such that p ∈ V and q ∈ Q and ρ(p, q) = v.

(32) For every pseudo metric space M and for all elements V, Q of M^{}and for every element v of holds the distance between V and Q is v if and only if the distance between Q and V is v.

Let M be a pseudo metric space, and let V, Q be elements of M^{}. The functor ρ^{∘}(V, Q) yields a subset of and is defined as follows:

(Def.6) ρ^{∘}(V, Q) = {v : the distance between V and Q is v }, where v ranges over elements of .

The following two propositions are true:

4The proposition (25) was either repeated or obvious.

5The proposition (30) was either repeated or obvious.

(33) For every pseudo metric space M and for all elements V, Q of M^{}holds ρ^{∘}(V, Q) = {v : the distance between V and Q is v }, where v ranges over elements of .

(34) For every pseudo metric space M and for all elements V, Q of M^{}and for every element v of holds v ∈ ρ^{∘}(V, Q) if and only if the distance between V and Q is v.

Let M be a pseudo metric space, and let v be an element of . The functor ρM^{}^{−1} (v) yields a subset of [: M^{}, M^{}:] and is defined as follows:

(Def.7) ρM^{}^{−1} (v) = {W : ⋁_{V,Q}[W = ⟨⟨V, Q⟩⟩∧ the distance between V and Q is v ]}, where W ranges over elements of [: M^{}, M^{}:], and V, Q range over elements of M^{}.

One can prove the following two propositions:

(35) For every pseudo metric space M and for every element v of holds ρM^{}^{−1} (v) = {W : ⋁_{V,Q}[W = ⟨⟨V, Q⟩⟩∧ the distance between V and Q is v ]}, where W ranges over elements of [: M^{}, M^{}:], and V, Q range over elements of M^{}.

(36) For every pseudo metric space M and for every element v of and for every element W of [: M^{}, M^{}:] holds W ∈ ρM^{}^{−1} (v) if and only if there exist elements V, Q of M^{}such that W = ⟨⟨V, Q⟩⟩ and the distance between V and Q is v.

Let M be a pseudo metric space. The functor ρ^{∘}(M^{}, M^{}) yields a subset of and is defined by:

(Def.8) ρ^{∘}(M^{}, M^{}) = {v : ⋁_{V,Q} the distance between V and Q is v }, where v ranges over elements of , and V, Q range over elements of M^{}.

The following two propositions are true:

(37) For every pseudo metric space M holds ρ^{∘}(M^{}, M^{}) = {v : ⋁_{V,Q} the distance between V and Q is v }, where v ranges over elements of , and V, Q range over elements of M^{}.

(38) For every pseudo metric space M and for every element v of holds v ∈ ρ^{∘}(M^{}, M^{}) if and only if there exist elements V, Q of M^{}such that the distance between V and Q is v.

Let M be a pseudo metric space. The functor dom_{1} ρM^{}yields a subset of M^{}and is defined as follows:

(Def.9) dom_{1} ρM^{}= {V : ⋁_{Q} ⋁_{v} the distance between V and Q is v }, where V ranges over elements of M^{}, and Q ranges over elements of M^{}, and v ranges over elements of .

We now state two propositions:

(39) For every pseudo metric space M holds dom_{1} ρM^{}= {V : ⋁_{Q} ⋁_{v} the distance between V and Q is v }, where V ranges over elements of M^{}, and Q ranges over elements of M^{}, and v ranges over elements of .

(40) For every pseudo metric space M and for every element V of M^{}holds V ∈ dom_{1} ρM^{}if and only if there exists an element Q of M^{}and there exists an element v of such that the distance between V and Q is v.

Let M be a pseudo metric space. The functor dom_{2} ρM^{}yields a subset of M^{}and is defined by:

(Def.10) dom_{2} ρM^{}= {Q : ⋁_{V} ⋁_{v} the distance between V and Q is v }, where Q ranges over elements of M^{}, and V ranges over elements of M^{}, and v ranges over elements of .

One can prove the following two propositions:

(41) For every pseudo metric space M holds dom_{2} ρM^{}= {Q : ⋁_{V} ⋁_{v} the distance between V and Q is v }, where Q ranges over elements of M^{}, and V ranges over elements of M^{}, and v ranges over elements of .

(42) For every pseudo metric space M and for every element Q of M^{}holds Q ∈ dom_{2} ρM^{}if and only if there exists an element V of M^{}and there exists an element v of such that the distance between V and Q is v.

Let M be a pseudo metric space. The functor dom ρM^{}yielding a subset of [: M^{}, M^{}:] is defined as follows:

(Def.11) dom ρM^{}= {V_{1} : ⋁_{V,Q} ⋁_{v}[V_{1} = ⟨⟨V, Q⟩⟩∧ the distance between V and Q is v ]}, where V_{1} ranges over elements of [: M^{}, M^{}:], and V, Q range over elements of M^{}, and v ranges over elements of .

We now state two propositions:

(43) For every pseudo metric space M holds dom ρM^{}= {V_{1} : ⋁_{V,Q} ⋁_{v}[V_{1} = ⟨⟨V, Q⟩⟩∧ the distance between V and Q is v ]}, where V_{1} ranges over elements of [: M^{}, M^{}:], and V, Q range over elements of M^{}, and v ranges over elements of .

(44) For every pseudo metric space M and for every element V_{1} of [: M^{}, M^{}:] holds V_{1} ∈ dom ρM^{}if and only if there exist elements V, Q of M^{} and there exists an element v of such that V_{1} = ⟨⟨V, Q⟩⟩ and the distance between V and Q is v.

Let M be a pseudo metric space. The functor graph ρM^{}yielding a subset of [: M^{}, M^{}, :] is defined by:

(Def.12) graph ρM^{}= {V_{2} : ⋁_{V,Q} ⋁_{v}[V_{2} = ⟨⟨V, Q, v⟩⟩∧ the distance between V and Q is v ]}, where V_{2} ranges over elements of [: M^{}, M^{}, :], and V, Q range over elements of M^{}, and v ranges over elements of .

The following propositions are true:

(45) For every pseudo metric space M holds graph ρM^{}= {V_{2} : ⋁_{V,Q} ⋁_{v}[V_{2} = ⟨⟨V, Q, v⟩⟩∧ the distance between V and Q is v ]}, where V_{2} ranges over elements of [: M^{}, M^{}, :], and V, Q range over elements of M^{}, and v ranges over elements of .

(46) For every pseudo metric space M and for every element V_{2} of [: M^{}, M^{}, :] holds V_{2} ∈ graph ρM^{}if and only if there exist elements V, Q of M^{}and there exists an element v of such that V_{2} = ⟨⟨V, Q, v⟩⟩ and the distance between V and Q is v.

(47) For every pseudo metric space M holds dom_{1} ρM^{}= dom_{2} ρM^{}.

(48) For every pseudo metric space M holds graph ρM^{}⊆ [: dom_{1} ρM^{}, dom_{2} ρM^{}, ρ^{∘}(M^{}, M^{}) :].

(49) Let M be a pseudo metric space. Then for all elements V, Q of M^{} and for all elements p_{1}, q_{1}, p_{2}, q_{2} of the carrier of M and for all elements v_{1}, v_{2} of such that p_{1} ∈ V and q_{1} ∈ Q and ρ(p_{1}, q_{1}) = v_{1} and p_{2} ∈ V and q_{2} ∈ Q and ρ(p_{2}, q_{2}) = v_{2} holds v_{1} = v_{2}.

The following two propositions are true:

(50) For every pseudo metric space M and for all elements V, Q of M^{}and for all elements v_{1}, v_{2} of such that the distance between V and Q is v_{1} and the distance between V and Q is v_{2} holds v_{1} = v_{2}.

(52)^{6} For every pseudo metric space M and for every elements V, Q of M^{} there exists an element v of such that the distance between V and Q is v.

Let M be a pseudo metric space. The functor ρM^{}yielding a function from [: M^{}, M^{}:] into is defined as follows:

(Def.13) for all elements V, Q of M^{}and for all elements p, q of the carrier of M such that p ∈ V and q ∈ Q holds ρM^{}(V, Q) = ρ(p, q).

One can prove the following propositions:

(53) For every pseudo metric space M and for every function F from [: M^{}, M^{}:] into holds F = ρM^{}if and only if for all elements V, Q of M^{}and for all elements p, q of the carrier of M such that p ∈ V and q ∈ Q holds F (V, Q) = ρ(p, q).

(54) For every pseudo metric space M and for all elements V, Q of M^{}holds ρM^{}(V, Q) = 0 if and only if V = Q.

(55) For every pseudo metric space M and for all elements V, Q of M^{}holds

ρM^{}(V, Q) = ρM^{}(Q, V).

(56) For every pseudo metric space M and for all elements V, Q, W of M^{}

holds ρM^{}(V, W) ≤ ρM^{}(V, Q) + ρM^{}(Q, W).

Let M be a pseudo metric space. The functor M_{/} yields a metric space and is defined as follows:

(Def.14) M_{/} = ⟨M^{}, ρM^{}⟩.

We now state the proposition

(57) For every pseudo metric space M holds M_{/} = ⟨M^{}, ρM^{}⟩.

References

[1] Czesław Byliński. Binary operations. Formalized Mathematics, 1(1):175–180, 1990.

6The proposition (51) was either repeated or obvious.

On Pseudometric Spaces 211

[2] Czesław Byliński. Functions and their basic properties. Formalized Mathematics, 1(1):55–65, 1990.

[3] Czesław Byliński. Functions from a set to a set. Formalized Mathematics, 1(1):153–164, 1990.

[4] Krzysztof Hryniewiecki. Basic properties of real numbers. Formalized Mathematics, 1(1):35–40, 1990.

[5] Stanisława Kanas, Adam Lecko, and Mariusz Startek. Metric spaces. Formalized Mathematics, 1(3):607–610, 1990.

[6] Adam Lecko and Mariusz Startek. Submetric spaces - part I. Formalized Mathematics, 2(2):199–203, 1991.

[7] Andrzej Trybulec. Binary operations applied to functions. Formalized Mathematics, 1(2):329–334, 1990.

[8] Andrzej Trybulec. Domains and their Cartesian products. Formalized Mathematics, 1(1):115–122, 1990.

[9] Andrzej Trybulec. Tarski Grothendieck set theory. Formalized Mathematics, 1(1):9–11, 1990.

[10] Andrzej Trybulec. Tuples, projections and Cartesian products. Formalized Mathematics, 1(1):97–105, 1990.

[11] Andrzej Trybulec and Czesław Byliński. Some properties of real numbers. Formalized Mathematics, 1(3):445–449, 1990.

[12] Zinaida Trybulec. Properties of subsets. Formalized Mathematics, 1(1):67–71, 1990.

[13] Zinaida Trybulec and Halina Świe‘czkowska. Boolean properties of sets. Formalized Mathematics, 1(1):17–23, 1990.

[14] Edmund Woronowicz. Relations and their basic properties. Formalized Mathematics, 1(1):73–83, 1990.

212

Real Exponents and Logarithms ^{1}

Konrad Raczkowski Warsaw University Białystok Andrzej Ne‘dzusiak Warsaw University Białystok

Summary. Definitions and properties of the following concepts: root, real exponent and logarithm. Also the number e is defined.

MML Identifier: POWER.

The papers [11], [2], [9], [1], [7], [5], [6], [13], [12], [4], [3], [8], and [10] provide the notation and terminology for this paper. For simplicity we follow the rules: a, b, c, d denote real numbers, m, n, m_{1}, m_{2} denote natural numbers, k, l denote integers, and p denotes a rational number. One can prove the following propositions:

(1) If there exists m such that n = 2 · m, then (−a)n_{}= an_{}.

(2) If there exists m such that n = 2 · m + 1, then (−a)n_{}= −an_{}.

(3) If a ≥ 0 or there exists m such that n = 2 · m, then an_{}≥ 0. Let us consider n, a. The functor ^{n} \sqrt{a} yields a real number and is defined by:

(Def.1) (i) ^{n} \sqrt{a} = root_{n}(a) if a ≥ 0 and n ≥ 1,

(ii) ^{n} \sqrt{a} = − root_{n}(−a) if a < 0 and there exists m such that n = 2 · m + 1. One can prove the following propositions:

(4) For all a, n holds if a ≥ 0 and n ≥ 1, then ^{n} \sqrt{a} = root_{n}(a) but if a < 0 and there exists m such that n = 2 · m + 1, then ^{n} \sqrt{a} = − root_{n}(−a).

(5) If n ≥ 1 and a ≥ 0 or there exists m such that n = 2 · m + 1, then

n \sqrt{a}n_{}= a and ^{n} \sqrt{an_{}}= a.

(6) If n ≥ 1, then ^{n} \sqrt{0} = 0.

(7) If n ≥ 1, then ^{n} \sqrt{1} = 1.

(8) If a ≥ 0 and n ≥ 1, then ^{n} \sqrt{a} ≥ 0.

(9) If there exists m such that n = 2 · m + 1, then ^{n} \sqrt{−1} = −1.

(10) ^{1} \sqrt{a} = a.

1Supported by RPBP-III.24.C8

214 Konrad Raczkowski and Andrzej Ne‘dzusiak

(11) If there exists m such that n = 2 · m + 1, then ^{n} \sqrt{a} = − ^{n} \sqrt{−a}.

(12) If n ≥ 1 and a ≥ 0 and b ≥ 0 or there exists m such that n = 2 · m + 1, then ^{n} \sqrt{a · b} = ^{n} \sqrt{a} · ^{n} \sqrt{b}.

(13) If a > 0 and n ≥ 1 or a ≠ 0 and there exists m such that n = 2 · m + 1, then ^{n} \sqrt{\frac{1}{a}} = \frac{1}{\sqrt[n]{a}}.

(14) If a ≥ 0 and b > 0 and n ≥ 1 or b ≠ 0 and there exists m such that

n = 2 · m + 1, then ^{n} \sqrt{\frac{a}{b}} = \begin{matrix}^{n} & \sqrt{a} \\ ^{n} & \sqrt{b} \end{matrix}.

(15) If a ≥ 0 and n ≥ 1 and m ≥ 1 or there exist m_{1}, m_{2} such that n = 2 · m_{1} + 1 and m = 2 · m_{2} + 1, then ^{n} \sqrt{\sqrt[m]{a}} = ^{n·m} \sqrt{a}.

(16) If a ≥ 0 and n ≥ 1 and m ≥ 1 or there exist m_{1}, m_{2} such that

n = 2 · m_{1} + 1 and m = 2 · m_{2} + 1, then ^{n} \sqrt{a} · ^{m} \sqrt{a} = ^{n·m} \sqrt{an+m_{}}.

(17) If a ≤ b but 0 ≤ a and n ≥ 1 or there exists m such that n = 2 · m + 1, then ^{n} \sqrt{a} ≤ ^{n} \sqrt{b}.

(18) If a < b but a ≥ 0 and n ≥ 1 or there exists m such that n = 2 · m + 1, then ^{n} \sqrt{a} < ^{n} \sqrt{b}.

(19) If a ≥ 1 and n ≥ 1, then ^{n} \sqrt{a} ≥ 1 and a ≥ ^{n} \sqrt{a}.

(20) If a ≤ −1 and there exists m such that n = 2 · m + 1, then ^{n} \sqrt{a} ≤ −1 and a ≤ ^{n} \sqrt{a}.

(21) If a ≥ 0 and a < 1 and n ≥ 1, then a ≤ ^{n} \sqrt{a} and ^{n} \sqrt{a} < 1.

(22) If a > −1 and a ≤ 0 and there exists m such that n = 2 · m + 1, then a ≥ ^{n} \sqrt{a} and ^{n} \sqrt{a} > −1.

(23) If a > 0 and n ≥ 1, then ^{n} \sqrt{a} − 1 ≤ \frac{a−1}{n}.

(24) For every sequence of real numbers s and for every a such that a > 0 and for every n such that n ≥ 1 holds s(n) = ^{n} \sqrt{a} holds s is convergent and lim s = 1.

Let us consider a, b. The functor a^{b} yielding a real number is defined as follows:

(Def.2) (i) a^{b} = ab_{}if a > 0,

(ii) a^{b} = 0 if a = 0 and b > 0, (iii) there exists k such that k = b and a^{b} = ak_{}if a < 0 and b is an integer.

One can prove the following propositions:

(25) Given a, b. Then if a > 0, then a^{b} = ab_{}but if a = 0 and b > 0, then a^{b} = 0 but if a < 0 and b is an integer, then there exists k such that k = b

and a^{b} = ak_{}.

(26) If a > 0, then a^{b} = ab_{}.

(27) If b > 0, then 0^{b} = 0.

(28) If a < 0, then a^{k} = ak_{}.

(29) If a ≠ 0, then a^{0} = 1.

(30) a^{1} = a.

(31) 1^{a} = 1.

(32) If a > 0, then a^{b+c} = a^{b} · a^{c}.

(33) If a > 0, then a^{−c} = \frac{1}{a^{c}}.

(34) If a > 0, then a^{b−c} = \frac{a^{b}}{a^{c}}.

(35) If a > 0 and b > 0, then (a · b)^{c} = a^{c} · b^{c}.

(36) If a > 0 and b > 0, then \frac{a}{b}^{c} = \frac{a^{c}}{b^{c}}.

(37) If a > 0, then \frac{1}{a}^{b} = a^{−b}.

(38) If a > 0, then (a^{b})^{c} = a^{b·c}.

(39) If a > 0, then a^{b} > 0.

(40) If a > 1 and b > 0, then a^{b} > 1.

(41) If a > 1 and b < 0, then a^{b} < 1.

(42) If a > 0 and a < b and c > 0, then a^{c} < b^{c}.

(43) If a > 0 and a < b and c < 0, then a^{c} > b^{c}.

(44) If a < b and c > 1, then c^{a} < c^{b}.

(45) If a < b and c > 0 and c < 1, then c^{a} > c^{b}.

(46) If a ≠ 0, then a^{n} = an_{}.

(47) If n ≥ 1, then a^{n} = an_{}.

(48) If a ≠ 0, then a^{n} = a^{n}.

(49) If n ≥ 1, then a^{n} = a^{n}.

(50) If a ≠ 0, then a^{k} = ak_{}.

(51) If a > 0, then a^{p} = ap_{}.

(52) If a ≥ 0 and n ≥ 1, then a^{\frac{1}{n}} = ^{n} \sqrt{a}.

(53) a^{2} = a^{2}.

(54) If a ≠ 0 and there exists l such that k = 2 · l, then (−a)^{k} = a^{k}.

(55) If a ≠ 0 and there exists l such that k = 2 · l + 1, then (−a)^{k} = −a^{k}. Next we state two propositions:

(56) If −1 < a, then (1 + a)^{n} ≥ 1 + n · a.

(57) If a > 0 and a ≠ 1 and c ≠ d, then a^{c} ≠ a^{d}.

Let us consider a, b. Let us assume that a > 0 and a ≠ 1 and b > 0. The functor log_{a} b yields a real number and is defined by: (Def.3) a^{log_{a} b} = b.

The following propositions are true:

(58) For all a, b, c such that a > 0 and a ≠ 1 and b > 0 holds c = log_{a} b if and only if a^{c} = b.

(59) If a > 0 and a ≠ 1, then log_{a} 1 = 0.

(60) If a > 0 and a ≠ 1, then log_{a} a = 1.

(61) If a > 0 and a ≠ 1 and b > 0 and c > 0, then log_{a} b + log_{a} c = log_{a}(b · c).

(62) If a > 0 and a ≠ 1 and b > 0 and c > 0, then log_{a} b − log_{a} c = log_{a} \frac{b}{c}.

216 Konrad Raczkowski and Andrzej Ne‘dzusiak

(63) If a > 0 and a ≠ 1 and b > 0, then log_{a}(b^{c}) = c · log_{a} b.

(64) If a > 0 and a ≠ 1 and b > 0 and b ≠ 1 and c > 0, then log_{a} c = log_{a} b · log_{b} c.

(65) If a > 1 and b > 0 and c > b, then log_{a} c > log_{a} b.

(66) If a > 0 and a < 1 and b > 0 and c > b, then log_{a} c < log_{a} b.

(67) For every sequence of real numbers s such that for every n holds s(n) = (1 + \frac{1}{n+1})^{n+1} holds s is convergent.

The real number e is defined as follows: (Def.4) for every sequence of real numbers s such that for every n holds s(n) =

(1 + \frac{1}{n+1})^{n+1} holds e = lim s.

References

[1] Grzegorz Bancerek. The fundamental properties of natural numbers. Formalized Mathematics, 1(1):41–46, 1990.

[2] Krzysztof Hryniewiecki. Basic properties of real numbers. Formalized Mathematics, 1(1):35–40, 1990.

[3] Andrzej Kondracki. Basic properties of rational numbers. Formalized Mathematics, 1(5):841–845, 1990.

[4] Jarosław Kotowicz. Convergent real sequences. Upper and lower bound of sets of real numbers. Formalized Mathematics, 1(3):477–481, 1990.

[5] Jarosław Kotowicz. Convergent sequences and the limit of sequences. Formalized Mathematics, 1(2):273–275, 1990.

[6] Jarosław Kotowicz. Monotone real sequences. Subsequences. Formalized Mathematics, 1(3):471–475, 1990.

[7] Jarosław Kotowicz. Real sequences and basic operations on them. Formalized Mathematics, 1(2):269–272, 1990.

[8] Rafał Kwiatek. Factorial and Newton coeffitients. Formalized Mathematics, 1(5):887– 890, 1990.

[9] Jan Popiołek. Some properties of functions modul and signum. Formalized Mathematics, 1(2):263–264, 1990.

[10] Konrad Raczkowski. Integer and rational exponents. Formalized Mathematics, 2(1):125– 130, 1991.

[11] Andrzej Trybulec. Tarski Grothendieck set theory. Formalized Mathematics, 1(1):9–11, 1990.

[12] Andrzej Trybulec and Czesław Byliński. Some properties of real numbers. Formalized Mathematics, 1(3):445–449, 1990.

[13] Michał J. Trybulec. Integers. Formalized Mathematics, 1(3):501–505, 1990.

Hessenberg Theorem ^{1}

Eugeniusz Kusak Warsaw University Białystok Wojciech Leończuk Warsaw University Białystok

Summary. We prove the Hessenberg theorem which states that every Pappian projective space is Desarguesian.

MML Identifier: HESSENBE.

The terminology and notation used in this paper are introduced in the following articles: [7], [1], [2], [3], [4], [5], and [6]. We follow a convention: P_{1} denotes a projective space defined in terms of collinearity and a, a′, a_{1}, a_{2}, a_{3}, b, b′, b_{1}, b_{2}, c, c′, c_{1}, c_{3}, d, d′, e, o, p, p_{1}, p_{2}, p_{3}, q, q_{1}, q_{2}, q_{3}, r, s, x, y, z denote elements of the points of P_{1}. One can prove the following propositions:

(1) If a, b and c are collinear, then b, a and c are collinear.

(2) If a, b and c are collinear, then a, c and b are collinear.

(3) If a, b and c are collinear, then b, c and a are collinear and c, a and b are collinear and b, a and c are collinear and a, c and b are collinear and c, b and a are collinear.

(4) If a ≠ b and a, b and c are collinear and a, b and d are collinear, then a, c and d are collinear.

(5) If p ≠ q and a, b and p are collinear and a, b and q are collinear and p, q and r are collinear, then a, b and r are collinear.

(6) If p ≠ q, then there exists r such that p, q and r are not collinear.

(7) There exist q, r such that p, q and r are not collinear.

(8) If a, b and c are not collinear and a, b and b′ are collinear and a ≠ b′, then a, b′ and c are not collinear.

(9) If a, b and c are not collinear and a, b and d are collinear and a, c and d are collinear, then a = d.

1Supported by RPBP.III-24.C6

(10) If o, a and d are not collinear and o, d and d′ are collinear and a, d and s are collinear and d ≠ d′ and a′, d′ and s are collinear and o, a and a′ are collinear and o ≠ a′, then s ≠ d.

(11) If a, b and c are not collinear and a, b and b′ are collinear and a, c and c′ are collinear and a ≠ b′, then b′ ≠ c′.

(12) If a_{1}, a_{2} and a_{3} are not collinear and a_{1}, a_{2} and c_{3} are collinear and a_{2}, a_{3} and c_{1} are collinear and a_{1}, a_{3} and z are collinear and c_{1}, c_{3} and z are collinear and c_{3} ≠ a_{1} and c_{3} ≠ a_{2} and c_{1} ≠ a_{2} and c_{1} ≠ a_{3}, then a_{1} ≠ z and a_{3} ≠ z.

(13) If a, b and c are not collinear and a, b and d are collinear and c, e and d are collinear and e ≠ c and d ≠ a, then e, a and c are not collinear.

(14) If p_{1}, p_{2} and q_{1} are not collinear and p_{1}, p_{2} and q_{2} are collinear and q_{1}, q_{2} and q_{3} are collinear and p_{1} ≠ q_{2} and q_{2} ≠ q_{3}, then p_{2}, p_{1} and q_{3} are not collinear.

(15) If p_{1}, p_{2} and q_{1} are not collinear and p_{1}, p_{2} and p_{3} are collinear and q_{1}, q_{2} and p_{3} are collinear and p_{3} ≠ q_{2} and p_{2} ≠ p_{3}, then p_{3}, p_{2} and q_{2} are not collinear.

(16) If p_{1}, p_{2} and q_{1} are not collinear and p_{1}, p_{2} and p_{3} are collinear and q_{1}, q_{2} and p_{1} are collinear and p_{1} ≠ p_{3} and p_{1} ≠ q_{2}, then p_{3}, p_{1} and q_{2} are not collinear.

(17) If a_{1} ≠ a_{2} and b_{1} ≠ b_{2} and b_{1}, b_{2} and x are collinear and b_{1}, b_{2} and y are collinear and a_{1}, a_{2} and x are collinear and a_{1}, a_{2} and y are collinear and a_{1}, a_{2} and b_{1} are not collinear, then x = y.

(19)^{2} If o, a_{1} and a_{2} are not collinear and o, a_{1} and b_{1} are collinear and o, a_{2} and b_{2} are collinear and o ≠ b_{1} and o ≠ b_{2}, then o, b_{1} and b_{2} are not collinear.

We follow a convention: P_{1} denotes a Pappian projective plane defined in terms of collinearity and a_{1}, a_{2}, a_{3}, b_{1}, b_{2}, b_{3}, c_{1}, c_{2}, c_{3}, o, p_{1}, p_{2}, p_{3}, q_{1}, q_{2}, q_{3}, r_{1}, r_{2}, r_{3} denote elements of the points of P_{1}. We now state two propositions:

(20) Suppose that (i) p_{2} ≠ p_{3}, (ii) p_{1} ≠ p_{3}, (iii) q_{2} ≠ q_{3}, (iv) q_{1} ≠ q_{2},

(v) q_{1} ≠ q_{3}, (vi) p_{1}, p_{2} and q_{1} are not collinear, (vii) p_{1}, p_{2} and p_{3} are collinear, (viii) q_{1}, q_{2} and q_{3} are collinear, (ix) p_{1}, q_{2} and r_{3} are collinear,

(x) q_{1}, p_{2} and r_{3} are collinear, (xi) p_{1}, q_{3} and r_{2} are collinear, (xii) p_{3}, q_{1} and r_{2} are collinear, (xiii) p_{2}, q_{3} and r_{1} are collinear, (xiv) p_{3}, q_{2} and r_{1} are collinear.

2The proposition (18) was either repeated or obvious.

Then r_{1}, r_{2} and r_{3} are collinear.

(21) Suppose that (i) o ≠ b_{1}, (ii) a_{1} ≠ b_{1}, (iii) o ≠ b_{2}, (iv) a_{2} ≠ b_{2},

(v) o ≠ b_{3}, (vi) a_{3} ≠ b_{3}, (vii) o, a_{1} and a_{2} are not collinear, (viii) o, a_{1} and a_{3} are not collinear, (ix) o, a_{2} and a_{3} are not collinear,

(x) a_{1}, a_{2} and c_{3} are collinear, (xi) b_{1}, b_{2} and c_{3} are collinear, (xii) a_{2}, a_{3} and c_{1} are collinear, (xiii) b_{2}, b_{3} and c_{1} are collinear, (xiv) a_{1}, a_{3} and c_{2} are collinear, (xv) b_{1}, b_{3} and c_{2} are collinear, (xvi) o, a_{1} and b_{1} are collinear, (xvii) o, a_{2} and b_{2} are collinear, (xviii) o, a_{3} and b_{3} are collinear.

Then c_{1}, c_{2} and c_{3} are collinear. We see that the Pappian projective plane defined in terms of collinearity is

a Desarguesian projective plane defined in terms of collinearity.

We see that the Pappian projective space defined in terms of collinearity is a Desarguesian projective space defined in terms of collinearity.

References

[1] Wojciech Leończuk and Krzysztof Prażmowski. Projective spaces - part I. Formalized Mathematics, 1(4):767–776, 1990.

[2] Wojciech Leończuk and Krzysztof Prażmowski. Projective spaces - part II. Formalized Mathematics, 1(5):901–907, 1990.

[3] Wojciech Leoṅczuk and Krzysztof Prażmowski. Projective spaces - part III. Formalized Mathematics, 1(5):909–918, 1990.

[4] Wojciech Leończuk and Krzysztof Prażmowski. Projective spaces - part IV. Formalized Mathematics, 1(5):919–927, 1990.

[5] Wojciech Leończuk and Krzysztof Prażmowski. Projective spaces - part V. Formalized Mathematics, 1(5):929–938, 1990.

[6] Wojciech Leończuk and Krzysztof Prażmowski. Projective spaces - part VI. Formalized Mathematics, 1(5):939–947, 1990.

[7] Wojciech Skaba. The collinearity structure. Formalized Mathematics, 1(4):657–659, 1990.

220

Three-Argument Operations and Four-Argument Operations ^{1}

Michal Muzalewski Warsaw University Białystok

Wojciech Skaba University of Toruń

Summary. The article contains the definition of three- and fourargument operations. The article is also introduces a few operation related schemes: FuncEx3D, TriOpEx, Lambda3D, TriOpLambda, FuncEx4D, QuaOpEx, Lambda4D, QuaOpLambda.

MML Identifier: MULTOP 1.

The terminology and notation used in this paper have been introduced in the following articles: [4], [1], [2], [5], and [3]. Let f be a function, and let a, b, c be arbitrary. The functor f(a, b, c) is defined by: (Def.1) f(a, b, c) = f(⟨⟨a, b, c⟩⟩).

We now state the proposition

(1) For every function f and for arbitrary a, b, c holds f(a, b, c) = f(⟨⟨a, b, c⟩⟩). For simplicity we adopt the following rules: A, B, C, D are non-empty sets,

a is an element of A, b is an element of B, and c is an element of C. Let us consider A, B, C, D, and let f be a function from [: A, B, C:] into D, and let us consider a, b, c. Then f(a, b, c) is an element of D.

We adopt the following rules: X, Y, Z denote sets, T denotes a non-empty set, and x, y, z are arbitrary. One can prove the following propositions:

(2) For all functions f_{1}, f_{2} from [: X, Y, Z:] into T such that T ≠ ∅ and for all x, y, z such that x ∈ X and y ∈ Y and z ∈ Z holds f_{1}(⟨⟨x, y, z⟩⟩) = f_{2}(⟨⟨x, y, z⟩⟩) holds f_{1} = f_{2}.

(3) For all functions f_{1}, f_{2} from [: A, B, C:] into D such that for all a, b, c holds f_{1}(⟨⟨a, b, c⟩⟩) = f_{2}(⟨⟨a, b, c⟩⟩) holds f_{1} = f_{2}.

1Supported by RPBP.III-24.C6

(4) For all functions f_{1}, f_{2} from [: A, B, C:] into D such that for every element a of A and for every element b of B and for every element c of C holds f_{1}(a, b, c) = f_{2}(a, b, c) holds f_{1} = f_{2}.

Let us consider A. A ternary operation on A is a function from [: A, A, A:] into A.

In this article we present several logical schemes. The scheme FuncEx3D concerns a non-empty set A, a non-empty set B, a non-empty set C, a nonempty set D, and a 4-ary predicate P, and states that:

there exists a function f from [: A, B, C:] into D such that for every element x of A and for every element y of B and for every element z of C holds P[x, y, z, f(⟨⟨x, y, z⟩⟩)] provided the following requirements are met:

• for every element x of A and for every element y of B and for every element z of C there exists an element t of D such that P[x, y, z, t],

• for every element x of A and for every element y of B and for every element z of C and for all elements t_{1}, t_{2} of D such that P[x, y, z, t_{1}] and P[x, y, z, t_{2}] holds t_{1} = t_{2}.

The scheme TriOpEx concerns a non-empty set A, and a 4-ary predicate P, and states that:

there exists a ternary operation o on A such that for all elements a, b, c of A holds P[a, b, c, o(a, b, c)] provided the parameters meet the following requirements:

• for every elements x, y, z of A there exists an element t of A such that P[x, y, z, t],

• for all elements x, y, z of A and for all elements t_{1}, t_{2} of A such that P[x, y, z, t_{1}] and P[x, y, z, t_{2}] holds t_{1} = t_{2}.

The scheme Lambda3D concerns a non-empty set A, a non-empty set B, a non-empty set C, a non-empty set D, and a ternary functor F yielding an element of D and states that:

there exists a function f from [: A, B, C:] into D such that for every element x of A and for every element y of B and for every element z of C holds f(⟨⟨x, y, z⟩⟩) = F(x, y, z) for all values of the parameters.

The scheme TriOpLambda concerns a non-empty set A and a ternary functor F yielding an element of A and states that:

there exists a ternary operation o on A such that for all elements a, b, c of A holds o(a, b, c) = F(a, b, c) for all values of the parameters.

Let f be a function, and let a, b, c, d be arbitrary. The functor f(a, b, c, d) is defined as follows: (Def.2) f(a, b, c, d) = f(⟨⟨a, b, c, d⟩⟩).

One can prove the following proposition

(5) For every function f and for arbitrary a, b, c, d holds f(a, b, c, d) = f(⟨⟨a, b, c, d⟩⟩).

For simplicity we adopt the following rules: A, B, C, D, E will be non-empty sets, a will be an element of A, b will be an element of B, c will be an element of C, and d will be an element of D. Let us consider A, B, C, D, E, and let f be a function from [: A, B, C, D:] into E, and let us consider a, b, c, d. Then f(a, b, c, d) is an element of E.

We adopt the following rules: X, Y, Z, S will be sets, T will be a non-empty set, and x, y, z, s will be arbitrary. The following three propositions are true:

(6) Let f_{1}, f_{2} be functions from [: X, Y, Z, S:] into T. Then if T ≠ ∅ and for all x, y, z, s such that x ∈ X and y ∈ Y and z ∈ Z and s ∈ S holds f_{1}(⟨⟨x, y, z, s⟩⟩) = f_{2}(⟨⟨x, y, z, s⟩⟩), then f_{1} = f_{2}.

(7) For all functions f_{1}, f_{2} from [: A, B, C, D:] into E such that for all a, b, c, d holds f_{1}(⟨⟨a, b, c, d⟩⟩) = f_{2}(⟨⟨a, b, c, d⟩⟩) holds f_{1} = f_{2}.

(8) For all functions f_{1}, f_{2} from [: A, B, C, D:] into E such that for every element a of A and for every element b of B and for every element c of C and for every element d of D holds f_{1}(a, b, c, d) = f_{2}(a, b, c, d) holds f_{1} = f_{2}.

Let us consider A. A quadrary operation on A is a function from [: A, A, A, A:] into A.

Now we present four schemes. The scheme FuncEx4D concerns a non-empty set A, a non-empty set B, a non-empty set C, a non-empty set D, a non-empty set E, and a 5-ary predicate P, and states that:

there exists a function f from [: A, B, C, D:] into E such that for every element x of A and for every element y of B and for every element z of C and for every element s of D holds P[x, y, z, s, f(⟨⟨x, y, z, s⟩⟩)] provided the parameters have the following properties:

• for every element x of A and for every element y of B and for every element z of C and for every element s of D there exists an element t of E such that P[x, y, z, s, t],

• for every element x of A and for every element y of B and for every element z of C and for every element s of D and for all elements t_{1}, t_{2} of E such that P[x, y, z, s, t_{1}] and P[x, y, z, s, t_{2}] holds t_{1} = t_{2}.

The scheme QuaOpEx deals with a non-empty set A, and a 5-ary predicate P, and states that:

there exists a quadrary operation o on A such that for all elements a, b, c, d of A holds P[a, b, c, d, o(a, b, c, d)] provided the parameters meet the following requirements:

• for every elements x, y, z, s of A there exists an element t of A such that P[x, y, z, s, t],

• for all elements x, y, z, s of A and for all elements t_{1}, t_{2} of A such that P[x, y, z, s, t_{1}] and P[x, y, z, s, t_{2}] holds t_{1} = t_{2}.

The scheme Lambda4D concerns a non-empty set A, a non-empty set B, a non-empty set C, a non-empty set D, a non-empty set E, and a 4-ary functor F yielding an element of E and states that:

there exists a function f from [: A, B, C, D:] into E such that for every element x of A and for every element y of B and for every element z of C and for every element s of D holds f(⟨⟨x, y, z, s⟩⟩) = F(x, y, z, s) for all values of the parameters.

The scheme QuaOpLambda deals with a non-empty set A and a 4-ary functor F yielding an element of A and states that:

there exists a quadrary operation o on A such that for all elements a, b, c, d of A holds o(a, b, c, d) = F(a, b, c, d) for all values of the parameters.

References

[1] Czesław Byliński. Functions and their basic properties. Formalized Mathematics, 1(1):55– 65, 1990.

[2] Czesław Byliński. Functions from a set to a set. Formalized Mathematics, 1(1):153–164, 1990.

[3] Andrzej Trybulec. Domains and their Cartesian products. Formalized Mathematics, 1(1):115–122, 1990.

[4] Andrzej Trybulec. Tarski Grothendieck set theory. Formalized Mathematics, 1(1):9–11, 1990.

[5] Andrzej Trybulec. Tuples, projections and Cartesian products. Formalized Mathematics, 1(1):97–105, 1990.

Incidence Projective Spaces

Wojciech Leończuk^{1} Warsaw University Białystok Krzysztof Prażmowski^{2} Warsaw University Białystok

Summary. A basis for investigations on incidence projective spaces. With every projective space defined in terms of collinearity relation we associate the incidence structure consisting of points and lines of the given space. We introduce the general notion of projective space defined in terms of incidence and define several properties of such structures (like satisfability of the Desargues Axiom and conditions on the dimension).

MML Identifier: INCPROJ.

The papers [7], [8], [6], [1], [2], [3], [4], and [5] provide the notation and terminology for this paper. We consider projective incidence structures which are systems

⟨points, lines, an incidence⟩, where the points constitute a non-empty set, the lines constitute a non-empty set, and the incidence is a relation between the points and the lines.

We see that the projective space defined in terms of collinearity is a proper collinearity space.

For simplicity we follow a convention: C_{1} will be a proper collinearity space, x, y will be arbitrary, Y will be a set, and B will be an element of 2^{the points of C_{1}}. Let us consider C_{1}. We see that the line of C_{1} is an element of 2^{the points of C_{1}}.

Let us consider C_{1}. The functor L(C_{1}) yielding a non-empty set is defined by: (Def.1) L(C_{1}) = {B : B is a line of C_{1}}.

We now state two propositions:

(1) L(C_{1}) = {B : B is a line of C_{1}}.

(2) For every x holds x is a line of C_{1} if and only if x is an element of L(C_{1}).

1Supported by RPBP.III-24.C6

2Supported by RPBP.III-24.C2

Let us consider C_{1}. The functor I_{C_{1}} yields a relation between the points of C_{1} and L(C_{1}) and is defined by: (Def.2) for all x, y holds ⟨⟨x, y⟩⟩ ∈ I_{C_{1}} if and only if x ∈ the points of C_{1} and

y ∈ L(C_{1}) and there exists Y such that y = Y and x ∈ Y.

Let us consider C_{1}. The functor Inc-ProjSp(C_{1}) yields a projective incidence structure and is defined by: (Def.3) Inc-ProjSp(C_{1}) = ⟨ the points of C_{1}, L(C_{1}), I_{C_{1}}⟩.

Next we state four propositions:

(3) Inc-ProjSp(C_{1}) = ⟨ the points of C_{1}, L(C_{1}), I_{C_{1}}⟩.

(4) For every C_{1} holds the points of Inc-ProjSp(C_{1}) = the points of C_{1} and the lines of Inc-ProjSp(C_{1}) = L(C_{1}) and the incidence of Inc-ProjSp(C_{1}) = I_{C_{1}}.

(5) For every x holds x is a line of C_{1} if and only if x is an element of the lines of Inc-ProjSp(C_{1}).

(6) For every x holds x is an element of the points of Inc-ProjSp(C_{1}) if and only if x is an element of the points of C_{1}.

For simplicity we adopt the following rules: a, b, c, p, q, s will be elements of the points of Inc-ProjSp(C_{1}), P, Q, S will be elements of the lines of Inc-ProjSp(C_{1}), P′ will be a line of C_{1}, and a′, b′, c′, p′ will be elements of the points of C_{1}. Let I_{1} be a projective incidence structure, and let s be an element of the points of I_{1}, and let S be an element of the lines of I_{1}. The predicate s | S is defined as follows: (Def.4) ⟨⟨s, S⟩⟩ ∈ the incidence of I_{1}.

One can prove the following propositions:

(7) s | S if and only if ⟨⟨s, S⟩⟩ ∈ I_{C_{1}}.

(8) If p = p′ and P = P′, then p | P if and only if p′ ∈ P′.

(9) There exist a′, b′, c′ such that a′ ≠ b′ and b′ ≠ c′ and c′ ≠ a′.

(10) For every a′ there exists b′ such that a′ ≠ b′.

(11) If p | P and q | P and p | Q and q | Q, then p = q or P = Q.

(12) For every p, q there exists P such that p | P and q | P.

(13) If a = a′ and b = b′ and c = c′, then a′, b′ and c′ are collinear if and only if there exists P such that a | P and b | P and c | P.

(14) There exist p, P such that p P.

For simplicity we follow the rules: C_{1} is a projective space defined in terms of collinearity, a, b, c, d, p, q are elements of the points of Inc-ProjSp(C_{1}), P, Q, S, M, N are elements of the lines of Inc-ProjSp(C_{1}), and a′, b′, c′, d′, p′ are elements of the points of C_{1}. One can prove the following propositions:

(15) For every P there exist a, b, c such that a ≠ b and b ≠ c and c ≠ a and a | P and b | P and c | P.

(16) Suppose that (i) a | M, (ii) b | M, (iii) c | N, (iv) d | N,

(v) p | M, (vi) p | N, (vii) a | P, (viii) c | P, (ix) b | Q,

(x) d | Q, (xi) p P, (xii) p Q, (xiii) M ≠ N.

Then there exists q such that q | P and q | Q.

(17) If for every a′, b′, c′, d′ there exists p′ such that a′, b′ and p′ are collinear and c′, d′ and p′ are collinear, then for every M, N there exists q such that q | M and q | N.

(18) If there exist elements p, p_{1}, r, r_{1} of the points of C_{1} such that for no element s of the points of C_{1} holds p, p_{1} and s are collinear and r, r_{1} and s are collinear, then there exist M, N such that for no q holds q | M and q | N.

(19) Suppose for every elements p, p_{1}, q, q_{1}, r_{2} of the points of C_{1} there exist elements r, r_{1} of the points of C_{1} such that p, q and r are collinear and p_{1}, q_{1} and r_{1} are collinear and r_{2}, r and r_{1} are collinear. Then for every a, M, N there exist b, c, S such that a | S and b | S and c | S and b | M and c | N.

We now define two new predicates. Let x, y, z be arbitrary. We say that x, y, z are mutually different if and only if: (Def.5) x ≠ y and y ≠ z and z ≠ x. Let u be arbitrary. We say that x, y, z, u are mutually different if and only if: (Def.6) x ≠ y and y ≠ z and z ≠ x and u ≠ x and u ≠ y and u ≠ z.

We now define two new predicates. Let C_{2} be a projective incidence structure, and let a, b be elements of the points of C_{2}, and let M be an element of the lines of C_{2}. The predicate a, b | M is defined as follows: (Def.7) a | M and b | M. Let c be an element of the points of C_{2}. The predicate a, b, c | M is defined by: (Def.8) a | M and b | M and c | M.

We now state three propositions:

(20) Suppose that

(i) for all elements p_{1}, r_{2}, q, r_{1}, q_{1}, p, r of the points of C_{1} such that p_{1}, r_{2} and q are collinear and r_{1}, q_{1} and q are collinear and p_{1}, r_{1} and p are collinear and r_{2}, q_{1} and p are collinear and p_{1}, q_{1} and r are collinear and r_{2}, r_{1} and r are collinear and p, q and r are collinear holds p_{1}, r_{2} and q_{1} are collinear or p_{1}, r_{2} and r_{1} are collinear or p_{1}, r_{1} and q_{1} are collinear or r_{2}, r_{1} and q_{1} are collinear. Let p, q, r, s, a, b, c be elements of the points of Inc-ProjSp(C_{1}). Let L, Q, R, S, A, B, C be elements of the lines of Inc-ProjSp(C_{1}). Suppose that

(ii) q L, (iii) r L, (iv) p Q,

(v) s Q, (vi) p R, (vii) r R, (viii) q S, (ix) s S,

(x) a, p, s | L, (xi) a, q, r | Q, (xii) b, q, s | R, (xiii) b, p, r | S, (xiv) c, p, q | A, (xv) c, r, s | B, (xvi) a, b | C.

Then c C.

(21) Suppose that

(i) for all elements o, p_{1}, p_{2}, p_{3}, q_{1}, q_{2}, q_{3}, r_{1}, r_{2}, r_{3} of the points of C_{1} such that o ≠ q_{1} and p_{1} ≠ q_{1} and o ≠ q_{2} and p_{2} ≠ q_{2} and o ≠ q_{3} and p_{3} ≠ q_{3} and o, p_{1} and p_{2} are not collinear and o, p_{1} and p_{3} are not collinear and o, p_{2} and p_{3} are not collinear and p_{1}, p_{2} and r_{3} are collinear and q_{1}, q_{2} and r_{3} are collinear and p_{2}, p_{3} and r_{1} are collinear and q_{2}, q_{3} and r_{1} are collinear and p_{1}, p_{3} and r_{2} are collinear and q_{1}, q_{3} and r_{2} are collinear and o, p_{1} and q_{1} are collinear and o, p_{2} and q_{2} are collinear and o, p_{3} and q_{3} are collinear holds r_{1}, r_{2} and r_{3} are collinear. Let o, b_{1}, a_{1}, b_{2}, a_{2}, b_{3}, a_{3}, r, s, t be elements of the points of Inc-ProjSp(C_{1}). Let C_{3}, C_{4}, C_{5}, A_{1}, A_{2}, A_{3}, B_{1}, B_{2}, B_{3} be elements of the lines of Inc-ProjSp(C_{1}). Suppose that

(ii) o, b_{1}, a_{1} | C_{3}, (iii) o, a_{2}, b_{2} | C_{4}, (iv) o, a_{3}, b_{3} | C_{5},

(v) a_{3}, a_{2}, t | A_{1}, (vi) a_{3}, r, a_{1} | A_{2}, (vii) a_{2}, s, a_{1} | A_{3}, (viii) t, b_{2}, b_{3} | B_{1}, (ix) b_{1}, r, b_{3} | B_{2},

(x) b_{1}, s, b_{2} | B_{3}, (xi) C_{3}, C_{4}, C_{5} are mutually different, (xii) o ≠ a_{1}, (xiii) o ≠ a_{2}, (xiv) o ≠ a_{3}, (xv) o ≠ b_{1}, (xvi) o ≠ b_{2}, (xvii) o ≠ b_{3}, (xviii) a_{1} ≠ b_{1}, (xix) a_{2} ≠ b_{2}, (xx) a_{3} ≠ b_{3}.

Then there exists an element O of the lines of Inc-ProjSp(C_{1}) such that r, s, t | O.

(22) Suppose that

(i) for all elements o, p_{1}, p_{2}, p_{3}, q_{1}, q_{2}, q_{3}, r_{1}, r_{2}, r_{3} of the points of C_{1} such that o ≠ p_{2} and o ≠ p_{3} and p_{2} ≠ p_{3} and p_{1} ≠ p_{2} and p_{1} ≠ p_{3} and o ≠ q_{2} and o ≠ q_{3} and q_{2} ≠ q_{3} and q_{1} ≠ q_{2} and q_{1} ≠ q_{3} and o, p_{1} and q_{1} are not collinear and o, p_{1} and p_{2} are collinear and o, p_{1} and p_{3} are collinear and o, q_{1} and q_{2} are collinear and o, q_{1} and q_{3} are collinear and p_{1}, q_{2} and r_{3} are collinear and q_{1}, p_{2} and r_{3} are collinear and p_{1}, q_{3} and r_{2} are collinear and p_{3}, q_{1} and r_{2} are collinear and p_{2}, q_{3} and r_{1} are collinear and p_{3}, q_{2} and r_{1} are collinear holds r_{1}, r_{2} and r_{3} are collinear. Let o, a_{1}, a_{2}, a_{3}, b_{1}, b_{2}, b_{3}, c_{1}, c_{2}, c_{3} be elements of the points of Inc-ProjSp(C_{1}). Let A_{1}, A_{2}, A_{3}, B_{1}, B_{2}, B_{3}, C_{3}, C_{4}, C_{5} be elements of the lines of Inc-ProjSp(C_{1}). Suppose that

(ii) o, a_{1}, a_{2}, a_{3} are mutually different, (iii) o, b_{1}, b_{2}, b_{3} are mutually different, (iv) A_{3} ≠ B_{3},

(v) o | A_{3}, (vi) o | B_{3}, (vii) a_{2}, b_{3}, c_{1} | A_{1}, (viii) a_{3}, b_{1}, c_{2} | B_{1}, (ix) a_{1}, b_{2}, c_{3} | C_{3},

(x) a_{1}, b_{3}, c_{2} | A_{2}, (xi) a_{3}, b_{2}, c_{1} | B_{2}, (xii) a_{2}, b_{1}, c_{3} | C_{4}, (xiii) b_{1}, b_{2}, b_{3} | A_{3}, (xiv) a_{1}, a_{2}, a_{3} | B_{3}, (xv) c_{1}, c_{2} | C_{5}.

Then c_{3} | C_{5}. A projective incidence structure is called a projective space defined in terms

of incidence if: (Def.9) (i) for all elements p, q of the points of it and for all elements P, Q of

the lines of it such that p | P and q | P and p | Q and q | Q holds p = q or P = Q,

(ii) for every elements p, q of the points of it there exists an element P of the lines of it such that p | P and q | P, (iii) there exists an element p of the points of it and there exists an element

P of the lines of it such that p P, (iv) for every element P of the lines of it there exist elements a, b, c of the

points of it such that a ≠ b and b ≠ c and c ≠ a and a | P and b | P and c | P,

(v) for all elements a, b, c, d, p, q of the points of it and for all elements M, N, P, Q of the lines of it such that a | M and b | M and c | N and d | N and p | M and p | N and a | P and c | P and b | Q and d | Q and p P and p Q and M ≠ N there exists an element q of the points of it such that q | P and q | Q.

Let C_{1} be a projective space defined in terms of collinearity. Then Inc-ProjSp(C_{1}) is a projective space defined in terms of incidence. A projective space defined in terms of incidence is 2-dimensional if:

(Def.10) for every elements M, N of the lines of it there exists an element q of the points of it such that q | M and q | N.

A projective space defined in terms of incidence is at least 3-dimensional if: (Def.11) there exist elements M, N of the lines of it such that for no element q

of the points of it holds q | M and q | N.

A projective space defined in terms of incidence is at most 3-dimensional if: (Def.12) for every element a of the points of it and for every elements M, N of

the lines of it there exist elements b, c of the points of it and there exists an element S of the lines of it such that a | S and b | S and c | S and b | M and c | N.

A projective space defined in terms of incidence is 3-dimensional if: (Def.13) it is at most 3-dimensional and it is at least 3-dimensional.

A projective space defined in terms of incidence is Fanoian if: (Def.14) Let p, q, r, s, a, b, c be elements of the points of it . Let L, Q, R, S,

A, B, C be elements of the lines of it . Suppose that

(i) q L, (ii) r L, (iii) p Q, (iv) s Q,

(v) p R, (vi) r R, (vii) q S, (viii) s S, (ix) a, p, s | L,

(x) a, q, r | Q, (xi) b, q, s | R, (xii) b, p, r | S, (xiii) c, p, q | A, (xiv) c, r, s | B, (xv) a, b | C.

Then c C.

A projective space defined in terms of incidence is Desarguesian if: (Def.15) Let o, b_{1}, a_{1}, b_{2}, a_{2}, b_{3}, a_{3}, r, s, t be elements of the points of it . Let

C_{3}, C_{4}, C_{5}, A_{1}, A_{2}, A_{3}, B_{1}, B_{2}, B_{3} be elements of the lines of it . Suppose that

(i) o, b_{1}, a_{1} | C_{3}, (ii) o, a_{2}, b_{2} | C_{4}, (iii) o, a_{3}, b_{3} | C_{5}, (iv) a_{3}, a_{2}, t | A_{1},

(v) a_{3}, r, a_{1} | A_{2}, (vi) a_{2}, s, a_{1} | A_{3}, (vii) t, b_{2}, b_{3} | B_{1}, (viii) b_{1}, r, b_{3} | B_{2}, (ix) b_{1}, s, b_{2} | B_{3},

(x) C_{3}, C_{4}, C_{5} are mutually different, (xi) o ≠ a_{1}, (xii) o ≠ a_{2}, (xiii) o ≠ a_{3}, (xiv) o ≠ b_{1}, (xv) o ≠ b_{2}, (xvi) o ≠ b_{3}, (xvii) a_{1} ≠ b_{1}, (xviii) a_{2} ≠ b_{2}, (xix) a_{3} ≠ b_{3}.

Then there exists an element O of the lines of it such that r, s, t | O.

A projective space defined in terms of incidence is Pappian if: (Def.16) Let o, a_{1}, a_{2}, a_{3}, b_{1}, b_{2}, b_{3}, c_{1}, c_{2}, c_{3} be elements of the points of it .

Let A_{1}, A_{2}, A_{3}, B_{1}, B_{2}, B_{3}, C_{3}, C_{4}, C_{5} be elements of the lines of it . Suppose that

(i) o, a_{1}, a_{2}, a_{3} are mutually different, (ii) o, b_{1}, b_{2}, b_{3} are mutually different, (iii) A_{3} ≠ B_{3}, (iv) o | A_{3},

(v) o | B_{3}, (vi) a_{2}, b_{3}, c_{1} | A_{1}, (vii) a_{3}, b_{1}, c_{2} | B_{1}, (viii) a_{1}, b_{2}, c_{3} | C_{3}, (ix) a_{1}, b_{3}, c_{2} | A_{2},

(x) a_{3}, b_{2}, c_{1} | B_{2}, (xi) a_{2}, b_{1}, c_{3} | C_{4}, (xii) b_{1}, b_{2}, b_{3} | A_{3}, (xiii) a_{1}, a_{2}, a_{3} | B_{3}, (xiv) c_{1}, c_{2} | C_{5}.

232 Wojciech Leończuk et al.

Then c_{3} | C_{5}.

References

[1] Wojciech Leończuk and Krzysztof Prażmowski. Projective spaces - part I. Formalized Mathematics, 1(4):767–776, 1990.

[2] Wojciech Leoṅczuk and Krzysztof Prażmowski. Projective spaces - part III. Formalized Mathematics, 1(5):909–918, 1990.

[3] Wojciech Leończuk and Krzysztof Prażmowski. Projective spaces - part IV. Formalized Mathematics, 1(5):919–927, 1990.

[4] Wojciech Leończuk and Krzysztof Prażmowski. Projective spaces - part V. Formalized Mathematics, 1(5):929–938, 1990.

[5] Wojciech Leończuk and Krzysztof Prażmowski. Projective spaces - part VI. Formalized Mathematics, 1(5):939–947, 1990.

[6] Wojciech Skaba. The collinearity structure. Formalized Mathematics, 1(4):657–659, 1990.

[7] Andrzej Trybulec. Tarski Grothendieck set theory. Formalized Mathematics, 1(1):9–11, 1990.

[8] Edmund Woronowicz. Relations defined on sets. Formalized Mathematics, 1(1):181–186, 1990.

One-Dimensional Congruence of Segments, Basic Facts and Midpoint Relation ^{1}

Barbara Konstanta Siedlce Agricultural and Pedagogical University

Urszula Kowieska Siedlce Agricultural and Pedagogical University

Grzegorz Lewandowski Siedlce Agricultural and Pedagogical University

Krzysztof Prażmowski Warsaw University Białystok

Summary. We study the theory of one-dimensional congruence of segments. The theory is characterized by a suitable formal axiom system; as a model of this system one can take the structure obtained from any weak directed geometrical bundle, with the congruence interpreted as in the case of ”classical” vectors. Preliminary consequences of our axiom system are proved, basic relations of maximal distance and of midpoint are defined, and several fundamental properties of them are established.

MML Identifier: AFVECT01.

The papers [8], [2], [3], [10], [7], [4], [1], [5], [6], and [9] provide the terminology and notation for this paper. In the sequel A_{1} will be a weak affine vector space. Let us consider A_{1}, and let a, b, c, d be elements of the points of A_{1}. The predicate a, b c, d is defined as follows: (Def.1) a, b c, d or a, b d, c.

An affine structure is called a weak segment-congruence space if: (Def.2) (i) there exist elements a, b of the points of it such that a ≠ b,

(ii) for all elements a, b of the points of it holds a, b b, a,

1Supported by RPBP.III-24.C3

(iii) for all elements a, b of the points of it such that a, b a, a holds a = b, (iv) for all elements a, b, c, d, p, q of the points of it such that a, b p, q

and c, d p, q holds a, b c, d,

(v) for every elements a, c of the points of it there exists an element b of the points of it such that a, b b, c,

(vi) for all elements a, a′, b, b′, p of the points of it such that a ≠ a′ and

b ≠ b′ and p, a p, a′ and p, b p, b′ holds a, b a′, b′, (vii) for all elements a, b of the points of it holds a = b or there exists an

element c of the points of it such that a ≠ c and a, b b, c or there exist elements p, p′ of the points of it such that p ≠ p′ and a, b p, p′ and a, p p, b and a, p′ p′, b,

(viii) for all elements a, b, b′, p, p′, c of the points of it such that a, b b, c

and b, b′ p, p′ and b, p p, b′ and b, p′ p′, b′ holds a, b′ b′, c, (ix) for all elements a, b, b′, c of the points of it such that a ≠ c and b ≠ b′

and a, b b, c and a, b′ b′, c there exist elements p, p′ of the points of it such that p ≠ p′ and b, b′ p, p′ and b, p p, b′ and b, p′ p′, b′,

(x) for all elements a, b, c, p, p′, q, q′ of the points of it such that a, b p, p′ and a, c q, q′ and a, p p, b and a, q q, c and a, p′ p′, b and a, q′ q′, c there exist elements r, r′ of the points of it such that b, c r, r′ and b, r r, c and b, r′ r′, c.

We adopt the following rules: A_{1} is a weak segment-congruence space and a, b, b′, b′′, c, d, p, p′ are elements of the points of A_{1}. Let us consider A_{1}, and let a, b, c, d be elements of the points of A_{1}. The predicate a, b c, d is defined by: (Def.3) a, b c, d.

We now state several propositions:

(1) a, b a, b.

(2) If a, b c, d, then c, d a, b.

(3) If a, b c, d, then a, b d, c.

(4) If a, b c, d, then b, a c, d.

(5) For all a, b holds a, a b, b.

(6) If a, b c, c, then a = b.

(7) If a, b p, p′ and p, p′ b, c and a, b b, c and a, p p, b and a, p′ p′, b, then a = c.

(8) If a, b a, b′ and a, b′ a, b′′ and a, b a, b′′, then b = b′ or b = b′′ or b′ = b′′.

Let us consider A_{1}, a, b. We say that a, b are in a maximal distance if and only if: (Def.4) there exist p, p′ such that p ≠ p′ and a, b p, p′ and a, p p, b and

a, p′ p′, b.

Let us consider A_{1}, a, b, c. We say that b is a midpoint of a, c if and only if: (Def.5) a = b and b = c and a = c or a = c and a, b are in a maximal distance

or a ≠ c and a, b b, c.

One-Dimensional Congruence of Segments, … 235

Next we state three propositions: (11)^{2} If a ≠ b and a, b are not in a maximal distance, then there exists c such

that a ≠ c and a, b b, c.

(12) If a, b are in a maximal distance and a, b b, c, then a = c.

(13) If a, b are in a maximal distance, then a ≠ b.

References

[1] Czesław Byliński. Binary operations. Formalized Mathematics, 1(1):175–180, 1990.

[2] Czesław Byliński. Functions and their basic properties. Formalized Mathematics, 1(1):55–65, 1990.

[3] Czesław Byliński. Functions from a set to a set. Formalized Mathematics, 1(1):153–164, 1990.

[4] Eugeniusz Kusak, Wojciech Leończuk, and Michał Muzalewski. Abelian groups, fields and vector spaces. Formalized Mathematics, 1(2):335–342, 1990.

[5] Grzegorz Lewandowski and Krzysztof Prażmowski. A construction of an abstract space of congruence of vectors. Formalized Mathematics, 1(4):685–688, 1990.

[6] Grzegorz Lewandowski, Krzysztof Prażmowski, and Bożena Lewandowska. Directed geometrical bundles and their analytical representation. Formalized Mathematics, 2(1):135– 141, 1991.

[7] Henryk Oryszczyszyn and Krzysztof Prażmowski. Analytical ordered affine spaces. Formalized Mathematics, 1(3):601–605, 1990.

[8] Andrzej Trybulec. Tarski Grothendieck set theory. Formalized Mathematics, 1(1):9–11, 1990.

[9] Andrzej Trybulec. Tuples, projections and Cartesian products. Formalized Mathematics, 1(1):97–105, 1990.

[10] Edmund Woronowicz. Relations defined on sets. Formalized Mathematics, 1(1):181–186, 1990.

Received October 4, 1990

2The propositions (9)–(10) were either repeated or obvious.

236

Algebra of Normal Forms

Andrzej Trybulec Warsaw University Białystok

Summary. We mean by a normal form a finite set of ordered pairs of subsets of a fixed set that fulfils two conditions: elements of it consist of disjoint sets and elements of it are incomparable w.r.t. inclusion. The underlying set corresponds to a set of propositional variables but is arbitrary. The correspodents to a normal form of a formula, e.g. a disjunctive normal form, is as follows. The normal form is the set of disjuncts and a disjunct is an ordered pair consisting of the sets of propostional variables that occur in the non-negated and negated disjunct. The requirement that the element of a normal form consists of disjoint sets means that contradictory disjuncts have been removed, and the second condition means that the absorption law has been used to shorten the normal form. We construct a lattice ⟨ , ⊔, ⊓⟩ , where a⊔b = μ(a∪b) and a ⊓ b = μc, c being the set of all pairs ⟨X_{1} ∪ Y_{1}, X_{2} ∪ Y_{2}⟩, ⟨X_{1}, X_{2}⟩ ∈ a and ⟨Y_{1}, Y_{2}⟩ ∈ b, which consist of disjoint sets. μa denotes here the set of all minimal, w.r.t. inclusion, elements of a. We prove that the lattice of normal forms over a set defined in this way is distributive and that ∅ is the minimal element of it.

MML Identifier: NORMFORM.

The terminology and notation used here have been introduced in the following articles: [8], [9], [3], [4], [1], [5], [2], [6], [10], [7], and [11]. In the sequel A, B, C, D will be sets. We now state two propositions:

(1) If A ⊆ B and C ⊆ D and B misses D, then A misses C.

(2) If A \ B ⊆ C, then A ⊆ B ∪ C. In the sequel A, B will denote Boolean domains and x, y will denote elements

of [: A, B:]. We now define five new constructions. Let us consider A, B, x, y. The predicate x ⊆ y is defined by: (Def.1) x_{1} ⊆ y_{1} and x_{2} ⊆ y_{2}. The functor x ∪ y yielding an element of [: A, B:] is defined as follows: (Def.2) x ∪ y = ⟨⟨x_{1} ∪ y_{1}, x_{2} ∪ y_{2}⟩⟩. The functor x ∩ y yielding an element of [: A, B:] is defined as follows:

(Def.3) x ∩ y = ⟨⟨x_{1} ∩ y_{1}, x_{2} ∩ y_{2}⟩⟩. The functor x \ y yields an element of [: A, B:] and is defined as follows: (Def.4) x \ y = ⟨⟨x_{1} \ y_{1}, x_{2} \ y_{2}⟩⟩. The functor x− . y yields an element of [: A, B:] and is defined as follows: (Def.5) x− . y = ⟨⟨x_{1}− . y_{1}, x_{2}− . y_{2}⟩⟩.

In the sequel X will be a set and a, b, c will be elements of [: A, B:]. We now state a number of propositions:

(3) a ⊆ a.

(4) If a ⊆ b and b ⊆ a, then a = b.

(5) If a ⊆ b and b ⊆ c, then a ⊆ c.

(6) a ∪ b = ⟨⟨a_{1} ∪ b_{1}, a_{2} ∪ b_{2}⟩⟩.

(7) a ∩ b = ⟨⟨a_{1} ∩ b_{1}, a_{2} ∩ b_{2}⟩⟩.

(8) a \ b = ⟨⟨a_{1} \ b_{1}, a_{2} \ b_{2}⟩⟩.

(9) a− . b = ⟨⟨a_{1}− . b_{1}, a_{2}− . b_{2}⟩⟩.

(10) (a ∪ b)_{1} = a_{1} ∪ b_{1} and (a ∪ b)_{2} = a_{2} ∪ b_{2}.

(11) (a ∩ b)_{1} = a_{1} ∩ b_{1} and (a ∩ b)_{2} = a_{2} ∩ b_{2}.

(12) (a \ b)_{1} = a_{1} \ b_{1} and (a \ b)_{2} = a_{2} \ b_{2}.

(13) (a− . b)_{1} = a_{1}− . b_{1} and (a− . b)_{2} = a_{2}− . b_{2}.

(14) a ∪ a = a.

(15) a ∪ b = b ∪ a.

(16) a ∪ b ∪ c = a ∪ (b ∪ c).

(17) a ∩ a = a.

(18) a ∩ b = b ∩ a.

(19) a ∩ b ∩ c = a ∩ (b ∩ c).

(20) a ∩ (b ∪ c) = a ∩ b ∪ a ∩ c.

(21) a ∪ b ∩ a = a.

(22) a ∩ (b ∪ a) = a. (24)^{1} a ∪ b ∩ c = (a ∪ b) ∩ (a ∪ c).

(25) If a ⊆ c and b ⊆ c, then a ∪ b ⊆ c.

(26) a ⊆ a ∪ b and b ⊆ a ∪ b.

(27) If a = a ∪ b, then b ⊆ a.

(28) If a ⊆ b, then c ∪ a ⊆ c ∪ b and a ∪ c ⊆ b ∪ c.

(29) (a \ b) ∪ b = a ∪ b.

(30) If a \ b ⊆ c, then a ⊆ b ∪ c.

(31) If a ⊆ b ∪ c, then a \ c ⊆ b.

In the sequel a will be an element of [: Fin X, Fin X:]. Let A be a set. The functor FinUnion_{A} yields a binary operation on [: Fin A, Fin A:] and is defined by:

1The proposition (23) was either repeated or obvious.

(Def.6) for all elements x, y of [: Fin A, Fin A:] holds FinUnion_{A}(x, y) = x ∪ y.

In the sequel A will denote a set. Let X be a non-empty set, and let A be a set, and let B be an element of Fin X, and let f be a function from X into [: Fin A, Fin A:]. The functor FinUnion(B, f) yields an element of [: Fin A, Fin A:] and is defined as follows: (Def.7) FinUnion(B, f) = FinUnion_{A} - ∑_{B} f.

The following propositions are true:

(32) FinUnion_{A} is idempotent.

(33) FinUnion_{A} is commutative.

(34) FinUnion_{A} is associative.

(35) For every non-empty set X and for every function f from X into [: Fin A, Fin A:] and for every element B of Fin X and for every element x of X such that x ∈ B holds f(x) ⊆ FinUnion(B, f).

(36) ⟨⟨0_{A}, 0_{A}⟩⟩ is a unity w.r.t. FinUnion_{A}.

(37) FinUnion_{A} has a unity.

(38) 1_{FinUnion_{A}} = ⟨⟨0_{A}, 0_{A}⟩⟩.

(39) For every element x of [: Fin A, Fin A:] holds 1_{FinUnion_{A}} ⊆ x.

(40) For every non-empty set X and for every function f from X into [: Fin A, Fin A:] and for every element B of Fin X and for every element c of [: Fin A, Fin A:] such that for every element x of X such that x ∈ B holds f(x) ⊆ c holds FinUnion(B, f) ⊆ c.

(41) For every non-empty set X and for every element B of Fin X and for all functions f, g from X into [: Fin A, Fin A:] such that f B = g B holds FinUnion(B, f) = FinUnion(B, g).

Let us consider X. The functor DP(X) yields a non-empty subset of [: Fin X, Fin X:] and is defined as follows: (Def.8) DP(X) = {a : a_{1} misses a_{2} }.

The following proposition is true

(42) For every element y of [: Fin X, Fin X:] holds y ∈ DP(X) if and only if

y_{1} ∩ y_{2} = ∅. In the sequel x, y will denote elements of [: Fin X, Fin X:] and a, b will denote

elements of DP(X). We now state several propositions:

(43) If y ∈ DP(X) and x ∈ DP(X), then y ∪ x ∈ DP(X) if and only if y_{1} ∩ x_{2} ∪ x_{1} ∩ y_{2} = ∅.

(44) a_{1} ∩ a_{2} = ∅.

(45) If x ⊆ b, then x is an element of DP(X).

(46) For no arbitrary x holds x ∈ a_{1} and x ∈ a_{2}.

(47) If a ∪ b ∉ DP(X), then there exists an element p of X such that p ∈ a_{1} and p ∈ b_{2} or p ∈ b_{1} and p ∈ a_{2}.

(48) a_{1} misses a_{2}.

(49) If x_{1} misses x_{2}, then x is an element of DP(X).

(50) For all sets V, W such that V ⊆ a_{1} and W ⊆ a_{2} holds ⟨⟨V, W ⟩⟩ is an

element of DP(X). In this article we present several logical schemes. The scheme LambdaX

concerns a non-empty set A, a non-empty set B, a non-empty subset C of A, and a unary functor F yielding an element of C and states that:

there exists a function f from B into C such that for every element x of B holds f(x) = F(x) for all values of the parameters.

The scheme BinOpLambdaX deals with a non-empty set A, a non-empty subset B of A, and a binary functor F yielding an element of B and states that:

there exists a binary operation o on B such that for all elements a, b of B holds o(a, b) = F(a, b) for all values of the parameters.

For simplicity we follow a convention: A will be a set, x will be an element of [: Fin A, Fin A:], a, b, c, s, t will be elements of DP(A), and B, C, D will be elements of Fin DP(A). Let us consider A. The normal forms over A yields a non-empty subset of Fin DP(A) and is defined as follows: (Def.9) the normal forms over A = {B : a ∈ B ∧ b ∈ B ∧ a ⊆ b ⇒ a = b}.

In the sequel K, L, M are elements of the normal forms over A. Next we state three propositions:

(51) ∅ ∈ the normal forms over A.

(52) If B ∈ the normal forms over A and a ∈ B and b ∈ B and a ⊆ b, then a = b.

(53) If for all a, b such that a ∈ B and b ∈ B and a ⊆ b holds a = b, then

B ∈ the normal forms over A. We now define two new functors. Let us consider A, B. The functor μB

yielding an element of the normal forms over A is defined by: (Def.10) μB = {t : s ∈ B ∧ s ⊆ t ⇔ s = t}.

Let us consider C. The functor B ^{}C yielding an element of Fin DP(A) is defined as follows:

(Def.11) B ^{}C = DP(A) ∩ {s ∪ t : s ∈ B ∧ t ∈ C}.

The following propositions are true:

(54) B ^{}C = DP(A) ∩ {s ∪ t : s ∈ B ∧ t ∈ C}.

(55) If x ∈ B ^{}C, then there exist b, c such that b ∈ B and c ∈ C and x = b ∪ c.

(56) If b ∈ B and c ∈ C and b ∪ c ∈ DP(A), then b ∪ c ∈ B ^{}C.

(57) If b ∈ B and c ∈ C and a = b ∪ c, then a ∈ B ^{}C.

(58) If a ∈ μB, then a ∈ B but if b ∈ B and b ⊆ a, then b = a.

(59) If a ∈ μB, then a ∈ B.

(60) If a ∈ μB and b ∈ B and b ⊆ a, then b = a.

(61) If a ∈ B and for every b such that b ∈ B and b ⊆ a holds b = a, then

a ∈ μB. We now define two new functors. Let us consider A. The functor ⊔_{A} yields

a binary operation on the normal forms over A and is defined by: (Def.12) ⊔_{A}(K, L) = μ(K ∪ L).

The functor ⊓_{A} yielding a binary operation on the normal forms over A is defined by:

(Def.13) ⊓_{A}(K, L) = μ(K ^{}L).

One can prove the following propositions:

(62) ⊔_{A}(K, L) = μ(K ∪ L).

(63) ⊓_{A}(K, L) = μ(K ^{}L).

Let A be a non-empty set, and let B be a non-empty subset of A, and let O be a binary operation on B, and let a, b be elements of B. Then O(a, b) is an element of B.

One can prove the following propositions:

(64) μB ⊆ B.

(65) If b ∈ B, then there exists c such that c ⊆ b and c ∈ μB.

(66) μK = K.

(67) μ(B ∪ C) ⊆ μB ∪ C.

(68) μ(μB ∪ C) = μ(B ∪ C).

(69) μ(B ∪ μC) = μ(B ∪ C).

(70) If B ⊆ C, then B ^{}D ⊆ C ^{}D.

(71) μ(B ^{}C) ⊆ μB ^{}C.

(72) B ^{}C = C ^{}B.

(73) If B ⊆ C, then D^{}B ⊆ D^{}C.

(74) μ(μB ^{}C) = μ(B ^{}C).

(75) μ(B ^{}μC) = μ(B ^{}C).

(76) K ^{}(L^{}M) = K ^{}L^{}M.

(77) K ^{}(L ∪ M) = K ^{}L ∪ K ^{}M.

(78) B ⊆ B ^{}B.

(79) μ(K ^{}K) = μK.

Let us consider A. The lattice of normal forms over A yields a lower bound lattice and is defined as follows:

(Def.14) the lattice of normal forms over A = ⟨the normal forms over A, ⊔_{A}, ⊓_{A}⟩.

The following propositions are true:

(80) The lattice of normal forms over A = ⟨the normal forms over A, ⊔_{A}, ⊓_{A}⟩.

(81) The lattice of normal forms over A is a distributive lattice.

(82) The carrier of the lattice of normal forms over A = the normal forms over A.

242 Andrzej Trybulec

(83) The join operation of the lattice of normal forms over A = ⊔_{A}.

(84) The meet operation of the lattice of normal forms over A = ⊓_{A}.

(85) ∅ is an element of the carrier of the lattice of normal forms over A.

(86) ⊥_{The lattice of normal forms over A} = ∅.

(87) The join operation of the lattice of normal forms over A has a unity.

References

[1] Czesław Byliński. Basic functions and operations on functions. Formalized Mathematics, 1(1):245–254, 1990.

[2] Czesław Byliński. Binary operations. Formalized Mathematics, 1(1):175–180, 1990.

[3] Czesław Byliński. Functions and their basic properties. Formalized Mathematics, 1(1):55–65, 1990.

[4] Czesław Byliński. Functions from a set to a set. Formalized Mathematics, 1(1):153–164, 1990.

[5] Agata Darmochwał. Finite sets. Formalized Mathematics, 1(1):165–167, 1990.

[6] Andrzej Trybulec. Domains and their Cartesian products. Formalized Mathematics, 1(1):115–122, 1990.

[7] Andrzej Trybulec. Semilattice operations on finite subsets. Formalized Mathematics, 1(2):369–376, 1990.

[8] Andrzej Trybulec. Tarski Grothendieck set theory. Formalized Mathematics, 1(1):9–11, 1990.

[9] Andrzej Trybulec. Tuples, projections and Cartesian products. Formalized Mathematics, 1(1):97–105, 1990.

[10] Andrzej Trybulec and Agata Darmochwał. Boolean domains. Formalized Mathematics, 1(1):187–190, 1990.

[11] Stanisław Żukowski. Introduction to lattice theory. Formalized Mathematics, 1(1):215– 222, 1990.

Ordered Rings - Part I

Michał Muzalewski Warsaw University Białystok Lesław W. Szczerba Siedlce University

Summary. This series of papers is devoted to the notion of the ordered ring, and one of its most important cases: the notion of ordered field. It follows the results of [5]. The idea of the notion of order in the ring is based on that of positive cone i.e. the set of positive elements. Positive cone has to contain at least squares of all elements, and has to be closed under sum and product. Therefore the key notions of this theory are that of square, sum of squares, product of squares, etc. and finally elements generated from squares by means of sums and products. Part I contains definitions of all those key notions and inclusions between them.

MML Identifier: O RING 1.

The papers [1], [2], [6], [3], and [4] provide the notation and terminology for this paper. For simplicity we adopt the following convention: i, j, k, n will be natural numbers, R will be a field structure, x, y will be scalars of R, and f will be a finite sequence of elements of the carrier of R. Let us consider R, f, k. Let us assume that 0 ≠ k and k ≤ len f. The functor f ^{∘} k yields a scalar of R and is defined by: (Def.1) f ^{∘} k = f(k).

Let us consider R, x. The functor x^{2} yields a scalar of R and is defined as follows: (Def.2) x^{2} = x · x.

Let us consider R, x. We say that x is a square if and only if: (Def.3) there exists a scalar y of R such that x = y^{2}.

Let us consider R, f. We say that f is a sequence of sums of squares if and only if: (Def.4) len f ≠ 0 and f ^{∘} 1 is a square and for every n such that n ≠ 0 and

n < len f there exists y such that y is a square and f ^{∘} (n + 1) = f ^{∘} n + y.

Let us consider R, x. We say that x is a sum of squares if and only if:

(Def.5) there exists f such that f is a sequence of sums of squares and x = f ^{∘} len f.

Let us consider R, f. We say that f is a sequence of products of squares if and only if:

(Def.6) len f ≠ 0 and f ^{∘} 1 is a square and for every n such that n ≠ 0 and n < len f there exists y such that y is a square and f ^{∘} (n + 1) = f ^{∘} n · y.

Let us consider R, x. We say that x is a product of squares if and only if:

(Def.7) there exists f such that f is a sequence of products of squares and x = f ^{∘} len f.

Let us consider R, f. We say that f is a sequence of sums of products of squares if and only if:

(Def.8) len f ≠ 0 and f ^{∘} 1 is a product of squares and for every n such that n ≠ 0 and n < len f there exists y such that y is a product of squares and f ^{∘} (n + 1) = f ^{∘} n + y.

Let us consider R, x. We say that x is a sum of products of squares if and only if:

(Def.9) there exists f such that f is a sequence of sums of products of squares and x = f ^{∘} len f.

Let us consider R, f. We say that f is a sequence of amalgams of squares if and only if:

(Def.10) (i) len f ≠ 0,

(ii) for every n such that n ≠ 0 and n ≤ len f holds f ^{∘} n is a product of squares or there exist i, j such that f ^{∘} n = f ^{∘} i · f ^{∘} j and i ≠ 0 and i < n and j ≠ 0 and j < n.

Let us consider R, x. We say that x is a amalgam of squares if and only if:

(Def.11) there exists f such that f is a sequence of amalgams of squares and x = f ^{∘} len f.

Let us consider R, f. We say that f is a sequence of sums of amalgams of squares if and only if:

(Def.12) len f ≠ 0 and f ^{∘} 1 is a amalgam of squares and for every n such that n ≠ 0 and n < len f there exists y such that y is a amalgam of squares and f ^{∘} (n + 1) = f ^{∘} n + y.

Let us consider R, x. We say that x is a sum of amalgams of squares if and only if:

(Def.13) there exists f such that f is a sequence of sums of amalgams of squares and x = f ^{∘} len f.

Let us consider R, f. We say that f is a generation from squares if and only if:

(Def.14) (i) len f ≠ 0,

(ii) for every n such that n ≠ 0 and n ≤ len f holds f ^{∘} n is a amalgam of squares or there exist i, j such that f^{∘} n = f^{∘} i · f^{∘} j or f^{∘} n = f^{∘} i + f^{∘} j but i ≠ 0 and i < n and j ≠ 0 and j < n.

Let us consider R, x. We say that x is generated from squares if and only if: (Def.15) there exists f such that f is a generation from squares and x = f^{∘} len f.

The following propositions are true:

(1) If x is a square, then x is a sum of squares and x is a product of squares and x is a sum of products of squares and x is a amalgam of squares and x is a sum of amalgams of squares and x is generated from squares.

(2) If x is a sum of squares, then x is a sum of products of squares and x is a sum of amalgams of squares and x is generated from squares.

(3) If x is a product of squares, then x is a sum of products of squares and x is a amalgam of squares and x is a sum of amalgams of squares and x is generated from squares.

(4) If x is a sum of products of squares, then x is a sum of amalgams of squares and x is generated from squares.

(5) If x is a amalgam of squares, then x is a sum of amalgams of squares and x is generated from squares.

(6) If x is a sum of amalgams of squares, then x is generated from squares.

References

[1] Grzegorz Bancerek. The fundamental properties of natural numbers. Formalized Mathematics, 1(1):41–46, 1990.

[2] Grzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite sequences. Formalized Mathematics, 1(1):107–114, 1990.

[3] Eugeniusz Kusak, Wojciech Leończuk, and Michał Muzalewski. Abelian groups, fields and vector spaces. Formalized Mathematics, 1(2):335–342, 1990.

[4] Michał Muzalewski. Construction of rings and left-, right-, and bi-modules over a ring. Formalized Mathematics, 2(1):3–11, 1991.

[5] Wanda Szmielew. From Affine to Euclidean Geometry. Volume 27, PWN – D.Reidel Publ. Co., Warszawa – Dordrecht, 1983.

[6] Andrzej Trybulec. Tarski Grothendieck set theory. Formalized Mathematics, 1(1):9–11, 1990.

246

Ordered Rings - Part II

Michał Muzalewski Warsaw University Białystok Lesław W. Szczerba Siedlce University

Summary. This series of papers is devoted to the notion of the ordered ring, and one of its most important cases: the notion of ordered field. It follows the results of [6]. The idea of the notion of order in the ring is based on that of positive cone i.e. the set of positive elements. Positive cone has to contain at least squares of all elements, and has to be closed under sum and product. Therefore the key notions of this theory are that of square, sum of squares, product of squares, etc. and finally elements generated from squares by means of sums and products. Part II contains the classification of sums of such elements.

MML Identifier: O RING 2.

The terminology and notation used here are introduced in the following articles: [1], [2], [7], [3], [4], and [5]. In the sequel R is a field structure and x, y are scalars of R. One can prove the following propositions:

(1) If x is a square and y is a square or x is a sum of squares and y is a square, then x + y is a sum of squares.

(2) If x is a sum of products of squares and y is a square or x is a sum of products of squares and y is a product of squares, then x + y is a sum of products of squares.

(3) If x is a amalgam of squares and y is a product of squares or x is a amalgam of squares and y is a amalgam of squares or x is a sum of amalgams of squares and y is a square or x is a sum of amalgams of squares and y is a product of squares or x is a sum of amalgams of squares and y is a amalgam of squares, then x + y is a sum of amalgams of squares.

(4) If x is a square and y is a sum of squares or x is a square and y is a product of squares or x is a square and y is a sum of products of squares or x is a square and y is a amalgam of squares or x is a square and y is a sum of amalgams of squares or x is a square and y is generated from squares, then x + y is generated from squares.

(5) If x is a sum of squares and y is a sum of squares or x is a sum of squares and y is a product of squares or x is a sum of squares and y is a sum of products of squares or x is a sum of squares and y is a amalgam of squares or x is a sum of squares and y is a sum of amalgams of squares or x is a sum of squares and y is generated from squares, then x + y is generated from squares.

(6) If x is a product of squares and y is a square or x is a product of squares and y is a sum of squares or x is a product of squares and y is a product of squares or x is a product of squares and y is a sum of products of squares or x is a product of squares and y is a amalgam of squares or x is a product of squares and y is a sum of amalgams of squares or x is a product of squares and y is generated from squares, then x + y is generated from squares.

(7) If x is a sum of products of squares and y is a sum of squares or x is a sum of products of squares and y is a sum of products of squares or x is a sum of products of squares and y is a amalgam of squares or x is a sum of products of squares and y is a sum of amalgams of squares or x is a sum of products of squares and y is generated from squares, then x + y is generated from squares.

(8) If x is a amalgam of squares and y is a square or x is a amalgam of squares and y is a sum of squares or x is a amalgam of squares and y is a sum of products of squares or x is a amalgam of squares and y is a sum of amalgams of squares or x is a amalgam of squares and y is generated from squares, then x + y is generated from squares.

(9) If x is a sum of amalgams of squares and y is a sum of squares or x is a sum of amalgams of squares and y is a sum of products of squares or x is a sum of amalgams of squares and y is a sum of amalgams of squares or x is a sum of amalgams of squares and y is generated from squares, then x + y is generated from squares.

(10) If x is generated from squares and y is a square or x is generated from squares and y is a sum of squares or x is generated from squares and y is a product of squares or x is generated from squares and y is a sum of products of squares or x is generated from squares and y is a amalgam of squares or x is generated from squares and y is a sum of amalgams of squares or x is generated from squares and y is generated from squares, then x + y is generated from squares.

References

[1] Grzegorz Bancerek. The fundamental properties of natural numbers. Formalized Mathematics, 1(1):41–46, 1990.

[2] Grzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite sequences. Formalized Mathematics, 1(1):107–114, 1990.

[3] Eugeniusz Kusak, Wojciech Leończuk, and Michał Muzalewski. Abelian groups, fields and vector spaces. Formalized Mathematics, 1(2):335–342, 1990.

Ordered Rings - Part II 249

[4] Michał Muzalewski. Construction of rings and left-, right-, and bi-modules over a ring. Formalized Mathematics, 2(1):3–11, 1991.

[5] Michał Muzalewski and Lesław W. Szczerba. Ordered rings - part I. Formalized Mathematics, 2(2):243–245, 1991.

[6] Wanda Szmielew. From Affine to Euclidean Geometry. Volume 27, PWN – D.Reidel Publ. Co., Warszawa – Dordrecht, 1983.

[7] Andrzej Trybulec. Tarski Grothendieck set theory. Formalized Mathematics, 1(1):9–11, 1990.

250

Ordered Rings - Part III

Michał Muzalewski Warsaw University Białystok Lesław W. Szczerba Siedlce University

Summary. This series of papers is devoted to the notion of the ordered ring, and one of its most important cases: the notion of ordered field. It follows the results of [6]. The idea of the notion of order in the ring is based on that of positive cone i.e. the set of positive elements. Positive cone has to contain at least squares of all elements, and has to be closed under sum and product. Therefore the key notions of this theory are that of square, sum of squares, product of squares, etc. and finally elements generated from squares by means of sums and products. Part III contains the classification of products of such elements.

MML Identifier: O RING 3.

The papers [1], [2], [7], [3], [4], and [5] provide the terminology and notation for this paper. In the sequel R will denote a field structure and x, y will denote scalars of R. Next we state a number of propositions:

(1) If x is a square and y is a square, then x · y is a product of squares.

(2) If x is a product of squares and y is a square, then x · y is a product of squares.

(3) If x is a square and y is a product of squares or x is a square and y is a amalgam of squares, then x · y is a amalgam of squares.

(4) If x is a product of squares and y is a product of squares or x is a product of squares and y is a amalgam of squares, then x · y is a amalgam of squares.

(5) If x is a amalgam of squares and y is a square or x is a amalgam of squares and y is a product of squares or x is a amalgam of squares and y is a amalgam of squares, then x · y is a amalgam of squares.

(6) If x is a square and y is a sum of squares or x is a square and y is a sum of products of squares or x is a square and y is a sum of amalgams of squares or x is a square and y is generated from squares, then x · y is generated from squares.

(7) If x is a sum of squares and y is a square or x is a sum of squares and y is a sum of squares or x is a sum of squares and y is a product of squares or x is a sum of squares and y is a sum of products of squares or x is a sum of squares and y is a amalgam of squares or x is a sum of squares and y is a sum of amalgams of squares or x is a sum of squares and y is generated from squares, then x · y is generated from squares.

(8) If x is a product of squares and y is a sum of squares or x is a product of squares and y is a sum of products of squares or x is a product of squares and y is a sum of amalgams of squares or x is a product of squares and y is generated from squares, then x · y is generated from squares.

(9) If x is a sum of products of squares and y is a square or x is a sum of products of squares and y is a sum of squares or x is a sum of products of squares and y is a product of squares or x is a sum of products of squares and y is a sum of products of squares or x is a sum of products of squares and y is a amalgam of squares or x is a sum of products of squares and y is a sum of amalgams of squares or x is a sum of products of squares and y is generated from squares, then x · y is generated from squares.

(10) If x is a amalgam of squares and y is a sum of squares or x is a amalgam of squares and y is a sum of products of squares or x is a amalgam of squares and y is a sum of amalgams of squares or x is a amalgam of squares and y is generated from squares, then x · y is generated from squares.

(11) If x is a sum of amalgams of squares and y is a square or x is a sum of amalgams of squares and y is a sum of squares or x is a sum of amalgams of squares and y is a product of squares or x is a sum of amalgams of squares and y is a sum of products of squares or x is a sum of amalgams of squares and y is a amalgam of squares or x is a sum of amalgams of squares and y is a sum of amalgams of squares or x is a sum of amalgams of squares and y is generated from squares, then x · y is generated from squares.

(12) If x is generated from squares and y is a square or x is generated from squares and y is a sum of squares or x is generated from squares and y is a product of squares or x is generated from squares and y is a sum of products of squares or x is generated from squares and y is a amalgam of squares or x is generated from squares and y is a sum of amalgams of squares or x is generated from squares and y is generated from squares, then x · y is generated from squares.

References

[1] Grzegorz Bancerek. The fundamental properties of natural numbers. Formalized Mathematics, 1(1):41–46, 1990.

[2] Grzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite sequences. Formalized Mathematics, 1(1):107–114, 1990.

Ordered Rings - Part III 253

[3] Eugeniusz Kusak, Wojciech Leończuk, and Michał Muzalewski. Abelian groups, fields and vector spaces. Formalized Mathematics, 1(2):335–342, 1990.

[4] Michał Muzalewski. Construction of rings and left-, right-, and bi-modules over a ring. Formalized Mathematics, 2(1):3–11, 1991.

[5] Michał Muzalewski and Lesław W. Szczerba. Ordered rings - part I. Formalized Mathematics, 2(2):243–245, 1991.

[6] Wanda Szmielew. From Affine to Euclidean Geometry. Volume 27, PWN – D.Reidel Publ. Co., Warszawa – Dordrecht, 1983.

[7] Andrzej Trybulec. Tarski Grothendieck set theory. Formalized Mathematics, 1(1):9–11, 1990.

254

N-Tuples and Cartesian Products for n=5 ^{1}

Michał Muzalewski Warsaw University Białystok

Wojciech Skaba University of Toruń

Summary. This article defines ordered n-tuples, projections and Cartesian products for n=5. We prove many theorems concerning the basic properties of the n-tuples and Cartesian products that may be utilized in several further, more challenging applications. A few of these theorems are a strightforward consequence of the regularity axiom. The article originated as an upgrade of the article [5].

MML Identifier: MCART 2.

The notation and terminology used in this paper are introduced in the following articles: [4], [3], [6], [2], [1], and [5]. For simplicity we follow a convention: v will be arbitrary, x_{1}, x_{2}, x_{3}, x_{4}, x_{5} will be arbitrary, y_{1}, y_{2}, y_{3}, y_{4}, y_{5} will be arbitrary, z will be arbitrary, X, X_{1}, X_{2}, X_{3}, X_{4}, X_{5} will denote sets, Y, Y_{1}, Y_{2}, Y_{3}, Y_{4}, Y_{5}, Y_{6}, Y_{7} will denote sets, Z will denote a set, x_{6} will denote an element of X_{1}, x_{7} will denote an element of X_{2}, x_{8} will denote an element of X_{3}, and x_{9} will denote an element of X_{4}. We now state two propositions:

(1) If X ≠ ∅, then there exists Y such that Y ∈ X and for all Y_{1}, Y_{2}, Y_{3}, Y_{4}, Y_{5}, Y_{6} such that Y_{1} ∈ Y_{2} and Y_{2} ∈ Y_{3} and Y_{3} ∈ Y_{4} and Y_{4} ∈ Y_{5} and Y_{5} ∈ Y_{6} and Y_{6} ∈ Y holds Y_{1} misses X.

(2) If X ≠ ∅, then there exists Y such that Y ∈ X and for all Y_{1}, Y_{2}, Y_{3}, Y_{4}, Y_{5}, Y_{6}, Y_{7} such that Y_{1} ∈ Y_{2} and Y_{2} ∈ Y_{3} and Y_{3} ∈ Y_{4} and Y_{4} ∈ Y_{5} and Y_{5} ∈ Y_{6} and Y_{6} ∈ Y_{7} and Y_{7} ∈ Y holds Y_{1} misses X.

Let us consider x_{1}, x_{2}, x_{3}, x_{4}, x_{5}. The functor ⟨⟨x_{1}, x_{2}, x_{3}, x_{4}, x_{5}⟩⟩ is defined as follows: (Def.1) ⟨⟨x_{1}, x_{2}, x_{3}, x_{4}, x_{5}⟩⟩ = ⟨⟨⟨⟨x_{1}, x_{2}, x_{3}, x_{4}⟩⟩, x_{5}⟩⟩.

One can prove the following propositions:

(3) ⟨⟨x_{1}, x_{2}, x_{3}, x_{4}, x_{5}⟩⟩ = ⟨⟨⟨⟨⟨⟨⟨⟨x_{1}, x_{2}⟩⟩, x_{3}⟩⟩, x_{4}⟩⟩, x_{5}⟩⟩.

(4) ⟨⟨x_{1}, x_{2}, x_{3}, x_{4}, x_{5}⟩⟩ = ⟨⟨⟨⟨x_{1}, x_{2}, x_{3}, x_{4}⟩⟩, x_{5}⟩⟩.

1Supported by RPBP.III-24.C6

(5) ⟨⟨x_{1}, x_{2}, x_{3}, x_{4}, x_{5}⟩⟩ = ⟨⟨⟨⟨x_{1}, x_{2}, x_{3}⟩⟩, x_{4}, x_{5}⟩⟩.

(6) ⟨⟨x_{1}, x_{2}, x_{3}, x_{4}, x_{5}⟩⟩ = ⟨⟨⟨⟨x_{1}, x_{2}⟩⟩, x_{3}, x_{4}, x_{5}⟩⟩.

(7) If ⟨⟨x_{1}, x_{2}, x_{3}, x_{4}, x_{5}⟩⟩ = ⟨⟨y_{1}, y_{2}, y_{3}, y_{4}, y_{5}⟩⟩, then x_{1} = y_{1} and x_{2} = y_{2} and x_{3} = y_{3} and x_{4} = y_{4} and x_{5} = y_{5}.

(8) If X ≠ ∅, then there exists v such that v ∈ X and for no x_{1}, x_{2}, x_{3}, x_{4}, x_{5} holds x_{1} ∈ X or x_{2} ∈ X but v = ⟨⟨x_{1}, x_{2}, x_{3}, x_{4}, x_{5}⟩⟩.

Let us consider X_{1}, X_{2}, X_{3}, X_{4}, X_{5}. The functor [: X_{1}, X_{2}, X_{3}, X_{4}, X_{5} :] yields a set and is defined as follows: (Def.2) [: X_{1}, X_{2}, X_{3}, X_{4}, X_{5} :] = [: [: X_{1}, X_{2}, X_{3}, X_{4} :], X_{5} :].

The following propositions are true:

(9) [: X_{1}, X_{2}, X_{3}, X_{4}, X_{5} :] = [: [: [: [: X_{1}, X_{2} :], X_{3} :], X_{4} :], X_{5} :].

(10) [: X_{1}, X_{2}, X_{3}, X_{4}, X_{5} :] = [: [: X_{1}, X_{2}, X_{3}, X_{4} :], X_{5} :].

(11) [: X_{1}, X_{2}, X_{3}, X_{4}, X_{5} :] = [: [: X_{1}, X_{2}, X_{3} :], X_{4}, X_{5} :].

(12) [: X_{1}, X_{2}, X_{3}, X_{4}, X_{5} :] = [: [: X_{1}, X_{2} :], X_{3}, X_{4}, X_{5} :].

(13) X_{1} ≠ ∅ and X_{2} ≠ ∅ and X_{3} ≠ ∅ and X_{4} ≠ ∅ and X_{5} ≠ ∅ if and only if [: X_{1}, X_{2}, X_{3}, X_{4}, X_{5} :] ≠ ∅.

(14) Suppose X_{1} ≠ ∅ and X_{2} ≠ ∅ and X_{3} ≠ ∅ and X_{4} ≠ ∅ and X_{5} ≠ ∅. Then if [: X_{1}, X_{2}, X_{3}, X_{4}, X_{5} :] = [: Y_{1}, Y_{2}, Y_{3}, Y_{4}, Y_{5} :], then X_{1} = Y_{1} and X_{2} = Y_{2} and X_{3} = Y_{3} and X_{4} = Y_{4} and X_{5} = Y_{5}.

(15) If [: X_{1}, X_{2}, X_{3}, X_{4}, X_{5} :] ≠ ∅ and [: X_{1}, X_{2}, X_{3}, X_{4}, X_{5} :] = [: Y_{1}, Y_{2}, Y_{3}, Y_{4}, Y_{5} :], then X_{1} = Y_{1} and X_{2} = Y_{2} and X_{3} = Y_{3} and X_{4} = Y_{4} and X_{5} = Y_{5}.

(16) If [: X, X, X, X, X:] = [: Y, Y, Y, Y, Y :], then X = Y.

In the sequel x_{10} will be an element of X_{5}. We now state the proposition (17) If X_{1} ≠ ∅ and X_{2} ≠ ∅ and X_{3} ≠ ∅ and X_{4} ≠ ∅ and X_{5} ≠ ∅, then for

every element x of [: X_{1}, X_{2}, X_{3}, X_{4}, X_{5} :] there exist x_{6}, x_{7}, x_{8}, x_{9}, x_{10} such that x = ⟨⟨x_{6}, x_{7}, x_{8}, x_{9}, x_{10}⟩⟩.

We now define five new functors. Let us consider X_{1}, X_{2}, X_{3}, X_{4}, X_{5}. Let us assume that X_{1} ≠ ∅ and X_{2} ≠ ∅ and X_{3} ≠ ∅ and X_{4} ≠ ∅ and X_{5} ≠ ∅. Let x be an element of [: X_{1}, X_{2}, X_{3}, X_{4}, X_{5} :]. The functor x_{1} yields an element of X_{1} and is defined as follows: (Def.3) if x = ⟨⟨x_{1}, x_{2}, x_{3}, x_{4}, x_{5}⟩⟩, then x_{1} = x_{1}. The functor x_{2} yields an element of X_{2} and is defined as follows: (Def.4) if x = ⟨⟨x_{1}, x_{2}, x_{3}, x_{4}, x_{5}⟩⟩, then x_{2} = x_{2}. The functor x_{3} yielding an element of X_{3} is defined as follows: (Def.5) if x = ⟨⟨x_{1}, x_{2}, x_{3}, x_{4}, x_{5}⟩⟩, then x_{3} = x_{3}. The functor x_{4} yielding an element of X_{4} is defined as follows: (Def.6) if x = ⟨⟨x_{1}, x_{2}, x_{3}, x_{4}, x_{5}⟩⟩, then x_{4} = x_{4}. The functor x_{5} yields an element of X_{5} and is defined by: (Def.7) if x = ⟨⟨x_{1}, x_{2}, x_{3}, x_{4}, x_{5}⟩⟩, then x_{5} = x_{5}.

One can prove the following propositions:

(18) Suppose X_{1} ≠ ∅ and X_{2} ≠ ∅ and X_{3} ≠ ∅ and X_{4} ≠ ∅ and X_{5} ≠ ∅. Then for every element x of [: X_{1}, X_{2}, X_{3}, X_{4}, X_{5} :] and for all x_{1}, x_{2}, x_{3}, x_{4}, x_{5} such that x = ⟨⟨x_{1}, x_{2}, x_{3}, x_{4}, x_{5}⟩⟩ holds x_{1} = x_{1} and x_{2} = x_{2} and x_{3} = x_{3} and x_{4} = x_{4} and x_{5} = x_{5}.

(19) If X_{1} ≠ ∅ and X_{2} ≠ ∅ and X_{3} ≠ ∅ and X_{4} ≠ ∅ and X_{5} ≠ ∅, then for every element x of [: X_{1}, X_{2}, X_{3}, X_{4}, X_{5} :] holds x = ⟨⟨x_{1}, x_{2}, x_{3}, x_{4}, x_{5}⟩⟩.

(20) Suppose X_{1} ≠ ∅ and X_{2} ≠ ∅ and X_{3} ≠ ∅ and X_{4} ≠ ∅ and X_{5} ≠ ∅. Let x be an element of [: X_{1}, X_{2}, X_{3}, X_{4}, X_{5} :]. Then x_{1} = x qua any_{1}_{1}_{1}_{1} and x_{2} = x qua any_{1}_{1}_{1}_{2} and x_{3} = x qua any_{1}_{1}_{2} and x_{4} = x qua any_{1}_{2} and x_{5} = x qua any_{2}.

(21) If X_{1} ⊆ [: X_{1}, X_{2}, X_{3}, X_{4}, X_{5} :] or X_{1} ⊆ [: X_{2}, X_{3}, X_{4}, X_{5}, X_{1} :] or X_{1} ⊆ [: X_{3}, X_{4}, X_{5}, X_{1}, X_{2} :] or X_{1} ⊆ [: X_{4}, X_{5}, X_{1}, X_{2}, X_{3} :] or X_{1} ⊆ [: X_{5}, X_{1}, X_{2}, X_{3}, X_{4} :], then X_{1} = ∅.

(22) If [: X_{1}, X_{2}, X_{3}, X_{4}, X_{5} :] meets [: Y_{1}, Y_{2}, Y_{3}, Y_{4}, Y_{5} :], then X_{1} meets Y_{1} and X_{2} meets Y_{2} and X_{3} meets Y_{3} and X_{4} meets Y_{4} and X_{5} meets Y_{5}.

(23) [: {x_{1}}, {x_{2}}, {x_{3}}, {x_{4}}, {x_{5}}:] = {⟨⟨x_{1}, x_{2}, x_{3}, x_{4}, x_{5}⟩⟩}.

For simplicity we adopt the following rules: A_{1} is a subset of X_{1}, A_{2} is a subset of X_{2}, A_{3} is a subset of X_{3}, A_{4} is a subset of X_{4}, A_{5} is a subset of X_{5}, and x is an element of [: X_{1}, X_{2}, X_{3}, X_{4}, X_{5} :]. One can prove the following propositions:

(24) Suppose X_{1} ≠ ∅ and X_{2} ≠ ∅ and X_{3} ≠ ∅ and X_{4} ≠ ∅ and X_{5} ≠ ∅. Then for all x_{1}, x_{2}, x_{3}, x_{4}, x_{5} such that x = ⟨⟨x_{1}, x_{2}, x_{3}, x_{4}, x_{5}⟩⟩ holds x_{1} = x_{1} and x_{2} = x_{2} and x_{3} = x_{3} and x_{4} = x_{4} and x_{5} = x_{5}.

(25) If X_{1} ≠ ∅ and X_{2} ≠ ∅ and X_{3} ≠ ∅ and X_{4} ≠ ∅ and X_{5} ≠ ∅ and for all x_{6}, x_{7}, x_{8}, x_{9}, x_{10} such that x = ⟨⟨x_{6}, x_{7}, x_{8}, x_{9}, x_{10}⟩⟩ holds y_{1} = x_{6}, then y_{1} = x_{1}.

(26) If X_{1} ≠ ∅ and X_{2} ≠ ∅ and X_{3} ≠ ∅ and X_{4} ≠ ∅ and X_{5} ≠ ∅ and for all x_{6}, x_{7}, x_{8}, x_{9}, x_{10} such that x = ⟨⟨x_{6}, x_{7}, x_{8}, x_{9}, x_{10}⟩⟩ holds y_{2} = x_{7}, then y_{2} = x_{2}.

(27) If X_{1} ≠ ∅ and X_{2} ≠ ∅ and X_{3} ≠ ∅ and X_{4} ≠ ∅ and X_{5} ≠ ∅ and for all x_{6}, x_{7}, x_{8}, x_{9}, x_{10} such that x = ⟨⟨x_{6}, x_{7}, x_{8}, x_{9}, x_{10}⟩⟩ holds y_{3} = x_{8}, then y_{3} = x_{3}.

(28) If X_{1} ≠ ∅ and X_{2} ≠ ∅ and X_{3} ≠ ∅ and X_{4} ≠ ∅ and X_{5} ≠ ∅ and for all x_{6}, x_{7}, x_{8}, x_{9}, x_{10} such that x = ⟨⟨x_{6}, x_{7}, x_{8}, x_{9}, x_{10}⟩⟩ holds y_{4} = x_{9}, then y_{4} = x_{4}.

(29) If X_{1} ≠ ∅ and X_{2} ≠ ∅ and X_{3} ≠ ∅ and X_{4} ≠ ∅ and X_{5} ≠ ∅ and for all x_{6}, x_{7}, x_{8}, x_{9}, x_{10} such that x = ⟨⟨x_{6}, x_{7}, x_{8}, x_{9}, x_{10}⟩⟩ holds y_{5} = x_{10}, then y_{5} = x_{5}.

(30) If z ∈ [: X_{1}, X_{2}, X_{3}, X_{4}, X_{5} :], then there exist x_{1}, x_{2}, x_{3}, x_{4}, x_{5} such that x_{1} ∈ X_{1} and x_{2} ∈ X_{2} and x_{3} ∈ X_{3} and x_{4} ∈ X_{4} and x_{5} ∈ X_{5} and z = ⟨⟨x_{1}, x_{2}, x_{3}, x_{4}, x_{5}⟩⟩.

(31) ⟨⟨x_{1}, x_{2}, x_{3}, x_{4}, x_{5}⟩⟩ ∈ [: X_{1}, X_{2}, X_{3}, X_{4}, X_{5} :] if and only if x_{1} ∈ X_{1} and x_{2} ∈ X_{2} and x_{3} ∈ X_{3} and x_{4} ∈ X_{4} and x_{5} ∈ X_{5}.

(32) If for every z holds z ∈ Z if and only if there exist x_{1}, x_{2}, x_{3}, x_{4}, x_{5} such that x_{1} ∈ X_{1} and x_{2} ∈ X_{2} and x_{3} ∈ X_{3} and x_{4} ∈ X_{4} and x_{5} ∈ X_{5} and z = ⟨⟨x_{1}, x_{2}, x_{3}, x_{4}, x_{5}⟩⟩, then Z = [: X_{1}, X_{2}, X_{3}, X_{4}, X_{5} :].

(33) Suppose X_{1} ≠ ∅ and X_{2} ≠ ∅ and X_{3} ≠ ∅ and X_{4} ≠ ∅ and X_{5} ≠ ∅ and Y_{1} ≠ ∅ and Y_{2} ≠ ∅ and Y_{3} ≠ ∅ and Y_{4} ≠ ∅ and Y_{5} ≠ ∅. Let x be an element of [: X_{1}, X_{2}, X_{3}, X_{4}, X_{5} :]. Then for every element y of [: Y_{1}, Y_{2}, Y_{3}, Y_{4}, Y_{5} :] such that x = y holds x_{1} = y_{1} and x_{2} = y_{2} and x_{3} = y_{3} and x_{4} = y_{4} and x_{5} = y_{5}.

(34) For every element x of [: X_{1}, X_{2}, X_{3}, X_{4}, X_{5} :] such that x ∈ [: A_{1}, A_{2}, A_{3}, A_{4}, A_{5} :] holds x_{1} ∈ A_{1} and x_{2} ∈ A_{2} and x_{3} ∈ A_{3} and x_{4} ∈ A_{4} and x_{5} ∈ A_{5}.

(35) If X_{1} ⊆ Y_{1} and X_{2} ⊆ Y_{2} and X_{3} ⊆ Y_{3} and X_{4} ⊆ Y_{4} and X_{5} ⊆ Y_{5}, then

[: X_{1}, X_{2}, X_{3}, X_{4}, X_{5} :] ⊆ [: Y_{1}, Y_{2}, Y_{3}, Y_{4}, Y_{5} :]. Let us consider X_{1}, X_{2}, X_{3}, X_{4}, X_{5}, A_{1}, A_{2}, A_{3}, A_{4}, A_{5}. Then [: A_{1}, A_{2}, A_{3},

A_{4}, A_{5} :] is a subset of [: X_{1}, X_{2}, X_{3}, X_{4}, X_{5} :].

The following three propositions are true:

(36) If X_{1} ≠ ∅ and X_{2} ≠ ∅, then for every element x_{11} of [: X_{1}, X_{2} :] there exists an element x_{6} of X_{1} and there exists an element x_{7} of X_{2} such that x_{11} = ⟨⟨x_{6}, x_{7}⟩⟩.

(37) If X_{1} ≠ ∅ and X_{2} ≠ ∅ and X_{3} ≠ ∅, then for every element x_{11} of [: X_{1}, X_{2}, X_{3} :] there exist x_{6}, x_{7}, x_{8} such that x_{11} = ⟨⟨x_{6}, x_{7}, x_{8}⟩⟩.

(38) If X_{1} ≠ ∅ and X_{2} ≠ ∅ and X_{3} ≠ ∅ and X_{4} ≠ ∅, then for every element x_{11} of [: X_{1}, X_{2}, X_{3}, X_{4} :] there exist x_{6}, x_{7}, x_{8}, x_{9} such that x_{11} = ⟨⟨x_{6}, x_{7}, x_{8}, x_{9}⟩⟩.

References

[1] Grzegorz Bancerek. The ordinal numbers. Formalized Mathematics, 1(1):91–96, 1990.

[2] Czesław Byliński. Functions and their basic properties. Formalized Mathematics, 1(1):55– 65, 1990.

[3] Andrzej Trybulec. Enumerated sets. Formalized Mathematics, 1(1):25–34, 1990.

[4] Andrzej Trybulec. Tarski Grothendieck set theory. Formalized Mathematics, 1(1):9–11, 1990.

[5] Andrzej Trybulec. Tuples, projections and Cartesian products. Formalized Mathematics, 1(1):97–105, 1990.

[6] Zinaida Trybulec. Properties of subsets. Formalized Mathematics, 1(1):67–71, 1990.

Ternary Fields ^{1}

Michał Muzalewski Warsaw University Białystok

Wojciech Skaba University of Toruń

Summary. The article contains part 3 of the set of papers concerning the theory of algebraic structures, based on the book [11] pp. 13-15 (pages 6-8 for English edition).

First the basic structure (F, 0, 1, T) is defined, where T is a ternary operation on F (three-argument operations have been introduced in the article [9]). Following it, the basic axioms of a Ternary Field are displayed, the mode is defined and its existence proved. The basic properties of a Ternary Field are also contemplated there.

MML Identifier: ALGSTR 3.

The articles [13], [12], [3], [4], [1], [2], [6], [5], [7], [8], [10], and [9] provide the notation and terminology for this paper. We consider ternary field structures which are systems

⟨a carrier, a zero, a unity, a operation⟩, where the carrier is a non-empty set, the zero is an element of the carrier, the unity is an element of the carrier, and the operation is a ternary operation on the carrier.

In the sequel F denotes a ternary field structure. Let us consider F. A scalar of F is an element of the carrier of F.

In the sequel a, b, c are scalars of F. Let us consider F, a, b, c. The functor T(a, b, c) yields a scalar of F and is defined by: (Def.1) T(a, b, c) = (the operation of F)(a, b, c).

Let us consider F. The functor 0_{F} yielding a scalar of F is defined as follows: (Def.2) 0_{F} = the zero of F.

Let us consider F. The functor 1_{F} yields a scalar of F and is defined by: (Def.3) 1_{F} = the unity of F.

The ternary operation T_{}on is defined as follows:

1Supported by RPBP.III-24.C6

(Def.4) for all real numbers a, b, c holds T_{}(a, b, c) = a · b + c.

The ternary field structure _{t} is defined by: (Def.5) _{t} = ⟨ , 0, 1, T_{}⟩.

Let a, b, c be scalars of _{t} . The functor T^{e}(a, b, c) yields a scalar of _{t} and is defined by: (Def.6) T^{e}(a, b, c) = (the operation of _{t} )(a, b, c).

We now state several propositions:

(1) For every scalar a of _{t} holds a is a real number.

(2) For every real number a holds a is a scalar of _{t} .

(3) For all real numbers u, u′, v, v′ such that u ≠ u′ there exists a real number x such that u · x + v = u′ · x + v′.

(5)^{2} For all scalars u, a, v of _{t} and for all real numbers z, x, y such that

u = z and a = x and v = y holds T(u, a, v) = z · x + y.

(6) 0 = 0_{_{t}} .

(7) 1 = 1_{_{t}} . A ternary field structure is called a ternary field if:

(Def.7) (i) 0_{it} ≠ 1_{it}, (ii) for every scalar a of it holds T(a, 1_{it}, 0_{it}) = a, (iii) for every scalar a of it holds T(1_{it}, a, 0_{it}) = a, (iv) for all scalars a, b of it holds T(a, 0_{it}, b) = b,

(v) for all scalars a, b of it holds T(0_{it}, a, b) = b, (vi) for every scalars u, a, b of it there exists a scalar v of it such that

T(u, a, v) = b, (vii) for all scalars u, a, v, v′ of it such that T(u, a, v) = T(u, a, v′) holds

v = v′, (viii) for all scalars a, a′ of it such that a ≠ a′ for every scalars b, b′ of it

there exist scalars u, v of it such that T(u, a, v) = b and T(u, a′, v) = b′, (ix) for all scalars u, u′ of it such that u ≠ u′ for every scalars v, v′ of it

there exists a scalar a of it such that T(u, a, v) = T(u′, a, v′),

(x) for all scalars a, a′, u, u′, v, v′ of it such that T(u, a, v) = T(u′, a, v′) and T(u, a′, v) = T(u′, a′, v′) holds a = a′ or u = u′.

We adopt the following convention: F is a ternary field and a, a′, b, c, x, x′, u, u′, v, v′ are scalars of F. We now state several propositions:

(8) If a ≠ a′ and T(u, a, v) = T(u′, a, v′) and T(u, a′, v) = T(u′, a′, v′), then u = u′ and v = v′.

(9) For every a, b, c there exists x such that T(a, b, x) = c.

(10) If T(a, b, x) = T(a, b, x′), then x = x′.

(11) If a ≠ 0_{F}, then for every b, c there exists x such that T(a, x, b) = c.

(12) If a ≠ 0_{F} and T(a, x, b) = T(a, x′, b), then x = x′.

(13) If a ≠ 0_{F}, then for every b, c there exists x such that T(x, a, b) = c.

2The proposition (4) was either repeated or obvious.

Ternary Fields 261

(14) If a ≠ 0_{F} and T(x, a, b) = T(x′, a, b), then x = x′.

References

[1] Czesław Byliński. Basic functions and operations on functions. Formalized Mathematics, 1(1):245–254, 1990.

[2] Czesław Byliński. Binary operations. Formalized Mathematics, 1(1):175–180, 1990.

[3] Czesław Byliński. Functions and their basic properties. Formalized Mathematics, 1(1):55–65, 1990.

[4] Czesław Byliński. Functions from a set to a set. Formalized Mathematics, 1(1):153–164, 1990.

[5] Krzysztof Hryniewiecki. Basic properties of real numbers. Formalized Mathematics, 1(1):35–40, 1990.

[6] Eugeniusz Kusak, Wojciech Leończuk, and Michał Muzalewski. Abelian groups, fields and vector spaces. Formalized Mathematics, 1(2):335–342, 1990.

[7] Michał Muzalewski. Midpoint algebras. Formalized Mathematics, 1(3):483–488, 1990.

[8] Michał Muzalewski and Wojciech Skaba. From loops to abelian multiplicative groups with zero. Formalized Mathematics, 1(5):833–840, 1990.

[9] Michal Muzalewski and Wojciech Skaba. Three-argument operations and four-argument operations. Formalized Mathematics, 2(2):221–224, 1991.

[10] Wojciech Skaba and Michał Muzalewski. From double loops to fields. Formalized Mathematics, 2(1):185–191, 1991.

[11] Wanda Szmielew. From Affine to Euclidean Geometry. Volume 27, PWN – D.Reidel Publ. Co., Warszawa – Dordrecht, 1983.

[12] Andrzej Trybulec. Enumerated sets. Formalized Mathematics, 1(1):25–34, 1990.

[13] Andrzej Trybulec. Tarski Grothendieck set theory. Formalized Mathematics, 1(1):9–11, 1990.

262

The σ-additive Measure Theory

Józef Białas University of Łódź

Summary. The article contains a definition and basic properties of a σ-additive, nonnegative measure, with values in \overline{}, the enlarged set of real numbers, where \overline{}denotes set \overline{}= ∪ \{−∞, +∞\} - by [11]. We present definitions of σ-field of sets, σ-additive measure, measurable sets, measure zero sets and the basic theorems describing relationships between the notions mentioned above. The work is the third part of the series of articles concerning the Lebesgue measure theory.

MML Identifier: MEASURE1.

The papers [13], [12], [7], [8], [5], [6], [1], [10], [2], [9], [3], and [4] provide the terminology and notation for this paper. One can prove the following four propositions:

(1) For all sets X, Y holds ⋃{X, Y, ∅} = ⋃{X, Y }.

(2) For every natural number n holds n = 0 or n = 1 or 1 < n. (4)^{1} For all Real numbers x, y, s, t such that 0\overline{}≤ x and 0\overline{}≤ s and x ≤ y

and s ≤ t holds x + s ≤ y + t.

(5) For all Real numbers x, y, z such that 0\overline{}≤ y and 0\overline{}≤ z and x = y + z and y < +∞ holds z = x − y.

Let X be a set. A set is called a non-empty family of subsets of X if: (Def.1) it ≠ ∅ and for an arbitrary A such that A ∈ it holds A ∈ 2^{X}.

One can prove the following propositions:

(6) For every set X and for every subset A of X holds {A} is a non-empty family of subsets of X.

(7) For every set X and for all subsets A, B of X holds {A, B} is a nonempty family of subsets of X.

(8) For every set X and for all subsets A, B, C of X holds {A, B, C} is a non-empty family of subsets of X.

1The proposition (3) was either repeated or obvious.

(9) For every set X holds {∅} is a non-empty family of subsets of X.

(10) For every set X holds {∅, X} is a non-empty family of subsets of X. (12)^{2} For every set X holds 2^{X} is a non-empty family of subsets of X.

The scheme DomsetFamEx concerns a set A, and a unary predicate P, and states that:

there exists a non-empty family F of subsets of A such that for every set B holds B ∈ F if and only if B ⊆ A and P[B] provided the following condition is satisfied:

• there exists a set B such that B ⊆ A and P[B]. Let X be a set, and let S be a non-empty family of subsets of X. The functor

X \ S yielding a non-empty family of subsets of X is defined as follows: (Def.2) for every set A holds A ∈ X \ S if and only if there exists a set B such

that B ∈ S and A = X \ B.

We now state three propositions:

(13) For every set X and for every non-empty family S of subsets of X and for every set A holds A ∈ X \ S if and only if there exists a set B such that B ∈ S and A = X \ B.

(14) For every set X and for every non-empty family S of subsets of X holds S = X \ (X \ S).

(15) For every set X and for every non-empty family S of subsets of X holds

⋂ S = X \ ⋃(X \ S) and ⋃ S = X \ ⋂(X \ S). Let X be a set. A non-empty family of subsets of X is said to be a field of

subsets of X if: (Def.3) for every set A such that A ∈ it holds X \ A ∈ it and for all sets A, B

such that A ∈ it and B ∈ it holds A ∪ B ∈ it.

The following propositions are true: (17)^{3} For every set X and for every field S of subsets of X holds S = X \ S.

(18) For every set X and for an arbitrary M holds M is a field of subsets of X if and only if there exists a non-empty family S of subsets of X such that M = S and for every set A such that A ∈ S holds X \ A ∈ S and for all sets A, B such that A ∈ S and B ∈ S holds A ∪ B ∈ S.

(19) For every set X and for every non-empty family S of subsets of X holds S is a field of subsets of X if and only if for every set A such that A ∈ S holds X \ A ∈ S and for all sets A, B such that A ∈ S and B ∈ S holds A ∩ B ∈ S.

(20) For every set X and for every field S of subsets of X and for all sets A, B such that A ∈ S and B ∈ S holds A \ B ∈ S.

(21) For every set X and for every field S of subsets of X holds ∅ ∈ S and X ∈ S.

2The proposition (11) was either repeated or obvious.

3The proposition (16) was either repeated or obvious.

The σ-additive Measure Theory 265

Let X be a set, and let S be a non-empty family of subsets of X, and let F be a function from S into \overline{}, and let A be an element of S. Then F (A) is a Real number.

Let F be a function from into \overline{}, and let n be a natural number. Then F (n) is a Real number.

Let X be a set, and let S be a non-empty family of subsets of X, and let F be a function from S into \overline{}. We say that F is non-negative if and only if: (Def.4) for every element A of S holds 0\overline{}≤ F (A).

We now state the proposition (23)^{4} For every set X and for every field S of subsets of X there exists a

function M from S into \overline{}such that M is non-negative and M(∅) = 0\overline{} and for all elements A, B of S such that A ∩ B = ∅ holds M(A ∪ B) = M(A) + M(B).

Let X be a set, and let S be a field of subsets of X. A function from S into \overline{}is called a measure on S if: (Def.5) it is non-negative and it(∅) = 0\overline{}and for all elements A, B of S such

that A ∩ B = ∅ holds it(A ∪ B) = it(A) + it(B).

Next we state two propositions: (25)^{5} For every set X and for every field S of subsets of X and for every

measure M on S and for all elements A, B of S such that A ⊆ B holds M(A) ≤ M(B).

(26) For every set X and for every field S of subsets of X and for every measure M on S and for all elements A, B of S such that A ⊆ B and M(A) < +∞ holds M(B \ A) = M(B) − M(A).

Let X be a set, and let S be a field of subsets of X, and let A, B be elements of S. Then A ∪ B is an element of S.

Let X be a set, and let S be a field of subsets of X, and let A, B be elements of S. Then A ∩ B is an element of S.

Let X be a set, and let S be a field of subsets of X, and let A, B be elements of S. Then A \ B is an element of S.

The following proposition is true

(27) For every set X and for every field S of subsets of X and for every measure M on S and for all elements A, B of S holds M(A ∪ B) ≤ M(A) + M(B).

Let X be a set, and let S be a field of subsets of X, and let M be a measure on S, and let A be a set. We say that A is measurable w.r.t. M if and only if: (Def.6) A ∈ S.

The following proposition is true (29)^{6} For every set X and for every field S of subsets of X and for every

4The proposition (22) was either repeated or obvious.

5The proposition (24) was either repeated or obvious.

measure M on S holds ∅ is measurable w.r.t. M and X is measurable w.r.t. M and for all sets A, B such that A is measurable w.r.t. M and B is measurable w.r.t. M holds X \ A is measurable w.r.t. M and A ∪ B is measurable w.r.t. M and A ∩ B is measurable w.r.t. M.

Let X be a set, and let S be a field of subsets of X, and let M be a measure on S. An element of S is called a set of measure zero w.r.t. M if:

(Def.7) M(it) = 0\overline{}.

The following propositions are true: (31)^{7} For every set X and for every field S of subsets of X and for every

measure M on S and for every element A of S and for every set B of measure zero w.r.t. M such that A ⊆ B holds A is a set of measure zero w.r.t. M.

(32) For every set X and for every field S of subsets of X and for every measure M on S and for all sets A, B of measure zero w.r.t. M holds A ∪ B is a set of measure zero w.r.t. M and A ∩ B is a set of measure zero w.r.t. M and A \ B is a set of measure zero w.r.t. M.

(33) For every set X and for every field S of subsets of X and for every measure M on S and for every element A of S and for every set B of measure zero w.r.t. M holds M(A ∪ B) = M(A) and M(A ∩ B) = 0\overline{}and M(A \ B) = M(A).

(34) For every set X and for every subset A of X there exists a function F from into 2^{X} such that rng F = {A}.

(35) For every set X and for every subset A of X there exists a function F from into {A} such that for every natural number n holds F (n) = A.

Let X be a set. A non-empty family of subsets of X is said to be a denumerable family of subsets of X if:

(Def.8) there exists a function F from into 2^{X} such that it = rng F.

We now state several propositions: (37)^{8} For every set X and for every denumerable family S of subsets of X

there exists a function F from into 2^{X} such that S = rng F.

(38) For every set X and for every subsets A, B, C of X there exists a function F from into 2^{X} such that rng F = {A, B, C} and F (0) = A and F (1) = B and for every natural number n such that 1 < n holds F (n) = C.

(39) For every set X and for all subsets A, B of X holds {A, B, ∅} is a denumerable family of subsets of X.

6The proposition (28) was either repeated or obvious.

7The proposition (30) was either repeated or obvious.

8The proposition (36) was either repeated or obvious.

(40) For every set X and for every subsets A, B of X there exists a function F from into 2^{X} such that rng F = {A, B} and F (0) = A and for every natural number n such that 0 < n holds F (n) = B.

(41) For every set X and for all subsets A, B of X holds {A, B} is a denumerable family of subsets of X.

(42) For every set X and for every denumerable family S of subsets of X

holds X \ S is a denumerable family of subsets of X. Let X be a set. A non-empty family of subsets of X is said to be a σ-field

of subsets of X if:

(Def.9) for every set A such that A ∈ it holds X \ A ∈ it and for every denumerable family M of subsets of X such that M ⊆ it holds ⋃ M ∈ it.

One can prove the following propositions: (44)^{9} For every set X and for every non-empty family S of subsets of X such

that S is a σ-field of subsets of X holds S is a field of subsets of X.

(45) For every set X and for every σ-field S of subsets of X holds ∅ ∈ S and X ∈ S.

(46) For every set X and for every σ-field S of subsets of X and for all sets A, B such that A ∈ S and B ∈ S holds A ∪ B ∈ S and A ∩ B ∈ S.

(47) For every set X and for every σ-field S of subsets of X and for all sets A, B such that A ∈ S and B ∈ S holds A \ B ∈ S.

(48) For every set X and for every σ-field S of subsets of X holds S = X \S.

(49) For every set X and for every non-empty family S of subsets of X holds S is a σ-field of subsets of X if and only if for every set A such that A ∈ S holds X \ A ∈ S and for every denumerable family M of subsets of X such that M ⊆ S holds ⋂ M ∈ S.

Let X be a set, and let S be a σ-field of subsets of X. A function from into S is said to be a sequence of separated subsets of S if:

(Def.10) for all natural numbers n, m such that n ≠ m holds it(n) ∩ it(m) = ∅.

We now state the proposition (51)^{10} For every set X and for every σ-field S of subsets of X and for every

function F from into S and for every function M from S into \overline{}holds M · F is a function from into \overline{}.

Let X be a set, and let S be a σ-field of subsets of X, and let F be a function from into S. Then rng F is a non-empty family of subsets of X.

Let X be a set, and let S be a σ-field of subsets of X, and let F be a function from into S, and let M be a function from S into \overline{}. Then M · F is a function from into \overline{}.

Next we state several propositions:

9The proposition (43) was either repeated or obvious.

10The proposition (50) was either repeated or obvious.

(52) For every set X and for every σ-field S of subsets of X and for every function F from into S holds rng F is a denumerable family of subsets of X.

(53) For every set X and for every σ-field S of subsets of X and for every function F from into S holds ⋃ rng F is an element of S.

(54) For every set X and for every σ-field S of subsets of X and for every function F from into S and for every function M from S into \overline{}such that M is non-negative holds M · F is non-negative.

(55) For every set X and for every σ-field S of subsets of X and for every Real numbers a, b there exists a function M from S into \overline{}such that for every element A of S holds if A = ∅, then M(A) = a but if A ≠ ∅, then M(A) = b.

(56) For every set X and for every σ-field S of subsets of X there exists a function M from S into \overline{}such that for every element A of S holds if A = ∅, then M(A) = 0\overline{}but if A ≠ ∅, then M(A) = +∞.

(57) For every set X and for every σ-field S of subsets of X there exists a function M from S into \overline{}such that for every element A of S holds M(A) = 0\overline{}.

(58) For every set X and for every σ-field S of subsets of X there exists a function M from S into \overline{}such that M is non-negative and M(∅) = 0\overline{} and for every sequence F of separated subsets of S holds ∑(M · F) = M(⋃ rng F).

Let X be a set, and let S be a σ-field of subsets of X. A function from S into \overline{}is said to be a σ-measure on S if:

(Def.11) it is non-negative and it(∅) = 0\overline{}and for every sequence F of separated subsets of S holds ∑(it · F) = it(⋃ rng F).

Let X be a set. We see that the σ-field of subsets of X is a field of subsets of X.

One can prove the following propositions: (60)^{11} For every set X and for every σ-field S of subsets of X and for every

σ-measure M on S holds M is a measure on S.

(61) For every set X and for every σ-field S of subsets of X and for every σ-measure M on S and for all elements A, B of S such that A ∩ B = ∅ holds M(A ∪ B) = M(A) + M(B).

(62) For every set X and for every σ-field S of subsets of X and for every σ-measure M on S and for all elements A, B of S such that A ⊆ B holds M(A) ≤ M(B).

(63) For every set X and for every σ-field S of subsets of X and for every σ-measure M on S and for all elements A, B of S such that A ⊆ B and M(A) < +∞ holds M(B \ A) = M(B) − M(A).

11The proposition (59) was either repeated or obvious.

(64) For every set X and for every σ-field S of subsets of X and for every σ-measure M on S and for all elements A, B of S holds M(A ∪ B) ≤ M(A) + M(B).

Let X be a set, and let S be a σ-field of subsets of X, and let M be a σmeasure on S, and let A be a set. We say that A is measurable w.r.t. M if and only if:

(Def.12) A ∈ S.

Next we state two propositions: (66)^{12} For every set X and for every σ-field S of subsets of X and for every

σ-measure M on S holds ∅ is measurable w.r.t. M and X is measurable w.r.t. M and for all sets A, B such that A is measurable w.r.t. M and B is measurable w.r.t. M holds X \ A is measurable w.r.t. M and A ∪ B is measurable w.r.t. M and A ∩ B is measurable w.r.t. M.

(67) For every set X and for every σ-field S of subsets of X and for every σ-measure M on S and for every denumerable family T of subsets of X such that for every set A such that A ∈ T holds A is measurable w.r.t. M holds ⋃ T is measurable w.r.t. M and ⋂ T is measurable w.r.t. M.

Let X be a set, and let S be a σ-field of subsets of X, and let M be a σ-measure on S. An element of S is called a set of measure zero w.r.t. M if:

(Def.13) M(it) = 0\overline{}.

Next we state three propositions: (69)^{13} For every set X and for every σ-field S of subsets of X and for every

σ-measure M on S and for every element A of S and for every set B of measure zero w.r.t. M such that A ⊆ B holds A is a set of measure zero w.r.t. M.

(70) For every set X and for every σ-field S of subsets of X and for every σ-measure M on S and for all sets A, B of measure zero w.r.t. M holds A ∪ B is a set of measure zero w.r.t. M and A ∩ B is a set of measure zero w.r.t. M and A \ B is a set of measure zero w.r.t. M.

(71) For every set X and for every σ-field S of subsets of X and for every σ-measure M on S and for every element A of S and for every set B of measure zero w.r.t. M holds M(A ∪ B) = M(A) and M(A ∩ B) = 0\overline{}and M(A \ B) = M(A).

References

[1] Grzegorz Bancerek. The fundamental properties of natural numbers. Formalized Mathematics, 1(1):41–46, 1990.

[2] Grzegorz Bancerek. The ordinal numbers. Formalized Mathematics, 1(1):91–96, 1990.

[3] Józef Białas. Infimum and supremum of the set of real numbers. Measure theory. Formalized Mathematics, 2(1):163–171, 1991.

12The proposition (65) was either repeated or obvious.

13The proposition (68) was either repeated or obvious.

270 Józef Białas

[4] Józef Białas. Series of positive real numbers. Measure theory. Formalized Mathematics, 2(1):173–183, 1991.

[5] Czesław Byliński. Basic functions and operations on functions. Formalized Mathematics, 1(1):245–254, 1990.

[6] Czesław Byliński. Binary operations. Formalized Mathematics, 1(1):175–180, 1990.

[7] Czesław Byliński. Functions and their basic properties. Formalized Mathematics, 1(1):55–65, 1990.

[8] Czesław Byliński. Functions from a set to a set. Formalized Mathematics, 1(1):153–164, 1990.

[9] Krzysztof Hryniewiecki. Basic properties of real numbers. Formalized Mathematics, 1(1):35–40, 1990.

[10] Beata Padlewska. Families of sets. Formalized Mathematics, 1(1):147–152, 1990.

[11] R. Sikorski. Rachunek różniczkowy i całkowy - funkcje wielu zmiennych. PWN - Warszawa, 1968.

[12] Andrzej Trybulec. Enumerated sets. Formalized Mathematics, 1(1):25–34, 1990.

[13] Andrzej Trybulec. Tarski Grothendieck set theory. Formalized Mathematics, 1(1):9–11, 1990.

Incidence Projective Space (a reduction theorem in a plane) ^{1}

Eugeniusz Kusak Warsaw University Białystok Wojciech Leończuk Warsaw University Białystok

Summary. The article begins with basic facts concernig arbitrary projective spaces. Further we are concerned with Fano projective spaces (we prove it has a rank of at least four). Finally we confine ourselves to Desarguesian planes; we define the notion of perspectivity and we prove the reduction theorem for projectivities with concurrent axes.

MML Identifier: PROJRED1.

The articles [6], [8], [5], [7], [9], [10], [4], [3], [1], and [2] provide the terminology and notation for this paper. We adopt the following convention: I_{1} will be a projective space defined in terms of incidence, a, b, c, d, p, q, o, r, s will be elements of the points of I_{1}, and A, B, C, P, Q will be elements of the lines of I_{1}. We now state a number of propositions:

(1) There exists a such that a A.

(2) There exists A such that a A.

(3) If A ≠ B, then there exist a, b such that a | A and a B and b | B and b A.

(4) If a ≠ b, then there exist A, B such that a | A and a B and b | B and b A.

(5) There exist A, B, C such that a | A and a | B and a | C and A ≠ B and B ≠ C and C ≠ A.

(6) There exists a such that a A and a B.

(7) There exists a such that a | A.

(8) If a | A and b | A, then there exists c such that c | A and c ≠ a and c ≠ b.

1Supported by RPBP.III-24.C6

(9) There exists A such that a A and b A.

(10) If A ≠ B and o | A and o | B and p | A and p ≠ o and q | B, then p ≠ q.

(11) If o ≠ a and o ≠ b and A ≠ B and o | A and o | B and a | A and a | C and b | B and b | C, then A ≠ C.

(12) Suppose o | A and o | B and A ≠ B and a | A and o ≠ a and b | B and c | B and b ≠ c and a | P and b | P and a | Q and c | Q. Then P ≠ Q.

(13) If a, b, c | A, then a, c, b | A and b, a, c | A and b, c, a | A and c, a, b | A and c, b, a | A.

(14) Let I_{1} be a Desarguesian projective space defined in terms of incidence. Let o, b_{1}, a_{1}, b_{2}, a_{2}, b_{3}, a_{3}, r, s, t be elements of the points of I_{1}. Let C_{1}, C_{2}, C_{3}, A_{1}, A_{2}, A_{3}, B_{1}, B_{2}, B_{3} be elements of the lines of I_{1}. Suppose that

(i) o, b_{1}, a_{1} | C_{1}, (ii) o, a_{2}, b_{2} | C_{2}, (iii) o, a_{3}, b_{3} | C_{3}, (iv) a_{3}, a_{2}, t | A_{1},

(v) a_{3}, r, a_{1} | A_{2}, (vi) a_{2}, s, a_{1} | A_{3}, (vii) t, b_{2}, b_{3} | B_{1}, (viii) b_{1}, r, b_{3} | B_{2}, (ix) b_{1}, s, b_{2} | B_{3},

(x) C_{1}, C_{2}, C_{3} are mutually different, (xi) o ≠ a_{3}, (xii) o ≠ b_{1}, (xiii) o ≠ b_{2}, (xiv) a_{2} ≠ b_{2}.

Then there exists an element O of the lines of I_{1} such that r, s, t | O.

(15) Suppose there exist A, a, b, c, d such that a | A and b | A and c | A and d | A and a, b, c, d are mutually different. Then for every B there exist p, q, r, s such that p | B and q | B and r | B and s | B and p, q, r, s are mutually different.

We follow a convention: I_{1} will be a Fanoian projective space defined in terms of incidence, a, b, c, d, p, q, r, s will be elements of the points of I_{1}, and A, B, C, D, L, Q, R, S will be elements of the lines of I_{1}. The following propositions are true:

(16) There exist p, q, r, s, a, b, c, A, B, C, Q, L, R, S, D such that q L and r L and p Q and s Q and p R and r R and q S and s S and a, p, s | L and a, q, r | Q and b, q, s | R and b, p, r | S and c, p, q | A and c, r, s | B and a, b | C and c C.

(17) There exist a, A, B, C, D such that a | A and a | B and a | C and a | D and A, B, C, D are mutually different.

(18) There exist a, b, c, d, A such that a | A and b | A and c | A and d | A and a, b, c, d are mutually different.

(19) There exist p, q, r, s such that p | B and q | B and r | B and s | B and

p, q, r, s are mutually different. We follow a convention: I_{1} will denote a Desarguesian 2-dimensional projec-

tive space defined in terms of incidence, c, p, q, x, y will denote elements of the points of I_{1}, and K, L, R, X will denote elements of the lines of I_{1}. Let us consider I_{1}, K, L, p. Let us assume that p K and p L. The functor π_{p}(K → L) yields a partial function from the points of I_{1} to the points of I_{1} and is defined as follows: (Def.1) dom π_{p}(K → L) ⊆ the points of I_{1} and for every x holds x ∈ dom π_{p}(K →

L) if and only if x | K and for all x, y such that x | K and y | L holds π_{p}(K → L)(x) = y if and only if there exists X such that p | X and x | X and y | X.

One can prove the following propositions:

(20) Suppose p K and p L. Then (i) dom π_{p}(K → L) ⊆ the points of I_{1}, (ii) for every x holds x ∈ dom π_{p}(K → L) if and only if x | K, (iii) for all x, y such that x | K and y | L holds π_{p}(K → L)(x) = y if and

only if there exists X such that p | X and x | X and y | X.

(21) If p K, then for every x such that x | K holds π_{p}(K → K)(x) = x.

(22) If p K and p L and x | K, then π_{p}(K → L)(x) is an element of the points of I_{1}.

(23) If p K and p L and x | K and y = π_{p}(K → L)(x), then y | L.

(24) If p K and p L and y ∈ rng π_{p}(K → L), then y | L.

(25) Suppose p K and p L and q L and q R. Then dom(π_{q}(L → R) · π_{p}(K → L)) = dom π_{p}(K → L) and rng(π_{q}(L → R) · π_{p}(K → L)) = rng π_{q}(L → R).

(26) Let a_{1}, b_{1}, a_{2}, b_{2} be elements of the points of I_{1}. Then if p K and p L and a_{1} | K and b_{1} | K and π_{p}(K → L)(a_{1}) = a_{2} and π_{p}(K → L)(b_{1}) = b_{2} and a_{2} = b_{2}, then a_{1} = b_{1}.

(27) If p K and p L and x | K and x | L, then π_{p}(K → L)(x) = x. We now state the proposition

(28) Suppose p K and p L and q L and q R and c | K and c | L and c | R and K ≠ R. Then there exists an element o of the points of I_{1} such that o K and o R and π_{q}(L → R) · π_{p}(K → L) = π_{o}(K → R).

References

[1] Czesław Byliński. Functions and their basic properties. Formalized Mathematics, 1(1):55–65, 1990.

[2] Czesław Byliński. Partial functions. Formalized Mathematics, 1(2):357–367, 1990.

[3] Wojciech Leończuk and Krzysztof Prażmowski. Incidence projective spaces. Formalized Mathematics, 2(2):225–232, 1991.

[4] Andrzej Trybulec. Domains and their Cartesian products. Formalized Mathematics, 1(1):115–122, 1990.

274 Eugeniusz Kusak and Wojciech Leończuk

[5] Andrzej Trybulec. Enumerated sets. Formalized Mathematics, 1(1):25–34, 1990.

[6] Andrzej Trybulec. Tarski Grothendieck set theory. Formalized Mathematics, 1(1):9–11, 1990.

[7] Zinaida Trybulec. Properties of subsets. Formalized Mathematics, 1(1):67–71, 1990.

[8] Zinaida Trybulec and Halina Świe‘czkowska. Boolean properties of sets. Formalized Mathematics, 1(1):17–23, 1990.

[9] Edmund Woronowicz. Relations and their basic properties. Formalized Mathematics, 1(1):73–83, 1990.

[10] Edmund Woronowicz. Relations defined on sets. Formalized Mathematics, 1(1):181–186, 1990.

Groups, Rings, Left- and Right-Modules ^{1}

Michał Muzalewski Warsaw University Białystok

Wojciech Skaba University of Toruń

Summary. The notion of group was defined as a group structure introduced in the article [6]. The article contains the basic properties of groups, rings, left- and right-modules of an associative ring.

MML Identifier: MOD 1.

The articles [11], [10], [13], [3], [1], [12], [9], [4], [2], [5], [6], [7], and [8] provide the notation and terminology for this paper. A group structure is called a group if: (Def.1) for all elements x, y, z of it holds x + y + z = x + (y + z) and x + 0_{it} = x

and x + −x = 0_{it}.

In the sequel G denotes a group structure and x, y denote elements of G. We see that the Abelian group is a group.

Let us consider G, x, y. The functor x−′y yielding an element of G is defined by: (Def.2) x −′ y = x + −y.

In the sequel G denotes a group and u, v, w denote elements of G. One can prove the following propositions:

(1) (−v) + v = 0_{G}.

(2) 0_{G} + v = v.

(3) v + w = 0_{G} if and only if −v = w.

(4) −0_{G} = 0_{G}.

(5) (i) −(v + w) = (−w) −′ v,

(ii) − − v = v, (iii) −((−v) + w) = (−w) + v, (iv) −(v −′ w) = w −′ v, (v) −((−v) −′ w) = w + v, (vi) u −′ (v + w) = u −′ w −′ v.

1Supported by RPBP.III-24.C6

(6) 0_{G} −′ v = −v and v −′ 0_{G} = v.

In the sequel G denotes an Abelian group and u, v, w denote elements of G. The following four propositions are true:

(7) (i) −(v + w) = (−w) − v,

(ii) − − v = v, (iii) −((−v) + w) = (−w) + v, (iv) −(v − w) = w − v,

(v) −((−v) − w) = w + v, (vi) u − (v + w) = u − w − v.

(8) 0_{G} − v = −v and v − 0_{G} = v.

(9) (−u) − v = (−v) − u and (−u) + v = v − u and u − v = (−v) + u and u − v − w = u − w − v.

(10) (i) −(v + w) = (−v) − w, (ii) −((−v) + w) = v − w, (iii) −(v − w) = (−v) + w, (iv) −((−v) − w) = v + w,

(v) u − (v + w) = u − v − w.

For simplicity we adopt the following convention: R will denote an associative ring, a, b will denote scalars of R, V will denote a left module over R, and v, w will denote vectors of V. We now state several propositions:

(11) −(a − b) = (−a) + b.

(12) a + 0_{R} = a and 0_{R} + a = a.

(13) If a = 0_{R} or b = 0_{R}, then a · b = 0_{R}.

(14) (−1_{R}) · a = −a and a · −1_{R} = −a.

(15) a = 0_{R} if and only if −a = 0_{R}.

(16) v + −v = Θ_{V} and (−v) + v = Θ_{V}.

(17) −Θ_{V} = Θ_{V}.

(18) v + w = Θ_{V} if and only if −v = w.

(19) Θ_{V} + v = v and v + Θ_{V} = v and Θ_{V} − v = −v and v − Θ_{V} = v. In the sequel x, y denote scalars of R. Next we state several propositions:

(20) 0_{R} · v = Θ_{V} and (−1_{R}) · v = −v and x · (Θ_{V}) = Θ_{V}.

(21) −x · v = (−x) · v and w − x · v = w + (−x) · v.

(22) x · −v = −x · v.

(23) x · (v − w) = x · v − x · w.

(24) v − x · (y · w) = v − x · y · w.

In the sequel F will be a skew field, x will be a scalar of F, V will be a left module over F, and v will be a vector of V. The following two propositions are true:

(25) x · v = Θ_{V} if and only if x = 0_{F} or v = Θ_{V}.

(26) If x ≠ 0_{F}, then x^{−1} · (x · v) = v.

We adopt the following rules: V will denote a left module over R and v, v_{1}, v_{2}, u, w will denote vectors of V. The following propositions are true:

(27) v − v = Θ_{V}.

(28) (i) − − v = v, (ii) −(v + w) = (−v) + −w, (iii) −((−v) + w) = v + −w, (iv) −(v + w) = (−v) − w,

(v) −(v − w) = (−v) + w, (vi) −((−v) + w) = v − w, (vii) −((−v) − w) = v + w.

(29) (u + v) − w = u + (v − w).

(30) v = v_{1} + v_{2} if and only if v_{1} = v − v_{2}.

(31) v − (u − w) = (v − u) + w.

(32) If v + u = v or u + v = v, then u = Θ_{V}.

In the sequel R denotes an associative ring, V denotes a right module over R, and v, w denote vectors of V. We now state four propositions:

(33) v + −v = Θ_{V} and (−v) + v = Θ_{V}.

(34) −Θ_{V} = Θ_{V}.

(35) v + w = Θ_{V} if and only if −v = w.

(36) Θ_{V} + v = v and v + Θ_{V} = v and Θ_{V} − v = −v and v − Θ_{V} = v. In the sequel x, y are scalars of R. We now state several propositions:

(37) v · 0_{R} = Θ_{V} and v · −1_{R} = −v and (Θ_{V}) · x = Θ_{V}.

(38) −v · x = v · −x and w − v · x = w + v · −x.

(39) (−v) · x = −v · x.

(40) (v − w) · x = v · x − w · x.

(41) v − w · y · x = v − w · (y · x).

In the sequel F denotes a skew field, x denotes a scalar of F, V denotes a right module over F, and v denotes a vector of V. One can prove the following two propositions:

(42) v · x = Θ_{V} if and only if x = 0_{F} or v = Θ_{V}.

(43) If x ≠ 0_{F}, then v · x · x^{−1} = v.

We follow the rules: V will denote a right module over R and v, v_{1}, v_{2}, u, w will denote vectors of V. The following propositions are true:

(44) v − v = Θ_{V}.

(45) (i) − − v = v, (ii) −(v + w) = (−v) + −w, (iii) −((−v) + w) = v + −w, (iv) −(v + w) = (−v) − w,

278 Michał Muzalewski and Wojciech Skaba

(v) −(v − w) = (−v) + w, (vi) −((−v) + w) = v − w, (vii) −((−v) − w) = v + w.

(46) (u + v) − w = u + (v − w).

(47) v = v_{1} + v_{2} if and only if v_{1} = v − v_{2}.

(48) v − (u − w) = (v − u) + w.

(49) If v + u = v or u + v = v, then u = Θ_{V}.

References

[1] Grzegorz Bancerek. The ordinal numbers. Formalized Mathematics, 1(1):91–96, 1990.

[2] Czesław Byliński. Binary operations. Formalized Mathematics, 1(1):175–180, 1990.

[3] Czesław Byliński. Functions and their basic properties. Formalized Mathematics, 1(1):55–65, 1990.

[4] Czesław Byliński. Functions from a set to a set. Formalized Mathematics, 1(1):153–164, 1990.

[5] Krzysztof Hryniewiecki. Basic properties of real numbers. Formalized Mathematics, 1(1):35–40, 1990.

[6] Eugeniusz Kusak, Wojciech Leończuk, and Michał Muzalewski. Abelian groups, fields and vector spaces. Formalized Mathematics, 1(2):335–342, 1990.

[7] Michał Muzalewski. Construction of rings and left-, right-, and bi-modules over a ring. Formalized Mathematics, 2(1):3–11, 1991.

[8] Michał Muzalewski and Lesław W. Szczerba. Construction of finite sequences over ring and left-, right-, and bi-modules over a ring. Formalized Mathematics, 2(1):97–104, 1991.

[9] Andrzej Trybulec. Domains and their Cartesian products. Formalized Mathematics, 1(1):115–122, 1990.

[10] Andrzej Trybulec. Enumerated sets. Formalized Mathematics, 1(1):25–34, 1990.

[11] Andrzej Trybulec. Tarski Grothendieck set theory. Formalized Mathematics, 1(1):9–11, 1990.

[12] Andrzej Trybulec. Tuples, projections and Cartesian products. Formalized Mathematics, 1(1):97–105, 1990.

[13] Zinaida Trybulec. Properties of subsets. Formalized Mathematics, 1(1):67–71, 1990.

Finite Sums of Vectors in Left Module over Associative Ring ^{1}

Michał Muzalewski Warsaw University Białystok

Wojciech Skaba University of Toruń

Summary. Definition of a finite sequence of the vectors of Left Module over Associative Ring and some theorems concerning these sums. Written as a generalization of the article [11].

MML Identifier: LMOD 1.

The terminology and notation used here have been introduced in the following papers: [10], [3], [2], [4], [6], [12], [9], [5], [1], [7], and [8]. For simplicity we adopt the following convention: x is arbitrary, R is an associative ring, a is a scalar of R, V is a left module over R, and v, v_{1}, v_{2}, w, u are vectors of V. Let us consider R, V, x. The predicate x ∈ V is defined by: (Def.1) x ∈ the carrier of the carrier of V.

The following two propositions are true:

(1) x ∈ V if and only if x ∈ the carrier of the carrier of V.

(2) v ∈ V.

We adopt the following convention: F, G, H will denote finite sequences of elements of the carrier of the carrier of V, f will denote a function from into the carrier of the carrier of V, and i, j, k, n will denote natural numbers. Let us consider R, V, F. The functor ∑ F yielding a vector of V is defined by: (Def.2) there exists f such that ∑ F = f(len F) and f(0) = Θ_{V} and for all j,

v such that j < len F and v = F (j + 1) holds f(j + 1) = f(j) + v. One can prove the following propositions:

(3) If there exists f such that u = f(len F) and f(0) = Θ_{V} and for all j, v such that j < len F and v = F (j + 1) holds f(j + 1) = f(j) + v, then u = ∑ F.

1Supported by RPBP.III-24.C6

(4) There exists f such that ∑ F = f(len F) and f(0) = Θ_{V} and for all j, v such that j < len F and v = F (j + 1) holds f(j + 1) = f(j) + v.

(5) If k ∈ Seg n and len F = n, then F (k) is a vector of V.

(6) If len F = len G + 1 and G = F Seg len G and v = F (len F), then ∑ F = ∑ G + v.

(7) ∑(F ^{}G) = ∑ F + ∑ G.

(8) If len F = len G and len F = len H and for every k such that k ∈ Seg len F holds H(k) = π_{k}F + π_{k}G, then ∑ H = ∑ F + ∑ G.

(9) If len F = len G and for all k, v such that k ∈ Seg len F and v = G(k) holds F (k) = a · v, then ∑ F = a · ∑ G.

(10) If len F = len G and for every k such that k ∈ Seg len F holds G(k) = a · π_{k}F, then ∑ G = a · ∑ F.

(11) If len F = len G and for all k, v such that k ∈ Seg len F and v = G(k) holds F (k) = −v, then ∑ F = − ∑ G.

(12) If len F = len G and for every k such that k ∈ Seg len F holds G(k) = −π_{k}F, then ∑ G = − ∑ F.

(13) If len F = len G and len F = len H and for every k such that k ∈ Seg len F holds H(k) = π_{k}F − π_{k}G, then ∑ H = ∑ F − ∑ G.

(14) If rng F = rng G and F is one-to-one and G is one-to-one, then ∑ F = ∑ G.

(15) For all F, G and for every permutation f of dom F such that len F = len G and for every i such that i ∈ dom G holds G(i) = F (f(i)) holds ∑ F = ∑ G.

(16) For every permutation f of dom F such that G = F ·f holds ∑ F = ∑ G.

(17) ∑ ε_{the carrier of the carrier of V} = Θ_{V}.

(18) ∑⟨v⟩ = v.

(19) ∑⟨v, u⟩ = v + u.

(20) ∑⟨v, u, w⟩ = v + u + w.

(21) a · ∑ ε_{the carrier of the carrier of V} = Θ_{V}.

(22) a · ∑⟨v⟩ = a · v.

(23) a · ∑⟨v, u⟩ = a · v + a · u.

(24) a · ∑⟨v, u, w⟩ = a · v + a · u + a · w.

(25) − ∑ ε_{the carrier of the carrier of V} = Θ_{V}.

(26) − ∑⟨v⟩ = −v.

(27) − ∑⟨v, u⟩ = (−v) − u.

(28) − ∑⟨v, u, w⟩ = (−v) − u − w.

(29) ∑⟨v, w⟩ = ∑⟨w, v⟩.

(30) ∑⟨v, w⟩ = ∑⟨v⟩ + ∑⟨w⟩.

(31) ∑⟨Θ_{V} , Θ_{V} ⟩ = Θ_{V}.

(32) ∑⟨Θ_{V} , v⟩ = v and ∑⟨v, Θ_{V} ⟩ = v.

Finite Sums of Vectors in Left Module over … 281

(33) ∑⟨v, −v⟩ = Θ_{V} and ∑⟨−v, v⟩ = Θ_{V}.

We now state a number of propositions:

(34) ∑⟨v, −w⟩ = v − w and ∑⟨−w, v⟩ = v − w.

(35) ∑⟨−v, −w⟩ = −(v + w) and ∑⟨−w, −v⟩ = −(v + w).

(36) ∑⟨u, v, w⟩ = ∑⟨u⟩ + ∑⟨v⟩ + ∑⟨w⟩.

(37) ∑⟨u, v, w⟩ = ∑⟨u, v⟩ + w.

(38) ∑⟨u, v, w⟩ = ∑⟨v, w⟩ + u.

(39) ∑⟨u, v, w⟩ = ∑⟨u, w⟩ + v.

(40) ∑⟨u, v, w⟩ = ∑⟨u, w, v⟩.

(41) ∑⟨u, v, w⟩ = ∑⟨v, u, w⟩.

(42) ∑⟨u, v, w⟩ = ∑⟨v, w, u⟩.

(43) ∑⟨u, v, w⟩ = ∑⟨w, u, v⟩.

(44) ∑⟨u, v, w⟩ = ∑⟨w, v, u⟩.

(45) ∑⟨Θ_{V} , Θ_{V} , Θ_{V} ⟩ = Θ_{V}.

(46) ∑⟨Θ_{V} , Θ_{V} , v⟩ = v and ∑⟨Θ_{V} , v, Θ_{V} ⟩ = v and ∑⟨v, Θ_{V} , Θ_{V} ⟩ = v.

(47) ∑⟨Θ_{V} , u, v⟩ = u + v and ∑⟨u, v, Θ_{V} ⟩ = u + v and ∑⟨u, Θ_{V} , v⟩ = u + v.

(48) If len F = 0, then ∑ F = Θ_{V}.

(49) If len F = 1, then ∑ F = F (1).

(50) If len F = 2 and v_{1} = F (1) and v_{2} = F (2), then ∑ F = v_{1} + v_{2}.

(51) If len F = 3 and v_{1} = F (1) and v_{2} = F (2) and v = F (3), then ∑ F = v_{1} + v_{2} + v.

References

[1] Grzegorz Bancerek. The fundamental properties of natural numbers. Formalized Mathematics, 1(1):41–46, 1990.

[2] Grzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite sequences. Formalized Mathematics, 1(1):107–114, 1990.

[3] Czesław Byliński. Functions and their basic properties. Formalized Mathematics, 1(1):55–65, 1990.

[4] Czesław Byliński. Functions from a set to a set. Formalized Mathematics, 1(1):153–164, 1990.

[5] Krzysztof Hryniewiecki. Basic properties of real numbers. Formalized Mathematics, 1(1):35–40, 1990.

[6] Eugeniusz Kusak, Wojciech Leończuk, and Michał Muzalewski. Abelian groups, fields and vector spaces. Formalized Mathematics, 1(2):335–342, 1990.

[7] Michał Muzalewski. Construction of rings and left-, right-, and bi-modules over a ring. Formalized Mathematics, 2(1):3–11, 1991.

[8] Michał Muzalewski and Lesław W. Szczerba. Construction of finite sequences over ring and left-, right-, and bi-modules over a ring. Formalized Mathematics, 2(1):97–104, 1991.

[9] Andrzej Trybulec. Domains and their Cartesian products. Formalized Mathematics, 1(1):115–122, 1990.

[10] Andrzej Trybulec. Tarski Grothendieck set theory. Formalized Mathematics, 1(1):9–11, 1990.

[11] Wojciech A. Trybulec. Finite sums of vectors in vector space. Formalized Mathematics, 1(5):851–854, 1990.

282 Michał Muzalewski and Wojciech Skaba

[12] Wojciech A. Trybulec. Pigeon hole principle. Formalized Mathematics, 1(3):575–579,

1990.

Received October 22, 1990

Submodules and Cosets of Submodules in Left Module over Associative Ring ^{1}

Michał Muzalewski Warsaw University Białystok

Wojciech Skaba University of Toruń

Summary. Notions of Submodules in Left Module over Associative Ring and Cosets of Submodules in Left Module over Associative Ring. A few basic theorems related to these notions are proved. This article originated as a generalization of the article [12].

MML Identifier: LMOD 2.

The notation and terminology used here are introduced in the following articles: [8], [2], [14], [13], [10], [11], [7], [1], [3], [9], [4], [6], and [5]. For simplicity we follow a convention: x will be arbitrary, R will be an associative ring, a will be a scalar of R, V, X, Y will be left modules over R, and u, v, v_{1}, v_{2} will be vectors of V. Let us consider R, V. A subset of V is a subset of the carrier of the carrier of V.

In the sequel V_{1}, V_{2}, V_{3} will denote subsets of V. Let us consider R, V, V_{1}. We say that V_{1} is linearly closed if and only if: (Def.1) for all v, u such that v ∈ V_{1} and u ∈ V_{1} holds v + u ∈ V_{1} and for all a,

v such that v ∈ V_{1} holds a · v ∈ V_{1}.

We now state a number of propositions:

(1) If for all v, u such that v ∈ V_{1} and u ∈ V_{1} holds v + u ∈ V_{1} and for all a, v such that v ∈ V_{1} holds a · v ∈ V_{1}, then V_{1} is linearly closed.

(2) If V_{1} is linearly closed, then for all v, u such that v ∈ V_{1} and u ∈ V_{1} holds v + u ∈ V_{1}.

(3) If V_{1} is linearly closed, then for all a, v such that v ∈ V_{1} holds a·v ∈ V_{1}.

(4) If V_{1} ≠ ∅ and V_{1} is linearly closed, then Θ_{V} ∈ V_{1}.

(5) If V_{1} is linearly closed, then for every v such that v ∈ V_{1} holds −v ∈ V_{1}.

1Supported by RPBP.III-24.C6

(6) If V_{1} is linearly closed, then for all v, u such that v ∈ V_{1} and u ∈ V_{1} holds v − u ∈ V_{1}.

(7) {Θ_{V} } is linearly closed.

(8) If the carrier of the carrier of V = V_{1}, then V_{1} is linearly closed.

(9) If V_{1} is linearly closed and V_{2} is linearly closed and V_{3} = {v + u : v ∈ V_{1} ∧ u ∈ V_{2}}, then V_{3} is linearly closed.

(10) If V_{1} is linearly closed and V_{2} is linearly closed, then V_{1} ∩ V_{2} is linearly

closed. Let us consider R, V. A left module over R is called a submodule of V if:

(Def.2) the carrier of the carrier of it ⊆ the carrier of the carrier of V and the zero of the carrier of it = the zero of the carrier of V and the addition of the carrier of it = (the addition of the carrier of V) [: the carrier of the carrier of it, the carrier of the carrier of it :] and the left multiplication of it = (the left multiplication of V) [: the carrier of R, the carrier of the carrier of it :].

We now state the proposition

(11) If the carrier of the carrier of X ⊆ the carrier of the carrier of V and the zero of the carrier of X = the zero of the carrier of V and the addition of the carrier of X = (the addition of the carrier of V) [: the carrier of the carrier of X, the carrier of the carrier of X:] and the left multiplication of X = (the left multiplication of V) [: the carrier of R, the carrier of the carrier of X:], then X is a submodule of V.

We follow a convention: W, W_{1}, W_{2} denote submodules of V and w, w_{1}, w_{2} denote vectors of W. The following propositions are true:

(12) The carrier of the carrier of W ⊆ the carrier of the carrier of V.

(13) The zero of the carrier of W = the zero of the carrier of V.

(14) The addition of the carrier of W = (the addition of the carrier of V) [: the carrier of the carrier of W, the carrier of the carrier of W :].

(15) The left multiplication of W = (the left multiplication of V) [: the carrier of R, the carrier of the carrier of W :].

(16) If x ∈ W_{1} and W_{1} is a submodule of W_{2}, then x ∈ W_{2}.

(17) If x ∈ W, then x ∈ V.

(18) w is a vector of V.

(19) Θ_{W} = Θ_{V}.

(20) Θ_{W_{1}} = Θ_{W_{2}}.

(21) If w_{1} = v and w_{2} = u, then w_{1} + w_{2} = v + u.

(22) If w = v, then a · w = a · v.

(23) If w = v, then −v = −w.

(24) If w_{1} = v and w_{2} = u, then w_{1} − w_{2} = v − u.

(25) Θ_{V} ∈ W.

(26) Θ_{W_{1}} ∈ W_{2}.

(27) Θ_{W} ∈ V.

(28) If u ∈ W and v ∈ W, then u + v ∈ W.

(29) If v ∈ W, then a · v ∈ W.

(30) If v ∈ W, then −v ∈ W.

(31) If u ∈ W and v ∈ W, then u − v ∈ W.

(32) V is a submodule of V.

(33) If V is a submodule of X and X is a submodule of V, then V = X.

(34) If V is a submodule of X and X is a submodule of Y, then V is a submodule of Y.

(35) If the carrier of the carrier of W_{1} ⊆ the carrier of the carrier of W_{2}, then W_{1} is a submodule of W_{2}.

(36) If for every v such that v ∈ W_{1} holds v ∈ W_{2}, then W_{1} is a submodule of W_{2}.

(37) If the carrier of the carrier of W_{1} = the carrier of the carrier of W_{2}, then W_{1} = W_{2}.

(38) If for every v holds v ∈ W_{1} if and only if v ∈ W_{2}, then W_{1} = W_{2}.

(39) If the carrier of the carrier of W = the carrier of the carrier of V, then W = V.

(40) If for every v holds v ∈ W, then W = V.

(41) If the carrier of the carrier of W = V_{1}, then V_{1} is linearly closed.

(42) If V_{1} ≠ ∅ and V_{1} is linearly closed, then there exists W such that V_{1} =

the carrier of the carrier of W. Let us consider R, V. The functor 0_{V} yields a submodule of V and is defined

as follows: (Def.3) the carrier of the carrier of 0_{V} = {Θ_{V} }.

Let us consider R, V. The functor Ω_{V} yielding a submodule of V is defined by: (Def.4) Ω_{V} = V.

The following propositions are true:

(43) The carrier of the carrier of 0_{V} = {Θ_{V} }.

(44) If the carrier of the carrier of W = {Θ_{V} }, then W = 0_{V}.

(45) Ω_{V} = V.

(46) x ∈ 0_{V} if and only if x = Θ_{V}.

(47) 0_{W} = 0_{V}.

(48) 0_{W_{1}} = 0_{W_{2}}.

(49) 0_{W} is a submodule of V.

(50) 0_{V} is a submodule of W.

(51) 0_{W_{1}} is a submodule of W_{2}.

(52) W is a submodule of Ω_{V}.

(53) V is a submodule of Ω_{V}.

Let us consider R, V, v, W. The functor v + W yields a subset of V and is defined by: (Def.5) v + W = {v + u : u ∈ W }.

Let us consider R, V, W. A subset of V is said to be a coset of W if: (Def.6) there exists v such that it = v + W.

In the sequel B, C are cosets of W. One can prove the following propositions:

(54) v + W = {v + u : u ∈ W }.

(55) There exists v such that C = v + W.

(56) If V_{1} = v + W, then V_{1} is a coset of W.

(57) x ∈ v + W if and only if there exists u such that u ∈ W and x = v + u.

(58) Θ_{V} ∈ v + W if and only if v ∈ W.

(59) v ∈ v + W.

(60) Θ_{V} + W = the carrier of the carrier of W.

(61) v + 0_{V} = {v}.

(62) v + Ω_{V} = the carrier of the carrier of V.

(63) Θ_{V} ∈ v + W if and only if v + W = the carrier of the carrier of W.

(64) v ∈ W if and only if v + W = the carrier of the carrier of W.

(65) If v ∈ W, then a · v + W = the carrier of the carrier of W.

(66) u ∈ W if and only if v + W = v + u + W.

(67) u ∈ W if and only if v + W = (v − u) + W.

(68) v ∈ u + W if and only if u + W = v + W.

(69) If u ∈ v_{1} + W and u ∈ v_{2} + W, then v_{1} + W = v_{2} + W.

(70) If v ∈ W, then a · v ∈ v + W.

(71) If v ∈ W, then −v ∈ v + W.

(72) u + v ∈ v + W if and only if u ∈ W.

(73) v − u ∈ v + W if and only if u ∈ W.

(74) u ∈ v+W if and only if there exists v_{1} such that v_{1} ∈ W and u = v+v_{1}.

(75) u ∈ v+W if and only if there exists v_{1} such that v_{1} ∈ W and u = v−v_{1}.

(76) There exists v such that v_{1} ∈ v + W and v_{2} ∈ v + W if and only if v_{1} − v_{2} ∈ W.

(77) If v +W = u+W, then there exists v_{1} such that v_{1} ∈ W and v +v_{1} = u.

(78) If v +W = u+W, then there exists v_{1} such that v_{1} ∈ W and v −v_{1} = u.

(79) v + W_{1} = v + W_{2} if and only if W_{1} = W_{2}.

(80) If v + W_{1} = u + W_{2}, then W_{1} = W_{2}.

In the sequel C_{1} denotes a coset of W_{1} and C_{2} denotes a coset of W_{2}. Next we state a number of propositions:

(81) There exists C such that v ∈ C.

(82) C is linearly closed if and only if C = the carrier of the carrier of W.

(83) If C_{1} = C_{2}, then W_{1} = W_{2}.

Submodules and Cosets of Submodules in Left … 287

(84) {v} is a coset of 0_{V}.

(85) If V_{1} is a coset of 0_{V}, then there exists v such that V_{1} = {v}.

(86) The carrier of the carrier of W is a coset of W.

(87) The carrier of the carrier of V is a coset of Ω_{V}.

(88) If V_{1} is a coset of Ω_{V}, then V_{1} = the carrier of the carrier of V.

(89) Θ_{V} ∈ C if and only if C = the carrier of the carrier of W.

(90) u ∈ C if and only if C = u + W.

(91) If u ∈ C and v ∈ C, then there exists v_{1} such that v_{1} ∈ W and u+v_{1} = v.

(92) If u ∈ C and v ∈ C, then there exists v_{1} such that v_{1} ∈ W and u−v_{1} = v.

(93) There exists C such that v_{1} ∈ C and v_{2} ∈ C if and only if v_{1} − v_{2} ∈ W.

(94) If u ∈ B and u ∈ C, then B = C.

References

[1] Czesław Byliński. Binary operations. Formalized Mathematics, 1(1):175–180, 1990.

[2] Czesław Byliński. Functions from a set to a set. Formalized Mathematics, 1(1):153–164, 1990.

[3] Eugeniusz Kusak, Wojciech Leończuk, and Michał Muzalewski. Abelian groups, fields and vector spaces. Formalized Mathematics, 1(2):335–342, 1990.

[4] Michał Muzalewski. Construction of rings and left-, right-, and bi-modules over a ring. Formalized Mathematics, 2(1):3–11, 1991.

[5] Michał Muzalewski and Wojciech Skaba. Finite sums of vectors in left module over associative ring. Formalized Mathematics, 2(2):279–282, 1991.

[6] Michał Muzalewski and Lesław W. Szczerba. Construction of finite sequences over ring and left-, right-, and bi-modules over a ring. Formalized Mathematics, 2(1):97–104, 1991.

[7] Andrzej Trybulec. Domains and their Cartesian products. Formalized Mathematics, 1(1):115–122, 1990.

[8] Andrzej Trybulec. Tarski Grothendieck set theory. Formalized Mathematics, 1(1):9–11, 1990.

[9] Wojciech A. Trybulec. Finite sums of vectors in vector space. Formalized Mathematics, 1(5):851–854, 1990.

[10] Wojciech A. Trybulec. Groups. Formalized Mathematics, 1(5):821–827, 1990.

[11] Wojciech A. Trybulec. Subgroup and cosets of subgroups. Formalized Mathematics, 1(5):855–864, 1990.

[12] Wojciech A. Trybulec. Subspaces and cosets of subspaces in vector space. Formalized Mathematics, 1(5):865–870, 1990.

[13] Zinaida Trybulec. Properties of subsets. Formalized Mathematics, 1(1):67–71, 1990.

[14] Zinaida Trybulec and Halina Świe‘czkowska. Boolean properties of sets. Formalized Mathematics, 1(1):17–23, 1990.

288

Operations on Submodules in Left Module over Associative Ring ^{1}

Michał Muzalewski Warsaw University Białystok

Wojciech Skaba University of Toruń

Summary. Definition of sum, direct sum and intersection of submodules. We prove a number of theorems related to these notions. This article originated as a generalization of the article [10].

MML Identifier: LMOD 3.

The terminology and notation used here are introduced in the following papers: [1], [12], [14], [9], [8], [13], [2], [11], [7], [3], [4], [5], and [6]. For simplicity we adopt the following rules: R denotes an associative ring, V denotes a left module over R, W, W_{1}, W_{2}, W_{3} denote submodules of V, u, u_{1}, u_{2}, v, v_{1}, v_{2} denote vectors of V, and x is arbitrary. Let us consider R, V, W_{1}, W_{2}. The functor W_{1} + W_{2} yields a submodule of V and is defined by: (Def.1) the carrier of the carrier of W_{1} + W_{2} = {v + u : v ∈ W_{1} ∧ u ∈ W_{2}}.

Let us consider R, V, W_{1}, W_{2}. The functor W_{1} ∩ W_{2} yielding a submodule of V is defined by: (Def.2) the carrier of the carrier of W_{1} ∩ W_{2} = (the carrier of the carrier of

W_{1})∩ (the carrier of the carrier of W_{2}). One can prove the following propositions:

(1) The carrier of the carrier of W_{1} + W_{2} = {v + u : v ∈ W_{1} ∧ u ∈ W_{2}}.

(2) If the carrier of the carrier of W = {v + u : v ∈ W_{1} ∧ u ∈ W_{2}}, then W = W_{1} + W_{2}.

(3) The carrier of the carrier of W_{1} ∩ W_{2} = (the carrier of the carrier of W_{1})∩ (the carrier of the carrier of W_{2}).

(4) If the carrier of the carrier of W = (the carrier of the carrier of W_{1})∩ (the carrier of the carrier of W_{2}), then W = W_{1} ∩ W_{2}.

1Supported by RPBP.III-24.C6

(5) x ∈ W_{1} + W_{2} if and only if there exist v_{1}, v_{2} such that v_{1} ∈ W_{1} and v_{2} ∈ W_{2} and x = v_{1} + v_{2}.

(6) If v ∈ W_{1} or v ∈ W_{2}, then v ∈ W_{1} + W_{2}.

(7) x ∈ W_{1} ∩ W_{2} if and only if x ∈ W_{1} and x ∈ W_{2}.

(8) W + W = W.

(9) W_{1} + W_{2} = W_{2} + W_{1}.

(10) W_{1} + (W_{2} + W_{3}) = W_{1} + W_{2} + W_{3}.

(11) W_{1} is a submodule of W_{1} + W_{2} and W_{2} is a submodule of W_{1} + W_{2}.

(12) W_{1} is a submodule of W_{2} if and only if W_{1} + W_{2} = W_{2}.

(13) 0_{V} + W = W and W + 0_{V} = W.

(14) 0_{V} + Ω_{V} = V and Ω_{V} + 0_{V} = V.

(15) Ω_{V} + W = V and W + Ω_{V} = V.

(16) Ω_{V} + Ω_{V} = V.

(17) W ∩ W = W.

(18) W_{1} ∩ W_{2} = W_{2} ∩ W_{1}.

(19) W_{1} ∩ (W_{2} ∩ W_{3}) = W_{1} ∩ W_{2} ∩ W_{3}.

(20) W_{1} ∩ W_{2} is a submodule of W_{1} and W_{1} ∩ W_{2} is a submodule of W_{2}.

(21) W_{1} is a submodule of W_{2} if and only if W_{1} ∩ W_{2} = W_{1}.

(22) If W_{1} is a submodule of W_{2}, then W_{1} ∩ W_{3} is a submodule of W_{2} ∩ W_{3}.

(23) If W_{1} is a submodule of W_{3}, then W_{1} ∩ W_{2} is a submodule of W_{3}.

(24) If W_{1} is a submodule of W_{2} and W_{1} is a submodule of W_{3}, then W_{1} is a submodule of W_{2} ∩ W_{3}.

(25) 0_{V} ∩ W = 0_{V} and W ∩ 0_{V} = 0_{V}.

(26) 0_{V} ∩ Ω_{V} = 0_{V} and Ω_{V} ∩ 0_{V} = 0_{V}.

(27) Ω_{V} ∩ W = W and W ∩ Ω_{V} = W.

(28) Ω_{V} ∩ Ω_{V} = V.

(29) W_{1} ∩ W_{2} is a submodule of W_{1} + W_{2}.

(30) W_{1} ∩ W_{2} + W_{2} = W_{2}.

(31) W_{1} ∩ (W_{1} + W_{2}) = W_{1}.

One can prove the following propositions:

(32) W_{1} ∩ W_{2} + W_{2} ∩ W_{3} is a submodule of W_{2} ∩ (W_{1} + W_{3}).

(33) If W_{1} is a submodule of W_{2}, then W_{2} ∩(W_{1} +W_{3}) = W_{1} ∩W_{2} +W_{2} ∩W_{3}.

(34) W_{2} + W_{1} ∩ W_{3} is a submodule of (W_{1} + W_{2}) ∩ (W_{2} + W_{3}).

(35) If W_{1} is a submodule of W_{2}, then W_{2}+W_{1}∩W_{3} = (W_{1}+W_{2})∩(W_{2}+W_{3}).

(36) If W_{1} is a submodule of W_{3}, then W_{1} + W_{2} ∩ W_{3} = (W_{1} + W_{2}) ∩ W_{3}.

(37) W_{1} + W_{2} = W_{2} if and only if W_{1} ∩ W_{2} = W_{1}.

(38) If W_{1} is a submodule of W_{2}, then W_{1} + W_{3} is a submodule of W_{2} + W_{3}.

(39) If W_{1} is a submodule of W_{2}, then W_{1} is a submodule of W_{2} + W_{3}.

(40) If W_{1} is a submodule of W_{3} and W_{2} is a submodule of W_{3}, then W_{1}+W_{2} is a submodule of W_{3}.

(41) There exists W such that the carrier of the carrier of W = (the carrier of the carrier of W_{1})∪ (the carrier of the carrier of W_{2}) if and only if W_{1} is a submodule of W_{2} or W_{2} is a submodule of W_{1}.

Let us consider R, V. The functor Sub(V) yields a non-empty set and is defined by: (Def.3) for every x holds x ∈ Sub(V) if and only if x is a submodule of V.

In the sequel D denotes a non-empty set. One can prove the following three propositions:

(42) If for every x holds x ∈ D if and only if x is a submodule of V, then D = Sub(V).

(43) x ∈ Sub(V) if and only if x is a submodule of V.

(44) V ∈ Sub(V).

Let us consider R, V, W_{1}, W_{2}. We say that V is the direct sum of W_{1} and W_{2} if and only if: (Def.4) V = W_{1} + W_{2} and W_{1} ∩ W_{2} = 0_{V}.

One can prove the following two propositions: (46)^{2} If V is the direct sum of W_{1} and W_{2}, then V is the direct sum of W_{2}

and W_{1}.

(47) V is the direct sum of 0_{V} and Ω_{V} and V is the direct sum of Ω_{V} and

0_{V}. In the sequel C_{1} will denote a coset of W_{1} and C_{2} will denote a coset of W_{2}.

Next we state several propositions:

(48) If C_{1} ∩ C_{2} ≠ ∅, then C_{1} ∩ C_{2} is a coset of W_{1} ∩ W_{2}.

(49) V is the direct sum of W_{1} and W_{2} if and only if for every C_{1}, C_{2} there exists v such that C_{1} ∩ C_{2} = {v}.

(50) W_{1} + W_{2} = V if and only if for every v there exist v_{1}, v_{2} such that v_{1} ∈ W_{1} and v_{2} ∈ W_{2} and v = v_{1} + v_{2}.

(51) If V is the direct sum of W_{1} and W_{2} and v = v_{1} + v_{2} and v = u_{1} + u_{2} and v_{1} ∈ W_{1} and u_{1} ∈ W_{1} and v_{2} ∈ W_{2} and u_{2} ∈ W_{2}, then v_{1} = u_{1} and v_{2} = u_{2}.

(52) Suppose V = W_{1} + W_{2} and there exists v such that for all v_{1}, v_{2}, u_{1}, u_{2} such that v = v_{1} + v_{2} and v = u_{1} + u_{2} and v_{1} ∈ W_{1} and u_{1} ∈ W_{1} and v_{2} ∈ W_{2} and u_{2} ∈ W_{2} holds v_{1} = u_{1} and v_{2} = u_{2}. Then V is the direct sum of W_{1} and W_{2}.

In the sequel t will be an element of [: the carrier of the carrier of V, the carrier of the carrier of V :]. Let us consider R, V, v, W_{1}, W_{2}. Let us assume that V is the direct sum of W_{1} and W_{2}. The functor v < (W_{1}, W_{2}) yielding an element of [: the carrier of the carrier of V, the carrier of the carrier of V :] is defined as follows: (Def.5) v = (v < (W_{1}, W_{2}))_{1} +(v < (W_{1}, W_{2}))_{2} and (v < (W_{1}, W_{2}))_{1} ∈ W_{1} and

2The proposition (45) was either repeated or obvious.

(v < (W_{1}, W_{2}))_{2} ∈ W_{2}. The following propositions are true:

(53) If V is the direct sum of W_{1} and W_{2} and t_{1} + t_{2} = v and t_{1} ∈ W_{1} and t_{2} ∈ W_{2}, then t = v < (W_{1}, W_{2}).

(54) If V is the direct sum of W_{1} and W_{2}, then (v < (W_{1}, W_{2}))_{1} + (v < (W_{1}, W_{2}))_{2} = v.

(55) If V is the direct sum of W_{1} and W_{2}, then (v < (W_{1}, W_{2}))_{1} ∈ W_{1}.

(56) If V is the direct sum of W_{1} and W_{2}, then (v < (W_{1}, W_{2}))_{2} ∈ W_{2}.

(57) If V is the direct sum of W_{1} and W_{2}, then (v < (W_{1}, W_{2}))_{1} = (v < (W_{2}, W_{1}))_{2}.

(58) If V is the direct sum of W_{1} and W_{2}, then

(v < (W_{1}, W_{2}))_{2} = (v < (W_{2}, W_{1}))_{1}. In the sequel A_{1}, A_{2} will denote elements of Sub(V). Let us consider R, V.

The functor SubJoin V yields a binary operation on Sub(V) and is defined as follows: (Def.6) for all A_{1}, A_{2}, W_{1}, W_{2} such that A_{1} = W_{1} and A_{2} = W_{2} holds

(SubJoin V)(A_{1}, A_{2}) = W_{1} + W_{2}. Let us consider R, V. The functor SubMeet V yielding a binary operation

on Sub(V) is defined as follows: (Def.7) for all A_{1}, A_{2}, W_{1}, W_{2} such that A_{1} = W_{1} and A_{2} = W_{2} holds

(SubMeet V)(A_{1}, A_{2}) = W_{1} ∩ W_{2}. In the sequel o is a binary operation on Sub(V). Next we state several

propositions:

(59) If A_{1} = W_{1} and A_{2} = W_{2}, then SubJoin V (A_{1}, A_{2}) = W_{1} + W_{2}.

(60) If for all A_{1}, A_{2}, W_{1}, W_{2} such that A_{1} = W_{1} and A_{2} = W_{2} holds o(A_{1}, A_{2}) = W_{1} + W_{2}, then o = SubJoin V.

(61) If A_{1} = W_{1} and A_{2} = W_{2}, then SubMeet V (A_{1}, A_{2}) = W_{1} ∩ W_{2}.

(62) If for all A_{1}, A_{2}, W_{1}, W_{2} such that A_{1} = W_{1} and A_{2} = W_{2} holds o(A_{1}, A_{2}) = W_{1} ∩ W_{2}, then o = SubMeet V.

(63) ⟨Sub(V), SubJoin V, SubMeet V ⟩ is a lattice.

(64) ⟨Sub(V), SubJoin V, SubMeet V ⟩ is a lower bound lattice.

(65) ⟨Sub(V), SubJoin V, SubMeet V ⟩ is an upper bound lattice.

(66) ⟨Sub(V), SubJoin V, SubMeet V ⟩ is a bound lattice.

(67) ⟨Sub(V), SubJoin V, SubMeet V ⟩ is a modular lattice.

References

[1] Czesław Byliński. Binary operations. Formalized Mathematics, 1(1):175–180, 1990.

Operations on Submodules in Left Module over … 293

[2] Eugeniusz Kusak, Wojciech Leończuk, and Michał Muzalewski. Abelian groups, fields and vector spaces. Formalized Mathematics, 1(2):335–342, 1990.

[3] Michał Muzalewski. Construction of rings and left-, right-, and bi-modules over a ring. Formalized Mathematics, 2(1):3–11, 1991.

[4] Michał Muzalewski and Wojciech Skaba. Finite sums of vectors in left module over associative ring. Formalized Mathematics, 2(2):279–282, 1991.

[5] Michał Muzalewski and Wojciech Skaba. Submodules and cosets of submodules in left module over associative ring. Formalized Mathematics, 2(2):283–287, 1991.

[6] Michał Muzalewski and Lesław W. Szczerba. Construction of finite sequences over ring and left-, right-, and bi-modules over a ring. Formalized Mathematics, 2(1):97–104, 1991.

[7] Andrzej Trybulec. Domains and their Cartesian products. Formalized Mathematics, 1(1):115–122, 1990.

[8] Andrzej Trybulec. Tarski Grothendieck set theory. Formalized Mathematics, 1(1):9–11, 1990.

[9] Andrzej Trybulec. Tuples, projections and Cartesian products. Formalized Mathematics, 1(1):97–105, 1990.

[10] Wojciech A. Trybulec. Operations on subspaces in vector space. Formalized Mathematics, 1(5):871–876, 1990.

[11] Zinaida Trybulec. Properties of subsets. Formalized Mathematics, 1(1):67–71, 1990.

[12] Zinaida Trybulec and Halina Świe‘czkowska. Boolean properties of sets. Formalized Mathematics, 1(1):17–23, 1990.

[13] Edmund Woronowicz. Relations defined on sets. Formalized Mathematics, 1(1):181–186, 1990.

[14] Stanisław Żukowski. Introduction to lattice theory. Formalized Mathematics, 1(1):215– 222, 1990.

294

Linear Combinations in Left Module over Associative Ring ^{1}

Michał Muzalewski Warsaw University Białystok

Wojciech Skaba University of Toruń

Summary. Notion of linear combination of vectors in Left Module over Associative Ring, defined as a function from the carrier of Left Module over Associative Ring to the carrier of this Ring. The following operations are included: addition, subtraction of combinations and multiplication of a combination by a scalar of the Ring. Following it, the sum of a finite set of vectors and the sum of linear combinations is defined. Many theorems are proved. This article originated as a generalization of the article [19].

MML Identifier: LMOD 4.

The articles [22], [7], [5], [3], [6], [8], [21], [17], [15], [16], [2], [4], [18], [20], [1], [9], [10], [11], [13], [12], and [14] provide the terminology and notation for this paper. For simplicity we follow a convention: R will be an associative ring, V will be a left module over R, a, b will be scalars of R, x will be arbitrary, i will be a natural number, u, v, v_{1}, v_{2}, v_{3} will be vectors of V, F, G will be finite sequences of elements of the carrier of the carrier of V, A, B will be subsets of V, and f will be a function from the carrier of the carrier of V into the carrier of R. Let D be a non-empty set. Then ∅_{D} is a subset of D.

Let us consider R, V. A subset of V is said to be a finite subset of V if: (Def.1) it is finite.

In the sequel S, T denote finite subsets of V. Let us consider R, V, S, T. Then S ∪ T is a finite subset of V. Then S ∩ T is a finite subset of V. Then S \ T is a finite subset of V. Then S− . T is a finite subset of V.

Let us consider R, V. The functor 0_{V} yields a finite subset of V and is defined as follows: (Def.2) 0_{V} = ∅.

1Supported by RPBP.III-24.C6

One can prove the following proposition (2)^{2} 0_{V} = ∅. Let us consider R, V, T. The functor ∑ T yields a vector of V and is defined

as follows: (Def.3) there exists F such that rng F = T and F is one-to-one and ∑ T = ∑ F.

One can prove the following two propositions:

(3) There exists F such that rng F = T and F is one-to-one and ∑ T = ∑ F.

(4) If rng F = T and F is one-to-one and v = ∑ F, then v = ∑ T. Let us consider R, V, v. Then {v} is a finite subset of V. Let us consider R, V, v_{1}, v_{2}. Then {v_{1}, v_{2}} is a finite subset of V. Let us consider R, V, v_{1}, v_{2}, v_{3}. Then {v_{1}, v_{2}, v_{3}} is a finite subset of V. We now state a number of propositions:

(5) ∑(0_{V}) = Θ_{V}.

(6) ∑{v} = v.

(7) If v_{1} ≠ v_{2}, then ∑{v_{1}, v_{2}} = v_{1} + v_{2}.

(8) If v_{1} ≠ v_{2} and v_{2} ≠ v_{3} and v_{1} ≠ v_{3}, then ∑{v_{1}, v_{2}, v_{3}} = v_{1} + v_{2} + v_{3}.

(9) If T misses S, then ∑(T ∪ S) = ∑ T + ∑ S.

(10) ∑(T ∪ S) = (∑ T + ∑ S) − ∑(T ∩ S).

(11) ∑(T ∩ S) = (∑ T + ∑ S) − ∑(T ∪ S).

(12) ∑(T \ S) = ∑(T ∪ S) − ∑ S.

(13) ∑(T \ S) = ∑ T − ∑(T ∩ S).

(14) ∑(T − . S) = ∑(T ∪ S) − ∑(T ∩ S).

(15) ∑(T − . S) = ∑(T \ S) + ∑(S \ T).

Let us consider R, V. An element of (the carrier of R)^{the carrier of the carrier of V} is called a linear combination of V if: (Def.4) there exists T such that for every v such that v ∉ T holds it(v) = 0_{R}.

In the sequel K, L, L_{1}, L_{2}, L_{3} are linear combinations of V. We now state the proposition

(16) There exists T such that for every v such that v ∉ T holds L(v) = 0_{R}. In the sequel E is an element of (the carrier of R)^{the carrier of the carrier of V}.

Next we state the proposition

(17) If there exists T such that for every v such that v ∉ T holds E(v) = 0_{R},

then E is a linear combination of V. Let us consider R, V, L. The functor support L yields a finite subset of V

and is defined as follows: (Def.5) support L = {v : L(v) ≠ 0_{R}}.

The following propositions are true:

2The proposition (1) was either repeated or obvious.

(18) support L = {v : L(v) ≠ 0_{R}}.

(19) x ∈ support L if and only if there exists v such that x = v and L(v) ≠ 0_{R}.

(20) L(v) = 0_{R} if and only if v ∉ support L.

Let us consider R, V. The functor 0_{LC_{V}} yielding a linear combination of V is defined by: (Def.6) support 0_{LC_{V}} = ∅.

We now state two propositions:

(21) L = 0_{LC_{V}} if and only if support L = ∅.

(22) 0_{LC_{V}} (v) = 0_{R}.

Let us consider R, V, A. A linear combination of V is called a linear combination of A if: (Def.7) support it ⊆ A.

We now state the proposition

(23) If support L ⊆ A, then L is a linear combination of A.

In the sequel l will denote a linear combination of A. We now state several propositions:

(24) support l ⊆ A.

(25) If A ⊆ B, then l is a linear combination of B.

(26) 0_{LC_{V}} is a linear combination of A.

(27) For every linear combination l of ∅_{the carrier of the carrier of V} holds l = 0_{LC_{V}}.

(28) L is a linear combination of support L.

Let us consider R, V, F, f. The functor fF yields a finite sequence of elements of the carrier of the carrier of V and is defined by: (Def.8) len(fF) = len F and for every i such that i ∈ dom(fF) holds (fF)(i) =

f(π_{i}F) · π_{i}F. We now state several propositions:

(29) len(fF) = len F.

(30) For every i such that i ∈ dom(fF) holds (fF)(i) = f(π_{i}F) · π_{i}F.

(31) If len G = len F and for every i such that i ∈ dom G holds G(i) = f(π_{i}F) · π_{i}F, then G = fF.

(32) If i ∈ dom F and v = F (i), then (fF)(i) = f(v) · v.

(33) fε_{the carrier of the carrier of V} = ε_{the carrier of the carrier of V}.

(34) f⟨v⟩ = ⟨f(v) · v⟩.

(35) f⟨v_{1}, v_{2}⟩ = ⟨f(v_{1}) · v_{1}, f(v_{2}) · v_{2}⟩.

(36) f⟨v_{1}, v_{2}, v_{3}⟩ = ⟨f(v_{1}) · v_{1}, f(v_{2}) · v_{2}, f(v_{3}) · v_{3}⟩.

(37) f(F ^{}G) = (fF)^{}(fG).

Let us consider R, V, L. The functor ∑ L yields a vector of V and is defined as follows:

(Def.9) there exists F such that F is one-to-one and rng F = support L and

∑ L = ∑(LF). The following propositions are true:

(38) There exists F such that F is one-to-one and rng F = support L and ∑ L = ∑(LF).

(39) If F is one-to-one and rng F = support L and u = ∑(LF), then u = ∑ L.

(40) If 0_{R} ≠ 1_{R}, then A ≠ ∅ and A is linearly closed if and only if for every l holds ∑ l ∈ A.

(41) ∑ 0_{LC_{V}} = Θ_{V}.

(42) For every linear combination l of ∅_{the carrier of the carrier of V} holds ∑ l = Θ_{V}.

(43) For every linear combination l of {v} holds ∑ l = l(v) · v.

(44) If v_{1} ≠ v_{2}, then for every linear combination l of {v_{1}, v_{2}} holds ∑ l = l(v_{1}) · v_{1} + l(v_{2}) · v_{2}.

(45) If support L = ∅, then ∑ L = Θ_{V}.

(46) If support L = {v}, then ∑ L = L(v) · v.

(47) If support L = {v_{1}, v_{2}} and v_{1} ≠ v_{2}, then ∑ L = L(v_{1}) · v_{1} + L(v_{2}) · v_{2}. Let us consider R, V, L_{1}, L_{2}. Let us note that one can characterize the

predicate L_{1} = L_{2} by the following (equivalent) condition: (Def.10) for every v holds L_{1}(v) = L_{2}(v).

Next we state the proposition

(48) If for every v holds L_{1}(v) = L_{2}(v), then L_{1} = L_{2}.

Let us consider R, V, L_{1}, L_{2}. The functor L_{1} + L_{2} yielding a linear combination of V is defined by:

(Def.11) for every v holds (L_{1} + L_{2})(v) = L_{1}(v) + L_{2}(v).

The following propositions are true:

(49) If for every v holds L(v) = L_{1}(v) + L_{2}(v), then L = L_{1} + L_{2}.

(50) (L_{1} + L_{2})(v) = L_{1}(v) + L_{2}(v).

(51) support(L_{1} + L_{2}) ⊆ support L_{1} ∪ support L_{2}.

(52) If L_{1} is a linear combination of A and L_{2} is a linear combination of A, then L_{1} + L_{2} is a linear combination of A.

(53) For every commutative ring R and for every left module V over R and for all linear combinations L_{1}, L_{2} of V holds L_{1} + L_{2} = L_{2} + L_{1}.

(54) L_{1} + (L_{2} + L_{3}) = L_{1} + L_{2} + L_{3}.

(55) For every commutative ring R and for every left module V over R and

for every linear combination L of V holds L+0_{LC_{V}} = L and 0_{LC_{V}} +L = L. Let us consider R, V, a, L. The functor a · L yielding a linear combination

of V is defined as follows: (Def.12) for every v holds (a · L)(v) = a · L(v).

One can prove the following propositions:

(56) If for every v holds K(v) = a · L(v), then K = a · L.

(57) (a · L)(v) = a · L(v).

(58) support(a · L) ⊆ support L.

In the sequel R_{1} denotes an integral domain, V_{1} denotes a left module over R_{1}, L_{4} denotes a linear combination of V_{1}, and a_{1} denotes a scalar of R_{1}. Next we state several propositions:

(59) If a_{1} ≠ 0_{R_{1}}, then support(a_{1} · L_{4}) = support L_{4}.

(60) 0_{R} · L = 0_{LC_{V}}.

(61) If L is a linear combination of A, then a · L is a linear combination of A.

(62) (a + b) · L = a · L + b · L.

(63) a · (L_{1} + L_{2}) = a · L_{1} + a · L_{2}.

(64) a · (b · L) = a · b · L.

(65) (1_{R}) · L = L.

Let us consider R, V, L. The functor −L yields a linear combination of V and is defined as follows:

(Def.13) −L = (−1_{R}) · L.

One can prove the following propositions:

(66) −L = (−1_{R}) · L.

(67) (−L)(v) = −L(v).

(68) If L_{1} + L_{2} = 0_{LC_{V}}, then L_{2} = −L_{1}.

(69) support −L = support L.

(70) If L is a linear combination of A, then −L is a linear combination of A.

(71) − − L = L.

Let us consider R, V, L_{1}, L_{2}. The functor L_{1}−L_{2} yields a linear combination of V and is defined by:

(Def.14) L_{1} − L_{2} = L_{1} + −L_{2}.

One can prove the following propositions:

(72) L_{1} − L_{2} = L_{1} + −L_{2}.

(73) (L_{1} − L_{2})(v) = L_{1}(v) − L_{2}(v).

(74) support(L_{1} − L_{2}) ⊆ support L_{1} ∪ support L_{2}.

(75) If L_{1} is a linear combination of A and L_{2} is a linear combination of A, then L_{1} − L_{2} is a linear combination of A.

(76) L − L = 0_{LC_{V}}.

(77) ∑(L_{1} + L_{2}) = ∑ L_{1} + ∑ L_{2}.

For simplicity we adopt the following convention: R will be an integral domain, V will be a left module over R, L, L_{1}, L_{2} will be linear combinations of V, and a will be a scalar of R. We now state three propositions:

(78) ∑(a · L) = a · ∑ L.

(79) ∑ −L = − ∑ L.

(80) ∑(L_{1} − L_{2}) = ∑ L_{1} − ∑ L_{2}.

References

[1] Grzegorz Bancerek. Cardinal numbers. Formalized Mathematics, 1(2):377–382, 1990.

[2] Grzegorz Bancerek. The fundamental properties of natural numbers. Formalized Mathematics, 1(1):41–46, 1990.

[3] Grzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite sequences. Formalized Mathematics, 1(1):107–114, 1990.

[4] Czesław Byliński. Binary operations. Formalized Mathematics, 1(1):175–180, 1990.

[5] Czesław Byliński. Functions and their basic properties. Formalized Mathematics, 1(1):55–65, 1990.

[6] Czesław Byliński. Functions from a set to a set. Formalized Mathematics, 1(1):153–164, 1990.

[7] Agata Darmochwał. Finite sets. Formalized Mathematics, 1(1):165–167, 1990.

[8] Krzysztof Hryniewiecki. Basic properties of real numbers. Formalized Mathematics, 1(1):35–40, 1990.

[9] Eugeniusz Kusak, Wojciech Leończuk, and Michał Muzalewski. Abelian groups, fields and vector spaces. Formalized Mathematics, 1(2):335–342, 1990.

[10] Michał Muzalewski. Construction of rings and left-, right-, and bi-modules over a ring. Formalized Mathematics, 2(1):3–11, 1991.

[11] Michał Muzalewski and Wojciech Skaba. Finite sums of vectors in left module over associative ring. Formalized Mathematics, 2(2):279–282, 1991.

[12] Michał Muzalewski and Wojciech Skaba. Operations on submodules in left module over associative ring. Formalized Mathematics, 2(2):289–293, 1991.

[13] Michał Muzalewski and Wojciech Skaba. Submodules and cosets of submodules in left module over associative ring. Formalized Mathematics, 2(2):283–287, 1991.

[14] Michał Muzalewski and Lesław W. Szczerba. Construction of finite sequences over ring and left-, right-, and bi-modules over a ring. Formalized Mathematics, 2(1):97–104, 1991.

[15] Andrzej Trybulec. Domains and their Cartesian products. Formalized Mathematics, 1(1):115–122, 1990.

[16] Andrzej Trybulec. Function domains and Frænkel operator. Formalized Mathematics, 1(3):495–500, 1990.

[17] Andrzej Trybulec. Tarski Grothendieck set theory. Formalized Mathematics, 1(1):9–11, 1990.

[18] Andrzej Trybulec and Czesław Byliński. Some properties of real numbers. Formalized Mathematics, 1(3):445–449, 1990.

[19] Wojciech A. Trybulec. Linear combinations in vector space. Formalized Mathematics, 1(5):877–882, 1990.

[20] Wojciech A. Trybulec. Pigeon hole principle. Formalized Mathematics, 1(3):575–579, 1990.

[21] Zinaida Trybulec. Properties of subsets. Formalized Mathematics, 1(1):67–71, 1990.

[22] Zinaida Trybulec and Halina Świe‘czkowska. Boolean properties of sets. Formalized Mathematics, 1(1):17–23, 1990.

Linear Independence in Left Module over Domain ^{1}

Michał Muzalewski Warsaw University Białystok

Wojciech Skaba University of Toruń

Summary. Notion of submodule generated by a set of vectors and linear independence of a set of vectors. A few theorems originated as a generalization of the theorems from the article [18].

MML Identifier: LMOD 5.

The articles [22], [5], [3], [2], [4], [6], [21], [16], [14], [15], [1], [17], [19], [20], [7], [8], [9], [12], [11], [10], and [13] provide the terminology and notation for this paper. For simplicity we adopt the following rules: x is arbitrary, R is an associative ring, V is a left module over R, v, v_{1}, v_{2} are vectors of V, A, B are subsets of V, and l is a linear combination of A. We now define two new predicates. Let us consider R, V, A. We say that A is linearly independent if and only if: (Def.1) for every l such that ∑ l = Θ_{V} holds support l = ∅. A is linearly dependent stands for A is not linearly independent.

One can prove the following propositions:

(2)^{2} If A ⊆ B and B is linearly independent, then A is linearly independent.

(3) If 0_{R} ≠ 1_{R} and A is linearly independent, then Θ_{V} ∉ A.

(4) ∅_{the carrier of the carrier of V} is linearly independent.

(5) If 0_{R} ≠ 1_{R} and {v_{1}, v_{2}} is linearly independent, then v_{1} ≠ Θ_{V} and v_{2} ≠ Θ_{V}.

(6) If 0_{R} ≠ 1_{R}, then {v, Θ_{V} } is linearly dependent and {Θ_{V} , v} is linearly dependent.

1Supported by RPBP.III-24.C6

2The proposition (1) was either repeated or obvious.

For simplicity we follow the rules: R will be an integral domain, V will be a left module over R, W will be a submodule of V, A, B will be subsets of V, and l will be a linear combination of A. Let us consider R, V, A. The functor Lin(A) yields a submodule of V and is defined as follows: (Def.2) the carrier of the carrier of Lin(A) = {∑ l}.

One can prove the following propositions:

(7) If the carrier of the carrier of W = {∑ l}, then W = Lin(A).

(8) The carrier of the carrier of Lin(A) = {∑ l}.

(9) x ∈ Lin(A) if and only if there exists l such that x = ∑ l.

(10) If x ∈ A, then x ∈ Lin(A).

We now state several propositions:

(11) Lin(∅_{the carrier of the carrier of V}) = 0_{V}.

(12) If Lin(A) = 0_{V}, then A = ∅ or A = {Θ_{V} }.

(13) If 0_{R} ≠ 1_{R} and A = the carrier of the carrier of W, then Lin(A) = W.

(14) If 0_{R} ≠ 1_{R} and A = the carrier of the carrier of V, then Lin(A) = V.

(15) If A ⊆ B, then Lin(A) is a submodule of Lin(B).

(16) If Lin(A) = V and A ⊆ B, then Lin(B) = V.

(17) Lin(A ∪ B) = Lin(A) + Lin(B).

(18) Lin(A ∩ B) is a submodule of Lin(A) ∩ Lin(B).

References

[1] Grzegorz Bancerek. The fundamental properties of natural numbers. Formalized Mathematics, 1(1):41–46, 1990.

[2] Grzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite sequences. Formalized Mathematics, 1(1):107–114, 1990.

[3] Czesław Byliński. Functions and their basic properties. Formalized Mathematics, 1(1):55–65, 1990.

[4] Czesław Byliński. Functions from a set to a set. Formalized Mathematics, 1(1):153–164, 1990.

[5] Agata Darmochwał. Finite sets. Formalized Mathematics, 1(1):165–167, 1990.

[6] Krzysztof Hryniewiecki. Basic properties of real numbers. Formalized Mathematics, 1(1):35–40, 1990.

[7] Eugeniusz Kusak, Wojciech Leończuk, and Michał Muzalewski. Abelian groups, fields and vector spaces. Formalized Mathematics, 1(2):335–342, 1990.

[8] Michał Muzalewski. Construction of rings and left-, right-, and bi-modules over a ring. Formalized Mathematics, 2(1):3–11, 1991.

[9] Michał Muzalewski and Wojciech Skaba. Finite sums of vectors in left module over associative ring. Formalized Mathematics, 2(2):279–282, 1991.

[10] Michał Muzalewski and Wojciech Skaba. Linear combinations in left module over associative ring. Formalized Mathematics, 2(2):295–300, 1991.

[11] Michał Muzalewski and Wojciech Skaba. Operations on submodules in left module over associative ring. Formalized Mathematics, 2(2):289–293, 1991.

[12] Michał Muzalewski and Wojciech Skaba. Submodules and cosets of submodules in left module over associative ring. Formalized Mathematics, 2(2):283–287, 1991.

[13] Michał Muzalewski and Lesław W. Szczerba. Construction of finite sequences over ring and left-, right-, and bi-modules over a ring. Formalized Mathematics, 2(1):97–104, 1991.

Linear Independence in Left Module over … 303

[14] Andrzej Trybulec. Domains and their Cartesian products. Formalized Mathematics, 1(1):115–122, 1990.

[15] Andrzej Trybulec. Function domains and Frænkel operator. Formalized Mathematics, 1(3):495–500, 1990.

[16] Andrzej Trybulec. Tarski Grothendieck set theory. Formalized Mathematics, 1(1):9–11, 1990.

[17] Andrzej Trybulec and Czesław Byliński. Some properties of real numbers. Formalized Mathematics, 1(3):445–449, 1990.

[18] Wojciech A. Trybulec. Basis of vector space. Formalized Mathematics, 1(5):883–885, 1990.

[19] Wojciech A. Trybulec. Partially ordered sets. Formalized Mathematics, 1(2):313–319, 1990.

[20] Wojciech A. Trybulec. Pigeon hole principle. Formalized Mathematics, 1(3):575–579, 1990.

[21] Zinaida Trybulec. Properties of subsets. Formalized Mathematics, 1(1):67–71, 1990.

[22] Zinaida Trybulec and Halina Świe‘czkowska. Boolean properties of sets. Formalized Mathematics, 1(1):17–23, 1990.

304

Calculus of Propositions ^{1}

Jan Popiołek Warsaw University Białystok Andrzej Trybulec Warsaw University Białystok

Summary. Continues the analysis of the classical language of first order (see [6], [1], [3], [4], [2]). Three connectives : truth, negation and conjuction are primary (see [6]). The others (alternative, implication and equivalence) are defined with respect to them (see [1]). We prove some important tautologies of the calculus of propositions. Most of them are given as axioms of the classical logical calculus (see [5]). In the last part of our article we give some basic rules of inference.

MML Identifier: PROCAL 1.

The notation and terminology used here have been introduced in the papers [3] and [4]. In the sequel p, q, r, s are elements of CQC−WFF. One can prove the following propositions:

(1) ¬(p ∧ ¬p) ∈ Taut.

(2) p ∨ ¬p ∈ Taut.

(3) p ⇒ p ∨ q ∈ Taut.

(4) q ⇒ p ∨ q ∈ Taut.

(5) p ∨ q ⇒ (¬p ⇒ q) ∈ Taut.

(6) ¬(p ∨ q) ⇒ ¬p ∧ ¬q ∈ Taut.

(7) ¬p ∧ ¬q ⇒ ¬(p ∨ q) ∈ Taut.

(8) p ∨ q ⇒ q ∨ p ∈ Taut.

(9) ¬p ∨ p ∈ Taut.

(10) ¬(p ∨ q) ⇒ ¬p ∈ Taut.

(11) p ∨ p ⇒ p ∈ Taut.

(12) p ⇒ p ∨ p ∈ Taut.

(13) p ∧ ¬p ⇒ q ∈ Taut.

(14) (p ⇒ q) ⇒ ¬p ∨ q ∈ Taut.

1Supported by RPBP.III-24

(15) p ∧ q ⇒ ¬(p ⇒ ¬q) ∈ Taut.

(16) ¬(p ⇒ ¬q) ⇒ p ∧ q ∈ Taut.

(17) ¬(p ∧ q) ⇒ ¬p ∨ ¬q ∈ Taut.

(18) ¬p ∨ ¬q ⇒ ¬(p ∧ q) ∈ Taut.

(19) p ∧ q ⇒ p ∈ Taut.

(20) p ∧ q ⇒ p ∨ q ∈ Taut.

(21) p ∧ q ⇒ q ∈ Taut.

(22) p ⇒ p ∧ p ∈ Taut.

(23) (p ⇔ q) ⇒ (p ⇒ q) ∈ Taut.

(24) (p ⇔ q) ⇒ (q ⇒ p) ∈ Taut.

(25) p ∨ q ∨ r ⇒ p ∨ (q ∨ r) ∈ Taut.

(26) p ∧ q ∧ r ⇒ p ∧ (q ∧ r) ∈ Taut.

(27) p ∨ (q ∨ r) ⇒ p ∨ q ∨ r ∈ Taut.

(28) p ⇒ (q ⇒ p ∧ q) ∈ Taut.

(29) (p ⇒ q) ⇒ ((q ⇒ p) ⇒ (p ⇔ q)) ∈ Taut.

(30) p ∨ q ⇔ q ∨ p ∈ Taut.

(31) (p ∧ q ⇒ r) ⇒ (p ⇒ (q ⇒ r)) ∈ Taut.

The following propositions are true:

(32) (p ⇒ (q ⇒ r)) ⇒ (p ∧ q ⇒ r) ∈ Taut.

(33) (r ⇒ p) ⇒ ((r ⇒ q) ⇒ (r ⇒ p ∧ q)) ∈ Taut.

(34) (p ∨ q ⇒ r) ⇒ (p ⇒ r) ∨ (q ⇒ r) ∈ Taut.

(35) (p ⇒ r) ⇒ ((q ⇒ r) ⇒ (p ∨ q ⇒ r)) ∈ Taut.

(36) (p ⇒ r) ∧ (q ⇒ r) ⇒ (p ∨ q ⇒ r) ∈ Taut.

(37) (p ⇒ q ∧ ¬q) ⇒ ¬p ∈ Taut.

(38) (p ∨ q) ∧ (p ∨ r) ⇒ p ∨ q ∧ r ∈ Taut.

(39) p ∧ (q ∨ r) ⇒ p ∧ q ∨ p ∧ r ∈ Taut.

(40) (p ∨ r) ∧ (q ∨ r) ⇒ p ∧ q ∨ r ∈ Taut.

(41) (p ∨ q) ∧ r ⇒ p ∧ r ∨ q ∧ r ∈ Taut.

(42) If p ∈ Taut, then p ∨ q ∈ Taut.

(43) If q ∈ Taut, then p ∨ q ∈ Taut.

(44) If p ∧ q ∈ Taut, then p ∈ Taut.

(45) If p ∧ q ∈ Taut, then q ∈ Taut.

(46) If p ∧ q ∈ Taut, then p ∨ q ∈ Taut.

(47) If p ∈ Taut and q ∈ Taut, then p ∧ q ∈ Taut.

(48) If p ⇒ q ∈ Taut, then p ∨ r ⇒ q ∨ r ∈ Taut.

(49) If p ⇒ q ∈ Taut, then r ∨ p ⇒ r ∨ q ∈ Taut.

(50) If p ⇒ q ∈ Taut, then r ∧ p ⇒ r ∧ q ∈ Taut.

(51) If p ⇒ q ∈ Taut, then p ∧ r ⇒ q ∧ r ∈ Taut.

(52) If r ⇒ p ∈ Taut and r ⇒ q ∈ Taut, then r ⇒ p ∧ q ∈ Taut.

Calculus of Propositions 307

(53) If p ⇒ r ∈ Taut and q ⇒ r ∈ Taut, then p ∨ q ⇒ r ∈ Taut.

(54) If p ∨ q ∈ Taut and ¬p ∈ Taut, then q ∈ Taut.

(55) If p ∨ q ∈ Taut and ¬q ∈ Taut, then p ∈ Taut.

(56) If p ⇒ q ∈ Taut and r ⇒ s ∈ Taut, then p ∧ r ⇒ q ∧ s ∈ Taut.

(57) If p ⇒ q ∈ Taut and r ⇒ s ∈ Taut, then p ∨ r ⇒ q ∨ s ∈ Taut.

(58) If p ∧ ¬q ⇒ ¬p ∈ Taut, then p ⇒ q ∈ Taut.

References

[1] Grzegorz Bancerek. Connectives and subformulae of the first order language. Formalized Mathematics, 1(3):451–458, 1990.

[2] Grzegorz Bancerek, Agata Darmochwał, and Andrzej Trybulec. Propositional calculus. Formalized Mathematics, 2(1):147–150, 1991.

[3] Czesław Byliński. A classical first order language. Formalized Mathematics, 1(4):669–676, 1990.

[4] Agata Darmochwał. A first–order predicate calculus. Formalized Mathematics, 1(4):689– 695, 1990.

[5] Andrzej Grzegorczyk. Zarys logiki matematycznej. PWN, Warsaw, 1973.

[6] Piotr Rudnicki and Andrzej Trybulec. A first order language. Formalized Mathematics, 1(2):303–311, 1990.

308

Calculus of Quantifiers. Deduction Theorem

Agata Darmochwał Warsaw Uniwersity Białystok

Summary. Some tautologies of the Classical Quantifier Calculus. The deduction theorem is also proved.

MML Identifier: CQC THE2.

The papers [11], [13], [8], [2], [5], [3], [12], [10], [9], [1], [6], [4], and [7] provide the terminology and notation for this paper. For simplicity we adopt the following convention: X will denote a subset of CQC−WFF, F, G, p, q, r will denote elements of CQC−WFF, s, h will denote formulae, and x, y will denote bound variables. Next we state a number of propositions:

(1) If ⊢ p ⇒ (q ⇒ r), then ⊢ p ∧ q ⇒ r.

(2) If ⊢ p ⇒ (q ⇒ r), then ⊢ q ∧ p ⇒ r.

(3) If ⊢ p ∧ q ⇒ r, then ⊢ p ⇒ (q ⇒ r).

(4) If ⊢ p ∧ q ⇒ r, then ⊢ q ⇒ (p ⇒ r).

(5) y ∈ snb(∀_{x}s) if and only if y ∈ snb(s) and y ≠ x.

(6) y ∈ snb(∃_{x}s) if and only if y ∈ snb(s) and y ≠ x.

(7) y ∈ snb(s ⇒ h) if and only if y ∈ snb(s) or y ∈ snb(h).

(8) y ∈ snb(¬s) if and only if y ∈ snb(s).

(9) y ∈ snb(s ∧ h) if and only if y ∈ snb(s) or y ∈ snb(h).

(10) y ∈ snb(s ∨ h) if and only if y ∈ snb(s) or y ∈ snb(h).

(11) x ∉ snb(∀_{x,y}s) and y ∉ snb(∀_{x,y}s).

(12) x ∉ snb(∃_{x,y}s) and y ∉ snb(∃_{x,y}s).

(13) If F is closed, then x ∉ snb(F).

(14) s ⇒ h(x) = (s(x)) ⇒ (h(x)).

(15) s ∨ h(x) = (s(x)) ∨ (h(x)).

(16) ∃_{x}p(x) = ∃_{x}p.

(17) If x ≠ y, then ∃_{x}p(y) = ∃_{x}(p(y)).

(18) ⊢ p ⇒ ∃_{x}p.

(19) If ⊢ p, then ⊢ ∃_{x}p.

(20) ⊢ ∀_{x}p ⇒ ∃_{x}p.

(21) ⊢ ∀_{x}p ⇒ ∃_{y}p.

(22) If ⊢ p ⇒ q and x ∉ snb(q), then ⊢ (∃_{x}p) ⇒ q.

(23) If x ∉ snb(p), then ⊢ (∃_{x}p) ⇒ p.

(24) If x ∉ snb(p) and ⊢ ∃_{x}p, then ⊢ p.

(25) If p = h(x) and q = h(y) and y ∉ snb(h), then ⊢ p ⇒ ∃_{y}q.

(26) If ⊢ p, then ⊢ ∀_{x}p.

(27) If x ∉ snb(p), then ⊢ p ⇒ ∀_{x}p.

(28) If p = h(x) and q = h(y) and x ∉ snb(h), then ⊢ ∀_{x}p ⇒ q.

(29) If y ∉ snb(p), then ⊢ ∀_{x}p ⇒ ∀_{y}p.

(30) If p = h(x) and q = h(y) and x ∉ snb(h) and y ∉ snb(p), then ⊢ ∀_{x}p ⇒ ∀_{y}q.

(31) If x ∉ snb(p), then ⊢ (∃_{x}p) ⇒ ∃_{y}p.

One can prove the following propositions:

(32) If p = h(x) and q = h(y) and x ∉ snb(q) and y ∉ snb(h), then ⊢ (∃_{x}p) ⇒ ∃_{y}q.

(34)^{1} ⊢ ∀_{x}(p ⇒ q) ⇒ (∀_{x}p ⇒ ∀_{x}q).

(35) If ⊢ ∀_{x}(p ⇒ q), then ⊢ ∀_{x}p ⇒ ∀_{x}q.

(36) ⊢ ∀_{x}(p ⇔ q) ⇒ (∀_{x}p ⇔ ∀_{x}q).

(37) If ⊢ ∀_{x}(p ⇔ q), then ⊢ ∀_{x}p ⇔ ∀_{x}q.

(38) ⊢ ∀_{x}(p ⇒ q) ⇒ ((∃_{x}p) ⇒ ∃_{x}q).

(39) If ⊢ ∀_{x}(p ⇒ q), then ⊢ (∃_{x}p) ⇒ ∃_{x}q.

(40) ⊢ ∀_{x}(p ∧ q) ⇒ ∀_{x}p ∧ ∀_{x}q and ⊢ ∀_{x}p ∧ ∀_{x}q ⇒ ∀_{x}(p ∧ q).

(41) ⊢ ∀_{x}(p ∧ q) ⇔ ∀_{x}p ∧ ∀_{x}q.

(42) ⊢ ∀_{x}(p ∧ q) if and only if ⊢ ∀_{x}p ∧ ∀_{x}q.

(43) ⊢ ∀_{x}p ∨ ∀_{x}q ⇒ ∀_{x}(p ∨ q).

(44) ⊢ (∃_{x}p ∨ q) ⇒ (∃_{x}p) ∨ ∃_{x}q and ⊢ (∃_{x}p) ∨ ∃_{x}q ⇒ ∃_{x}p ∨ q.

(45) ⊢ (∃_{x}p ∨ q) ⇔ (∃_{x}p) ∨ ∃_{x}q.

(46) ⊢ ∃_{x}p ∨ q if and only if ⊢ (∃_{x}p) ∨ ∃_{x}q.

(47) ⊢ (∃_{x}p ∧ q) ⇒ (∃_{x}p) ∧ ∃_{x}q.

(48) If ⊢ ∃_{x}p ∧ q, then ⊢ (∃_{x}p) ∧ ∃_{x}q.

(49) ⊢ ∀_{x}¬¬p ⇒ ∀_{x}p and ⊢ ∀_{x}p ⇒ ∀_{x}¬¬p.

(50) ⊢ ∀_{x}¬¬p ⇔ ∀_{x}p.

(51) ⊢ (∃_{x}¬¬p) ⇒ ∃_{x}p and ⊢ (∃_{x}p) ⇒ ∃_{x}¬¬p.

1The proposition (33) was either repeated or obvious.

(52) ⊢ (∃_{x}¬¬p) ⇔ ∃_{x}p.

(53) ⊢ ¬∃_{x}¬p ⇒ ∀_{x}p and ⊢ ∀_{x}p ⇒ ¬∃_{x}¬p.

(54) ⊢ ¬∃_{x}¬p ⇔ ∀_{x}p.

(55) ⊢ ¬∀_{x}p ⇒ ∃_{x}¬p and ⊢ (∃_{x}¬p) ⇒ ¬∀_{x}p.

(56) ⊢ ¬∀_{x}p ⇔ ∃_{x}¬p.

(57) ⊢ ¬∃_{x}p ⇒ ∀_{x}¬p and ⊢ ∀_{x}¬p ⇒ ¬∃_{x}p.

(58) ⊢ ∀_{x}¬p ⇔ ¬∃_{x}p.

(59) ⊢ ∀_{x}∀_{y}p ⇒ ∀_{y}∀_{x}p and ⊢ ∀_{x,y}p ⇒ ∀_{y,x}p.

(60) If p = h(x) and q = h(y) and y ∉ snb(h), then ⊢ ∀_{x}∀_{y}q ⇒ ∀_{x}p.

(61) ⊢ (∃_{x}∃_{y}p) ⇒ ∃_{y}∃_{x}p and ⊢ (∃_{x,y}p) ⇒ (∃_{y,x}p).

(62) If p = h(x) and q = h(y) and y ∉ snb(h), then ⊢ (∃_{x}p) ⇒ (∃_{x,y}q). We now state a number of propositions:

(63) ⊢ (∃_{x}∀_{y}p) ⇒ ∀_{y}∃_{x}p.

(64) ⊢ ∃_{x}p ⇔ p.

(65) ⊢ (∃_{x}p ⇒ q) ⇒ (∀_{x}p ⇒ ∃_{x}q) and ⊢ (∀_{x}p ⇒ ∃_{x}q) ⇒ ∃_{x}p ⇒ q.

(66) ⊢ (∃_{x}p ⇒ q) ⇔ (∀_{x}p ⇒ ∃_{x}q).

(67) ⊢ ∃_{x}p ⇒ q if and only if ⊢ ∀_{x}p ⇒ ∃_{x}q.

(68) ⊢ ∀_{x}(p ∧ q) ⇒ p ∧ ∀_{x}q.

(69) ⊢ ∀_{x}(p ∧ q) ⇒ ∀_{x}p ∧ q.

(70) If x ∉ snb(p), then ⊢ p ∧ ∀_{x}q ⇒ ∀_{x}(p ∧ q).

(71) If x ∉ snb(p) and ⊢ p ∧ ∀_{x}q, then ⊢ ∀_{x}(p ∧ q).

(72) If x ∉ snb(p), then ⊢ p ∨ ∀_{x}q ⇒ ∀_{x}(p ∨ q) and ⊢ ∀_{x}(p ∨ q) ⇒ p ∨ ∀_{x}q.

(73) If x ∉ snb(p), then ⊢ p ∨ ∀_{x}q ⇔ ∀_{x}(p ∨ q).

(74) If x ∉ snb(p), then ⊢ p ∨ ∀_{x}q if and only if ⊢ ∀_{x}(p ∨ q).

(75) If x ∉ snb(p), then ⊢ p ∧ ∃_{x}q ⇒ ∃_{x}p ∧ q and ⊢ (∃_{x}p ∧ q) ⇒ p ∧ ∃_{x}q.

(76) If x ∉ snb(p), then ⊢ p ∧ ∃_{x}q ⇔ ∃_{x}p ∧ q.

(77) If x ∉ snb(p), then ⊢ p ∧ ∃_{x}q if and only if ⊢ ∃_{x}p ∧ q.

(78) If x ∉ snb(p), then ⊢ ∀_{x}(p ⇒ q) ⇒ (p ⇒ ∀_{x}q) and ⊢ (p ⇒ ∀_{x}q) ⇒ ∀_{x}(p ⇒ q).

(79) If x ∉ snb(p), then ⊢ (p ⇒ ∀_{x}q) ⇔ ∀_{x}(p ⇒ q).

(80) If x ∉ snb(p), then ⊢ ∀_{x}(p ⇒ q) if and only if ⊢ p ⇒ ∀_{x}q.

(81) If x ∉ snb(q), then ⊢ (∃_{x}p ⇒ q) ⇒ (∀_{x}p ⇒ q).

(82) ⊢ (∀_{x}p ⇒ q) ⇒ ∃_{x}p ⇒ q.

(83) If x ∉ snb(q), then ⊢ ∀_{x}p ⇒ q if and only if ⊢ ∃_{x}p ⇒ q.

(84) If x ∉ snb(q), then ⊢ ((∃_{x}p) ⇒ q) ⇒ ∀_{x}(p ⇒ q) and ⊢ ∀_{x}(p ⇒ q) ⇒ ((∃_{x}p) ⇒ q).

(85) If x ∉ snb(q), then ⊢ ((∃_{x}p) ⇒ q) ⇔ ∀_{x}(p ⇒ q).

(86) If x ∉ snb(q), then ⊢ (∃_{x}p) ⇒ q if and only if ⊢ ∀_{x}(p ⇒ q).

(87) If x ∉ snb(p), then ⊢ (∃_{x}p ⇒ q) ⇒ (p ⇒ ∃_{x}q).

312 Agata Darmochwał

(88) ⊢ (p ⇒ ∃_{x}q) ⇒ ∃_{x}p ⇒ q.

(89) If x ∉ snb(p), then ⊢ (p ⇒ ∃_{x}q) ⇔ ∃_{x}p ⇒ q.

(90) If x ∉ snb(p), then ⊢ p ⇒ ∃_{x}q if and only if ⊢ ∃_{x}p ⇒ q.

(91) {p} ⊢ p.

(92) Cn({p} ∪ {q}) = Cn{p ∧ q}.

(93) {p, q} ⊢ r if and only if {p ∧ q} ⊢ r.

The following propositions are true:

(94) If X ⊢ p, then X ⊢ ∀_{x}p.

(95) If x ∉ snb(p), then X ⊢ ∀_{x}(p ⇒ q) ⇒ (p ⇒ ∀_{x}q).

(96) If F is closed and X ∪ {F } ⊢ G, then X ⊢ F ⇒ G.

References

[1] Grzegorz Bancerek. Connectives and subformulae of the first order language. Formalized Mathematics, 1(3):451–458, 1990.

[2] Grzegorz Bancerek. The fundamental properties of natural numbers. Formalized Mathematics, 1(1):41–46, 1990.

[3] Grzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite sequences. Formalized Mathematics, 1(1):107–114, 1990.

[4] Czesław Byliński. A classical first order language. Formalized Mathematics, 1(4):669– 676, 1990.

[5] Czesław Byliński. Functions and their basic properties. Formalized Mathematics, 1(1):55–65, 1990.

[6] Czesław Byliński and Grzegorz Bancerek. Variables in formulae of the first order language. Formalized Mathematics, 1(3):459–469, 1990.

[7] Agata Darmochwał. A first–order predicate calculus. Formalized Mathematics, 1(4):689– 695, 1990.

[8] Krzysztof Hryniewiecki. Basic properties of real numbers. Formalized Mathematics, 1(1):35–40, 1990.

[9] Piotr Rudnicki and Andrzej Trybulec. A first order language. Formalized Mathematics, 1(2):303–311, 1990.

[10] Andrzej Trybulec. Domains and their Cartesian products. Formalized Mathematics, 1(1):115–122, 1990.

[11] Andrzej Trybulec. Tarski Grothendieck set theory. Formalized Mathematics, 1(1):9–11, 1990.

[12] Andrzej Trybulec. Tuples, projections and Cartesian products. Formalized Mathematics, 1(1):97–105, 1990.

[13] Zinaida Trybulec. Properties of subsets. Formalized Mathematics, 1(1):67–71, 1990.

Calculus of Quantifiers. Deduction Theorem 313

alalalalalal alalalalalalal

Index of MML Identifiers

AFVECT01 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 233 CQC THE2 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 309 HESSENBE . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 217 INCPROJ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 225 LMOD 1 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .279 LMOD 2 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .283 LMOD 3 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .289 LMOD 4 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .295 LMOD 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .301 MCART 2 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 255 MCART 3 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 259 MEASURE1 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 263 METRIC 2 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 205 METRIC 3 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 193 MOD 1 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .275 MULTOP 1 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 221 NORMFORM . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 237 O RING 1 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 243 O RING 2 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 247 O RING 3 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 251 POWER . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 213 PROCAL 1 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 305 PROJRED1 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 271 SUB METR . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 199

Contents Form. Math. 2 (2)

Metrics in Cartesian Product

By Stanisława Kanas and Jan Stankiewicz . . . . . . . . . . . . . . 193

Submetric Spaces - Part I

By Adam Lecko and Mariusz Startek . . . . . . . . . . . . . . . . . . . . 199

On Pseudometric Spaces

By Adam Lecko and Mariusz Startek . . . . . . . . . . . . . . . . . . . . 205

Real Exponents and Logarithms

By Konrad Raczkowski and Andrzej Ne‘dzusiak . . . . . . . 213

Hessenberg Theorem

By Eugeniusz Kusak and Wojciech Leończuk . . . . . . . . . . . 217

Three-Argument Operations and Four-Argument Operations

By Michal Muzalewski and Wojciech Skaba . . . . . . . . . . . . 221

Incidence Projective Spaces

By Wojciech Leończuk et al. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 225

One-Dimensional Congruence of Segments, Basic Facts and Midpoint Relation

By Barbara Konstanta et al. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 233

Algebra of Normal Forms

By Andrzej Trybulec . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 237

Ordered Rings - Part I

By Michał Muzalewski et al. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 243

Ordered Rings - Part II

By Michał Muzalewski et al. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 247

Ordered Rings - Part III

By Michał Muzalewski et al. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 251

Continued on inside back cover

N-Tuples and Cartesian Products for n=5

By Michał Muzalewski and Wojciech Skaba . . . . . . . . . . . . 255

Ternary Fields

By Michał Muzalewski and Wojciech Skaba . . . . . . . . . . . . 259

The σ-additive Measure Theory

By Józef Białas . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 263

Incidence Projective Space (a reduction theorem in a plane)

By Eugeniusz Kusak and Wojciech Leończuk . . . . . . . . . . . 271

Groups, Rings, Left- and Right-Modules

By Michał Muzalewski and Wojciech Skaba . . . . . . . . . . . . 275

Finite Sums of Vectors in Left Module over Associative Ring

By Michał Muzalewski and Wojciech Skaba . . . . . . . . . . . . 279

Submodules and Cosets of Submodules in Left Module over Associative Ring

By Michał Muzalewski and Wojciech Skaba . . . . . . . . . . . . 283

Operations on Submodules in Left Module over Associative Ring

By Michał Muzalewski and Wojciech Skaba . . . . . . . . . . . . 289

Linear Combinations in Left Module over Associative Ring

By Michał Muzalewski and Wojciech Skaba . . . . . . . . . . . . 295

Linear Independence in Left Module over Domain

By Michał Muzalewski and Wojciech Skaba . . . . . . . . . . . . 301

Calculus of Propositions

By Jan Popiołek and Andrzej Trybulec . . . . . . . . . . . . . . . . . 305

Calculus of Quantifiers. Deduction Theorem

By Agata Darmochwał . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 309

Index of MML Identifiers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 314