set M = GramMatrix (f,b);
set MT = (GramMatrix (f,b)) @ ;
for i, j being Nat st [i,j] in Indices (GramMatrix (f,b)) holds
(GramMatrix (f,b)) * (i,j) = ((GramMatrix (f,b)) @) * (i,j)
proof
let i, j be Nat; :: thesis: ( [i,j] in Indices (GramMatrix (f,b)) implies (GramMatrix (f,b)) * (i,j) = ((GramMatrix (f,b)) @) * (i,j) )
assume A1: [i,j] in Indices (GramMatrix (f,b)) ; :: thesis: (GramMatrix (f,b)) * (i,j) = ((GramMatrix (f,b)) @) * (i,j)
A2: [j,i] in Indices (GramMatrix (f,b)) by ;
Indices (GramMatrix (f,b)) = [:(Seg (rank V)),(Seg (rank V)):] by MATRIX_0:24;
then A3: ( i in Seg (rank V) & j in Seg (rank V) ) by ;
len b = rank V by ZMATRLIN:49;
then A4: ( i in dom b & j in dom b ) by ;
thus (GramMatrix (f,b)) * (i,j) = f . ((b /. i),(b /. j)) by
.= f . ((b /. j),(b /. i)) by defSymForm
.= (BilinearM (f,b,b)) * (j,i) by
.= ((GramMatrix (f,b)) @) * (i,j) by ; :: thesis: verum
end;
then GramMatrix (f,b) = (GramMatrix (f,b)) @ by MATRIX_0:27;
hence GramMatrix (f,b) is symmetric by MATRIX_6:def 5; :: thesis: verum