let x, y be FinSequence of COMPLEX ; for M being Matrix of COMPLEX st len x = len M & len y = width M holds
(QuadraticForm (x,M,y)) *' = QuadraticForm ((x *'),(M *'),(y *'))
let M be Matrix of COMPLEX; ( len x = len M & len y = width M implies (QuadraticForm (x,M,y)) *' = QuadraticForm ((x *'),(M *'),(y *')) )
assume that
A1:
len x = len M
and
A2:
len y = width M
; (QuadraticForm (x,M,y)) *' = QuadraticForm ((x *'),(M *'),(y *'))
A3:
len (y *') = len y
by COMPLSP2:def 1;
then A4:
len (y *') = width (M *')
by A2, Def1;
len (M *') = len M
by Def1;
then A5:
len (x *') = len (M *')
by A1, COMPLSP2:def 1;
then A6: len (QuadraticForm ((x *'),(M *'),(y *'))) =
len (x *')
by A4, Def12
.=
len M
by A1, COMPLSP2:def 1
;
A7:
width ((QuadraticForm (x,M,y)) *') = width (QuadraticForm (x,M,y))
by Def1;
A8:
len ((QuadraticForm (x,M,y)) *') = len (QuadraticForm (x,M,y))
by Def1;
A9:
for i, j being Nat st [i,j] in Indices ((QuadraticForm (x,M,y)) *') holds
((QuadraticForm (x,M,y)) *') * (i,j) = (QuadraticForm ((x *'),(M *'),(y *'))) * (i,j)
proof
let i,
j be
Nat;
( [i,j] in Indices ((QuadraticForm (x,M,y)) *') implies ((QuadraticForm (x,M,y)) *') * (i,j) = (QuadraticForm ((x *'),(M *'),(y *'))) * (i,j) )
reconsider i9 =
i,
j9 =
j as
Element of
NAT by ORDINAL1:def 12;
assume A10:
[i,j] in Indices ((QuadraticForm (x,M,y)) *')
;
((QuadraticForm (x,M,y)) *') * (i,j) = (QuadraticForm ((x *'),(M *'),(y *'))) * (i,j)
then A11:
1
<= i
by Th1;
A12:
i <= len (QuadraticForm (x,M,y))
by A8, A10, Th1;
then A13:
i <= len x
by A1, A2, Def12;
i <= len M
by A1, A2, A12, Def12;
then A14:
i <= len (M *')
by Def1;
A15:
j <= width (QuadraticForm (x,M,y))
by A7, A10, Th1;
then A16:
j <= len y
by A1, A2, Def12;
j <= width M
by A1, A2, A15, Def12;
then A17:
j <= width (M *')
by Def1;
1
<= j
by A10, Th1;
then A18:
[i,j] in Indices (M *')
by A11, A14, A17, Th1;
A19:
j <= width M
by A1, A2, A15, Def12;
A20:
1
<= i
by A10, Th1;
A21:
1
<= j
by A10, Th1;
i <= len M
by A1, A2, A12, Def12;
then A22:
[i,j] in Indices M
by A21, A20, A19, Th1;
[i,j] in Indices (QuadraticForm (x,M,y))
by A11, A12, A21, A15, Th1;
then ((QuadraticForm (x,M,y)) *') * (
i,
j) =
((QuadraticForm (x,M,y)) * (i,j)) *'
by Def1
.=
(((x . i) * (M * (i,j))) * ((y . j) *')) *'
by A1, A2, A22, Def12
.=
(((x . i) * (M * (i9,j9))) * ((y *') . j)) *'
by A21, A16, COMPLSP2:def 1
.=
(((x . i) * (M * (i,j))) *') * (((y *') . j) *')
by COMPLEX1:35
.=
(((x . i) * (M * (i9,j9))) *') * (((y *') *') . j)
by A3, A21, A16, COMPLSP2:def 1
.=
(((x . i) *') * ((M * (i,j)) *')) * (((y *') *') . j)
by COMPLEX1:35
.=
(((x . i) *') * ((M *') * (i,j))) * (((y *') *') . j)
by A22, Def1
.=
(((x . i) *') * ((M *') * (i9,j9))) * (((y *') . j) *')
by A3, A21, A16, COMPLSP2:def 1
.=
(((x *') . i) * ((M *') * (i9,j9))) * (((y *') . j) *')
by A11, A13, COMPLSP2:def 1
.=
(QuadraticForm ((x *'),(M *'),(y *'))) * (
i,
j)
by A5, A4, A18, Def12
;
hence
((QuadraticForm (x,M,y)) *') * (
i,
j)
= (QuadraticForm ((x *'),(M *'),(y *'))) * (
i,
j)
;
verum
end;
A23: width ((QuadraticForm (x,M,y)) *') =
width (QuadraticForm (x,M,y))
by Def1
.=
len y
by A1, A2, Def12
;
A24: width (QuadraticForm ((x *'),(M *'),(y *'))) =
len (y *')
by A5, A4, Def12
.=
len y
by COMPLSP2:def 1
;
len ((QuadraticForm (x,M,y)) *') =
len (QuadraticForm (x,M,y))
by Def1
.=
len M
by A1, A2, Def12
;
hence
(QuadraticForm (x,M,y)) *' = QuadraticForm ((x *'),(M *'),(y *'))
by A6, A23, A24, A9, MATRIX_0:21; verum