let K be Field; 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; 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; ( 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*>*>
; 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; verum