let ra be non zero Element of F_Real; :: thesis: for M, O being invertible Matrix of 3,F_Real st O = symmetric_3 (1,1,(- 1),0,0,0) & M = ra * O holds
(homography M) .: absolute = absolute
let M, O be invertible Matrix of 3,F_Real; :: thesis: ( O = symmetric_3 (1,1,(- 1),0,0,0) & M = ra * O implies (homography M) .: absolute = absolute )
assume that
A1: O = symmetric_3 (1,1,(- 1),0,0,0) and
A2: M = ra * O ; :: thesis: (homography M) .: absolute = absolute
reconsider z1 = 1, z2 = - 1, z3 = 0 as Element of F_Real by XREAL_0:def 1;
O = <*<*z1,z3,z3*>,<*z3,z1,z3*>,<*z3,z3,z2*>*> by A1, PASCAL:def 3;
then ra * O = <*<*(ra * z1),(ra * z3),(ra * z3)*>,<*(ra * z3),(ra * z1),(ra * z3)*>,<*(ra * z3),(ra * z3),(ra * z2)*>*> by BKMODEL1:46
.= <*<*ra,0,0*>,<*0,ra,0*>,<*0,0,(- ra)*>*> ;
then A3: M = symmetric_3 (ra,ra,(- ra),0,0,0) by A2, PASCAL:def 3;
ra <> 0
proof
assume ra = 0 ; :: thesis: contradiction
then Det M = 0. F_Real ;
hence contradiction by LAPLACE:34; :: thesis: verum
end;
hence (homography M) .: absolute = absolute by A3, Th29; :: thesis: verum