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)

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

hence
M ~ = H ~
by P1, P2, ZMATRLIN:4; :: thesis: verum
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)

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;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
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