let p be Element of REAL 3; :: thesis: for f1, f2, f3 being PartFunc of (REAL 3),REAL holds curl (f1,f2,f3,p) = |[((partdiff (f3,p,2)) - (partdiff (f2,p,3))),((partdiff (f1,p,3)) - (partdiff (f3,p,1))),((partdiff (f2,p,1)) - (partdiff (f1,p,2)))]|
let f1, f2, f3 be PartFunc of (REAL 3),REAL; :: thesis: curl (f1,f2,f3,p) = |[((partdiff (f3,p,2)) - (partdiff (f2,p,3))),((partdiff (f1,p,3)) - (partdiff (f3,p,1))),((partdiff (f2,p,1)) - (partdiff (f1,p,2)))]|
curl (f1,f2,f3,p) = (|[(((partdiff (f3,p,2)) - (partdiff (f2,p,3))) * 1),(((partdiff (f3,p,2)) - (partdiff (f2,p,3))) * 0),(((partdiff (f3,p,2)) - (partdiff (f2,p,3))) * 0)]| + (((partdiff (f1,p,3)) - (partdiff (f3,p,1))) * |[0,jj,0]|)) + (((partdiff (f2,p,1)) - (partdiff (f1,p,2))) * |[0,0,jj]|) by EUCLID_8:59
.= (|[((partdiff (f3,p,2)) - (partdiff (f2,p,3))),0,0]| + |[(((partdiff (f1,p,3)) - (partdiff (f3,p,1))) * 0),(((partdiff (f1,p,3)) - (partdiff (f3,p,1))) * 1),(((partdiff (f1,p,3)) - (partdiff (f3,p,1))) * 0)]|) + (((partdiff (f2,p,1)) - (partdiff (f1,p,2))) * |[0,0,jj]|) by EUCLID_8:59
.= (|[((partdiff (f3,p,2)) - (partdiff (f2,p,3))),0,0]| + |[0,((partdiff (f1,p,3)) - (partdiff (f3,p,1))),0]|) + |[(((partdiff (f2,p,1)) - (partdiff (f1,p,2))) * 0),(((partdiff (f2,p,1)) - (partdiff (f1,p,2))) * 0),(((partdiff (f2,p,1)) - (partdiff (f1,p,2))) * 1)]| by EUCLID_8:59
.= |[(((partdiff (f3,p,2)) - (partdiff (f2,p,3))) + 0),(0 + ((partdiff (f1,p,3)) - (partdiff (f3,p,1)))),(0 + 0)]| + |[0,0,((partdiff (f2,p,1)) - (partdiff (f1,p,2)))]| by Lm4
.= |[(((partdiff (f3,p,2)) - (partdiff (f2,p,3))) + 0),(((partdiff (f1,p,3)) - (partdiff (f3,p,1))) + 0),(0 + ((partdiff (f2,p,1)) - (partdiff (f1,p,2))))]| by Lm4
.= |[((partdiff (f3,p,2)) - (partdiff (f2,p,3))),((partdiff (f1,p,3)) - (partdiff (f3,p,1))),((partdiff (f2,p,1)) - (partdiff (f1,p,2)))]| ;
hence curl (f1,f2,f3,p) = |[((partdiff (f3,p,2)) - (partdiff (f2,p,3))),((partdiff (f1,p,3)) - (partdiff (f3,p,1))),((partdiff (f2,p,1)) - (partdiff (f1,p,2)))]| ; :: thesis: verum