let a, b, c, d, e be Real; :: thesis: for u, v, w being Element of (TOP-REAL 3) st u = |[a,b,e]| & v = |[c,d,0]| & w = |[(a + c),(b + d),e]| holds
|{u,v,w}| = 0
let u, v, w be Element of (TOP-REAL 3); :: thesis: ( u = |[a,b,e]| & v = |[c,d,0]| & w = |[(a + c),(b + d),e]| implies |{u,v,w}| = 0 )
assume that
A1: u = |[a,b,e]| and
A2: v = |[c,d,0]| and
A3: w = |[(a + c),(b + d),e]| ; :: thesis: |{u,v,w}| = 0
A4: ( u `1 = a & u `2 = b & u `3 = e & v `1 = c & v `2 = d & v `3 = 0 & w `1 = a + c & w `2 = b + d & w `3 = e ) by A1, A2, A3, EUCLID_5:2;
|{u,v,w}| = (((((((u `1) * (v `2)) * (w `3)) - (((u `3) * (v `2)) * (w `1))) - (((u `1) * (v `3)) * (w `2))) + (((u `2) * (v `3)) * (w `1))) - (((u `2) * (v `1)) * (w `3))) + (((u `3) * (v `1)) * (w `2)) by ANPROJ_8:27
.= ((((a * d) * e) - ((e * d) * (a + c))) - ((b * c) * e)) + ((e * c) * (b + d)) by A4 ;
hence |{u,v,w}| = 0 ; :: thesis: verum