let n be Element of 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 A1: ( A is invertible & B is invertible ) ; :: thesis: ( A * B is invertible & Inv (A * B) = (Inv B) * (Inv A) )
A2: ((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 A1, Def6 ;
A3: (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 A1, 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 A2, Def5; :: thesis: Inv (A * B) = (Inv B) * (Inv A)
hence Inv (A * B) = (Inv B) * (Inv A) by A2, A3, Def6; :: thesis: verum