let n be Nat; :: thesis: for A, B being Matrix of n,REAL st A is invertible & B is invertible holds
( A * B is invertible & Inv (A * B) = (Inv B) * (Inv A) )
let A, B be Matrix of n,REAL; :: thesis: ( A is invertible & B is invertible implies ( A * B is invertible & Inv (A * B) = (Inv B) * (Inv A) ) )
assume that
A1: A is invertible and
A2: B is invertible ; :: thesis: ( A * B is invertible & Inv (A * B) = (Inv B) * (Inv A) )
A3: ((Inv B) * (Inv A)) * (A * B) = (((Inv B) * (Inv A)) * A) * B by Th28
.= ((Inv B) * ((Inv A) * A)) * B by Th28
.= ((Inv B) * (1_Rmatrix n)) * B by A1, Def6
.= (Inv B) * B by Th71
.= 1_Rmatrix n by A2, Def6 ;
A4: (A * B) * ((Inv B) * (Inv A)) = A * (B * ((Inv B) * (Inv A))) by Th28
.= A * ((B * (Inv B)) * (Inv A)) by Th28
.= A * ((1_Rmatrix n) * (Inv A)) by A2, Def6
.= (A * (1_Rmatrix n)) * (Inv A) by Th28
.= A * (Inv A) by Th71
.= 1_Rmatrix n by A1, Def6 ;
hence A * B is invertible by A3; :: thesis: Inv (A * B) = (Inv B) * (Inv A)
hence Inv (A * B) = (Inv B) * (Inv A) by A3, A4, Def6; :: thesis: verum