let F be preordered Field; :: thesis: for P being Preordering of F
for a being non zero b1 -ordered Element of F holds abs (P,(a ")) = (abs (P,a)) "
let P be Preordering of F; :: thesis: for a being non zero P -ordered Element of F holds abs (P,(a ")) = (abs (P,a)) "
let a be non zero P -ordered Element of F; :: thesis: abs (P,(a ")) = (abs (P,a)) "
AS: a in P \/ (- P) by defppp;
Y: a <> 0. F ;
- a <> - (0. F) ;
then X: ( not a " is zero & not - (a ") is zero & not - a is zero ) ;
(abs (P,(a "))) * (abs (P,a)) = 1_ F
proof
per cases ( a in P or a in - P ) by AS, XBOOLE_0:def 3;
suppose K: a in P ; :: thesis: (abs (P,(a "))) * (abs (P,a)) = 1_ F
then 0. F <= P,a ;
then L: abs (P,a) = a by av2;
0. F <= P,a " by K, REALALG1:27;
then abs (P,(a ")) = a " by av2;
hence (abs (P,(a "))) * (abs (P,a)) = 1_ F by Y, L, VECTSP_2:9; :: thesis: verum
end;
suppose a in - P ; :: thesis: (abs (P,(a "))) * (abs (P,a)) = 1_ F
then K: - a in - (- P) ;
then - (- a) <= P, 0. F ;
then L: abs (P,a) = - a by av3;
- ((- a) ") <= P, 0. F by K, X, REALALG1:27;
then a " <= P, 0. F by YZ;
then abs (P,(a ")) = - (a ") by av3;
hence (abs (P,(a "))) * (abs (P,a)) = (a ") * a by L, VECTSP_1:10
.= 1_ F by Y, VECTSP_2:9 ;
:: thesis: verum
end;
end;
end;
hence abs (P,(a ")) = (abs (P,a)) " by VECTSP_2:10; :: thesis: verum