let ra be Real; :: thesis: for M, N being Matrix of 3,F_Real
for MR, NR being Matrix of 3,REAL st MR = M & NR = N & N is symmetric & MR = ra * NR holds
M is symmetric
let M, N be Matrix of 3,F_Real; :: thesis: for MR, NR being Matrix of 3,REAL st MR = M & NR = N & N is symmetric & MR = ra * NR holds
M is symmetric
let MR, NR be Matrix of 3,REAL; :: thesis: ( MR = M & NR = N & N is symmetric & MR = ra * NR implies M is symmetric )
assume that
A1: ( MR = M & NR = N ) and
A2: N is symmetric and
A3: MR = ra * NR ; :: thesis: M is symmetric
width NR > 0 by MATRIX_0:23;
then M @ = ra * (NR @) by A1, A3, MATRIXR1:30
.= M by A1, A2, A3, MATRIX_6:def 5 ;
hence M is symmetric by MATRIX_6:def 5; :: thesis: verum