let P be Element of BK_model ; :: thesis: for h being Element of SubGroupK-isometry
for N being invertible Matrix of 3,F_Real st h = homography N holds
ex u being non zero Element of (TOP-REAL 3) st
( (homography N) . P = Dir u & u . 3 = 1 )
let h be Element of SubGroupK-isometry; :: thesis: for N being invertible Matrix of 3,F_Real st h = homography N holds
ex u being non zero Element of (TOP-REAL 3) st
( (homography N) . P = Dir u & u . 3 = 1 )
let N be invertible Matrix of 3,F_Real; :: thesis: ( h = homography N implies ex u being non zero Element of (TOP-REAL 3) st
( (homography N) . P = Dir u & u . 3 = 1 ) )
assume h = homography N ; :: thesis: ex u being non zero Element of (TOP-REAL 3) st
( (homography N) . P = Dir u & u . 3 = 1 )
then reconsider hP = (homography N) . P as Element of BK_model by Th31;
ex u being non zero Element of (TOP-REAL 3) st
( Dir u = hP & u . 3 = 1 & BK_to_REAL2 hP = |[(u . 1),(u . 2)]| ) by BKMODEL2:def 2;
hence ex u being non zero Element of (TOP-REAL 3) st
( (homography N) . P = Dir u & u . 3 = 1 ) ; :: thesis: verum