kill(all)$

fluid :appendix , vector identity 1,proof,version 1.0a,corrected
peter.vlasschaert@gmail.com,19/04/2019

load packages 
============

packages : vector analysis

load(vect)$

packages: other

load(lrats)$

proof : identity 1
==============

vec(G).grad(vec(G)) = curl(vec(G))*vec(G) + 1/2*grad(vec(G).vec(G))               (1)

How to use 'gradient'

nabla operator: gradient operator.
=============================

need :function?
==============

p1a:F(x,y,z);

p1b:grad(F(x,y,z));

p1c:express(p1b);

curl operator
===========

need :vector ?
==============

vec(G),curl(G)  ?  How to get it
---------------------------------------------

a) components vector G

p2a:declare(G,nonscalar)$
p2b:express(G);

b) curl ,definition from a vector 'G'

p2c:curl(G);

p2d:express(p2c);

vector product  ( = outer product),~
=================================

p3a:declare([A,B],nonscalar)$
p3b:A~B;

p3c:express(p3b);

scalar product ( = inner product),.
============================

A ≠ B  , both vectors.

p4a:A.B;
p4b:express(p4a);

A=B , both vectors.

p5a:A.A;
p5b:abs(A.A) =express(p5a);

operator , .
-----------------

p5c:abs(A).abs(A)=lhs(p5b);

operator, *
----------------

p5c1:abs(A)*abs(A) =lhs(p5b);

norm ,vector , always positive
=========================

p6a:abs(A) =sqrt(rhs(p5b));

proof :  

part 1
====

lhs : from  (1)   ?
===========

vec(G).grad(vec(G))  ?
what about :grad(vec(G)).vec(G) ?

p7a:G.grad(G);
p7a1:grad(G).G;
p7b:express(p7a);
p7b1:express(p7a1);

other representation ?  : mathematical better
----------------------------------

rem : G[x] => function1(x,y,z)
           Gy]  => function2(x,y,z)
           G[z] => function3(x,y,z)

 => ' no 'express' used from the 'above package:vector analysis'.

rem : express 'command' , we need to write full vector out.
 G => [G[x],G[y],G[z]]
rem : ' above and before diff .

component representation : see also  'p7b' and 'p7b1'
=============================================

p7c1: [G[x],G[y],G[z]].['diff(G[x],x),'diff(G[x],y),'diff(G[x],z)];
p7c2: [G[x],G[y],G[z]].['diff(G[y],x),'diff(G[y],y),'diff(G[y],z)];
p7c3: [G[x],G[y],G[z]].['diff(G[z],x),'diff(G[z],y),'diff(G[z],z)];

rem : scalar product can be' interchanged without 'change the result.
rem :  G is a vector.

part 2
=====

rhs : from  (1)   ?
===========

curl(vec(G))*vec(G) + 1/2*grad(vec(G).vec(G))    ?

part2a
---------
=>   curl(vec(G))*vec(G) 

p8a:curl(G)~G;

rem : vector product can't be interchanged between two vectors,
           result : sign change  + -> -

p8b:express(p8a);

p8b1:expand(p8b)$

three parts: 'p8b1'.
================

p8b1a:p8b1[1];
p8b1b:p8b1[2];
p8b1c:p8b1[3];

part2b
----------
=>   1/2*grad(vec(G).vec(G))    

p8c:G.G;

p8d:1/2*grad(p8c);
p8e:express(p8d);

combine : part2a and part2b
--------------------------------------------

p9:p8b1+p8e$

p9a:p9[1];
p9b:p9[2];
p9c:p9[3];

p10a:part(p9a,1) = G[x]*'diff(G[x],x)+G[y]*'diff(G[y],x)+G[z]*'diff(G[z],x);
p10b:part(p9b,1) = G[x]*'diff(G[x],y)+G[y]*'diff(G[y],y)+G[z]*'diff(G[z],y);
p10c:part(p9c,1) = G[x]*'diff(G[x],z)+G[y]*'diff(G[y],z)+G[z]*'diff(G[z],z);

rem : G[x] => function1(x,y,z)
           Gy]  => function2(x,y,z)
           G[z] => function3(x,y,z)

p11a:subst([p10a],p9a);
p11b:subst([p10b],p9b);
p11c:subst([p10c],p9c);

check :  part1  ?  part2
===================
=>  true or false.  ?

p12a:is(p7c1 = p11a);
p12b:is(p7c2 = p11b);
p12c:is(p7c3 = p11c);

if p12a = true and p12b = true and p12c = true then
  "proof finished" else " proof not finshed";