:: by Yuichi Futa , Hiroyuki Okazaki and Yasunari Shidama

::

:: Received February 18, 2015

:: Copyright (c) 2015-2018 Association of Mizar Users

theorem EQ2: :: ZMATRLIN:1

for D, E being non empty set

for M being Matrix of D

for L being Matrix of E

for i, j being Nat st M = L & [i,j] in Indices M holds

M * (i,j) = L * (i,j)

for M being Matrix of D

for L being Matrix of E

for i, j being Nat st M = L & [i,j] in Indices M holds

M * (i,j) = L * (i,j)

proof end;

theorem :: ZMATRLIN:2

for D, E being non empty set

for M being Matrix of D

for L being Matrix of E

for i being Nat st M = L & i in dom M holds

Line (M,i) = Line (L,i)

for M being Matrix of D

for L being Matrix of E

for i being Nat st M = L & i in dom M holds

Line (M,i) = Line (L,i)

proof end;

theorem :: ZMATRLIN:3

for D, E being non empty set

for M being Matrix of D

for L being Matrix of E

for i being Nat st M = L & i in Seg (width M) holds

Col (M,i) = Col (L,i)

for M being Matrix of D

for L being Matrix of E

for i being Nat st M = L & i in Seg (width M) holds

Col (M,i) = Col (L,i)

proof end;

theorem EQ40: :: ZMATRLIN:4

for D, E being non empty set

for M being Matrix of D

for L being Matrix of E st len M = len L & width M = width L & ( for i, j being Nat st [i,j] in Indices M holds

M * (i,j) = L * (i,j) ) holds

M = L

for M being Matrix of D

for L being Matrix of E st len M = len L & width M = width L & ( for i, j being Nat st [i,j] in Indices M holds

M * (i,j) = L * (i,j) ) holds

M = L

proof end;

theorem REALTOINT: :: ZMATRLIN:5

for D, E being non empty set

for M being Matrix of D st ( for i, j being Nat st [i,j] in Indices M holds

M * (i,j) in E ) holds

M is Matrix of E

for M being Matrix of D st ( for i, j being Nat st [i,j] in Indices M holds

M * (i,j) in E ) holds

M is Matrix of E

proof end;

theorem :: ZMATRLIN:6

for D, E being non empty set

for M being Matrix of D

for L being Matrix of E st M = L holds

M @ = L @

for M being Matrix of D

for L being Matrix of E st M = L holds

M @ = L @

proof end;

definition

let n, m be Nat;

let M be Matrix of n,m,INT;

:: original: inttorealM

redefine func inttorealM M -> Matrix of n,m,REAL;

correctness

coherence

inttorealM M is Matrix of n,m,REAL;

end;
let M be Matrix of n,m,INT;

:: original: inttorealM

redefine func inttorealM M -> Matrix of n,m,REAL;

correctness

coherence

inttorealM M is Matrix of n,m,REAL;

proof end;

definition

let n be Nat;

let M be Matrix of n,INT;

:: original: inttorealM

redefine func inttorealM M -> Matrix of n,REAL;

correctness

coherence

inttorealM M is Matrix of n,REAL;

end;
let M be Matrix of n,INT;

:: original: inttorealM

redefine func inttorealM M -> Matrix of n,REAL;

correctness

coherence

inttorealM M is Matrix of n,REAL;

proof end;

definition
end;

:: deftheorem defines integer ZMATRLIN:def 2 :

for M being Matrix of REAL holds

( M is integer iff M is Matrix of INT );

for M being Matrix of REAL holds

( M is integer iff M is Matrix of INT );

registration

existence

ex b_{1} being Matrix of REAL st b_{1} is integer ;

end;

cluster Relation-like NAT -defined REAL * -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V201() tabular FinSequence-yielding finite-support integer for Matrix of ;

correctness existence

ex b

proof end;

registration

let n, m be Nat;

existence

ex b_{1} being Matrix of n,m,REAL st b_{1} is integer ;

end;
cluster Relation-like NAT -defined REAL * -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V201() tabular V207( REAL ,n,m) FinSequence-yielding finite-support integer for Matrix of ,,;

correctness existence

ex b

proof end;

definition
end;

:: deftheorem defines realtointM ZMATRLIN:def 3 :

for M being integer Matrix of REAL holds realtointM M = M;

for M being integer Matrix of REAL holds realtointM M = M;

definition

let n, m be Nat;

let M be integer Matrix of n,m,REAL;

:: original: realtointM

redefine func realtointM M -> Matrix of n,m,INT;

correctness

coherence

realtointM M is Matrix of n,m,INT;

end;
let M be integer Matrix of n,m,REAL;

:: original: realtointM

redefine func realtointM M -> Matrix of n,m,INT;

correctness

coherence

realtointM M is Matrix of n,m,INT;

proof end;

definition

let n be Nat;

let M be integer Matrix of n,REAL;

:: original: realtointM

redefine func realtointM M -> Matrix of n,INT;

correctness

coherence

realtointM M is Matrix of n,INT;

end;
let M be integer Matrix of n,REAL;

:: original: realtointM

redefine func realtointM M -> Matrix of n,INT;

correctness

coherence

realtointM M is Matrix of n,INT;

proof end;

definition

let n, m be Nat;

correctness

coherence

n |-> (m |-> (0. INT.Ring)) is Matrix of n,m,INT.Ring;

end;
correctness

coherence

n |-> (m |-> (0. INT.Ring)) is Matrix of n,m,INT.Ring;

proof end;

:: deftheorem defines 0. ZMATRLIN:def 4 :

for n, m being Nat holds 0. (n,m) = n |-> (m |-> (0. INT.Ring));

for n, m being Nat holds 0. (n,m) = n |-> (m |-> (0. INT.Ring));

Th5: for V being free Z_Module

for KL1, KL2 being Linear_Combination of V

for X being Subset of V st X is linearly-independent & Carrier KL1 c= X & Carrier KL2 c= X & Sum KL1 = Sum KL2 holds

KL1 = KL2

by ZMODUL03:3;

theorem Th6: :: ZMATRLIN:8

for V being free Z_Module

for KL1, KL2, KL3 being Linear_Combination of V

for X being Subset of V st X is linearly-independent & Carrier KL1 c= X & Carrier KL2 c= X & Carrier KL3 c= X & Sum KL1 = (Sum KL2) + (Sum KL3) holds

KL1 = KL2 + KL3

for KL1, KL2, KL3 being Linear_Combination of V

for X being Subset of V st X is linearly-independent & Carrier KL1 c= X & Carrier KL2 c= X & Carrier KL3 c= X & Sum KL1 = (Sum KL2) + (Sum KL3) holds

KL1 = KL2 + KL3

proof end;

theorem Th7: :: ZMATRLIN:9

for V being free Z_Module

for a being Element of INT.Ring

for KL1, KL2 being Linear_Combination of V

for X being Subset of V st X is linearly-independent & Carrier KL1 c= X & Carrier KL2 c= X & a <> 0. INT.Ring & Sum KL1 = a * (Sum KL2) holds

KL1 = a * KL2

for a being Element of INT.Ring

for KL1, KL2 being Linear_Combination of V

for X being Subset of V st X is linearly-independent & Carrier KL1 c= X & Carrier KL2 c= X & a <> 0. INT.Ring & Sum KL1 = a * (Sum KL2) holds

KL1 = a * KL2

proof end;

theorem Th8: :: ZMATRLIN:10

for V being free finite-rank Z_Module

for W being Element of V

for b2 being Basis of V ex KL being Linear_Combination of V st

( W = Sum KL & Carrier KL c= b2 )

for W being Element of V

for b2 being Basis of V ex KL being Linear_Combination of V st

( W = Sum KL & Carrier KL c= b2 )

proof end;

definition

let V be free finite-rank Z_Module;

ex b_{1} being FinSequence of V st

( b_{1} is one-to-one & rng b_{1} is Basis of V )

end;
mode OrdBasis of V -> FinSequence of V means :defOrdBasis: :: ZMATRLIN:def 5

( it is one-to-one & rng it is Basis of V );

existence ( it is one-to-one & rng it is Basis of V );

ex b

( b

proof end;

:: deftheorem defOrdBasis defines OrdBasis ZMATRLIN:def 5 :

for V being free finite-rank Z_Module

for b_{2} being FinSequence of V holds

( b_{2} is OrdBasis of V iff ( b_{2} is one-to-one & rng b_{2} is Basis of V ) );

for V being free finite-rank Z_Module

for b

( b

theorem Th9: :: ZMATRLIN:11

for V1 being free finite-rank Z_Module

for a being Element of V1

for F being FinSequence of V1

for G being FinSequence of INT.Ring st len F = len G & ( for k being Nat

for v being Element of INT.Ring st k in dom F & v = G . k holds

F . k = v * a ) holds

Sum F = (Sum G) * a

for a being Element of V1

for F being FinSequence of V1

for G being FinSequence of INT.Ring st len F = len G & ( for k being Nat

for v being Element of INT.Ring st k in dom F & v = G . k holds

F . k = v * a ) holds

Sum F = (Sum G) * a

proof end;

theorem Th10: :: ZMATRLIN:12

for V1 being free finite-rank Z_Module

for a being Element of V1

for F being FinSequence of INT.Ring

for G being FinSequence of V1 st len F = len G & ( for k being Nat st k in dom F holds

G . k = (F /. k) * a ) holds

Sum G = (Sum F) * a

for a being Element of V1

for F being FinSequence of INT.Ring

for G being FinSequence of V1 st len F = len G & ( for k being Nat st k in dom F holds

G . k = (F /. k) * a ) holds

Sum G = (Sum F) * a

proof end;

definition

let V1 be free finite-rank Z_Module;

let p1 be FinSequence of INT.Ring;

let p2 be FinSequence of V1;

coherence

the lmult of V1 .: (p1,p2) is FinSequence of V1 ;

end;
let p1 be FinSequence of INT.Ring;

let p2 be FinSequence of V1;

coherence

the lmult of V1 .: (p1,p2) is FinSequence of V1 ;

:: deftheorem defines lmlt ZMATRLIN:def 6 :

for V1 being free finite-rank Z_Module

for p1 being FinSequence of INT.Ring

for p2 being FinSequence of V1 holds lmlt (p1,p2) = the lmult of V1 .: (p1,p2);

for V1 being free finite-rank Z_Module

for p1 being FinSequence of INT.Ring

for p2 being FinSequence of V1 holds lmlt (p1,p2) = the lmult of V1 .: (p1,p2);

theorem Th12: :: ZMATRLIN:13

for V1 being free finite-rank Z_Module

for p2 being FinSequence of V1

for p1 being FinSequence of INT.Ring st dom p1 = dom p2 holds

dom (lmlt (p1,p2)) = dom p1

for p2 being FinSequence of V1

for p1 being FinSequence of INT.Ring st dom p1 = dom p2 holds

dom (lmlt (p1,p2)) = dom p1

proof end;

theorem Th13: :: ZMATRLIN:14

for V1 being free finite-rank Z_Module

for M being Matrix of the carrier of V1 st len M = 0 holds

Sum (Sum M) = 0. V1

for M being Matrix of the carrier of V1 st len M = 0 holds

Sum (Sum M) = 0. V1

proof end;

theorem Th14: :: ZMATRLIN:15

for m being Nat

for V1 being free finite-rank Z_Module

for M being Matrix of m + 1, 0 , the carrier of V1 holds Sum (Sum M) = 0. V1

for V1 being free finite-rank Z_Module

for M being Matrix of m + 1, 0 , the carrier of V1 holds Sum (Sum M) = 0. V1

proof end;

theorem Th16: :: ZMATRLIN:16

for V1, V2 being Z_Module

for f being Function of V1,V2

for p being FinSequence of V1 st f is additive & f is homogeneous holds

f . (Sum p) = Sum (f * p)

for f being Function of V1,V2

for p being FinSequence of V1 st f is additive & f is homogeneous holds

f . (Sum p) = Sum (f * p)

proof end;

theorem Th17: :: ZMATRLIN:17

for V1, V2 being free finite-rank Z_Module

for f being Function of V1,V2

for a being FinSequence of INT.Ring

for p being FinSequence of V1 st len p = len a & f is additive & f is homogeneous holds

f * (lmlt (a,p)) = lmlt (a,(f * p))

for f being Function of V1,V2

for a being FinSequence of INT.Ring

for p being FinSequence of V1 st len p = len a & f is additive & f is homogeneous holds

f * (lmlt (a,p)) = lmlt (a,(f * p))

proof end;

theorem Th18: :: ZMATRLIN:18

for V2, V3 being free finite-rank Z_Module

for g being Function of V2,V3

for b2 being OrdBasis of V2

for a being FinSequence of INT.Ring st len a = len b2 & g is additive & g is homogeneous holds

g . (Sum (lmlt (a,b2))) = Sum (lmlt (a,(g * b2)))

for g being Function of V2,V3

for b2 being OrdBasis of V2

for a being FinSequence of INT.Ring st len a = len b2 & g is additive & g is homogeneous holds

g . (Sum (lmlt (a,b2))) = Sum (lmlt (a,(g * b2)))

proof end;

theorem Th19: :: ZMATRLIN:19

for V1 being free finite-rank Z_Module

for F, F1 being FinSequence of V1

for KL being Linear_Combination of V1

for p being Permutation of (dom F) st F1 = F * p holds

KL (#) F1 = (KL (#) F) * p

for F, F1 being FinSequence of V1

for KL being Linear_Combination of V1

for p being Permutation of (dom F) st F1 = F * p holds

KL (#) F1 = (KL (#) F) * p

proof end;

theorem Th20: :: ZMATRLIN:20

for V1 being free finite-rank Z_Module

for F being FinSequence of V1

for KL being Linear_Combination of V1 st F is one-to-one & Carrier KL c= rng F holds

Sum (KL (#) F) = Sum KL

for F being FinSequence of V1

for KL being Linear_Combination of V1 st F is one-to-one & Carrier KL c= rng F holds

Sum (KL (#) F) = Sum KL

proof end;

theorem Th21: :: ZMATRLIN:21

for V1, V2 being free finite-rank Z_Module

for f1, f2 being Function of V1,V2

for A being set

for p being FinSequence of V1 st rng p c= A & f1 is additive & f1 is homogeneous & f2 is additive & f2 is homogeneous & ( for v being Element of V1 st v in A holds

f1 . v = f2 . v ) holds

f1 . (Sum p) = f2 . (Sum p)

for f1, f2 being Function of V1,V2

for A being set

for p being FinSequence of V1 st rng p c= A & f1 is additive & f1 is homogeneous & f2 is additive & f2 is homogeneous & ( for v being Element of V1 st v in A holds

f1 . v = f2 . v ) holds

f1 . (Sum p) = f2 . (Sum p)

proof end;

theorem Th22: :: ZMATRLIN:22

for V1, V2 being free finite-rank Z_Module

for f1, f2 being Function of V1,V2 st f1 is additive & f1 is homogeneous & f2 is additive & f2 is homogeneous holds

for b1 being OrdBasis of V1 st len b1 > 0 & f1 * b1 = f2 * b1 holds

f1 = f2

for f1, f2 being Function of V1,V2 st f1 is additive & f1 is homogeneous & f2 is additive & f2 is homogeneous holds

for b1 being OrdBasis of V1 st len b1 > 0 & f1 * b1 = f2 * b1 holds

f1 = f2

proof end;

theorem Th27: :: ZMATRLIN:23

for k, m, n being Nat

for V being free finite-rank Z_Module

for M1 being Matrix of n,k, the carrier of V

for M2 being Matrix of m,k, the carrier of V holds Sum (M1 ^ M2) = (Sum M1) ^ (Sum M2)

for V being free finite-rank Z_Module

for M1 being Matrix of n,k, the carrier of V

for M2 being Matrix of m,k, the carrier of V holds Sum (M1 ^ M2) = (Sum M1) ^ (Sum M2)

proof end;

theorem Th29: :: ZMATRLIN:24

for V1 being free finite-rank Z_Module

for M1, M2 being Matrix of the carrier of V1 holds (Sum M1) + (Sum M2) = Sum (M1 ^^ M2)

for M1, M2 being Matrix of the carrier of V1 holds (Sum M1) + (Sum M2) = Sum (M1 ^^ M2)

proof end;

theorem Th30: :: ZMATRLIN:25

for V1 being free finite-rank Z_Module

for P1, P2 being FinSequence of V1 st len P1 = len P2 holds

Sum (P1 + P2) = (Sum P1) + (Sum P2)

for P1, P2 being FinSequence of V1 st len P1 = len P2 holds

Sum (P1 + P2) = (Sum P1) + (Sum P2)

proof end;

theorem Th31: :: ZMATRLIN:26

for V1 being free finite-rank Z_Module

for M1, M2 being Matrix of the carrier of V1 st len M1 = len M2 holds

(Sum (Sum M1)) + (Sum (Sum M2)) = Sum (Sum (M1 ^^ M2))

for M1, M2 being Matrix of the carrier of V1 st len M1 = len M2 holds

(Sum (Sum M1)) + (Sum (Sum M2)) = Sum (Sum (M1 ^^ M2))

proof end;

theorem Th32: :: ZMATRLIN:27

for V1 being free finite-rank Z_Module

for M being Matrix of the carrier of V1 holds Sum (Sum M) = Sum (Sum (M @))

for M being Matrix of the carrier of V1 holds Sum (Sum M) = Sum (Sum (M @))

proof end;

theorem Th33: :: ZMATRLIN:28

for m, n being Nat

for V1 being free finite-rank Z_Module

for M being Matrix of n,m,INT.Ring st n > 0 & m > 0 holds

for p, d being FinSequence of INT.Ring st len p = n & len d = m & ( for j being Nat st j in dom d holds

d /. j = Sum (mlt (p,(Col (M,j)))) ) holds

for b, c being FinSequence of V1 st len b = m & len c = n & ( for i being Nat st i in dom c holds

c /. i = Sum (lmlt ((Line (M,i)),b)) ) holds

Sum (lmlt (p,c)) = Sum (lmlt (d,b))

for V1 being free finite-rank Z_Module

for M being Matrix of n,m,INT.Ring st n > 0 & m > 0 holds

for p, d being FinSequence of INT.Ring st len p = n & len d = m & ( for j being Nat st j in dom d holds

d /. j = Sum (mlt (p,(Col (M,j)))) ) holds

for b, c being FinSequence of V1 st len b = m & len c = n & ( for i being Nat st i in dom c holds

c /. i = Sum (lmlt ((Line (M,i)),b)) ) holds

Sum (lmlt (p,c)) = Sum (lmlt (d,b))

proof end;

definition

let V be free finite-rank Z_Module;

let b1 be OrdBasis of V;

let W be Element of V;

ex b_{1} being FinSequence of INT.Ring st

( len b_{1} = len b1 & ex KL being Linear_Combination of V st

( W = Sum KL & Carrier KL c= rng b1 & ( for k being Nat st 1 <= k & k <= len b_{1} holds

b_{1} /. k = KL . (b1 /. k) ) ) )

for b_{1}, b_{2} being FinSequence of INT.Ring st len b_{1} = len b1 & ex KL being Linear_Combination of V st

( W = Sum KL & Carrier KL c= rng b1 & ( for k being Nat st 1 <= k & k <= len b_{1} holds

b_{1} /. k = KL . (b1 /. k) ) ) & len b_{2} = len b1 & ex KL being Linear_Combination of V st

( W = Sum KL & Carrier KL c= rng b1 & ( for k being Nat st 1 <= k & k <= len b_{2} holds

b_{2} /. k = KL . (b1 /. k) ) ) holds

b_{1} = b_{2}

end;
let b1 be OrdBasis of V;

let W be Element of V;

func W |-- b1 -> FinSequence of INT.Ring means :Def7: :: ZMATRLIN:def 7

( len it = len b1 & ex KL being Linear_Combination of V st

( W = Sum KL & Carrier KL c= rng b1 & ( for k being Nat st 1 <= k & k <= len it holds

it /. k = KL . (b1 /. k) ) ) );

existence ( len it = len b1 & ex KL being Linear_Combination of V st

( W = Sum KL & Carrier KL c= rng b1 & ( for k being Nat st 1 <= k & k <= len it holds

it /. k = KL . (b1 /. k) ) ) );

ex b

( len b

( W = Sum KL & Carrier KL c= rng b1 & ( for k being Nat st 1 <= k & k <= len b

b

proof end;

uniqueness for b

( W = Sum KL & Carrier KL c= rng b1 & ( for k being Nat st 1 <= k & k <= len b

b

( W = Sum KL & Carrier KL c= rng b1 & ( for k being Nat st 1 <= k & k <= len b

b

b

proof end;

:: deftheorem Def7 defines |-- ZMATRLIN:def 7 :

for V being free finite-rank Z_Module

for b1 being OrdBasis of V

for W being Element of V

for b_{4} being FinSequence of INT.Ring holds

( b_{4} = W |-- b1 iff ( len b_{4} = len b1 & ex KL being Linear_Combination of V st

( W = Sum KL & Carrier KL c= rng b1 & ( for k being Nat st 1 <= k & k <= len b_{4} holds

b_{4} /. k = KL . (b1 /. k) ) ) ) );

for V being free finite-rank Z_Module

for b1 being OrdBasis of V

for W being Element of V

for b

( b

( W = Sum KL & Carrier KL c= rng b1 & ( for k being Nat st 1 <= k & k <= len b

b

Lm1: for V being free finite-rank Z_Module

for b being OrdBasis of V

for W being Element of V holds dom (W |-- b) = dom b

proof end;

theorem Th34: :: ZMATRLIN:29

for V2 being free finite-rank Z_Module

for b2 being OrdBasis of V2

for v1, v2 being Vector of V2 st v1 |-- b2 = v2 |-- b2 holds

v1 = v2

for b2 being OrdBasis of V2

for v1, v2 being Vector of V2 st v1 |-- b2 = v2 |-- b2 holds

v1 = v2

proof end;

theorem Th35: :: ZMATRLIN:30

for V1 being free finite-rank Z_Module

for b1 being OrdBasis of V1

for v being Element of V1 holds v = Sum (lmlt ((v |-- b1),b1))

for b1 being OrdBasis of V1

for v being Element of V1 holds v = Sum (lmlt ((v |-- b1),b1))

proof end;

theorem Th36: :: ZMATRLIN:31

for V1 being free finite-rank Z_Module

for b1 being OrdBasis of V1

for d being FinSequence of INT.Ring st len d = len b1 holds

d = (Sum (lmlt (d,b1))) |-- b1

for b1 being OrdBasis of V1

for d being FinSequence of INT.Ring st len d = len b1 holds

d = (Sum (lmlt (d,b1))) |-- b1

proof end;

Lm2: for p being FinSequence

for k being set st k in dom p holds

len p > 0

proof end;

theorem Th37: :: ZMATRLIN:32

for V1, V2 being free finite-rank Z_Module

for f being Function of V1,V2

for b1 being OrdBasis of V1

for b2 being OrdBasis of V2

for a, d being FinSequence of INT.Ring st len a = len b1 holds

for j being Nat st j in dom b2 & len d = len b1 & ( for k being Nat st k in dom b1 holds

d . k = ((f . (b1 /. k)) |-- b2) /. j ) & len b1 > 0 holds

((Sum (lmlt (a,(f * b1)))) |-- b2) /. j = Sum (mlt (a,d))

for f being Function of V1,V2

for b1 being OrdBasis of V1

for b2 being OrdBasis of V2

for a, d being FinSequence of INT.Ring st len a = len b1 holds

for j being Nat st j in dom b2 & len d = len b1 & ( for k being Nat st k in dom b1 holds

d . k = ((f . (b1 /. k)) |-- b2) /. j ) & len b1 > 0 holds

((Sum (lmlt (a,(f * b1)))) |-- b2) /. j = Sum (mlt (a,d))

proof end;

definition

let V1, V2 be free finite-rank Z_Module;

let f be Function of V1,V2;

let b1 be FinSequence of V1;

let b2 be OrdBasis of V2;

ex b_{1} being Matrix of INT.Ring st

( len b_{1} = len b1 & ( for k being Nat st k in dom b1 holds

b_{1} /. k = (f . (b1 /. k)) |-- b2 ) )

for b_{1}, b_{2} being Matrix of INT.Ring st len b_{1} = len b1 & ( for k being Nat st k in dom b1 holds

b_{1} /. k = (f . (b1 /. k)) |-- b2 ) & len b_{2} = len b1 & ( for k being Nat st k in dom b1 holds

b_{2} /. k = (f . (b1 /. k)) |-- b2 ) holds

b_{1} = b_{2}

end;
let f be Function of V1,V2;

let b1 be FinSequence of V1;

let b2 be OrdBasis of V2;

func AutMt (f,b1,b2) -> Matrix of INT.Ring means :Def8: :: ZMATRLIN:def 8

( len it = len b1 & ( for k being Nat st k in dom b1 holds

it /. k = (f . (b1 /. k)) |-- b2 ) );

existence ( len it = len b1 & ( for k being Nat st k in dom b1 holds

it /. k = (f . (b1 /. k)) |-- b2 ) );

ex b

( len b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def8 defines AutMt ZMATRLIN:def 8 :

for V1, V2 being free finite-rank Z_Module

for f being Function of V1,V2

for b1 being FinSequence of V1

for b2 being OrdBasis of V2

for b_{6} being Matrix of INT.Ring holds

( b_{6} = AutMt (f,b1,b2) iff ( len b_{6} = len b1 & ( for k being Nat st k in dom b1 holds

b_{6} /. k = (f . (b1 /. k)) |-- b2 ) ) );

for V1, V2 being free finite-rank Z_Module

for f being Function of V1,V2

for b1 being FinSequence of V1

for b2 being OrdBasis of V2

for b

( b

b

Lm3: for V1, V2 being free finite-rank Z_Module

for f being Function of V1,V2

for b1 being OrdBasis of V1

for b2 being OrdBasis of V2 holds dom (AutMt (f,b1,b2)) = dom b1

proof end;

theorem Th38: :: ZMATRLIN:33

for V1, V2 being free finite-rank Z_Module

for f being Function of V1,V2

for b1 being OrdBasis of V1

for b2 being OrdBasis of V2 st len b1 = 0 holds

AutMt (f,b1,b2) = {}

for f being Function of V1,V2

for b1 being OrdBasis of V1

for b2 being OrdBasis of V2 st len b1 = 0 holds

AutMt (f,b1,b2) = {}

proof end;

theorem Th39: :: ZMATRLIN:34

for V1, V2 being free finite-rank Z_Module

for f being Function of V1,V2

for b1 being OrdBasis of V1

for b2 being OrdBasis of V2 st len b1 > 0 holds

width (AutMt (f,b1,b2)) = len b2

for f being Function of V1,V2

for b1 being OrdBasis of V1

for b2 being OrdBasis of V2 st len b1 > 0 holds

width (AutMt (f,b1,b2)) = len b2

proof end;

theorem :: ZMATRLIN:35

for V1, V2 being free finite-rank Z_Module

for f1, f2 being Function of V1,V2

for b1 being OrdBasis of V1

for b2 being OrdBasis of V2 st f1 is additive & f1 is homogeneous & f2 is additive & f2 is homogeneous & AutMt (f1,b1,b2) = AutMt (f2,b1,b2) & len b1 > 0 holds

f1 = f2

for f1, f2 being Function of V1,V2

for b1 being OrdBasis of V1

for b2 being OrdBasis of V2 st f1 is additive & f1 is homogeneous & f2 is additive & f2 is homogeneous & AutMt (f1,b1,b2) = AutMt (f2,b1,b2) & len b1 > 0 holds

f1 = f2

proof end;

LMEQ5: for f, g, h being Function st f | (dom g) = g & rng h c= dom g & rng h c= dom f holds

f * h = g * h

proof end;

LMLT12: multint = multreal | [:INT,INT:]

proof end;

theorem :: ZMATRLIN:37

for p, q being FinSequence of INT.Ring

for p1, q1 being FinSequence of F_Real st p = p1 & q = q1 holds

p "*" q = p1 "*" q1

for p1, q1 being FinSequence of F_Real st p = p1 & q = q1 holds

p "*" q = p1 "*" q1

proof end;

theorem ThComp1: :: ZMATRLIN:38

for V1, V2, V3 being free finite-rank Z_Module

for f being Function of V1,V2

for g being Function of V2,V3

for b1 being OrdBasis of V1

for b2 being OrdBasis of V2

for b3 being OrdBasis of V3 st g is additive & g is homogeneous & len b1 > 0 & len b2 > 0 holds

AutMt ((g * f),b1,b3) = (AutMt (f,b1,b2)) * (AutMt (g,b2,b3))

for f being Function of V1,V2

for g being Function of V2,V3

for b1 being OrdBasis of V1

for b2 being OrdBasis of V2

for b3 being OrdBasis of V3 st g is additive & g is homogeneous & len b1 > 0 & len b2 > 0 holds

AutMt ((g * f),b1,b3) = (AutMt (f,b1,b2)) * (AutMt (g,b2,b3))

proof end;

theorem :: ZMATRLIN:39

for V1, V2 being free finite-rank Z_Module

for f1, f2 being Function of V1,V2

for b1 being OrdBasis of V1

for b2 being OrdBasis of V2 holds AutMt ((f1 + f2),b1,b2) = (AutMt (f1,b1,b2)) + (AutMt (f2,b1,b2))

for f1, f2 being Function of V1,V2

for b1 being OrdBasis of V1

for b2 being OrdBasis of V2 holds AutMt ((f1 + f2),b1,b2) = (AutMt (f1,b1,b2)) + (AutMt (f2,b1,b2))

proof end;

theorem :: ZMATRLIN:40

for a being Element of INT.Ring

for V1, V2 being free finite-rank Z_Module

for f being Function of V1,V2

for b1 being OrdBasis of V1

for b2 being OrdBasis of V2 st a <> 0. INT.Ring holds

AutMt ((a * f),b1,b2) = a * (AutMt (f,b1,b2))

for V1, V2 being free finite-rank Z_Module

for f being Function of V1,V2

for b1 being OrdBasis of V1

for b2 being OrdBasis of V2 st a <> 0. INT.Ring holds

AutMt ((a * f),b1,b2) = a * (AutMt (f,b1,b2))

proof end;

theorem LmSign1B: :: ZMATRLIN:41

for D, E being non empty set

for n, m, i, j being Nat

for M being Matrix of n,m,D st 0 < n & M is Matrix of n,m,E & [i,j] in Indices M holds

M * (i,j) is Element of E

for n, m, i, j being Nat

for M being Matrix of n,m,D st 0 < n & M is Matrix of n,m,E & [i,j] in Indices M holds

M * (i,j) is Element of E

proof end;

theorem LmSign1C: :: ZMATRLIN:42

for F being FinSequence of F_Real st ( for i being Nat st i in dom F holds

F . i in INT ) holds

Sum F in INT

F . i in INT ) holds

Sum F in INT

proof end;

theorem LmSign1D: :: ZMATRLIN:43

for i being Nat

for j being Element of F_Real st j in INT holds

((power F_Real) . ((- (1_ F_Real)),i)) * j in INT

for j being Element of F_Real st j in INT holds

((power F_Real) . ((- (1_ F_Real)),i)) * j in INT

proof end;

theorem LmSign1F: :: ZMATRLIN:44

for n, i, j, k, m being Nat

for M being Matrix of n + 1,F_Real st 0 < n & M is Matrix of n + 1,INT & [i,j] in Indices M & [k,m] in Indices (Delete (M,i,j)) holds

(Delete (M,i,j)) * (k,m) is Element of INT

for M being Matrix of n + 1,F_Real st 0 < n & M is Matrix of n + 1,INT & [i,j] in Indices M & [k,m] in Indices (Delete (M,i,j)) holds

(Delete (M,i,j)) * (k,m) is Element of INT

proof end;

theorem LmSign1E: :: ZMATRLIN:45

for n, i, j being Nat

for M being Matrix of n + 1,F_Real st 0 < n & M is Matrix of n + 1,INT & [i,j] in Indices M holds

Delete (M,i,j) is Matrix of n,INT

for M being Matrix of n + 1,F_Real st 0 < n & M is Matrix of n + 1,INT & [i,j] in Indices M holds

Delete (M,i,j) is Matrix of n,INT

proof end;

theorem :: ZMATRLIN:47

registration
end;

theorem LMThMBF3: :: ZMATRLIN:50

for V being free finite-rank Z_Module

for b1, b2 being OrdBasis of V holds AutMt ((id V),b1,b2) is Matrix of rank V,INT.Ring

for b1, b2 being OrdBasis of V holds AutMt ((id V),b1,b2) is Matrix of rank V,INT.Ring

proof end;

theorem :: ZMATRLIN:51

for V being free finite-rank Z_Module

for b1, b2 being OrdBasis of V

for M being Matrix of rank V,F_Real st M = AutMt ((id V),b1,b2) holds

Det M in INT

for b1, b2 being OrdBasis of V

for M being Matrix of rank V,F_Real st M = AutMt ((id V),b1,b2) holds

Det M in INT

proof end;

theorem LmSign31X: :: ZMATRLIN:52

for V1 being free finite-rank Z_Module

for b1 being OrdBasis of V1

for i, j being Nat st i in dom b1 & j in dom b1 holds

( ( i = j implies ((b1 /. i) |-- b1) . j = 1 ) & ( i <> j implies ((b1 /. i) |-- b1) . j = 0 ) )

for b1 being OrdBasis of V1

for i, j being Nat st i in dom b1 & j in dom b1 holds

( ( i = j implies ((b1 /. i) |-- b1) . j = 1 ) & ( i <> j implies ((b1 /. i) |-- b1) . j = 0 ) )

proof end;

theorem LmSign31: :: ZMATRLIN:53

for V being free finite-rank Z_Module

for b1 being OrdBasis of V st rank V > 0 holds

AutMt ((id V),b1,b1) = 1. (INT.Ring,(rank V))

for b1 being OrdBasis of V st rank V > 0 holds

AutMt ((id V),b1,b1) = 1. (INT.Ring,(rank V))

proof end;

theorem LmSign3: :: ZMATRLIN:54

for V being free finite-rank Z_Module

for b1, b2 being OrdBasis of V st rank V > 0 holds

(AutMt ((id V),b1,b2)) * (AutMt ((id V),b2,b1)) = 1. (INT.Ring,(rank V))

for b1, b2 being OrdBasis of V st rank V > 0 holds

(AutMt ((id V),b1,b2)) * (AutMt ((id V),b2,b1)) = 1. (INT.Ring,(rank V))

proof end;

theorem ThSign1: :: ZMATRLIN:55

for V being free finite-rank Z_Module

for b1, b2 being OrdBasis of V

for M being Matrix of rank V,INT.Ring st M = AutMt ((id V),b1,b2) holds

|.(Det M).| = 1

for b1, b2 being OrdBasis of V

for M being Matrix of rank V,INT.Ring st M = AutMt ((id V),b1,b2) holds

|.(Det M).| = 1

proof end;

registration

let V be non empty ModuleStr over INT.Ring ;

ex b_{1} being Functional of V st

( b_{1} is additive & b_{1} is homogeneous & b_{1} is 0-preserving )

end;
cluster Relation-like the carrier of V -defined the carrier of INT.Ring -valued Function-like non empty total quasi_total V53() V54() V55() additive homogeneous 0-preserving for Functional of ;

existence ex b

( b

proof end;

definition

let V be non empty ModuleStr over INT.Ring ;

mode linear-Functional of V is additive homogeneous Functional of V;

end;
mode linear-Functional of V is additive homogeneous Functional of V;

theorem VS10Th1: :: ZMATRLIN:56

for a being Element of INT.Ring

for V being non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ModuleStr over INT.Ring

for v being Vector of V holds

( (0. INT.Ring) * v = 0. V & a * (0. V) = 0. V )

for V being non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ModuleStr over INT.Ring

for v being Vector of V holds

( (0. INT.Ring) * v = 0. V & a * (0. V) = 0. V )

proof end;

registration

let V be non empty ModuleStr over INT.Ring ;

ex b_{1} being Functional of V st

( b_{1} is additive & b_{1} is 0-preserving )

end;
cluster Relation-like the carrier of V -defined the carrier of INT.Ring -valued Function-like non empty total quasi_total V53() V54() V55() additive 0-preserving for Functional of ;

existence ex b

( b

proof end;

registration

let V be non empty right_zeroed ModuleStr over INT.Ring ;

coherence

for b_{1} being Functional of V st b_{1} is additive holds

b_{1} is 0-preserving

end;
coherence

for b

b

proof end;

registration

let V be non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ModuleStr over INT.Ring ;

coherence

for b_{1} being Functional of V st b_{1} is homogeneous holds

b_{1} is 0-preserving

end;
coherence

for b

b

proof end;

registration
end;

registration

let V be non empty ModuleStr over INT.Ring ;

ex b_{1} being Functional of V st b_{1} is constant

end;
cluster Relation-like the carrier of V -defined the carrier of INT.Ring -valued Function-like constant non empty total quasi_total V53() V54() V55() for Functional of ;

existence ex b

proof end;

definition

let V be non empty right_zeroed ModuleStr over INT.Ring ;

let f be 0-preserving Functional of V;

compatibility

( f is constant iff f = 0Functional V )

end;
let f be 0-preserving Functional of V;

compatibility

( f is constant iff f = 0Functional V )

proof end;

:: deftheorem defines constant ZMATRLIN:def 9 :

for V being non empty right_zeroed ModuleStr over INT.Ring

for f being 0-preserving Functional of V holds

( f is constant iff f = 0Functional V );

for V being non empty right_zeroed ModuleStr over INT.Ring

for f being 0-preserving Functional of V holds

( f is constant iff f = 0Functional V );

registration

let V be non empty right_zeroed ModuleStr over INT.Ring ;

ex b_{1} being Functional of V st

( b_{1} is constant & b_{1} is additive & b_{1} is 0-preserving )

end;
cluster Relation-like the carrier of V -defined the carrier of INT.Ring -valued Function-like constant non empty total quasi_total V53() V54() V55() additive 0-preserving for Functional of ;

existence ex b

( b

proof end;

LMPROJ1: for V being free Z_Module

for A, B being Subset of V st A c= B & B is Basis of V holds

ex F being linear-transformation of V,V st

( ( for v being Vector of V ex vA, vB being Vector of V st

( vA in Lin A & vB in Lin (B \ A) & v = vA + vB & F . v = vA ) ) & ( for v, vA, vB being Vector of V st vA in Lin A & vB in Lin (B \ A) & v = vA + vB holds

F . v = vA ) )

proof end;

definition

let V be free Z_Module;

let A, B be Subset of V;

assume AS: ( A c= B & B is Basis of V ) ;

ex b_{1} being linear-transformation of V,V st

( ( for v being Vector of V ex vA, vB being Vector of V st

( vA in Lin A & vB in Lin (B \ A) & v = vA + vB & b_{1} . v = vA ) ) & ( for v, vA, vB being Vector of V st vA in Lin A & vB in Lin (B \ A) & v = vA + vB holds

b_{1} . v = vA ) )
by LMPROJ1, AS;

uniqueness

for b_{1}, b_{2} being linear-transformation of V,V st ( for v being Vector of V ex vA, vB being Vector of V st

( vA in Lin A & vB in Lin (B \ A) & v = vA + vB & b_{1} . v = vA ) ) & ( for v, vA, vB being Vector of V st vA in Lin A & vB in Lin (B \ A) & v = vA + vB holds

b_{1} . v = vA ) & ( for v being Vector of V ex vA, vB being Vector of V st

( vA in Lin A & vB in Lin (B \ A) & v = vA + vB & b_{2} . v = vA ) ) & ( for v, vA, vB being Vector of V st vA in Lin A & vB in Lin (B \ A) & v = vA + vB holds

b_{2} . v = vA ) holds

b_{1} = b_{2}

end;
let A, B be Subset of V;

assume AS: ( A c= B & B is Basis of V ) ;

func Proj (A,B) -> linear-transformation of V,V means :: ZMATRLIN:def 10

( ( for v being Vector of V ex vA, vB being Vector of V st

( vA in Lin A & vB in Lin (B \ A) & v = vA + vB & it . v = vA ) ) & ( for v, vA, vB being Vector of V st vA in Lin A & vB in Lin (B \ A) & v = vA + vB holds

it . v = vA ) );

existence ( ( for v being Vector of V ex vA, vB being Vector of V st

( vA in Lin A & vB in Lin (B \ A) & v = vA + vB & it . v = vA ) ) & ( for v, vA, vB being Vector of V st vA in Lin A & vB in Lin (B \ A) & v = vA + vB holds

it . v = vA ) );

ex b

( ( for v being Vector of V ex vA, vB being Vector of V st

( vA in Lin A & vB in Lin (B \ A) & v = vA + vB & b

b

uniqueness

for b

( vA in Lin A & vB in Lin (B \ A) & v = vA + vB & b

b

( vA in Lin A & vB in Lin (B \ A) & v = vA + vB & b

b

b

proof end;

:: deftheorem defines Proj ZMATRLIN:def 10 :

for V being free Z_Module

for A, B being Subset of V st A c= B & B is Basis of V holds

for b_{4} being linear-transformation of V,V holds

( b_{4} = Proj (A,B) iff ( ( for v being Vector of V ex vA, vB being Vector of V st

( vA in Lin A & vB in Lin (B \ A) & v = vA + vB & b_{4} . v = vA ) ) & ( for v, vA, vB being Vector of V st vA in Lin A & vB in Lin (B \ A) & v = vA + vB holds

b_{4} . v = vA ) ) );

for V being free Z_Module

for A, B being Subset of V st A c= B & B is Basis of V holds

for b

( b

( vA in Lin A & vB in Lin (B \ A) & v = vA + vB & b

b

definition

let V be free Z_Module;

let B be Basis of V;

let u be Vector of V;

ex b_{1} being Function of V,INT.Ring st

( ( for v being Vector of V ex Lu being Linear_Combination of B st

( v = Sum Lu & b_{1} . v = Lu . u ) ) & ( for v being Vector of V

for Lv being Linear_Combination of B st v = Sum Lv holds

b_{1} . v = Lv . u ) & ( for v1, v2 being Vector of V holds b_{1} . (v1 + v2) = (b_{1} . v1) + (b_{1} . v2) ) & ( for v being Vector of V

for r being Element of INT.Ring holds b_{1} . (r * v) = r * (b_{1} . v) ) )

for b_{1}, b_{2} being Function of V,INT.Ring st ( for v being Vector of V ex Lu being Linear_Combination of B st

( v = Sum Lu & b_{1} . v = Lu . u ) ) & ( for v being Vector of V

for Lv being Linear_Combination of B st v = Sum Lv holds

b_{1} . v = Lv . u ) & ( for v1, v2 being Vector of V holds b_{1} . (v1 + v2) = (b_{1} . v1) + (b_{1} . v2) ) & ( for v being Vector of V

for r being Element of INT.Ring holds b_{1} . (r * v) = r * (b_{1} . v) ) & ( for v being Vector of V ex Lu being Linear_Combination of B st

( v = Sum Lu & b_{2} . v = Lu . u ) ) & ( for v being Vector of V

for Lv being Linear_Combination of B st v = Sum Lv holds

b_{2} . v = Lv . u ) & ( for v1, v2 being Vector of V holds b_{2} . (v1 + v2) = (b_{2} . v1) + (b_{2} . v2) ) & ( for v being Vector of V

for r being Element of INT.Ring holds b_{2} . (r * v) = r * (b_{2} . v) ) holds

b_{1} = b_{2}

end;
let B be Basis of V;

let u be Vector of V;

func Coordinate (u,B) -> Function of V,INT.Ring means :defCoord: :: ZMATRLIN:def 11

( ( for v being Vector of V ex Lu being Linear_Combination of B st

( v = Sum Lu & it . v = Lu . u ) ) & ( for v being Vector of V

for Lv being Linear_Combination of B st v = Sum Lv holds

it . v = Lv . u ) & ( for v1, v2 being Vector of V holds it . (v1 + v2) = (it . v1) + (it . v2) ) & ( for v being Vector of V

for r being Element of INT.Ring holds it . (r * v) = r * (it . v) ) );

existence ( ( for v being Vector of V ex Lu being Linear_Combination of B st

( v = Sum Lu & it . v = Lu . u ) ) & ( for v being Vector of V

for Lv being Linear_Combination of B st v = Sum Lv holds

it . v = Lv . u ) & ( for v1, v2 being Vector of V holds it . (v1 + v2) = (it . v1) + (it . v2) ) & ( for v being Vector of V

for r being Element of INT.Ring holds it . (r * v) = r * (it . v) ) );

ex b

( ( for v being Vector of V ex Lu being Linear_Combination of B st

( v = Sum Lu & b

for Lv being Linear_Combination of B st v = Sum Lv holds

b

for r being Element of INT.Ring holds b

proof end;

uniqueness for b

( v = Sum Lu & b

for Lv being Linear_Combination of B st v = Sum Lv holds

b

for r being Element of INT.Ring holds b

( v = Sum Lu & b

for Lv being Linear_Combination of B st v = Sum Lv holds

b

for r being Element of INT.Ring holds b

b

proof end;

:: deftheorem defCoord defines Coordinate ZMATRLIN:def 11 :

for V being free Z_Module

for B being Basis of V

for u being Vector of V

for b_{4} being Function of V,INT.Ring holds

( b_{4} = Coordinate (u,B) iff ( ( for v being Vector of V ex Lu being Linear_Combination of B st

( v = Sum Lu & b_{4} . v = Lu . u ) ) & ( for v being Vector of V

for Lv being Linear_Combination of B st v = Sum Lv holds

b_{4} . v = Lv . u ) & ( for v1, v2 being Vector of V holds b_{4} . (v1 + v2) = (b_{4} . v1) + (b_{4} . v2) ) & ( for v being Vector of V

for r being Element of INT.Ring holds b_{4} . (r * v) = r * (b_{4} . v) ) ) );

for V being free Z_Module

for B being Basis of V

for u being Vector of V

for b

( b

( v = Sum Lu & b

for Lv being Linear_Combination of B st v = Sum Lv holds

b

for r being Element of INT.Ring holds b

theorem PROJ4: :: ZMATRLIN:57

for V being free Z_Module

for B being Basis of V

for u being Vector of V holds (Coordinate (u,B)) . (0. V) = 0

for B being Basis of V

for u being Vector of V holds (Coordinate (u,B)) . (0. V) = 0

proof end;

theorem PROJ5: :: ZMATRLIN:58

for V being free Z_Module

for X being Basis of V

for v being Vector of V st v in X & v <> 0. V holds

(Coordinate (v,X)) . v = 1

for X being Basis of V

for v being Vector of V st v in X & v <> 0. V holds

(Coordinate (v,X)) . v = 1

proof end;

registration

let V be non trivial free Z_Module;

ex b_{1} being Functional of V st

( b_{1} is additive & b_{1} is homogeneous & not b_{1} is constant & not b_{1} is trivial )

end;
cluster Relation-like the carrier of V -defined the carrier of INT.Ring -valued Function-like non constant non empty non trivial total quasi_total V53() V54() V55() additive homogeneous for Functional of ;

existence ex b

( b

proof end;

theorem VS10Th28: :: ZMATRLIN:59

for V being non trivial free Z_Module

for f being V8() 0-preserving Functional of V ex v being Vector of V st

( v <> 0. V & f . v <> 0. INT.Ring )

for f being V8() 0-preserving Functional of V ex v being Vector of V st

( v <> 0. V & f . v <> 0. INT.Ring )

proof end;

definition

let V, W be ModuleStr over INT.Ring ;

[: the carrier of V, the carrier of W:] --> (0. INT.Ring) is Form of V,W ;

end;
func NulForm (V,W) -> Form of V,W equals :: ZMATRLIN:def 12

[: the carrier of V, the carrier of W:] --> (0. INT.Ring);

coherence [: the carrier of V, the carrier of W:] --> (0. INT.Ring);

[: the carrier of V, the carrier of W:] --> (0. INT.Ring) is Form of V,W ;

:: deftheorem defines NulForm ZMATRLIN:def 12 :

for V, W being ModuleStr over INT.Ring holds NulForm (V,W) = [: the carrier of V, the carrier of W:] --> (0. INT.Ring);

for V, W being ModuleStr over INT.Ring holds NulForm (V,W) = [: the carrier of V, the carrier of W:] --> (0. INT.Ring);

definition

let V, W be non empty ModuleStr over INT.Ring ;

let f, g be Form of V,W;

ex b_{1} being Form of V,W st

for v being Vector of V

for w being Vector of W holds b_{1} . (v,w) = (f . (v,w)) + (g . (v,w))

for b_{1}, b_{2} being Form of V,W st ( for v being Vector of V

for w being Vector of W holds b_{1} . (v,w) = (f . (v,w)) + (g . (v,w)) ) & ( for v being Vector of V

for w being Vector of W holds b_{2} . (v,w) = (f . (v,w)) + (g . (v,w)) ) holds

b_{1} = b_{2}

end;
let f, g be Form of V,W;

func f + g -> Form of V,W means :BLDef2: :: ZMATRLIN:def 13

for v being Vector of V

for w being Vector of W holds it . (v,w) = (f . (v,w)) + (g . (v,w));

existence for v being Vector of V

for w being Vector of W holds it . (v,w) = (f . (v,w)) + (g . (v,w));

ex b

for v being Vector of V

for w being Vector of W holds b

proof end;

uniqueness for b

for w being Vector of W holds b

for w being Vector of W holds b

b

proof end;

:: deftheorem BLDef2 defines + ZMATRLIN:def 13 :

for V, W being non empty ModuleStr over INT.Ring

for f, g, b_{5} being Form of V,W holds

( b_{5} = f + g iff for v being Vector of V

for w being Vector of W holds b_{5} . (v,w) = (f . (v,w)) + (g . (v,w)) );

for V, W being non empty ModuleStr over INT.Ring

for f, g, b

( b

for w being Vector of W holds b

definition

let V, W be non empty ModuleStr over INT.Ring ;

let f be Form of V,W;

let a be Element of INT.Ring;

ex b_{1} being Form of V,W st

for v being Vector of V

for w being Vector of W holds b_{1} . (v,w) = a * (f . (v,w))

for b_{1}, b_{2} being Form of V,W st ( for v being Vector of V

for w being Vector of W holds b_{1} . (v,w) = a * (f . (v,w)) ) & ( for v being Vector of V

for w being Vector of W holds b_{2} . (v,w) = a * (f . (v,w)) ) holds

b_{1} = b_{2}

end;
let f be Form of V,W;

let a be Element of INT.Ring;

func a * f -> Form of V,W means :BLDef3: :: ZMATRLIN:def 14

for v being Vector of V

for w being Vector of W holds it . (v,w) = a * (f . (v,w));

existence for v being Vector of V

for w being Vector of W holds it . (v,w) = a * (f . (v,w));

ex b

for v being Vector of V

for w being Vector of W holds b

proof end;

uniqueness for b

for w being Vector of W holds b

for w being Vector of W holds b

b

proof end;

:: deftheorem BLDef3 defines * ZMATRLIN:def 14 :

for V, W being non empty ModuleStr over INT.Ring

for f being Form of V,W

for a being Element of INT.Ring

for b_{5} being Form of V,W holds

( b_{5} = a * f iff for v being Vector of V

for w being Vector of W holds b_{5} . (v,w) = a * (f . (v,w)) );

for V, W being non empty ModuleStr over INT.Ring

for f being Form of V,W

for a being Element of INT.Ring

for b

( b

for w being Vector of W holds b

definition

let V, W be non empty ModuleStr over INT.Ring ;

let f be Form of V,W;

ex b_{1} being Form of V,W st

for v being Vector of V

for w being Vector of W holds b_{1} . (v,w) = - (f . (v,w))

for b_{1}, b_{2} being Form of V,W st ( for v being Vector of V

for w being Vector of W holds b_{1} . (v,w) = - (f . (v,w)) ) & ( for v being Vector of V

for w being Vector of W holds b_{2} . (v,w) = - (f . (v,w)) ) holds

b_{1} = b_{2}

end;
let f be Form of V,W;

func - f -> Form of V,W means :BLDef4: :: ZMATRLIN:def 15

for v being Vector of V

for w being Vector of W holds it . (v,w) = - (f . (v,w));

existence for v being Vector of V

for w being Vector of W holds it . (v,w) = - (f . (v,w));

ex b

for v being Vector of V

for w being Vector of W holds b

proof end;

uniqueness for b

for w being Vector of W holds b

for w being Vector of W holds b

b

proof end;

:: deftheorem BLDef4 defines - ZMATRLIN:def 15 :

for V, W being non empty ModuleStr over INT.Ring

for f, b_{4} being Form of V,W holds

( b_{4} = - f iff for v being Vector of V

for w being Vector of W holds b_{4} . (v,w) = - (f . (v,w)) );

for V, W being non empty ModuleStr over INT.Ring

for f, b

( b

for w being Vector of W holds b

definition

let V, W be non empty ModuleStr over INT.Ring ;

let f be Form of V,W;

compatibility

for b_{1} being Form of V,W holds

( b_{1} = - f iff b_{1} = (- (1. INT.Ring)) * f )

end;
let f be Form of V,W;

compatibility

for b

( b

proof end;

:: deftheorem defines - ZMATRLIN:def 16 :

for V, W being non empty ModuleStr over INT.Ring

for f being Form of V,W holds - f = (- (1. INT.Ring)) * f;

for V, W being non empty ModuleStr over INT.Ring

for f being Form of V,W holds - f = (- (1. INT.Ring)) * f;

definition

let V, W be non empty ModuleStr over INT.Ring ;

let f, g be Form of V,W;

correctness

coherence

f + (- g) is Form of V,W;

;

end;
let f, g be Form of V,W;

correctness

coherence

f + (- g) is Form of V,W;

;

:: deftheorem defines - ZMATRLIN:def 17 :

for V, W being non empty ModuleStr over INT.Ring

for f, g being Form of V,W holds f - g = f + (- g);

for V, W being non empty ModuleStr over INT.Ring

for f, g being Form of V,W holds f - g = f + (- g);

definition

let V, W be non empty ModuleStr over INT.Ring ;

let f, g be Form of V,W;

for b_{1} being Form of V,W holds

( b_{1} = f - g iff for v being Vector of V

for w being Vector of W holds b_{1} . (v,w) = (f . (v,w)) - (g . (v,w)) )

end;
let f, g be Form of V,W;

redefine func f - g means :BLDef7: :: ZMATRLIN:def 18

for v being Vector of V

for w being Vector of W holds it . (v,w) = (f . (v,w)) - (g . (v,w));

compatibility for v being Vector of V

for w being Vector of W holds it . (v,w) = (f . (v,w)) - (g . (v,w));

for b

( b

for w being Vector of W holds b

proof end;

:: deftheorem BLDef7 defines - ZMATRLIN:def 18 :

for V, W being non empty ModuleStr over INT.Ring

for f, g, b_{5} being Form of V,W holds

( b_{5} = f - g iff for v being Vector of V

for w being Vector of W holds b_{5} . (v,w) = (f . (v,w)) - (g . (v,w)) );

for V, W being non empty ModuleStr over INT.Ring

for f, g, b

( b

for w being Vector of W holds b

definition

let V, W be non empty ModuleStr over INT.Ring ;

let f, g be Form of V,W;

:: original: +

redefine func f + g -> Form of V,W;

commutativity

for f, g being Form of V,W holds f + g = g + f

end;
let f, g be Form of V,W;

:: original: +

redefine func f + g -> Form of V,W;

commutativity

for f, g being Form of V,W holds f + g = g + f

proof end;

theorem :: ZMATRLIN:60

for V, W being non empty ModuleStr over INT.Ring

for f being Form of V,W holds f + (NulForm (V,W)) = f

for f being Form of V,W holds f + (NulForm (V,W)) = f

proof end;

theorem :: ZMATRLIN:61

for V, W being non empty ModuleStr over INT.Ring

for f, g, h being Form of V,W holds (f + g) + h = f + (g + h)

for f, g, h being Form of V,W holds (f + g) + h = f + (g + h)

proof end;

theorem :: ZMATRLIN:62

for V, W being non empty ModuleStr over INT.Ring

for f being Form of V,W holds f - f = NulForm (V,W)

for f being Form of V,W holds f - f = NulForm (V,W)

proof end;

theorem :: ZMATRLIN:63

for V, W being non empty ModuleStr over INT.Ring

for a being Element of INT.Ring

for f, g being Form of V,W holds a * (f + g) = (a * f) + (a * g)

for a being Element of INT.Ring

for f, g being Form of V,W holds a * (f + g) = (a * f) + (a * g)

proof end;

theorem :: ZMATRLIN:64

for V, W being non empty ModuleStr over INT.Ring

for a, b being Element of INT.Ring

for f being Form of V,W holds (a + b) * f = (a * f) + (b * f)

for a, b being Element of INT.Ring

for f being Form of V,W holds (a + b) * f = (a * f) + (b * f)

proof end;

theorem :: ZMATRLIN:65

for V, W being non empty ModuleStr over INT.Ring

for a, b being Element of INT.Ring

for f being Form of V,W holds (a * b) * f = a * (b * f)

for a, b being Element of INT.Ring

for f being Form of V,W holds (a * b) * f = a * (b * f)

proof end;

theorem :: ZMATRLIN:66

for V, W being non empty ModuleStr over INT.Ring

for f being Form of V,W holds (1. INT.Ring) * f = f

for f being Form of V,W holds (1. INT.Ring) * f = f

proof end;

definition

let V, W be non empty ModuleStr over INT.Ring ;

let f be Form of V,W;

let v be Vector of V;

correctness

coherence

(curry f) . v is Functional of W;

;

end;
let f be Form of V,W;

let v be Vector of V;

correctness

coherence

(curry f) . v is Functional of W;

;

:: deftheorem defines FunctionalFAF ZMATRLIN:def 19 :

for V, W being non empty ModuleStr over INT.Ring

for f being Form of V,W

for v being Vector of V holds FunctionalFAF (f,v) = (curry f) . v;

for V, W being non empty ModuleStr over INT.Ring

for f being Form of V,W

for v being Vector of V holds FunctionalFAF (f,v) = (curry f) . v;

definition

let V, W be non empty ModuleStr over INT.Ring ;

let f be Form of V,W;

let w be Vector of W;

correctness

coherence

(curry' f) . w is Functional of V;

;

end;
let f be Form of V,W;

let w be Vector of W;

correctness

coherence

(curry' f) . w is Functional of V;

;

:: deftheorem defines FunctionalSAF ZMATRLIN:def 20 :

for V, W being non empty ModuleStr over INT.Ring

for f being Form of V,W

for w being Vector of W holds FunctionalSAF (f,w) = (curry' f) . w;

for V, W being non empty ModuleStr over INT.Ring

for f being Form of V,W

for w being Vector of W holds FunctionalSAF (f,w) = (curry' f) . w;

theorem BLTh8: :: ZMATRLIN:67

for V, W being non empty ModuleStr over INT.Ring

for f being Form of V,W

for v being Vector of V holds

( dom (FunctionalFAF (f,v)) = the carrier of W & rng (FunctionalFAF (f,v)) c= the carrier of INT.Ring & ( for w being Vector of W holds (FunctionalFAF (f,v)) . w = f . (v,w) ) )

for f being Form of V,W

for v being Vector of V holds

( dom (FunctionalFAF (f,v)) = the carrier of W & rng (FunctionalFAF (f,v)) c= the carrier of INT.Ring & ( for w being Vector of W holds (FunctionalFAF (f,v)) . w = f . (v,w) ) )

proof end;

theorem BLTh9: :: ZMATRLIN:68

for V, W being non empty ModuleStr over INT.Ring

for f being Form of V,W

for w being Vector of W holds

( dom (FunctionalSAF (f,w)) = the carrier of V & rng (FunctionalSAF (f,w)) c= the carrier of INT.Ring & ( for v being Vector of V holds (FunctionalSAF (f,w)) . v = f . (v,w) ) )

for f being Form of V,W

for w being Vector of W holds

( dom (FunctionalSAF (f,w)) = the carrier of V & rng (FunctionalSAF (f,w)) c= the carrier of INT.Ring & ( for v being Vector of V holds (FunctionalSAF (f,w)) . v = f . (v,w) ) )

proof end;

theorem BLTh10: :: ZMATRLIN:69

for V, W being non empty ModuleStr over INT.Ring

for v being Vector of V holds FunctionalFAF ((NulForm (V,W)),v) = 0Functional W

for v being Vector of V holds FunctionalFAF ((NulForm (V,W)),v) = 0Functional W

proof end;

theorem BLTh11: :: ZMATRLIN:70

for V, W being non empty ModuleStr over INT.Ring

for w being Vector of W holds FunctionalSAF ((NulForm (V,W)),w) = 0Functional V

for w being Vector of W holds FunctionalSAF ((NulForm (V,W)),w) = 0Functional V

proof end;

theorem BLTh12: :: ZMATRLIN:71

for V, W being non empty ModuleStr over INT.Ring

for f, g being Form of V,W

for w being Vector of W holds FunctionalSAF ((f + g),w) = (FunctionalSAF (f,w)) + (FunctionalSAF (g,w))

for f, g being Form of V,W

for w being Vector of W holds FunctionalSAF ((f + g),w) = (FunctionalSAF (f,w)) + (FunctionalSAF (g,w))

proof end;

theorem BLTh13: :: ZMATRLIN:72

for V, W being non empty ModuleStr over INT.Ring

for f, g being Form of V,W

for v being Vector of V holds FunctionalFAF ((f + g),v) = (FunctionalFAF (f,v)) + (FunctionalFAF (g,v))

for f, g being Form of V,W

for v being Vector of V holds FunctionalFAF ((f + g),v) = (FunctionalFAF (f,v)) + (FunctionalFAF (g,v))

proof end;

theorem BLTh14: :: ZMATRLIN:73

for V, W being non empty ModuleStr over INT.Ring

for f being Form of V,W

for a being Element of INT.Ring

for w being Vector of W holds FunctionalSAF ((a * f),w) = a * (FunctionalSAF (f,w))

for f being Form of V,W

for a being Element of INT.Ring

for w being Vector of W holds FunctionalSAF ((a * f),w) = a * (FunctionalSAF (f,w))

proof end;

theorem BLTh15: :: ZMATRLIN:74

for V, W being non empty ModuleStr over INT.Ring

for f being Form of V,W

for a being Element of INT.Ring

for v being Vector of V holds FunctionalFAF ((a * f),v) = a * (FunctionalFAF (f,v))

for f being Form of V,W

for a being Element of INT.Ring

for v being Vector of V holds FunctionalFAF ((a * f),v) = a * (FunctionalFAF (f,v))

proof end;

theorem :: ZMATRLIN:75

for V, W being non empty ModuleStr over INT.Ring

for f being Form of V,W

for w being Vector of W holds FunctionalSAF ((- f),w) = - (FunctionalSAF (f,w))

for f being Form of V,W

for w being Vector of W holds FunctionalSAF ((- f),w) = - (FunctionalSAF (f,w))

proof end;

theorem :: ZMATRLIN:76

for V, W being non empty ModuleStr over INT.Ring

for f being Form of V,W

for v being Vector of V holds FunctionalFAF ((- f),v) = - (FunctionalFAF (f,v))

for f being Form of V,W

for v being Vector of V holds FunctionalFAF ((- f),v) = - (FunctionalFAF (f,v))

proof end;

theorem :: ZMATRLIN:77

for V, W being non empty ModuleStr over INT.Ring

for f, g being Form of V,W

for w being Vector of W holds FunctionalSAF ((f - g),w) = (FunctionalSAF (f,w)) - (FunctionalSAF (g,w))

for f, g being Form of V,W

for w being Vector of W holds FunctionalSAF ((f - g),w) = (FunctionalSAF (f,w)) - (FunctionalSAF (g,w))

proof end;

theorem :: ZMATRLIN:78

for V, W being non empty ModuleStr over INT.Ring

for f, g being Form of V,W

for v being Vector of V holds FunctionalFAF ((f - g),v) = (FunctionalFAF (f,v)) - (FunctionalFAF (g,v))

for f, g being Form of V,W

for v being Vector of V holds FunctionalFAF ((f - g),v) = (FunctionalFAF (f,v)) - (FunctionalFAF (g,v))

proof end;

:: Two Form generated by Functionals

definition

let V, W be non empty ModuleStr over INT.Ring ;

let f be Functional of V;

let g be Functional of W;

ex b_{1} being Form of V,W st

for v being Vector of V

for w being Vector of W holds b_{1} . (v,w) = (f . v) * (g . w)

for b_{1}, b_{2} being Form of V,W st ( for v being Vector of V

for w being Vector of W holds b_{1} . (v,w) = (f . v) * (g . w) ) & ( for v being Vector of V

for w being Vector of W holds b_{2} . (v,w) = (f . v) * (g . w) ) holds

b_{1} = b_{2}

end;
let f be Functional of V;

let g be Functional of W;

func FormFunctional (f,g) -> Form of V,W means :BLDef10: :: ZMATRLIN:def 21

for v being Vector of V

for w being Vector of W holds it . (v,w) = (f . v) * (g . w);

existence for v being Vector of V

for w being Vector of W holds it . (v,w) = (f . v) * (g . w);

ex b

for v being Vector of V

for w being Vector of W holds b

proof end;

uniqueness for b

for w being Vector of W holds b

for w being Vector of W holds b

b

proof end;

:: deftheorem BLDef10 defines FormFunctional ZMATRLIN:def 21 :

for V, W being non empty ModuleStr over INT.Ring

for f being Functional of V

for g being Functional of W

for b_{5} being Form of V,W holds

( b_{5} = FormFunctional (f,g) iff for v being Vector of V

for w being Vector of W holds b_{5} . (v,w) = (f . v) * (g . w) );

for V, W being non empty ModuleStr over INT.Ring

for f being Functional of V

for g being Functional of W

for b

( b

for w being Vector of W holds b

theorem BLTh20: :: ZMATRLIN:79

for V, W being non empty ModuleStr over INT.Ring

for f being Functional of V

for v being Vector of V

for w being Vector of W holds (FormFunctional (f,(0Functional W))) . (v,w) = 0

for f being Functional of V

for v being Vector of V

for w being Vector of W holds (FormFunctional (f,(0Functional W))) . (v,w) = 0

proof end;

theorem BLTh21: :: ZMATRLIN:80

for V, W being non empty ModuleStr over INT.Ring

for g being Functional of W

for v being Vector of V

for w being Vector of W holds (FormFunctional ((0Functional V),g)) . (v,w) = 0

for g being Functional of W

for v being Vector of V

for w being Vector of W holds (FormFunctional ((0Functional V),g)) . (v,w) = 0

proof end;

theorem :: ZMATRLIN:81

for V, W being non empty ModuleStr over INT.Ring

for f being Functional of V holds FormFunctional (f,(0Functional W)) = NulForm (V,W)

for f being Functional of V holds FormFunctional (f,(0Functional W)) = NulForm (V,W)

proof end;

theorem :: ZMATRLIN:82

for V, W being non empty ModuleStr over INT.Ring

for g being Functional of W holds FormFunctional ((0Functional V),g) = NulForm (V,W)

for g being Functional of W holds FormFunctional ((0Functional V),g) = NulForm (V,W)

proof end;

theorem BLTh24: :: ZMATRLIN:83

for V, W being non empty ModuleStr over INT.Ring

for f being Functional of V

for g being Functional of W

for v being Vector of V holds FunctionalFAF ((FormFunctional (f,g)),v) = (f . v) * g

for f being Functional of V

for g being Functional of W

for v being Vector of V holds FunctionalFAF ((FormFunctional (f,g)),v) = (f . v) * g

proof end;

theorem BLTh25: :: ZMATRLIN:84

for V, W being non empty ModuleStr over INT.Ring

for f being Functional of V

for g being Functional of W

for w being Vector of W holds FunctionalSAF ((FormFunctional (f,g)),w) = (g . w) * f

for f being Functional of V

for g being Functional of W

for w being Vector of W holds FunctionalSAF ((FormFunctional (f,g)),w) = (g . w) * f

proof end;

:: Bilinear Forms and Their Properties

definition

let V, W be non empty ModuleStr over INT.Ring ;

let f be Form of V,W;

end;
let f be Form of V,W;

attr f is additiveFAF means :BLDef11: :: ZMATRLIN:def 22

for v being Vector of V holds FunctionalFAF (f,v) is additive ;

for v being Vector of V holds FunctionalFAF (f,v) is additive ;

attr f is additiveSAF means :BLDef12: :: ZMATRLIN:def 23

for w being Vector of W holds FunctionalSAF (f,w) is additive ;

for w being Vector of W holds FunctionalSAF (f,w) is additive ;

:: deftheorem BLDef11 defines additiveFAF ZMATRLIN:def 22 :

for V, W being non empty ModuleStr over INT.Ring

for f being Form of V,W holds

( f is additiveFAF iff for v being Vector of V holds FunctionalFAF (f,v) is additive );

for V, W being non empty ModuleStr over INT.Ring

for f being Form of V,W holds

( f is additiveFAF iff for v being Vector of V holds FunctionalFAF (f,v) is additive );

:: deftheorem BLDef12 defines additiveSAF ZMATRLIN:def 23 :

for V, W being non empty ModuleStr over INT.Ring

for f being Form of V,W holds

( f is additiveSAF iff for w being Vector of W holds FunctionalSAF (f,w) is additive );

for V, W being non empty ModuleStr over INT.Ring

for f being Form of V,W holds

( f is additiveSAF iff for w being Vector of W holds FunctionalSAF (f,w) is additive );

definition

let V, W be non empty ModuleStr over INT.Ring ;

let f be Form of V,W;

end;
let f be Form of V,W;

attr f is homogeneousFAF means :BLDef13: :: ZMATRLIN:def 24

for v being Vector of V holds FunctionalFAF (f,v) is homogeneous ;

for v being Vector of V holds FunctionalFAF (f,v) is homogeneous ;

attr f is homogeneousSAF means :BLDef14: :: ZMATRLIN:def 25

for w being Vector of W holds FunctionalSAF (f,w) is homogeneous ;

for w being Vector of W holds FunctionalSAF (f,w) is homogeneous ;

:: deftheorem BLDef13 defines homogeneousFAF ZMATRLIN:def 24 :

for V, W being non empty ModuleStr over INT.Ring

for f being Form of V,W holds

( f is homogeneousFAF iff for v being Vector of V holds FunctionalFAF (f,v) is homogeneous );

for V, W being non empty ModuleStr over INT.Ring

for f being Form of V,W holds

( f is homogeneousFAF iff for v being Vector of V holds FunctionalFAF (f,v) is homogeneous );

:: deftheorem BLDef14 defines homogeneousSAF ZMATRLIN:def 25 :

for V, W being non empty ModuleStr over INT.Ring

for f being Form of V,W holds

( f is homogeneousSAF iff for w being Vector of W holds FunctionalSAF (f,w) is homogeneous );

for V, W being non empty ModuleStr over INT.Ring

for f being Form of V,W holds

( f is homogeneousSAF iff for w being Vector of W holds FunctionalSAF (f,w) is homogeneous );

registration

let V, W be non empty ModuleStr over INT.Ring ;

coherence

NulForm (V,W) is additiveFAF

NulForm (V,W) is additiveSAF

end;
coherence

NulForm (V,W) is additiveFAF

proof end;

coherence NulForm (V,W) is additiveSAF

proof end;

registration

let V, W be non empty ModuleStr over INT.Ring ;

coherence

NulForm (V,W) is homogeneousFAF

NulForm (V,W) is homogeneousSAF

end;
coherence

NulForm (V,W) is homogeneousFAF

proof end;

coherence NulForm (V,W) is homogeneousSAF

proof end;

registration

let V, W be non empty ModuleStr over INT.Ring ;

ex b_{1} being Form of V,W st

( b_{1} is additiveFAF & b_{1} is homogeneousFAF & b_{1} is additiveSAF & b_{1} is homogeneousSAF )

end;
cluster Relation-like [: the carrier of V, the carrier of W:] -defined the carrier of INT.Ring -valued Function-like non empty total quasi_total V53() V54() V55() additiveFAF additiveSAF homogeneousFAF homogeneousSAF for Form of ,;

existence ex b

( b

proof end;

definition

let V, W be non empty ModuleStr over INT.Ring ;

mode bilinear-Form of V,W is additiveFAF additiveSAF homogeneousFAF homogeneousSAF Form of V,W;

end;
mode bilinear-Form of V,W is additiveFAF additiveSAF homogeneousFAF homogeneousSAF Form of V,W;

registration

let V, W be non empty ModuleStr over INT.Ring ;

let f be additiveFAF Form of V,W;

let v be Vector of V;

coherence

FunctionalFAF (f,v) is additive by BLDef11;

end;
let f be additiveFAF Form of V,W;

let v be Vector of V;

coherence

FunctionalFAF (f,v) is additive by BLDef11;

registration

let V, W be non empty ModuleStr over INT.Ring ;

let f be additiveSAF Form of V,W;

let w be Vector of W;

coherence

FunctionalSAF (f,w) is additive by BLDef12;

end;
let f be additiveSAF Form of V,W;

let w be Vector of W;

coherence

FunctionalSAF (f,w) is additive by BLDef12;

registration

let V, W be non empty ModuleStr over INT.Ring ;

let f be homogeneousFAF Form of V,W;

let v be Vector of V;

coherence

FunctionalFAF (f,v) is homogeneous by BLDef13;

end;
let f be homogeneousFAF Form of V,W;

let v be Vector of V;

coherence

FunctionalFAF (f,v) is homogeneous by BLDef13;

registration

let V, W be non empty ModuleStr over INT.Ring ;

let f be homogeneousSAF Form of V,W;

let w be Vector of W;

coherence

FunctionalSAF (f,w) is homogeneous by BLDef14;

end;
let f be homogeneousSAF Form of V,W;

let w be Vector of W;

coherence

FunctionalSAF (f,w) is homogeneous by BLDef14;

registration

let V, W be non empty ModuleStr over INT.Ring ;

let f be Functional of V;

let g be additive Functional of W;

coherence

FormFunctional (f,g) is additiveFAF

end;
let f be Functional of V;

let g be additive Functional of W;

coherence

FormFunctional (f,g) is additiveFAF

proof end;

registration

let V, W be non empty ModuleStr over INT.Ring ;

let f be additive Functional of V;

let g be Functional of W;

coherence

FormFunctional (f,g) is additiveSAF

end;
let f be additive Functional of V;

let g be Functional of W;

coherence

FormFunctional (f,g) is additiveSAF

proof end;

registration

let V, W be non empty ModuleStr over INT.Ring ;

let f be Functional of V;

let g be homogeneous Functional of W;

coherence

FormFunctional (f,g) is homogeneousFAF

end;
let f be Functional of V;

let g be homogeneous Functional of W;

coherence

FormFunctional (f,g) is homogeneousFAF

proof end;

registration

let V, W be non empty ModuleStr over INT.Ring ;

let f be homogeneous Functional of V;

let g be Functional of W;

coherence

FormFunctional (f,g) is homogeneousSAF

end;
let f be homogeneous Functional of V;

let g be Functional of W;

coherence

FormFunctional (f,g) is homogeneousSAF

proof end;

registration

let V be non trivial ModuleStr over INT.Ring ;

let W be Z_Module;

let f be Functional of V;

let g be Functional of W;

coherence

not FormFunctional (f,g) is trivial

end;
let W be Z_Module;

let f be Functional of V;

let g be Functional of W;

coherence

not FormFunctional (f,g) is trivial

proof end;

registration

let V be non empty ModuleStr over INT.Ring ;

let W be non trivial Z_Module;

let f be Functional of V;

let g be Functional of W;

coherence

not FormFunctional (f,g) is trivial

end;
let W be non trivial Z_Module;

let f be Functional of V;

let g be Functional of W;

coherence

not FormFunctional (f,g) is trivial

proof end;

registration

let V, W be non trivial free Z_Module;

let f be V8() 0-preserving Functional of V;

let g be V8() 0-preserving Functional of W;

coherence

not FormFunctional (f,g) is constant

end;
let f be V8() 0-preserving Functional of V;

let g be V8() 0-preserving Functional of W;

coherence

not FormFunctional (f,g) is constant

proof end;

registration

let V, W be non trivial free Z_Module;

ex b_{1} being Form of V,W st

( not b_{1} is trivial & not b_{1} is constant & b_{1} is additiveFAF & b_{1} is homogeneousFAF & b_{1} is additiveSAF & b_{1} is homogeneousSAF )

end;
cluster Relation-like [: the carrier of V, the carrier of W:] -defined the carrier of INT.Ring -valued Function-like non constant non empty non trivial total quasi_total V53() V54() V55() additiveFAF additiveSAF homogeneousFAF homogeneousSAF for Form of ,;

existence ex b

( not b

proof end;

registration

let V, W be non empty ModuleStr over INT.Ring ;

let f, g be additiveSAF Form of V,W;

correctness

coherence

f + g is additiveSAF ;

end;
let f, g be additiveSAF Form of V,W;

correctness

coherence

f + g is additiveSAF ;

proof end;

registration

let V, W be non empty ModuleStr over INT.Ring ;

let f, g be additiveFAF Form of V,W;

correctness

coherence

f + g is additiveFAF ;

end;
let f, g be additiveFAF Form of V,W;

correctness

coherence

f + g is additiveFAF ;

proof end;

registration

let V, W be non empty ModuleStr over INT.Ring ;

let f be additiveSAF Form of V,W;

let a be Element of INT.Ring;

correctness

coherence

a * f is additiveSAF ;

end;
let f be additiveSAF Form of V,W;

let a be Element of INT.Ring;

correctness

coherence

a * f is additiveSAF ;

proof end;

registration

let V, W be non empty ModuleStr over INT.Ring ;

let f be additiveFAF Form of V,W;

let a be Element of INT.Ring;

correctness

coherence

a * f is additiveFAF ;

end;
let f be additiveFAF Form of V,W;

let a be Element of INT.Ring;

correctness

coherence

a * f is additiveFAF ;

proof end;

registration

let V, W be non empty ModuleStr over INT.Ring ;

let f be additiveSAF Form of V,W;

correctness

coherence

- f is additiveSAF ;

;

end;
let f be additiveSAF Form of V,W;

correctness

coherence

- f is additiveSAF ;

;

registration

let V, W be non empty ModuleStr over INT.Ring ;

let f be additiveFAF Form of V,W;

correctness

coherence

- f is additiveFAF ;

;

end;
let f be additiveFAF Form of V,W;

correctness

coherence

- f is additiveFAF ;

;

registration

let V, W be non empty ModuleStr over INT.Ring ;

let f, g be additiveSAF Form of V,W;

correctness

coherence

f - g is additiveSAF ;

;

end;
let f, g be additiveSAF Form of V,W;

correctness

coherence

f - g is additiveSAF ;

;

registration

let V, W be non empty ModuleStr over INT.Ring ;

let f, g be additiveFAF Form of V,W;

correctness

coherence

f - g is additiveFAF ;

;

end;
let f, g be additiveFAF Form of V,W;

correctness

coherence

f - g is additiveFAF ;

;

registration

let V, W be non empty ModuleStr over INT.Ring ;

let f, g be homogeneousSAF Form of V,W;

correctness

coherence

f + g is homogeneousSAF ;

end;
let f, g be homogeneousSAF Form of V,W;

correctness

coherence

f + g is homogeneousSAF ;

proof end;

registration

let V, W be non empty ModuleStr over INT.Ring ;

let f, g be homogeneousFAF Form of V,W;

correctness

coherence

f + g is homogeneousFAF ;

end;
let f, g be homogeneousFAF Form of V,W;

correctness

coherence

f + g is homogeneousFAF ;

proof end;

registration

let V, W be non empty ModuleStr over INT.Ring ;

let f be homogeneousSAF Form of V,W;

let a be Element of INT.Ring;

correctness

coherence

a * f is homogeneousSAF ;

end;
let f be homogeneousSAF Form of V,W;

let a be Element of INT.Ring;

correctness

coherence

a * f is homogeneousSAF ;

proof end;

registration

let V, W be non empty ModuleStr over INT.Ring ;

let f be homogeneousFAF Form of V,W;

let a be Element of INT.Ring;

correctness

coherence

a * f is homogeneousFAF ;

end;
let f be homogeneousFAF Form of V,W;

let a be Element of INT.Ring;

correctness

coherence

a * f is homogeneousFAF ;

proof end;

registration

let V, W be non empty ModuleStr over INT.Ring ;

let f be homogeneousSAF Form of V,W;

correctness

coherence

- f is homogeneousSAF ;

;

end;
let f be homogeneousSAF Form of V,W;

correctness

coherence

- f is homogeneousSAF ;

;

registration

let V, W be non empty ModuleStr over INT.Ring ;

let f be homogeneousFAF Form of V,W;

correctness

coherence

- f is homogeneousFAF ;

;

end;
let f be homogeneousFAF Form of V,W;

correctness

coherence

- f is homogeneousFAF ;

;

registration

let V, W be non empty ModuleStr over INT.Ring ;

let f, g be homogeneousSAF Form of V,W;

correctness

coherence

f - g is homogeneousSAF ;

;

end;
let f, g be homogeneousSAF Form of V,W;

correctness

coherence

f - g is homogeneousSAF ;

;

registration

let V, W be non empty ModuleStr over INT.Ring ;

let f, g be homogeneousFAF Form of V,W;

correctness

coherence

f - g is homogeneousFAF ;

;

end;
let f, g be homogeneousFAF Form of V,W;

correctness

coherence

f - g is homogeneousFAF ;

;

theorem BLTh26: :: ZMATRLIN:85

for V, W being non empty ModuleStr over INT.Ring

for v, u being Vector of V

for w being Vector of W

for f being Form of V,W st f is additiveSAF holds

f . ((v + u),w) = (f . (v,w)) + (f . (u,w))

for v, u being Vector of V

for w being Vector of W

for f being Form of V,W st f is additiveSAF holds

f . ((v + u),w) = (f . (v,w)) + (f . (u,w))

proof end;

theorem BLTh27: :: ZMATRLIN:86

for V, W being non empty ModuleStr over INT.Ring

for v being Vector of V

for u, w being Vector of W

for f being Form of V,W st f is additiveFAF holds

f . (v,(u + w)) = (f . (v,u)) + (f . (v,w))

for v being Vector of V

for u, w being Vector of W

for f being Form of V,W st f is additiveFAF holds

f . (v,(u + w)) = (f . (v,u)) + (f . (v,w))

proof end;

theorem BLTh28: :: ZMATRLIN:87

for V, W being non empty ModuleStr over INT.Ring

for v, u being Vector of V

for w, t being Vector of W

for f being additiveFAF additiveSAF Form of V,W holds f . ((v + u),(w + t)) = ((f . (v,w)) + (f . (v,t))) + ((f . (u,w)) + (f . (u,t)))

for v, u being Vector of V

for w, t being Vector of W

for f being additiveFAF additiveSAF Form of V,W holds f . ((v + u),(w + t)) = ((f . (v,w)) + (f . (v,t))) + ((f . (u,w)) + (f . (u,t)))

proof end;

theorem BLTh29: :: ZMATRLIN:88

for V, W being non empty right_zeroed ModuleStr over INT.Ring

for f being additiveFAF Form of V,W

for v being Vector of V holds f . (v,(0. W)) = 0

for f being additiveFAF Form of V,W

for v being Vector of V holds f . (v,(0. W)) = 0

proof end;

theorem BLTh30: :: ZMATRLIN:89

for V, W being non empty right_zeroed ModuleStr over INT.Ring

for f being additiveSAF Form of V,W

for w being Vector of W holds f . ((0. V),w) = 0

for f being additiveSAF Form of V,W

for w being Vector of W holds f . ((0. V),w) = 0

proof end;

theorem BLTh31: :: ZMATRLIN:90

for V, W being non empty ModuleStr over INT.Ring

for v being Vector of V

for w being Vector of W

for a being Element of INT.Ring

for f being Form of V,W st f is homogeneousSAF holds

f . ((a * v),w) = a * (f . (v,w))

for v being Vector of V

for w being Vector of W

for a being Element of INT.Ring

for f being Form of V,W st f is homogeneousSAF holds

f . ((a * v),w) = a * (f . (v,w))

proof end;

theorem BLTh32: :: ZMATRLIN:91

for V, W being non empty ModuleStr over INT.Ring

for v being Vector of V

for w being Vector of W

for a being Element of INT.Ring

for f being Form of V,W st f is homogeneousFAF holds

f . (v,(a * w)) = a * (f . (v,w))

for v being Vector of V

for w being Vector of W

for a being Element of INT.Ring

for f being Form of V,W st f is homogeneousFAF holds

f . (v,(a * w)) = a * (f . (v,w))

proof end;

theorem :: ZMATRLIN:92

for V, W being non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ModuleStr over INT.Ring

for f being homogeneousSAF Form of V,W

for w being Vector of W holds f . ((0. V),w) = 0. INT.Ring

for f being homogeneousSAF Form of V,W

for w being Vector of W holds f . ((0. V),w) = 0. INT.Ring

proof end;

theorem :: ZMATRLIN:93

for V, W being non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ModuleStr over INT.Ring

for f being homogeneousFAF Form of V,W

for v being Vector of V holds f . (v,(0. W)) = 0. INT.Ring

for f being homogeneousFAF Form of V,W

for v being Vector of V holds f . (v,(0. W)) = 0. INT.Ring

proof end;

theorem BLTh35: :: ZMATRLIN:94

for V, W being Z_Module

for v, u being Vector of V

for w being Vector of W

for f being additiveSAF homogeneousSAF Form of V,W holds f . ((v - u),w) = (f . (v,w)) - (f . (u,w))

for v, u being Vector of V

for w being Vector of W

for f being additiveSAF homogeneousSAF Form of V,W holds f . ((v - u),w) = (f . (v,w)) - (f . (u,w))

proof end;

theorem BLTh36: :: ZMATRLIN:95

for V, W being Z_Module

for v being Vector of V

for w, t being Vector of W

for f being additiveFAF homogeneousFAF Form of V,W holds f . (v,(w - t)) = (f . (v,w)) - (f . (v,t))

for v being Vector of V

for w, t being Vector of W

for f being additiveFAF homogeneousFAF Form of V,W holds f . (v,(w - t)) = (f . (v,w)) - (f . (v,t))

proof end;

theorem BLTh37: :: ZMATRLIN:96

for V, W being Z_Module

for v, u being Vector of V

for w, t being Vector of W

for f being bilinear-Form of V,W holds f . ((v - u),(w - t)) = ((f . (v,w)) - (f . (v,t))) - ((f . (u,w)) - (f . (u,t)))

for v, u being Vector of V

for w, t being Vector of W

for f being bilinear-Form of V,W holds f . ((v - u),(w - t)) = ((f . (v,w)) - (f . (v,t))) - ((f . (u,w)) - (f . (u,t)))

proof end;

theorem :: ZMATRLIN:97

for V, W being non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ModuleStr over INT.Ring

for v, u being Vector of V

for w, t being Vector of W

for a, b being Element of INT.Ring

for f being bilinear-Form of V,W holds f . ((v + (a * u)),(w + (b * t))) = ((f . (v,w)) + (b * (f . (v,t)))) + ((a * (f . (u,w))) + (a * (b * (f . (u,t)))))

for v, u being Vector of V

for w, t being Vector of W

for a, b being Element of INT.Ring

for f being bilinear-Form of V,W holds f . ((v + (a * u)),(w + (b * t))) = ((f . (v,w)) + (b * (f . (v,t)))) + ((a * (f . (u,w))) + (a * (b * (f . (u,t)))))

proof end;

theorem :: ZMATRLIN:98

for V, W being Z_Module

for v, u being Vector of V

for w, t being Vector of W

for a, b being Element of INT.Ring

for f being bilinear-Form of V,W holds f . ((v - (a * u)),(w - (b * t))) = ((f . (v,w)) - (b * (f . (v,t)))) - ((a * (f . (u,w))) - (a * (b * (f . (u,t)))))

for v, u being Vector of V

for w, t being Vector of W

for a, b being Element of INT.Ring

for f being bilinear-Form of V,W holds f . ((v - (a * u)),(w - (b * t))) = ((f . (v,w)) - (b * (f . (v,t)))) - ((a * (f . (u,w))) - (a * (b * (f . (u,t)))))

proof end;

theorem :: ZMATRLIN:99

for V, W being non empty right_zeroed ModuleStr over INT.Ring

for f being Form of V,W st ( f is additiveFAF or f is additiveSAF ) holds

( f is constant iff for v being Vector of V

for w being Vector of W holds f . (v,w) = 0 )

for f being Form of V,W st ( f is additiveFAF or f is additiveSAF ) holds

( f is constant iff for v being Vector of V

for w being Vector of W holds f . (v,w) = 0 )

proof end;

definition

let V1, V2 be free finite-rank Z_Module;

let b1 be OrdBasis of V1;

let b2 be OrdBasis of V2;

let f be bilinear-Form of V1,V2;

ex b_{1} being Matrix of len b1, len b2,INT.Ring st

for i, j being Nat st i in dom b1 & j in dom b2 holds

b_{1} * (i,j) = f . ((b1 /. i),(b2 /. j))

for b_{1}, b_{2} being Matrix of len b1, len b2,INT.Ring st ( for i, j being Nat st i in dom b1 & j in dom b2 holds

b_{1} * (i,j) = f . ((b1 /. i),(b2 /. j)) ) & ( for i, j being Nat st i in dom b1 & j in dom b2 holds

b_{2} * (i,j) = f . ((b1 /. i),(b2 /. j)) ) holds

b_{1} = b_{2}

end;
let b1 be OrdBasis of V1;

let b2 be OrdBasis of V2;

let f be bilinear-Form of V1,V2;

func BilinearM (f,b1,b2) -> Matrix of len b1, len b2,INT.Ring means :defBilinearM: :: ZMATRLIN:def 26

for i, j being Nat st i in dom b1 & j in dom b2 holds

it * (i,j) = f . ((b1 /. i),(b2 /. j));

existence for i, j being Nat st i in dom b1 & j in dom b2 holds

it * (i,j) = f . ((b1 /. i),(b2 /. j));

ex b

for i, j being Nat st i in dom b1 & j in dom b2 holds

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem defBilinearM defines BilinearM ZMATRLIN:def 26 :

for V1, V2 being free finite-rank Z_Module

for b1 being OrdBasis of V1

for b2 being OrdBasis of V2

for f being bilinear-Form of V1,V2

for b_{6} being Matrix of len b1, len b2,INT.Ring holds

( b_{6} = BilinearM (f,b1,b2) iff for i, j being Nat st i in dom b1 & j in dom b2 holds

b_{6} * (i,j) = f . ((b1 /. i),(b2 /. j)) );

for V1, V2 being free finite-rank Z_Module

for b1 being OrdBasis of V1

for b2 being OrdBasis of V2

for f being bilinear-Form of V1,V2

for b

( b

b

theorem :: ZMATRLIN:100

theorem LMThMBF1X0: :: ZMATRLIN:101

for V being free finite-rank Z_Module

for F being linear-Functional of V

for y being FinSequence of V

for x, X, Y being FinSequence of INT.Ring st X = x & len y = len x & len X = len Y & ( for k being Nat st k in Seg (len x) holds

Y . k = F . (y /. k) ) holds

X "*" Y = F . (Sum (lmlt (x,y)))

for F being linear-Functional of V

for y being FinSequence of V

for x, X, Y being FinSequence of INT.Ring st X = x & len y = len x & len X = len Y & ( for k being Nat st k in Seg (len x) holds

Y . k = F . (y /. k) ) holds

X "*" Y = F . (Sum (lmlt (x,y)))

proof end;

theorem LMThMBF1X: :: ZMATRLIN:102

for V1, V2 being free finite-rank Z_Module

for b2, b3 being OrdBasis of V2

for f being bilinear-Form of V1,V2

for v1 being Vector of V1

for v2 being Vector of V2

for X, Y being FinSequence of INT.Ring st len X = len b2 & len Y = len b2 & ( for k being Nat st k in Seg (len b2) holds

Y . k = f . (v1,(b2 /. k)) ) & X = v2 |-- b2 holds

Y "*" X = f . (v1,v2)

for b2, b3 being OrdBasis of V2

for f being bilinear-Form of V1,V2

for v1 being Vector of V1

for v2 being Vector of V2

for X, Y being FinSequence of INT.Ring st len X = len b2 & len Y = len b2 & ( for k being Nat st k in Seg (len b2) holds

Y . k = f . (v1,(b2 /. k)) ) & X = v2 |-- b2 holds

Y "*" X = f . (v1,v2)

proof end;

theorem LMThMBF1Y: :: ZMATRLIN:103

for V1, V2 being free finite-rank Z_Module

for b1 being OrdBasis of V1

for f being bilinear-Form of V1,V2

for v1 being Vector of V1

for v2 being Vector of V2

for X, Y being FinSequence of INT.Ring st len X = len b1 & len Y = len b1 & ( for k being Nat st k in Seg (len b1) holds

Y . k = f . ((b1 /. k),v2) ) & X = v1 |-- b1 holds

X "*" Y = f . (v1,v2)

for b1 being OrdBasis of V1

for f being bilinear-Form of V1,V2

for v1 being Vector of V1

for v2 being Vector of V2

for X, Y being FinSequence of INT.Ring st len X = len b1 & len Y = len b1 & ( for k being Nat st k in Seg (len b1) holds

Y . k = f . ((b1 /. k),v2) ) & X = v1 |-- b1 holds

X "*" Y = f . (v1,v2)

proof end;

theorem ThMBF1: :: ZMATRLIN:104

for V1, V2 being free finite-rank Z_Module

for b1 being OrdBasis of V1

for b2, b3 being OrdBasis of V2

for f being bilinear-Form of V1,V2 st 0 < rank V1 holds

BilinearM (f,b1,b3) = (BilinearM (f,b1,b2)) * ((AutMt ((id V2),b3,b2)) @)

for b1 being OrdBasis of V1

for b2, b3 being OrdBasis of V2

for f being bilinear-Form of V1,V2 st 0 < rank V1 holds

BilinearM (f,b1,b3) = (BilinearM (f,b1,b2)) * ((AutMt ((id V2),b3,b2)) @)

proof end;

theorem ThMBF2: :: ZMATRLIN:105

for V1, V2 being free finite-rank Z_Module

for b1 being OrdBasis of V1

for b2 being OrdBasis of V2

for b3 being OrdBasis of V1

for f being bilinear-Form of V1,V2 st 0 < rank V1 holds

BilinearM (f,b3,b2) = (AutMt ((id V1),b3,b1)) * (BilinearM (f,b1,b2))

for b1 being OrdBasis of V1

for b2 being OrdBasis of V2

for b3 being OrdBasis of V1

for f being bilinear-Form of V1,V2 st 0 < rank V1 holds

BilinearM (f,b3,b2) = (AutMt ((id V1),b3,b1)) * (BilinearM (f,b1,b2))

proof end;

theorem ThMBF3: :: ZMATRLIN:106

for V being free finite-rank Z_Module

for b1, b2 being OrdBasis of V

for f being bilinear-Form of V,V st 0 < rank V holds

BilinearM (f,b2,b2) = ((AutMt ((id V),b2,b1)) * (BilinearM (f,b1,b1))) * ((AutMt ((id V),b2,b1)) @)

for b1, b2 being OrdBasis of V

for f being bilinear-Form of V,V st 0 < rank V holds

BilinearM (f,b2,b2) = ((AutMt ((id V),b2,b1)) * (BilinearM (f,b1,b1))) * ((AutMt ((id V),b2,b1)) @)

proof end;

theorem :: ZMATRLIN:107

for V being free finite-rank Z_Module

for b1, b2 being OrdBasis of V

for f being bilinear-Form of V,V holds |.(Det (BilinearM (f,b2,b2))).| = |.(Det (BilinearM (f,b1,b1))).|

for b1, b2 being OrdBasis of V

for f being bilinear-Form of V,V holds |.(Det (BilinearM (f,b2,b2))).| = |.(Det (BilinearM (f,b1,b1))).|

proof end;