let l, r be Real; :: thesis: for u, v, w being Element of (TOP-REAL 3)
for n11, n12, n13, n21, n22, n23, n31, n32, n33, nu1, nu2, nu3, nv1, nv2, nv3, nw1, nw2, nw3 being Real st nu3 <> 0 & nv3 <> 0 & nw3 <> 0 & r = (l * nv3) / (((1 - l) * nu3) + (l * nv3)) & ((1 - l) * nu3) + (l * nv3) <> 0 & w = ((1 - l) * u) + (l * v) & 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 holds
((1 - r) * |[(nu1 / nu3),(nu2 / nu3),1]|) + (r * |[(nv1 / nv3),(nv2 / nv3),1]|) = |[(nw1 / nw3),(nw2 / nw3),1]|
let u, v, w be Element of (TOP-REAL 3); :: thesis: for n11, n12, n13, n21, n22, n23, n31, n32, n33, nu1, nu2, nu3, nv1, nv2, nv3, nw1, nw2, nw3 being Real st nu3 <> 0 & nv3 <> 0 & nw3 <> 0 & r = (l * nv3) / (((1 - l) * nu3) + (l * nv3)) & ((1 - l) * nu3) + (l * nv3) <> 0 & w = ((1 - l) * u) + (l * v) & 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 holds
((1 - r) * |[(nu1 / nu3),(nu2 / nu3),1]|) + (r * |[(nv1 / nv3),(nv2 / nv3),1]|) = |[(nw1 / nw3),(nw2 / nw3),1]|
let n11, n12, n13, n21, n22, n23, n31, n32, n33, nu1, nu2, nu3, nv1, nv2, nv3, nw1, nw2, nw3 be Real; :: thesis: ( nu3 <> 0 & nv3 <> 0 & nw3 <> 0 & r = (l * nv3) / (((1 - l) * nu3) + (l * nv3)) & ((1 - l) * nu3) + (l * nv3) <> 0 & w = ((1 - l) * u) + (l * v) & 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 implies ((1 - r) * |[(nu1 / nu3),(nu2 / nu3),1]|) + (r * |[(nv1 / nv3),(nv2 / nv3),1]|) = |[(nw1 / nw3),(nw2 / nw3),1]| )
assume A1: ( nu3 <> 0 & nv3 <> 0 & nw3 <> 0 & r = (l * nv3) / (((1 - l) * nu3) + (l * nv3)) & ((1 - l) * nu3) + (l * nv3) <> 0 & w = ((1 - l) * u) + (l * v) & 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 ) ; :: thesis: ((1 - r) * |[(nu1 / nu3),(nu2 / nu3),1]|) + (r * |[(nv1 / nv3),(nv2 / nv3),1]|) = |[(nw1 / nw3),(nw2 / nw3),1]|
reconsider lu = (1 - l) * u, lv = l * v as Element of (TOP-REAL 3) ;
reconsider ru = (1 - l) * u, rv = l * v as Element of REAL 3 by EUCLID:22;
A2: now :: thesis: ( (lu + lv) . 1 = (lu . 1) + (lv . 1) & (lu + lv) . 2 = (lu . 2) + (lv . 2) & (lu + lv) . 3 = (lu . 3) + (lv . 3) )
thus (lu + lv) . 1 = (ru . 1) + (rv . 1) by RVSUM_1:11
.= (lu . 1) + (lv . 1) ; :: thesis: ( (lu + lv) . 2 = (lu . 2) + (lv . 2) & (lu + lv) . 3 = (lu . 3) + (lv . 3) )
thus (lu + lv) . 2 = (ru . 2) + (rv . 2) by RVSUM_1:11
.= (lu . 2) + (lv . 2) ; :: thesis: (lu + lv) . 3 = (lu . 3) + (lv . 3)
thus (lu + lv) . 3 = (ru . 3) + (rv . 3) by RVSUM_1:11
.= (lu . 3) + (lv . 3) ; :: thesis: verum
end;
A3: now :: thesis: ( w . 1 = ((1 - l) * (u . 1)) + (l * (v . 1)) & w . 2 = ((1 - l) * (u . 2)) + (l * (v . 2)) & w . 3 = ((1 - l) * (u . 3)) + (l * (v . 3)) )
thus w . 1 = ((1 - l) * (u . 1)) + ((l * v) . 1) by A1, A2, RVSUM_1:44
.= ((1 - l) * (u . 1)) + (l * (v . 1)) by RVSUM_1:44 ; :: thesis: ( w . 2 = ((1 - l) * (u . 2)) + (l * (v . 2)) & w . 3 = ((1 - l) * (u . 3)) + (l * (v . 3)) )
thus w . 2 = ((1 - l) * (u . 2)) + ((l * v) . 2) by A1, A2, RVSUM_1:44
.= ((1 - l) * (u . 2)) + (l * (v . 2)) by RVSUM_1:44 ; :: thesis: w . 3 = ((1 - l) * (u . 3)) + (l * (v . 3))
thus w . 3 = ((1 - l) * (u . 3)) + ((l * v) . 3) by A1, A2, RVSUM_1:44
.= ((1 - l) * (u . 3)) + (l * (v . 3)) by RVSUM_1:44 ; :: thesis: verum
end;
A4: now :: thesis: ( (((1 - r) * nu1) / nu3) + ((r * nv1) / nv3) = nw1 / nw3 & (((1 - r) * nu2) / nu3) + ((r * nv2) / nv3) = nw2 / nw3 )
now :: thesis: ( ((1 - r) * nu1) / nu3 = ((1 - l) * nu1) / (((1 - l) * nu3) + (l * nv3)) & (r * nv1) / nv3 = (l * nv1) / (((1 - l) * nu3) + (l * nv3)) )
thus ((1 - r) * nu1) / nu3 = ((((1 - l) * nu3) / (((1 - l) * nu3) + (l * nv3))) * nu1) / nu3 by A1, Th32
.= ((1 - l) * nu1) / (((1 - l) * nu3) + (l * nv3)) by A1, Th33 ; :: thesis: (r * nv1) / nv3 = (l * nv1) / (((1 - l) * nu3) + (l * nv3))
thus (r * nv1) / nv3 = (l * nv1) / (((1 - l) * nu3) + (l * nv3)) by A1, Th33; :: thesis: verum
end;
hence (((1 - r) * nu1) / nu3) + ((r * nv1) / nv3) = (((1 - l) * nu1) + (l * nv1)) / (((1 - l) * nu3) + (l * nv3))
.= nw1 / nw3 by A1, A3 ;
:: thesis: (((1 - r) * nu2) / nu3) + ((r * nv2) / nv3) = nw2 / nw3
now :: thesis: ( ((1 - r) * nu2) / nu3 = ((1 - l) * nu2) / (((1 - l) * nu3) + (l * nv3)) & (r * nv2) / nv3 = (l * nv2) / (((1 - l) * nu3) + (l * nv3)) )
thus ((1 - r) * nu2) / nu3 = ((((1 - l) * nu3) / (((1 - l) * nu3) + (l * nv3))) * nu2) / nu3 by A1, Th32
.= ((1 - l) * nu2) / (((1 - l) * nu3) + (l * nv3)) by A1, Th33 ; :: thesis: (r * nv2) / nv3 = (l * nv2) / (((1 - l) * nu3) + (l * nv3))
thus (r * nv2) / nv3 = (l * nv2) / (((1 - l) * nu3) + (l * nv3)) by A1, Th33; :: thesis: verum
end;
hence (((1 - r) * nu2) / nu3) + ((r * nv2) / nv3) = (((1 - l) * nu2) + (l * nv2)) / (((1 - l) * nu3) + (l * nv3))
.= nw2 / nw3 by A1, A3 ;
:: thesis: verum
end;
((1 - r) * |[(nu1 / nu3),(nu2 / nu3),1]|) + (r * |[(nv1 / nv3),(nv2 / nv3),1]|) = |[((1 - r) * (nu1 / nu3)),((1 - r) * (nu2 / nu3)),((1 - r) * 1)]| + (r * |[(nv1 / nv3),(nv2 / nv3),1]|) by EUCLID_5:8
.= |[(((1 - r) * nu1) / nu3),(((1 - r) * nu2) / nu3),(1 - r)]| + |[(r * (nv1 / nv3)),(r * (nv2 / nv3)),(r * 1)]| by EUCLID_5:8
.= |[((((1 - r) * nu1) / nu3) + ((r * nv1) / nv3)),((((1 - r) * nu2) / nu3) + ((r * nv2) / nv3)),((1 - r) + r)]| by EUCLID_5:6
.= |[(nw1 / nw3),(nw2 / nw3),1]| by A4 ;
hence ((1 - r) * |[(nu1 / nu3),(nu2 / nu3),1]|) + (r * |[(nv1 / nv3),(nv2 / nv3),1]|) = |[(nw1 / nw3),(nw2 / nw3),1]| ; :: thesis: verum