let R be non degenerated preordered Ring; :: thesis: for P being Preordering of R
for a, b being b₁ -ordered Element of R holds abs (P,(a * b)) = (abs (P,a)) * (abs (P,b))
let P be Preordering of R; :: thesis: 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; :: thesis: 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 ; :: thesis: 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 ; :: thesis: abs (P,(a * b)) = (abs (P,a)) * (abs (P,b))

then B: ( abs (P,a) = a & abs (P,b) = b ) by A, defa;
a * b in P * P by A, A1;
hence (abs (P,a)) * (abs (P,b)) = abs (P,(a * b)) by X, defa, B; :: thesis: verum

end;

suppose A1: b in - P ; :: thesis: 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 ; :: thesis: verum

end;

end;

end;

suppose A: a in - P ; :: thesis: 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 ; :: thesis: 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 ; :: thesis: verum

end;

suppose A1: b in P ; :: thesis: 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 ; :: thesis: verum

end;

end;

end;

end;