let p, q be Element of REAL 3; :: thesis: for f1, f2, f3, g1, g2, g3 being PartFunc of ,
for t1, t2 being Real st p = (VFunc f1,f2,f3) . t1 & q = (VFunc g1,g2,g3) . t2 holds
p + (- q) = |[((f1 . t1) - (g1 . t2)),((f2 . t1) - (g2 . t2)),((f3 . t1) - (g3 . t2))]|
let f1, f2, f3, g1, g2, g3 be PartFunc of ,; :: thesis: for t1, t2 being Real st p = (VFunc f1,f2,f3) . t1 & q = (VFunc g1,g2,g3) . t2 holds
p + (- q) = |[((f1 . t1) - (g1 . t2)),((f2 . t1) - (g2 . t2)),((f3 . t1) - (g3 . t2))]|
let t1, t2 be Real; :: thesis: ( p = (VFunc f1,f2,f3) . t1 & q = (VFunc g1,g2,g3) . t2 implies p + (- q) = |[((f1 . t1) - (g1 . t2)),((f2 . t1) - (g2 . t2)),((f3 . t1) - (g3 . t2))]| )
assume A1: ( p = (VFunc f1,f2,f3) . t1 & q = (VFunc g1,g2,g3) . t2 ) ; :: thesis: p + (- q) = |[((f1 . t1) - (g1 . t2)),((f2 . t1) - (g2 . t2)),((f3 . t1) - (g3 . t2))]|
A2: - q = |[((- 1) * (q . 1)),((- 1) * (q . 2)),((- 1) * (q . 3))]| by Lm3
.= |[(- (q . 1)),(- (q . 2)),(- (q . 3))]| ;
p + (- q) = |[((p . 1) + ((- q) . 1)),((p . 2) + ((- q) . 2)),((p . 3) + ((- q) . 3))]| by Lm4
.= |[((p . 1) + (- (q . 1))),((p . 2) + ((- q) . 2)),((p . 3) + ((- q) . 3))]| by A2, FINSEQ_1:62
.= |[((p . 1) + (- (q . 1))),((p . 2) + (- (q . 2))),((p . 3) + ((- q) . 3))]| by A2, FINSEQ_1:62
.= |[((p . 1) + (- (q . 1))),((p . 2) + (- (q . 2))),((p . 3) + (- (q . 3)))]| by A2, FINSEQ_1:62
.= |[((p . 1) - (q . 1)),((p . 2) - (q . 2)),((p . 3) - (q . 3))]|
.= |[((f1 . t1) - (q . 1)),((p . 2) - (q . 2)),((p . 3) - (q . 3))]| by A1, Th34
.= |[((f1 . t1) - (q . 1)),((f2 . t1) - (q . 2)),((p . 3) - (q . 3))]| by A1, Th34
.= |[((f1 . t1) - (q . 1)),((f2 . t1) - (q . 2)),((f3 . t1) - (q . 3))]| by A1, Th34
.= |[((f1 . t1) - (g1 . t2)),((f2 . t1) - (q . 2)),((f3 . t1) - (q . 3))]| by A1, Th34
.= |[((f1 . t1) - (g1 . t2)),((f2 . t1) - (g2 . t2)),((f3 . t1) - (q . 3))]| by A1, Th34
.= |[((f1 . t1) - (g1 . t2)),((f2 . t1) - (g2 . t2)),((f3 . t1) - (g3 . t2))]| by A1, Th34 ;
hence p + (- q) = |[((f1 . t1) - (g1 . t2)),((f2 . t1) - (g2 . t2)),((f3 . t1) - (g3 . t2))]| ; :: thesis: verum