let R be preordered domRing; for P being Preordering of R
for a, b being b1 -ordered Element of R holds abs (P,(a + b)) <= P,(abs (P,a)) + (abs (P,b))
let P be Preordering of R; for a, b being P -ordered Element of R holds abs (P,(a + b)) <= P,(abs (P,a)) + (abs (P,b))
let a, b be P -ordered Element of R; abs (P,(a + b)) <= P,(abs (P,a)) + (abs (P,b))
A1:
0. R <= P, abs (P,b)
by av0;
(0. R) + (abs (P,b)) <= P,(abs (P,a)) + (abs (P,b))
by c4, av0;
then A:
0. R <= P,(abs (P,a)) + (abs (P,b))
by c3, A1;
per cases
( not a + b is P -ordered or a + b is P -ordered )
;
suppose AS1:
a + b is
P -ordered
;
abs (P,(a + b)) <= P,(abs (P,a)) + (abs (P,b))now not (abs (P,a)) + (abs (P,b)) is P -negative assume
(abs (P,a)) + (abs (P,b)) is
P -negative
;
contradictionthen
- (0. R) < P,
- ((abs (P,a)) + (abs (P,b)))
by x2, c10;
then
(0. R) + ((abs (P,a)) + (abs (P,b))) < P,
(- ((abs (P,a)) + (abs (P,b)))) + ((abs (P,a)) + (abs (P,b)))
by c4, RLVECT_1:8;
then
(0. R) + (0. R) < P,
((abs (P,a)) + (abs (P,b))) + (- ((abs (P,a)) + (abs (P,b))))
by A, c2, c3;
hence
contradiction
by RLVECT_1:5;
verum end; then A1:
(
(abs (P,a)) + (abs (P,b)) is
P -ordered & not
(abs (P,a)) + (abs (P,b)) is
P -negative )
by A, XBOOLE_0:def 3;
B:
- ((abs (P,a)) + (abs (P,b))) <= P,
a + b
proof
- (abs (P,a)) <= P,
a
by ineq2;
then
(- (abs (P,a))) + (- (abs (P,b))) <= P,
a + (- (abs (P,b)))
by c4;
then B1:
- ((abs (P,a)) + (abs (P,b))) <= P,
a + (- (abs (P,b)))
by RLVECT_1:31;
- (abs (P,b)) <= P,
b
by ineq2;
then
a + (- (abs (P,b))) <= P,
a + b
by c4;
hence
- ((abs (P,a)) + (abs (P,b))) <= P,
a + b
by B1, c3;
verum
end; B1:
a + (abs (P,b)) <= P,
(abs (P,a)) + (abs (P,b))
by c4, ineq2;
a + b <= P,
(abs (P,a)) + (abs (P,b))
hence
abs (
P,
(a + b))
<= P,
(abs (P,a)) + (abs (P,b))
by AS1, A1, B, ineq1;
verum end; end;