let n be Nat; :: thesis: for M being Matrix of n,F_Real
for H being Matrix of n,F_Rat st M = H & M is invertible holds
( H is invertible & M ~ = H ~ )
let M be Matrix of n,F_Real; :: thesis: for H being Matrix of n,F_Rat st M = H & M is invertible holds
( H is invertible & M ~ = H ~ )
let H be Matrix of n,F_Rat; :: thesis: ( M = H & M is invertible implies ( H is invertible & M ~ = H ~ ) )
assume AS: ( M = H & M is invertible ) ; :: thesis: ( H is invertible & M ~ = H ~ )
then N1: 0. F_Real <> Det M by LAPLACE:34;
then P0: 0. F_Rat <> Det H by AS, ZMODLAT2:54;
hence H is invertible by LAPLACE:34; :: thesis: M ~ = H ~
Q0: Indices M = [:(Seg n),(Seg n):] by MATRIX_0:24;
P1: len (M ~) = n by MATRIX_0:24
.= len (H ~) by MATRIX_0:24 ;
P2: width (M ~) = n by MATRIX_0:24
.= width (H ~) by MATRIX_0:24 ;
P3A: Indices (M ~) = [:(Seg n),(Seg n):] by MATRIX_0:24;
P3B: Indices (H ~) = [:(Seg n),(Seg n):] by MATRIX_0:24;
for i, j being Nat st [i,j] in Indices (M ~) holds
(M ~) * (i,j) = (H ~) * (i,j)

proof

let i, j be Nat; :: thesis: ( [i,j] in Indices (M ~) implies (M ~) * (i,j) = (H ~) * (i,j) )
assume P01: [i,j] in Indices (M ~) ; :: thesis: (M ~) * (i,j) = (H ~) * (i,j)
then [i,j] in [:(Seg n),(Seg n):] by MATRIX_0:24;
then ( i in Seg n & j in Seg n ) by ZFMISC_1:87;
then P02: [j,i] in Indices M by Q0, ZFMISC_1:87;
set MM = Delete (M,j,i);
set HH = Delete (H,j,i);
Delete (M,j,i) = Delete (H,j,i)

proof

per cases ( n <= 1 or n > 1 ) ;

suppose n <= 1 ; :: thesis: Delete (M,j,i) = Delete (H,j,i)

then n - 1 <= 1 - 1 by XREAL_1:9;
then n -' 1 = 0 by XREAL_0:def 2;
hence Delete (M,j,i) = Delete (H,j,i) by MATRIX_0:22; :: thesis: verum

end;

suppose NN21: n > 1 ; :: thesis: Delete (M,j,i) = Delete (H,j,i)

then NN2: n - 1 > 1 - 1 by XREAL_1:14;
reconsider k = n - 1 as Nat by NN21;
( n = k + 1 & 0 < k ) by NN2;
hence Delete (M,j,i) = Delete (H,j,i) by AS, P02, ZMODLAT2:52; :: thesis: verum

end;

end;

end;

then S1: ((power F_Real) . ((- (1_ F_Real)),(i + j))) * (Minor (M,j,i)) = ((power F_Rat) . ((- (1_ F_Rat)),(i + j))) * (Minor (H,j,i)) by ZMODLAT2:54, ZMODLAT2:47;
thus (M ~) * (i,j) = (((Det M) ") * ((power F_Real) . ((- (1_ F_Real)),(i + j)))) * (Minor (M,j,i)) by P01, LAPLACE:36, AS
.= ((Det M) ") * (((power F_Real) . ((- (1_ F_Real)),(i + j))) * (Minor (M,j,i)))
.= ((Det H) ") * (((power F_Rat) . ((- (1_ F_Rat)),(i + j))) * (Minor (H,j,i))) by AS, N1, S1, GAUSSINT:14, GAUSSINT:21, ZMODLAT2:54
.= (((Det H) ") * ((power F_Rat) . ((- (1_ F_Rat)),(i + j)))) * (Minor (H,j,i))
.= (H ~) * (i,j) by P01, P0, P3A, P3B, LAPLACE:34, LAPLACE:36 ; :: thesis: verum

end;

hence M ~ = H ~ by P1, P2, ZMATRLIN:4; :: thesis: verum