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;
( [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))
;
(GramMatrix (f,b)) * (i,j) = ((GramMatrix (f,b)) @) * (i,j)
A2:
[j,i] in Indices (GramMatrix (f,b))
by A1, MATRIX_0:28;
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 A1, ZFMISC_1:87;
len b = rank V
by ZMATRLIN:49;
then A4:
(
i in dom b &
j in dom b )
by A3, FINSEQ_1:def 3;
thus (GramMatrix (f,b)) * (
i,
j) =
f . (
(b /. i),
(b /. j))
by A4, ZMODLAT1:def 32
.=
f . (
(b /. j),
(b /. i))
by defSymForm
.=
(BilinearM (f,b,b)) * (
j,
i)
by A4, ZMODLAT1:def 32
.=
((GramMatrix (f,b)) @) * (
i,
j)
by A2, MATRIX_0:def 6
;
verum
end;
then
GramMatrix (f,b) = (GramMatrix (f,b)) @
by MATRIX_0:27;
hence
GramMatrix (f,b) is symmetric
by MATRIX_6:def 5; verum