let N be Matrix of 3,F_Real; :: thesis: ( N = <*<*2,0,(- 1)*>,<*0,(sqrt 3),0*>,<*1,0,(- 2)*>*> implies ( Det N = (- 3) * (sqrt 3) & N is invertible ) )
assume A1: N = <*<*2,0,(- 1)*>,<*0,(sqrt 3),0*>,<*1,0,(- 2)*>*> ; :: thesis: ( Det N = (- 3) * (sqrt 3) & N is invertible )
reconsider a = 2, b = 0 , c = - 1, d = 0 , e = sqrt 3, f = 0 , g = 1, h = 0 , i = - 2 as Element of F_Real by XREAL_0:def 1;
Det N = ((((((a * e) * i) - ((c * e) * g)) - ((a * f) * h)) + ((b * f) * g)) - ((b * d) * i)) + ((c * d) * h) by A1, MATRIX_9:46;
then ( Det N = (- 3) * (sqrt 3) & Det N <> 0. F_Real ) by SQUARE_1:24;
hence ( Det N = (- 3) * (sqrt 3) & N is invertible ) by LAPLACE:34; :: thesis: verum