let P, Q, R, P9, Q9, R9 be non point_at_infty Element of (ProjectiveSpace (TOP-REAL 3)); :: thesis: for h being Element of SubGroupK-isometry
for N being invertible Matrix of 3,F_Real st h = homography N & P in BK_model & Q in BK_model & R in absolute & P9 = (homography N) . P & Q9 = (homography N) . Q & R9 = (homography N) . R & between RP3_to_T2 P, RP3_to_T2 Q, RP3_to_T2 R holds
between RP3_to_T2 P9, RP3_to_T2 Q9, RP3_to_T2 R9
let h be Element of SubGroupK-isometry; :: thesis: for N being invertible Matrix of 3,F_Real st h = homography N & P in BK_model & Q in BK_model & R in absolute & P9 = (homography N) . P & Q9 = (homography N) . Q & R9 = (homography N) . R & between RP3_to_T2 P, RP3_to_T2 Q, RP3_to_T2 R holds
between RP3_to_T2 P9, RP3_to_T2 Q9, RP3_to_T2 R9
let N be invertible Matrix of 3,F_Real; :: thesis: ( h = homography N & P in BK_model & Q in BK_model & R in absolute & P9 = (homography N) . P & Q9 = (homography N) . Q & R9 = (homography N) . R & between RP3_to_T2 P, RP3_to_T2 Q, RP3_to_T2 R implies between RP3_to_T2 P9, RP3_to_T2 Q9, RP3_to_T2 R9 )
assume that
A1: h = homography N and
A2: P in BK_model and
A3: Q in BK_model and
A4: R in absolute and
A5: P9 = (homography N) . P and
A6: Q9 = (homography N) . Q and
A7: R9 = (homography N) . R and
A8: between RP3_to_T2 P, RP3_to_T2 Q, RP3_to_T2 R ; :: thesis: between RP3_to_T2 P9, RP3_to_T2 Q9, RP3_to_T2 R9
consider n11, n12, n13, n21, n22, n23, n31, n32, n33 being Element of F_Real such that
A9: N = <*<*n11,n12,n13*>,<*n21,n22,n23*>,<*n31,n32,n33*>*> by PASCAL:3;
consider u being non zero Element of (TOP-REAL 3) such that
A10: ( P = Dir u & u `3 = 1 & RP3_to_REAL2 P = |[(u `1),(u `2)]| ) by Def05;
A11: |[(u `1),(u `2)]| = |[(u . 1),(u `2)]| by EUCLID_5:def 1
.= |[(u . 1),(u . 2)]| by EUCLID_5:def 2 ;
then A12: ( P = Dir u & u . 3 = 1 & RP3_to_REAL2 P = |[(u . 1),(u . 2)]| ) by A10, EUCLID_5:def 3;
consider v being non zero Element of (TOP-REAL 3) such that
A13: ( R = Dir v & v `3 = 1 & RP3_to_REAL2 R = |[(v `1),(v `2)]| ) by Def05;
A14: |[(v `1),(v `2)]| = |[(v . 1),(v `2)]| by EUCLID_5:def 1
.= |[(v . 1),(v . 2)]| by EUCLID_5:def 2 ;
then A15: ( R = Dir v & v . 3 = 1 & RP3_to_REAL2 R = |[(v . 1),(v . 2)]| ) by A13, EUCLID_5:def 3;
consider w being non zero Element of (TOP-REAL 3) such that
A16: ( Q = Dir w & w `3 = 1 & RP3_to_REAL2 Q = |[(w `1),(w `2)]| ) by Def05;
A17: |[(w `1),(w `2)]| = |[(w . 1),(w `2)]| by EUCLID_5:def 1
.= |[(w . 1),(w . 2)]| by EUCLID_5:def 2 ;
then A18: ( Q = Dir w & w . 3 = 1 & RP3_to_REAL2 Q = |[(w . 1),(w . 2)]| ) by A16, EUCLID_5:def 3;
reconsider nu1 = ((n11 * (u . 1)) + (n12 * (u . 2))) + n13, nu2 = ((n21 * (u . 1)) + (n22 * (u . 2))) + n23, nu3 = ((n31 * (u . 1)) + (n32 * (u . 2))) + n33, nv1 = ((n11 * (v . 1)) + (n12 * (v . 2))) + n13, nv2 = ((n21 * (v . 1)) + (n22 * (v . 2))) + n23, nv3 = ((n31 * (v . 1)) + (n32 * (v . 2))) + n33, nw1 = ((n11 * (w . 1)) + (n12 * (w . 2))) + n13, nw2 = ((n21 * (w . 1)) + (n22 * (w . 2))) + n23, nw3 = ((n31 * (w . 1)) + (n32 * (w . 2))) + n33 as Real ;
Tn2TR (RP3_to_T2 Q) in LSeg ((Tn2TR (RP3_to_T2 P)),(Tn2TR (RP3_to_T2 R))) by A8, GTARSKI2:20;
then consider l being Real such that
A19: ( 0 <= l & l <= 1 ) and
A20: Tn2TR (RP3_to_T2 Q) = ((1 - l) * (Tn2TR (RP3_to_T2 P))) + (l * (Tn2TR (RP3_to_T2 R))) by RLTOPSP1:76;
|[(w . 1),(w . 2)]| = |[((1 - l) * (u . 1)),((1 - l) * (u . 2))]| + (l * |[(v . 1),(v . 2)]|) by A20, A11, A10, A14, A17, A16, A13, EUCLID:58
.= |[((1 - l) * (u . 1)),((1 - l) * (u . 2))]| + |[(l * (v . 1)),(l * (v . 2))]| by EUCLID:58
.= |[(((1 - l) * (u . 1)) + (l * (v . 1))),(((1 - l) * (u . 2)) + (l * (v . 2)))]| by EUCLID:56 ;
then A21: ( w . 1 = ((1 - l) * (u . 1)) + (l * (v . 1)) & w . 2 = ((1 - l) * (u . 2)) + (l * (v . 2)) ) by FINSEQ_1:77;
set r = (l * nv3) / (((1 - l) * nu3) + (l * nv3));

now :: thesis: ( w = ((1 - l) * u) + (l * v) & nu3 <> 0 & nv3 <> 0 & nw3 <> 0 & nw3 = ((1 - l) * nu3) + (l * nv3) & ((1 - l) * nu3) + (l * nv3) <> 0 )

thus w = |[(w `1),(w `2),(w `3)]| by EUCLID_5:3
.= |[(w . 1),(w `2),(w `3)]| by EUCLID_5:def 1
.= |[(((1 - l) * (u . 1)) + (l * (v . 1))),(((1 - l) * (u . 2)) + (l * (v . 2))),(((1 - l) * 1) + (l * 1))]| by A16, A21, EUCLID_5:def 2
.= |[((1 - l) * (u . 1)),((1 - l) * (u . 2)),((1 - l) * 1)]| + |[(l * (v . 1)),(l * (v . 2)),(l * 1)]| by EUCLID_5:6
.= ((1 - l) * |[(u . 1),(u . 2),1]|) + |[(l * (v . 1)),(l * (v . 2)),(l * 1)]| by EUCLID_5:8
.= ((1 - l) * |[(u . 1),(u . 2),1]|) + (l * |[(v . 1),(v . 2),1]|) by EUCLID_5:8
.= ((1 - l) * u) + (l * |[(v . 1),(v . 2),(v . 3)]|) by A12, A15, Th35
.= ((1 - l) * u) + (l * v) by Th35 ; :: thesis: ( nu3 <> 0 & nv3 <> 0 & nw3 <> 0 & nw3 = ((1 - l) * nu3) + (l * nv3) & ((1 - l) * nu3) + (l * nv3) <> 0 )
thus nu3 <> 0 by A1, A2, A9, A12, Th20; :: thesis: ( nv3 <> 0 & nw3 <> 0 & nw3 = ((1 - l) * nu3) + (l * nv3) & ((1 - l) * nu3) + (l * nv3) <> 0 )
thus nv3 <> 0 by A1, A4, A9, A15, Th22; :: thesis: ( nw3 <> 0 & nw3 = ((1 - l) * nu3) + (l * nv3) & ((1 - l) * nu3) + (l * nv3) <> 0 )
thus A22: nw3 <> 0 by A3, A1, A9, A18, Th20; :: thesis: ( nw3 = ((1 - l) * nu3) + (l * nv3) & ((1 - l) * nu3) + (l * nv3) <> 0 )
thus nw3 = ((1 - l) * nu3) + (l * nv3) by A21; :: thesis: ((1 - l) * nu3) + (l * nv3) <> 0
thus ((1 - l) * nu3) + (l * nv3) <> 0 by A22, A21; :: thesis: verum

end;

then A23: ((1 - ((l * nv3) / (((1 - l) * nu3) + (l * nv3)))) * |[(nu1 / nu3),(nu2 / nu3),1]|) + (((l * nv3) / (((1 - l) * nu3) + (l * nv3))) * |[(nv1 / nv3),(nv2 / nv3),1]|) = |[(nw1 / nw3),(nw2 / nw3),1]| by Th34;
A24: ( 0 <= (l * nv3) / (((1 - l) * nu3) + (l * nv3)) & (l * nv3) / (((1 - l) * nu3) + (l * nv3)) <= 1 )

proof

now :: thesis: ( 0 <= l & l <= 1 & 0 < nu3 * nv3 )

thus ( 0 <= l & l <= 1 ) by A19; :: thesis: 0 < nu3 * nv3
thus 0 < nu3 * nv3 :: thesis: verum

proof

reconsider u1 = |[(u . 1),(u . 2)]|, v1 = |[(v . 1),(v . 2)]| as Element of (TOP-REAL 2) ;
A25: u1 . 1 = u1 `1
.= u . 1 by EUCLID:52 ;
A26: u1 . 2 = u1 `2
.= u . 2 by EUCLID:52 ;
A27: v1 . 1 = v1 `1
.= v . 1 by EUCLID:52 ;
A28: v1 . 2 = v1 `2
.= v . 2 by EUCLID:52 ;
reconsider m31 = n31, m32 = n32, m33 = n33 as Element of F_Real ;

now :: thesis: ( u1 in inside_of_circle (0,0,1) & v1 in circle (0,0,1) & ( for w1 being Element of (TOP-REAL 2) st w1 in closed_inside_of_circle (0,0,1) holds
((m31 * (w1 . 1)) + (m32 * (w1 . 2))) + m33 <> 0 ) )

reconsider PP = P as Element of BK_model by A2;
consider u3 being non zero Element of (TOP-REAL 3) such that
A29: ( Dir u3 = PP & u3 . 3 = 1 & BK_to_REAL2 PP = |[(u3 . 1),(u3 . 2)]| ) by BKMODEL2:def 2;
u3 = u by A12, A29, Th16;
hence u1 in inside_of_circle (0,0,1) by A29; :: thesis: ( v1 in circle (0,0,1) & ( for w1 being Element of (TOP-REAL 2) st w1 in closed_inside_of_circle (0,0,1) holds
((m31 * (w1 . 1)) + (m32 * (w1 . 2))) + m33 <> 0 ) )
thus v1 in circle (0,0,1) by A4, A15, BKMODEL1:84; :: thesis: for w1 being Element of (TOP-REAL 2) st w1 in closed_inside_of_circle (0,0,1) holds
((m31 * (w1 . 1)) + (m32 * (w1 . 2))) + m33 <> 0
thus for w1 being Element of (TOP-REAL 2) st w1 in closed_inside_of_circle (0,0,1) holds
((m31 * (w1 . 1)) + (m32 * (w1 . 2))) + m33 <> 0 by A1, A9, Th38; :: thesis: verum

end;

hence 0 < nu3 * nv3 by A25, A26, A27, A28, Th30; :: thesis: verum

end;

end;

hence ( 0 <= (l * nv3) / (((1 - l) * nu3) + (l * nv3)) & (l * nv3) / (((1 - l) * nu3) + (l * nv3)) <= 1 ) by Th31; :: thesis: verum

end;

now :: thesis: ( 0 <= (l * nv3) / (((1 - l) * nu3) + (l * nv3)) & (l * nv3) / (((1 - l) * nu3) + (l * nv3)) <= 1 & Tn2TR (RP3_to_T2 Q9) = ((1 - ((l * nv3) / (((1 - l) * nu3) + (l * nv3)))) * (Tn2TR (RP3_to_T2 P9))) + (((l * nv3) / (((1 - l) * nu3) + (l * nv3))) * (Tn2TR (RP3_to_T2 R9))) )

thus ( 0 <= (l * nv3) / (((1 - l) * nu3) + (l * nv3)) & (l * nv3) / (((1 - l) * nu3) + (l * nv3)) <= 1 ) by A24; :: thesis: Tn2TR (RP3_to_T2 Q9) = ((1 - ((l * nv3) / (((1 - l) * nu3) + (l * nv3)))) * (Tn2TR (RP3_to_T2 P9))) + (((l * nv3) / (((1 - l) * nu3) + (l * nv3))) * (Tn2TR (RP3_to_T2 R9)))
thus Tn2TR (RP3_to_T2 Q9) = ((1 - ((l * nv3) / (((1 - l) * nu3) + (l * nv3)))) * (Tn2TR (RP3_to_T2 P9))) + (((l * nv3) / (((1 - l) * nu3) + (l * nv3))) * (Tn2TR (RP3_to_T2 R9))) :: thesis: verum

proof

reconsider u2 = |[(nu1 / nu3),(nu2 / nu3),1]| as non zero Element of (TOP-REAL 3) ;
reconsider PP9 = P9 as non point_at_infty Point of (ProjectiveSpace (TOP-REAL 3)) ;
consider u3 being non zero Element of (TOP-REAL 3) such that
A30: ( PP9 = Dir u3 & u3 `3 = 1 & RP3_to_REAL2 PP9 = |[(u3 `1),(u3 `2)]| ) by Def05;

now :: thesis: ( Dir u3 = Dir u2 & u2 . 3 = 1 & u2 . 3 = u3 . 3 )

thus Dir u3 = Dir u2 by A1, A2, A9, A12, Th23, A5, A30; :: thesis: ( u2 . 3 = 1 & u2 . 3 = u3 . 3 )
thus u2 . 3 = u2 `3 by EUCLID_5:def 3
.= 1 by EUCLID_5:2 ; :: thesis: u2 . 3 = u3 . 3
hence u2 . 3 = u3 . 3 by A30, EUCLID_5:def 3; :: thesis: verum

end;

then u2 = u3 by BKMODEL1:43;
then A31: RP3_to_REAL2 P9 = |[(nu1 / nu3),(u2 `2)]| by A30, EUCLID_5:2
.= |[(nu1 / nu3),(nu2 / nu3)]| by EUCLID_5:2 ;
reconsider v2 = |[(nv1 / nv3),(nv2 / nv3),1]| as non zero Element of (TOP-REAL 3) ;
consider v3 being non zero Element of (TOP-REAL 3) such that
A32: ( Dir v3 = R9 & v3 `3 = 1 & RP3_to_REAL2 R9 = |[(v3 `1),(v3 `2)]| ) by Def05;

now :: thesis: ( Dir v3 = Dir v2 & v2 . 3 = 1 & v2 . 3 = v3 . 3 )

thus Dir v3 = Dir v2 by A15, A1, A4, A9, Th24, A7, A32; :: thesis: ( v2 . 3 = 1 & v2 . 3 = v3 . 3 )
thus v2 . 3 = v2 `3 by EUCLID_5:def 3
.= 1 by EUCLID_5:2 ; :: thesis: v2 . 3 = v3 . 3
hence v2 . 3 = v3 . 3 by A32, EUCLID_5:def 3; :: thesis: verum

end;

then v2 = v3 by BKMODEL1:43;
then A33: RP3_to_REAL2 R9 = |[(nv1 / nv3),(v2 `2)]| by A32, EUCLID_5:2
.= |[(nv1 / nv3),(nv2 / nv3)]| by EUCLID_5:2 ;
reconsider w2 = |[(nw1 / nw3),(nw2 / nw3),1]| as non zero Element of (TOP-REAL 3) ;
consider w3 being non zero Element of (TOP-REAL 3) such that
A34: ( Dir w3 = Q9 & w3 `3 = 1 & RP3_to_REAL2 Q9 = |[(w3 `1),(w3 `2)]| ) by Def05;

now :: thesis: ( Dir w3 = Dir w2 & w2 . 3 = 1 & w2 . 3 = w3 . 3 )

thus Dir w3 = Dir w2 by A3, A1, A9, A18, Th23, A6, A34; :: thesis: ( w2 . 3 = 1 & w2 . 3 = w3 . 3 )
thus w2 . 3 = w2 `3 by EUCLID_5:def 3
.= 1 by EUCLID_5:2 ; :: thesis: w2 . 3 = w3 . 3
hence w2 . 3 = w3 . 3 by A34, EUCLID_5:def 3; :: thesis: verum

end;

then w2 = w3 by BKMODEL1:43;
then A35: RP3_to_REAL2 Q9 = |[(nw1 / nw3),(w2 `2)]| by A34, EUCLID_5:2
.= |[(nw1 / nw3),(nw2 / nw3)]| by EUCLID_5:2 ;
RP3_to_REAL2 Q9 = ((1 - ((l * nv3) / (((1 - l) * nu3) + (l * nv3)))) * (RP3_to_REAL2 P9)) + (((l * nv3) / (((1 - l) * nu3) + (l * nv3))) * (RP3_to_REAL2 R9))

proof

reconsider a = nu1 / nu3, b = nu2 / nu3, c = nv1 / nv3, d = nv2 / nv3, e = nw1 / nw3, f = nw2 / nw3 as Real ;
((1 - ((l * nv3) / (((1 - l) * nu3) + (l * nv3)))) * |[a,b]|) + (((l * nv3) / (((1 - l) * nu3) + (l * nv3))) * |[c,d]|) = |[e,f]| by Th39, A23;
hence RP3_to_REAL2 Q9 = ((1 - ((l * nv3) / (((1 - l) * nu3) + (l * nv3)))) * (RP3_to_REAL2 P9)) + (((l * nv3) / (((1 - l) * nu3) + (l * nv3))) * (RP3_to_REAL2 R9)) by A31, A33, A35; :: thesis: verum

end;

hence Tn2TR (RP3_to_T2 Q9) = ((1 - ((l * nv3) / (((1 - l) * nu3) + (l * nv3)))) * (Tn2TR (RP3_to_T2 P9))) + (((l * nv3) / (((1 - l) * nu3) + (l * nv3))) * (Tn2TR (RP3_to_T2 R9))) ; :: thesis: verum

end;

end;

then Tn2TR (RP3_to_T2 Q9) in { (((1 - r) * (Tn2TR (RP3_to_T2 P9))) + (r * (Tn2TR (RP3_to_T2 R9)))) where r is Real : ( 0 <= r & r <= 1 ) } ;
then Tn2TR (RP3_to_T2 Q9) in LSeg ((Tn2TR (RP3_to_T2 P9)),(Tn2TR (RP3_to_T2 R9))) by RLTOPSP1:def 2;
hence between RP3_to_T2 P9, RP3_to_T2 Q9, RP3_to_T2 R9 by GTARSKI2:20; :: thesis: verum