let F be preordered Field; for P being Preordering of F
for a being Element of F st not - a in P holds
P + (a * P) is Preordering of F
let P be Preordering of F; for a being Element of F st not - a in P holds
P + (a * P) is Preordering of F
let a be Element of F; ( not - a in P implies P + (a * P) is Preordering of F )
assume ASS:
not - a in P
; P + (a * P) is Preordering of F
X:
( 0. F in P & 1. F in P & P + P c= P & P * P c= P & P /\ (- P) = {(0. F)} & SQ F c= P )
by REALALG1:25, REALALG1:def 14;
set S = P + (a * P);
A:
(P + (a * P)) + (P + (a * P)) c= P + (a * P)
proof
let o be
object ;
TARSKI:def 3 ( not o in (P + (a * P)) + (P + (a * P)) or o in P + (a * P) )
assume
o in (P + (a * P)) + (P + (a * P))
;
o in P + (a * P)
then consider c,
b being
Element of
F such that H1:
(
o = c + b &
c in P + (a * P) &
b in P + (a * P) )
;
consider c1,
c2 being
Element of
F such that H2:
(
c = c1 + c2 &
c1 in P &
c2 in a * P )
by H1;
consider b1,
b2 being
Element of
F such that H3:
(
b = b1 + b2 &
b1 in P &
b2 in a * P )
by H1;
consider c3 being
Element of
F such that H4:
(
c2 = a * c3 &
c3 in P )
by H2;
consider b3 being
Element of
F such that H5:
(
b2 = a * b3 &
b3 in P )
by H3;
H6:
c3 + b3 in P + P
by H4, H5;
c2 + b2 = a * (c3 + b3)
by H4, H5, VECTSP_1:def 3;
then H7:
c2 + b2 in a * P
by H6, X;
H8:
c1 + b1 in P + P
by H3, H2;
(c1 + b1) + (c2 + b2) =
((c1 + b1) + c2) + b2
by RLVECT_1:def 3
.=
((c1 + c2) + b1) + b2
by RLVECT_1:def 3
.=
o
by H1, H2, H3, RLVECT_1:def 3
;
hence
o in P + (a * P)
by H8, H7, X;
verum
end;
B:
(P + (a * P)) * (P + (a * P)) c= P + (a * P)
proof
let o be
object ;
TARSKI:def 3 ( not o in (P + (a * P)) * (P + (a * P)) or o in P + (a * P) )
assume
o in (P + (a * P)) * (P + (a * P))
;
o in P + (a * P)
then consider c,
b being
Element of
F such that H1:
(
o = c * b &
c in P + (a * P) &
b in P + (a * P) )
;
consider c1,
c2 being
Element of
F such that H2:
(
c = c1 + c2 &
c1 in P &
c2 in a * P )
by H1;
consider b1,
b2 being
Element of
F such that H3:
(
b = b1 + b2 &
b1 in P &
b2 in a * P )
by H1;
consider c3 being
Element of
F such that H4:
(
c2 = a * c3 &
c3 in P )
by H2;
consider b3 being
Element of
F such that H5:
(
b2 = a * b3 &
b3 in P )
by H3;
H6:
o =
(c1 * (b1 + (a * b3))) + ((a * c3) * (b1 + (a * b3)))
by H1, H2, H3, H4, H5, VECTSP_1:def 3
.=
((c1 * b1) + (c1 * (a * b3))) + ((a * c3) * (b1 + (a * b3)))
by VECTSP_1:def 2
.=
((c1 * b1) + (c1 * (a * b3))) + (((a * c3) * b1) + ((a * c3) * (a * b3)))
by VECTSP_1:def 2
.=
(c1 * b1) + ((c1 * (a * b3)) + (((a * c3) * b1) + ((a * c3) * (a * b3))))
by RLVECT_1:def 3
.=
(c1 * b1) + (((c1 * (a * b3)) + ((a * c3) * b1)) + ((a * c3) * (a * b3)))
by RLVECT_1:def 3
.=
(c1 * b1) + (((a * (c1 * b3)) + ((a * c3) * b1)) + ((a * c3) * (a * b3)))
by GROUP_1:def 3
.=
(c1 * b1) + (((a * (c1 * b3)) + (a * (c3 * b1))) + ((a * c3) * (a * b3)))
by GROUP_1:def 3
.=
(c1 * b1) + ((a * ((c1 * b3) + (c3 * b1))) + ((a * c3) * (a * b3)))
by VECTSP_1:def 2
.=
(c1 * b1) + ((a * ((c1 * b3) + (c3 * b1))) + (((a * c3) * a) * b3))
by GROUP_1:def 3
.=
(c1 * b1) + ((a * ((c1 * b3) + (c3 * b1))) + (((a * a) * c3) * b3))
by GROUP_1:def 3
.=
(c1 * b1) + ((a * ((c1 * b3) + (c3 * b1))) + ((a * a) * (c3 * b3)))
by GROUP_1:def 3
.=
((c1 * b1) + ((a * a) * (c3 * b3))) + (a * ((c1 * b3) + (c3 * b1)))
by RLVECT_1:def 3
;
E1:
c1 * b1 in { (c * b) where c, b is Element of F : ( c in P & b in P ) }
by H2, H3;
E2:
c3 * b3 in { (c * b) where c, b is Element of F : ( c in P & b in P ) }
by H4, H5;
a * a =
(a |^ 1) * a
by BINOM:8
.=
(a |^ 1) * (a |^ 1)
by BINOM:8
.=
a |^ (1 + 1)
by BINOM:10
.=
a ^2
by RING_5:3
;
then
a * a in P
by REALALG1:23;
then
(a * a) * (c3 * b3) in { (c * b) where c, b is Element of F : ( c in P & b in P ) }
by E2, X;
then E3:
(c1 * b1) + ((a * a) * (c3 * b3)) in { (c1 + c2) where c1, c2 is Element of F : ( c1 in P & c2 in P ) }
by X, E1;
E4:
c1 * b3 in { (c * b) where c, b is Element of F : ( c in P & b in P ) }
by H2, H5;
c3 * b1 in { (c * b) where c, b is Element of F : ( c in P & b in P ) }
by H4, H3;
then
(c1 * b3) + (c3 * b1) in { (c1 + c2) where c1, c2 is Element of F : ( c1 in P & c2 in P ) }
by X, E4;
then
a * ((c1 * b3) + (c3 * b1)) in a * P
by X;
hence
o in P + (a * P)
by H6, E3, X;
verum
end;
P c= P + (a * P)
by X, P1;
then C:
SQ F c= P + (a * P)
by X;
now not - (1. F) in P + (a * P)assume
- (1. F) in P + (a * P)
;
contradictionthen consider c1,
c2 being
Element of
F such that H2:
(
- (1. F) = c1 + c2 &
c1 in P &
c2 in a * P )
;
consider c3 being
Element of
F such that H3:
(
c2 = a * c3 &
c3 in P )
by H2;
0. F =
(c1 + (a * c3)) + (1. F)
by H2, H3, RLVECT_1:5
.=
(c1 + (1. F)) + (a * c3)
by RLVECT_1:def 3
;
then H4:
- (a * c3) =
((c1 + (1. F)) + (a * c3)) - (a * c3)
.=
(c1 + (1. F)) + ((a * c3) + (- (a * c3)))
by RLVECT_1:def 3
.=
(c1 + (1. F)) + (0. F)
by RLVECT_1:5
;
c3 <> 0. F
by H2, H3, REALALG1:26;
then
(c3 ") * c3 = 1. F
by VECTSP_1:def 10;
then H5:
- a =
(- a) * (c3 * (c3 "))
.=
((- a) * c3) * (c3 ")
by GROUP_1:def 3
.=
(c1 + (1. F)) * (c3 ")
by H4, VECTSP_1:9
;
H:
c1 + (1. F) in { (c1 + c2) where c1, c2 is Element of F : ( c1 in P & c2 in P ) }
by H2, X;
not
c3 is
zero
by H2, H3, REALALG1:26;
then
c3 " in P
by H3, REALALG1:27;
then
- a in { (c1 * c2) where c1, c2 is Element of F : ( c1 in P & c2 in P ) }
by H5, H, X;
hence
contradiction
by ASS, X;
verum end;
then
(P + (a * P)) /\ (- (P + (a * P))) = {(0. F)}
by C, B, REALALG1:21;
hence
P + (a * P) is Preordering of F
by A, B, C, REALALG1:def 14; verum