let l, r be Real; 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); 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; ( 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 )
; ((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 ( (lu + lv) . 1 = (lu . 1) + (lv . 1) & (lu + lv) . 2 = (lu . 2) + (lv . 2) & (lu + lv) . 3 = (lu . 3) + (lv . 3) )end;
A3:
now ( 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)) )end;
A4:
now ( (((1 - r) * nu1) / nu3) + ((r * nv1) / nv3) = nw1 / nw3 & (((1 - r) * nu2) / nu3) + ((r * nv2) / nv3) = nw2 / nw3 )now ( ((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
;
(r * nv1) / nv3 = (l * nv1) / (((1 - l) * nu3) + (l * nv3))thus
(r * nv1) / nv3 = (l * nv1) / (((1 - l) * nu3) + (l * nv3))
by A1, Th33;
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
;
(((1 - r) * nu2) / nu3) + ((r * nv2) / nv3) = nw2 / nw3now ( ((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
;
(r * nv2) / nv3 = (l * nv2) / (((1 - l) * nu3) + (l * nv3))thus
(r * nv2) / nv3 = (l * nv2) / (((1 - l) * nu3) + (l * nv3))
by A1, Th33;
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
;
verum
((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]|
; verum