let R be non degenerated preordered Ring; for P being Preordering of R
for a, b being b1 -ordered Element of R holds abs (P,(a * b)) = (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)) = (abs (P,a)) * (abs (P,b))
let a, b be P -ordered Element of R; abs (P,(a * b)) = (abs (P,a)) * (abs (P,b))
AS:
( a in P \/ (- P) & b in P \/ (- P) )
by defppp;
X:
P * P c= P
by REALALG1:def 14;
Y:
( (- P) * P c= - P & P * (- P) c= - P )
by v2;
Z:
(- P) * (- P) c= P
by v1;
per cases
( a in P or a in - P )
by AS, XBOOLE_0:def 3;
suppose A:
a in P
;
abs (P,(a * b)) = (abs (P,a)) * (abs (P,b))per cases
( b in P or b in - P )
by AS, XBOOLE_0:def 3;
suppose A1:
b in - P
;
abs (P,(a * b)) = (abs (P,a)) * (abs (P,b))then B:
(
abs (
P,
a)
= a &
abs (
P,
b)
= - b )
by A, defa;
C:
a * b in P * (- P)
by A, A1;
thus (abs (P,a)) * (abs (P,b)) =
- (a * b)
by VECTSP_1:8, B
.=
abs (
P,
(a * b))
by C, Y, defa
;
verum end; end; end; suppose A:
a in - P
;
abs (P,(a * b)) = (abs (P,a)) * (abs (P,b))per cases
( b in - P or b in P )
by AS, XBOOLE_0:def 3;
suppose A1:
b in - P
;
abs (P,(a * b)) = (abs (P,a)) * (abs (P,b))then B:
(
abs (
P,
a)
= - a &
abs (
P,
b)
= - b )
by A, defa;
C:
a * b in (- P) * (- P)
by A, A1;
thus (abs (P,a)) * (abs (P,b)) =
a * b
by VECTSP_1:10, B
.=
abs (
P,
(a * b))
by C, Z, defa
;
verum end; suppose A1:
b in P
;
abs (P,(a * b)) = (abs (P,a)) * (abs (P,b))then B:
(
abs (
P,
a)
= - a &
abs (
P,
b)
= b )
by A, defa;
C:
a * b in (- P) * P
by A, A1;
thus (abs (P,a)) * (abs (P,b)) =
- (a * b)
by VECTSP_1:9, B
.=
abs (
P,
(a * b))
by C, Y, defa
;
verum end; end; end; end;