Journal of Formalized Mathematics
Volume 1, 1989
University of Bialystok
Copyright (c) 1989 Association of Mizar Users

## Construction of a bilinear symmetric form in orthogonal vector space

Eugeniusz Kusak
Warsaw University, Bialystok
Wojciech Leonczuk
Warsaw University, Bialystok
Michal Muzalewski
Warsaw University, Bialystok

### Summary.

In this text we present unpublished results by Eu\-ge\-niusz Ku\-sak and Wojciech Leo\'nczuk. They contain an axiomatic description of the class of all spaces $\langle V$; $\perp_\xi \rangle$, where $V$ is a vector space over a field F, $\xi: V \times V \to F$ is a bilinear symmetric form i.e. $\xi(x,y) = \xi(y,x)$ and $x \perp_\xi y$ iff $\xi(x,y) = 0$ for $x$, $y \in V$. They also contain an effective construction of bilinear symmetric form $\xi$ for given orthogonal space $\langle V$; $\perp \rangle$ such that $\perp = \perp_\xi$. The basic tool used in this method is the notion of orthogonal projection J$(a,b,x)$ for $a,b,x \in V$. We should stress the fact that axioms of orthogonal and symplectic spaces differ only by one axiom, namely: $x\perp y+\varepsilon z \>\&\> y\perp z+\varepsilon x \Rightarrow z\perp x+\varepsilon y.$ For $\varepsilon=-1$ we get the axiom on three perpendiculars characterizing orthogonal geometry. For $\varepsilon=+1$ we get the axiom characterizing symplectic geometry - see [5].

Supported by RPBP.III-24.C6.

#### MML Identifier: ORTSP_1

The terminology and notation used in this paper have been introduced in the following articles [6] [3] [8] [1] [2] [7] [4] [9] [5]

Contents (PDF format)

#### Bibliography

[1] Czeslaw Bylinski. Functions and their basic properties. Journal of Formalized Mathematics, 1, 1989.
[2] Czeslaw Bylinski. Functions from a set to a set. Journal of Formalized Mathematics, 1, 1989.
[3] Czeslaw Bylinski. Some basic properties of sets. Journal of Formalized Mathematics, 1, 1989.
[4] Eugeniusz Kusak, Wojciech Leonczuk, and Michal Muzalewski. Abelian groups, fields and vector spaces. Journal of Formalized Mathematics, 1, 1989.
[5] Eugeniusz Kusak, Wojciech Leonczuk, and Michal Muzalewski. Construction of a bilinear antisymmetric form in symplectic vector space. Journal of Formalized Mathematics, 1, 1989.
[6] Andrzej Trybulec. Tarski Grothendieck set theory. Journal of Formalized Mathematics, Axiomatics, 1989.
[7] Wojciech A. Trybulec. Vectors in real linear space. Journal of Formalized Mathematics, 1, 1989.
[8] Zinaida Trybulec. Properties of subsets. Journal of Formalized Mathematics, 1, 1989.
[9] Edmund Woronowicz. Relations defined on sets. Journal of Formalized Mathematics, 1, 1989.