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