let P, Q, R, P9, Q9, R9 be POINT of BK-model-Plane; :: thesis: for p, q, r, p9, q9, r9 being Element of BK_model
for h being Element of SubGroupK-isometry
for N being invertible Matrix of 3,F_Real st h = homography N & between P,Q,R & P = p & Q = q & R = r & p9 = (homography N) . p & q9 = (homography N) . q & r9 = (homography N) . r & P9 = p9 & Q9 = q9 & R9 = r9 holds
between P9,Q9,R9
let p, q, r, p9, q9, r9 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 & between P,Q,R & P = p & Q = q & R = r & p9 = (homography N) . p & q9 = (homography N) . q & r9 = (homography N) . r & P9 = p9 & Q9 = q9 & R9 = r9 holds
between P9,Q9,R9
let h be Element of SubGroupK-isometry; :: thesis: for N being invertible Matrix of 3,F_Real st h = homography N & between P,Q,R & P = p & Q = q & R = r & p9 = (homography N) . p & q9 = (homography N) . q & r9 = (homography N) . r & P9 = p9 & Q9 = q9 & R9 = r9 holds
between P9,Q9,R9
let N be invertible Matrix of 3,F_Real; :: thesis: ( h = homography N & between P,Q,R & P = p & Q = q & R = r & p9 = (homography N) . p & q9 = (homography N) . q & r9 = (homography N) . r & P9 = p9 & Q9 = q9 & R9 = r9 implies between P9,Q9,R9 )
assume that
A1: h = homography N and
A2: between P,Q,R and
A3: P = p and
A4: Q = q and
A5: R = r and
A6: p9 = (homography N) . p and
A7: q9 = (homography N) . q and
A8: r9 = (homography N) . r and
A9: P9 = p9 and
A10: Q9 = q9 and
A11: R9 = r9 ; :: thesis: between P9,Q9,R9
consider n11, n12, n13, n21, n22, n23, n31, n32, n33 being Element of F_Real such that
A12: 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
A13: ( Dir u = p & u . 3 = 1 & BK_to_REAL2 p = |[(u . 1),(u . 2)]| ) by BKMODEL2:def 2;
consider v being non zero Element of (TOP-REAL 3) such that
A14: ( Dir v = r & v . 3 = 1 & BK_to_REAL2 r = |[(v . 1),(v . 2)]| ) by BKMODEL2:def 2;
consider w being non zero Element of (TOP-REAL 3) such that
A15: ( Dir w = q & w . 3 = 1 & BK_to_REAL2 q = |[(w . 1),(w . 2)]| ) by BKMODEL2:def 2;
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 ;
A16: ( BK_to_T2 P = BK_to_REAL2 p & Tn2TR (BK_to_T2 P) = BK_to_REAL2 p & BK_to_T2 Q = BK_to_REAL2 q & Tn2TR (BK_to_T2 Q) = BK_to_REAL2 q & BK_to_T2 R = BK_to_REAL2 r & Tn2TR (BK_to_T2 R) = BK_to_REAL2 r ) by A3, A4, A5, Th04;
then Tn2TR (BK_to_T2 Q) in LSeg ((Tn2TR (BK_to_T2 P)),(Tn2TR (BK_to_T2 R))) by A2, A3, A4, A5, BKMODEL3:def 7;
then consider l being Real such that
A17: ( 0 <= l & l <= 1 ) and
A18: Tn2TR (BK_to_T2 Q) = ((1 - l) * (Tn2TR (BK_to_T2 P))) + (l * (Tn2TR (BK_to_T2 R))) by RLTOPSP1:76;
|[(w . 1),(w . 2)]| = |[((1 - l) * (u . 1)),((1 - l) * (u . 2))]| + (l * |[(v . 1),(v . 2)]|) by A18, A16, A13, A14, A15, 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 A19: ( 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
.= |[(w . 1),(w . 2),(w `3)]| by EUCLID_5:def 2
.= |[(((1 - l) * (u . 1)) + (l * (v . 1))),(((1 - l) * (u . 2)) + (l * (v . 2))),(((1 - l) * 1) + (l * 1))]| by A15, A19, EUCLID_5:def 3
.= |[((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 A13, A14, 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, A12, A13, Th20; :: thesis: ( nv3 <> 0 & nw3 <> 0 & nw3 = ((1 - l) * nu3) + (l * nv3) & ((1 - l) * nu3) + (l * nv3) <> 0 )
thus nv3 <> 0 by A1, A12, A14, Th20; :: thesis: ( nw3 <> 0 & nw3 = ((1 - l) * nu3) + (l * nv3) & ((1 - l) * nu3) + (l * nv3) <> 0 )
thus A20: nw3 <> 0 by A1, A12, A15, Th20; :: thesis: ( nw3 = ((1 - l) * nu3) + (l * nv3) & ((1 - l) * nu3) + (l * nv3) <> 0 )
thus nw3 = ((1 - l) * nu3) + (l * nv3) by A19; :: thesis: ((1 - l) * nu3) + (l * nv3) <> 0
thus ((1 - l) * nu3) + (l * nv3) <> 0 by A19, A20; :: thesis: verum
end;
then A21: ((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;
A22: ( 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 A17; :: 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) ;
A23: u1 . 1 = u1 `1
.= u . 1 by EUCLID:52 ;
A24: u1 . 2 = u1 `2
.= u . 2 by EUCLID:52 ;
A25: v1 . 1 = v1 `1
.= v . 1 by EUCLID:52 ;
A26: v1 . 2 = v1 `2
.= v . 2 by EUCLID:52 ;
reconsider m31 = n31, m32 = n32, m33 = n33 as Element of F_Real ;
( u1 in inside_of_circle (0,0,1) & v1 in inside_of_circle (0,0,1) & ( for w1 being Element of (TOP-REAL 2) st w1 in inside_of_circle (0,0,1) holds
((m31 * (w1 . 1)) + (m32 * (w1 . 2))) + m33 <> 0 ) ) by A13, A14, A1, A12, Th36;
hence 0 < nu3 * nv3 by A23, A24, A25, A26, Th29; :: 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;
A27: ( BK_to_T2 P9 = BK_to_REAL2 p9 & Tn2TR (BK_to_T2 P9) = BK_to_REAL2 p9 & BK_to_T2 Q9 = BK_to_REAL2 q9 & Tn2TR (BK_to_T2 Q9) = BK_to_REAL2 q9 & BK_to_T2 R9 = BK_to_REAL2 r9 & Tn2TR (BK_to_T2 R9) = BK_to_REAL2 r9 ) by A9, A10, A11, Th04;
now :: thesis: ( 0 <= (l * nv3) / (((1 - l) * nu3) + (l * nv3)) & (l * nv3) / (((1 - l) * nu3) + (l * nv3)) <= 1 & Tn2TR (BK_to_T2 Q9) = ((1 - ((l * nv3) / (((1 - l) * nu3) + (l * nv3)))) * (Tn2TR (BK_to_T2 P9))) + (((l * nv3) / (((1 - l) * nu3) + (l * nv3))) * (Tn2TR (BK_to_T2 R9))) )
thus ( 0 <= (l * nv3) / (((1 - l) * nu3) + (l * nv3)) & (l * nv3) / (((1 - l) * nu3) + (l * nv3)) <= 1 ) by A22; :: thesis: Tn2TR (BK_to_T2 Q9) = ((1 - ((l * nv3) / (((1 - l) * nu3) + (l * nv3)))) * (Tn2TR (BK_to_T2 P9))) + (((l * nv3) / (((1 - l) * nu3) + (l * nv3))) * (Tn2TR (BK_to_T2 R9)))
thus Tn2TR (BK_to_T2 Q9) = ((1 - ((l * nv3) / (((1 - l) * nu3) + (l * nv3)))) * (Tn2TR (BK_to_T2 P9))) + (((l * nv3) / (((1 - l) * nu3) + (l * nv3))) * (Tn2TR (BK_to_T2 R9))) :: thesis: verum
proof
reconsider u2 = |[(nu1 / nu3),(nu2 / nu3),1]| as non zero Element of (TOP-REAL 3) ;
consider u3 being non zero Element of (TOP-REAL 3) such that
A28: ( Dir u3 = p9 & u3 . 3 = 1 & BK_to_REAL2 p9 = |[(u3 . 1),(u3 . 2)]| ) by BKMODEL2:def 2;
now :: thesis: ( Dir u3 = Dir u2 & u2 . 3 = 1 & u2 . 3 = u3 . 3 )
thus Dir u3 = Dir u2 by A28, A6, A1, A12, A13, Th23; :: 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 A28; :: thesis: verum
end;
then u2 = u3 by BKMODEL1:43;
then A29: BK_to_REAL2 p9 = |[(u2 `1),(u2 . 2)]| by A28, EUCLID_5:def 1
.= |[(u2 `1),(u2 `2)]| by EUCLID_5:def 2
.= |[(nu1 / nu3),(u2 `2)]| by 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
A30: ( Dir v3 = r9 & v3 . 3 = 1 & BK_to_REAL2 r9 = |[(v3 . 1),(v3 . 2)]| ) by BKMODEL2:def 2;
now :: thesis: ( Dir v3 = Dir v2 & v2 . 3 = 1 & v2 . 3 = v3 . 3 )
thus Dir v3 = Dir v2 by A30, A1, A12, A14, Th23, A8; :: 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 A30; :: thesis: verum
end;
then v2 = v3 by BKMODEL1:43;
then A31: BK_to_REAL2 r9 = |[(v2 `1),(v2 . 2)]| by A30, EUCLID_5:def 1
.= |[(v2 `1),(v2 `2)]| by EUCLID_5:def 2
.= |[(nv1 / nv3),(v2 `2)]| by 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
A32: ( Dir w3 = q9 & w3 . 3 = 1 & BK_to_REAL2 q9 = |[(w3 . 1),(w3 . 2)]| ) by BKMODEL2:def 2;
now :: thesis: ( Dir w3 = Dir w2 & w2 . 3 = 1 & w2 . 3 = w3 . 3 )
thus Dir w3 = Dir w2 by A32, A1, A12, A15, Th23, A7; :: 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 A32; :: thesis: verum
end;
then w2 = w3 by BKMODEL1:43;
then BK_to_REAL2 q9 = |[(w2 `1),(w2 . 2)]| by A32, EUCLID_5:def 1
.= |[(w2 `1),(w2 `2)]| by EUCLID_5:def 2
.= |[(nw1 / nw3),(w2 `2)]| by EUCLID_5:2
.= |[(nw1 / nw3),(nw2 / nw3)]| by EUCLID_5:2 ;
hence Tn2TR (BK_to_T2 Q9) = ((1 - ((l * nv3) / (((1 - l) * nu3) + (l * nv3)))) * (Tn2TR (BK_to_T2 P9))) + (((l * nv3) / (((1 - l) * nu3) + (l * nv3))) * (Tn2TR (BK_to_T2 R9))) by A27, A29, A31, Th39, A21; :: thesis: verum
end;
end;
then Tn2TR (BK_to_T2 Q9) in { (((1 - r) * (Tn2TR (BK_to_T2 P9))) + (r * (Tn2TR (BK_to_T2 R9)))) where r is Real : ( 0 <= r & r <= 1 ) } ;
then Tn2TR (BK_to_T2 Q9) in LSeg ((Tn2TR (BK_to_T2 P9)),(Tn2TR (BK_to_T2 R9))) by RLTOPSP1:def 2;
hence between P9,Q9,R9 by A27, A9, A10, A11, BKMODEL3:def 7; :: thesis: verum