let K be Field; :: thesis: for a, b, c, d, e, f, g, h, i being Element of K
for M being Matrix of 3,K st M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> holds
M @ = <*<*a,d,g*>,<*b,e,h*>,<*c,f,i*>*>
let a, b, c, d, e, f, g, h, i be Element of K; :: thesis: for M being Matrix of 3,K st M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> holds
M @ = <*<*a,d,g*>,<*b,e,h*>,<*c,f,i*>*>
let M be Matrix of 3,K; :: thesis: ( M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> implies M @ = <*<*a,d,g*>,<*b,e,h*>,<*c,f,i*>*> )
assume M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> ; :: thesis: M @ = <*<*a,d,g*>,<*b,e,h*>,<*c,f,i*>*>
then A1: ( a = M * (1,1) & b = M * (1,2) & c = M * (1,3) & d = M * (2,1) & e = M * (2,2) & f = M * (2,3) & g = M * (3,1) & h = M * (3,2) & i = M * (3,3) ) by Th04;
consider ap, bp, cp, dp, ep, fp, gp, hp, ip being Element of K such that
A2: M @ = <*<*ap,bp,cp*>,<*dp,ep,fp*>,<*gp,hp,ip*>*> by Th03;
A3: ( ap = (M @) * (1,1) & bp = (M @) * (1,2) & cp = (M @) * (1,3) & dp = (M @) * (2,1) & ep = (M @) * (2,2) & fp = (M @) * (2,3) & gp = (M @) * (3,1) & hp = (M @) * (3,2) & ip = (M @) * (3,3) ) by A2, Th04;
( [1,1] in Indices M & [1,2] in Indices M & [1,3] in Indices M & [2,1] in Indices M & [2,2] in Indices M & [2,3] in Indices M & [3,1] in Indices M & [3,2] in Indices M & [3,3] in Indices M ) by MATRIX_0:24, ANPROJ_8:1;
then ( M * (1,1) = (M @) * (1,1) & M * (1,2) = (M @) * (2,1) & M * (1,3) = (M @) * (3,1) & M * (2,1) = (M @) * (1,2) & M * (2,2) = (M @) * (2,2) & M * (2,3) = (M @) * (3,2) & M * (3,1) = (M @) * (1,3) & M * (3,2) = (M @) * (2,3) & M * (3,3) = (M @) * (3,3) ) by MATRIX_0:def 6;
hence M @ = <*<*a,d,g*>,<*b,e,h*>,<*c,f,i*>*> by A2, A1, A3; :: thesis: verum