let L be non trivial positive-definite RATional Z_Lattice; :: thesis: for b being OrdBasis of EMLat L
for i being Nat st i in dom b holds
ex v being Vector of () st
( () . ((b /. i),v) = 1 & ( for j being Nat st i <> j & j in dom b holds
() . ((b /. j),v) = 0 ) )

let b be OrdBasis of EMLat L; :: thesis: for i being Nat st i in dom b holds
ex v being Vector of () st
( () . ((b /. i),v) = 1 & ( for j being Nat st i <> j & j in dom b holds
() . ((b /. j),v) = 0 ) )

let i be Nat; :: thesis: ( i in dom b implies ex v being Vector of () st
( () . ((b /. i),v) = 1 & ( for j being Nat st i <> j & j in dom b holds
() . ((b /. j),v) = 0 ) ) )

assume A1: i in dom b ; :: thesis: ex v being Vector of () st
( () . ((b /. i),v) = 1 & ( for j being Nat st i <> j & j in dom b holds
() . ((b /. j),v) = 0 ) )

A2: dim L = dim () by ZMODLAT2:42;
consider a being Element of F_Real such that
A3: ( a is Element of INT.Ring & a <> 0 & a * (() ~) is Matrix of dim L,INT.Ring ) by ;
(GramMatrix b) ~ is_reverse_of GramMatrix b by MATRIX_6:def 4;
then A5: (() ~) * () = 1. (F_Real,(dim ())) by MATRIX_6:def 2
.= 1. (F_Real,(dim L)) by ZMODLAT2:42 ;
len (() ~) = dim () by MATRIX_0:def 2;
then width (() ~) = dim () by MATRIX_0:20
.= len () by MATRIX_0:def 2 ;
then A8: (a * (() ~)) * () = a * (1. (F_Real,(dim L))) by ;
AX1: len b = dim () by ZMATRLIN:49;
then A9: i in Seg (dim L) by ;
A10: Indices (1. (F_Real,(dim L))) = [:(Seg (dim L)),(Seg (dim L)):] by MATRIX_0:24;
then A11: [i,i] in Indices (1. (F_Real,(dim L))) by ;
A12: Indices (a * (1. (F_Real,(dim L)))) = [:(Seg (dim L)),(Seg (dim L)):] by MATRIX_0:24;
then A14: [i,i] in Indices ((a * (() ~)) * ()) by ;
AX3: width (a * (() ~)) = dim () by MATRIX_0:23
.= len () by MATRIX_0:def 2 ;
A15: (Line ((a * (() ~)),i)) "*" (Col ((),i)) = ((a * (() ~)) * ()) * (i,i) by
.= a * ((1. (F_Real,(dim L))) * (i,i)) by
.= a * () by
.= a ;
A16: for j being Nat st i <> j & j in dom b holds
(Line ((a * (() ~)),i)) "*" (Col ((),j)) = 0
proof
let j be Nat; :: thesis: ( i <> j & j in dom b implies (Line ((a * (() ~)),i)) "*" (Col ((),j)) = 0 )
assume B1: ( i <> j & j in dom b ) ; :: thesis: (Line ((a * (() ~)),i)) "*" (Col ((),j)) = 0
B2: j in Seg (dim L) by ;
then B3: [i,j] in Indices (1. (F_Real,(dim L))) by ;
[i,j] in Indices ((a * (() ~)) * ()) by ;
hence (Line ((a * (() ~)),i)) "*" (Col ((),j)) = ((a * (() ~)) * ()) * (i,j) by
.= a * ((1. (F_Real,(dim L))) * (i,j)) by
.= a * () by
.= 0 ;
:: thesis: verum
end;
reconsider I = rng b as Basis of () by ZMATRLIN:def 5;
defpred S1[ object , object ] means ( ( \$1 in I implies for n being Nat st n = (b ") . \$1 & n in dom b holds
\$2 = (a * (() ~)) * (i,n) ) & ( not \$1 in I implies \$2 = 0. INT.Ring ) );
A17: for x being Element of () ex y being Element of INT.Ring st S1[x,y]
proof
let x be Element of (); :: thesis: ex y being Element of INT.Ring st S1[x,y]
per cases ( x in I or not x in I ) ;
suppose B1: x in I ; :: thesis: ex y being Element of INT.Ring st S1[x,y]
b is one-to-one by ZMATRLIN:def 5;
then B3: (b ") . x in dom b by ;
then reconsider n = (b ") . x as Nat ;
reconsider aG = a * (() ~) as Matrix of dim L,INT.Ring by A3;
B4: Indices aG = [:(Seg (dim L)),(Seg (dim L)):] by MATRIX_0:24;
n in Seg (dim L) by ;
then B5: [i,n] in Indices aG by ;
aG * (i,n) is Element of INT.Ring ;
then reconsider y = (a * (() ~)) * (i,n) as Element of INT.Ring by ;
take y ; :: thesis: S1[x,y]
thus S1[x,y] by B1; :: thesis: verum
end;
end;
end;
consider l being Function of (),INT.Ring such that
A18: for x being Element of () holds S1[x,l . x] from l is Element of Funcs ( the carrier of (), the carrier of INT.Ring) by FUNCT_2:8;
then reconsider l = l as Linear_Combination of EMLat L by ;
reconsider ai = a as Element of INT.Ring by A3;
L1: len () = len b by MATRIX_0:24;
L2: width (a * (() ~)) = dim () by MATRIX_0:23
.= len b by ZMATRLIN:49 ;
Q7: len (Line ((a * (() ~)),i)) = len b by ;
Q8: len (Col ((),i)) = len b by ;
A31: len (ScFS ((b /. i),l,b)) = len b by defScFS
.= len (mlt ((Line ((a * (() ~)),i)),(Col ((),i)))) by ;
for k being Nat st 1 <= k & k <= len (ScFS ((b /. i),l,b)) holds
(mlt ((Line ((a * (() ~)),i)),(Col ((),i)))) . k = (ScFS ((b /. i),l,b)) . k
proof
let k be Nat; :: thesis: ( 1 <= k & k <= len (ScFS ((b /. i),l,b)) implies (mlt ((Line ((a * (() ~)),i)),(Col ((),i)))) . k = (ScFS ((b /. i),l,b)) . k )
assume AS1: ( 1 <= k & k <= len (ScFS ((b /. i),l,b)) ) ; :: thesis: (mlt ((Line ((a * (() ~)),i)),(Col ((),i)))) . k = (ScFS ((b /. i),l,b)) . k
then Q0: k in dom (ScFS ((b /. i),l,b)) by FINSEQ_3:25;
D0: ( 1 <= k & k <= len b ) by ;
then D1: k in dom b by FINSEQ_3:25;
then b . k in rng b by FUNCT_1:3;
then Q1: b /. k in I by ;
b is one-to-one by ZMATRLIN:def 5;
then Q2: k = (b ") . (b . k) by
.= (b ") . (b /. k) by ;
Q3: l . (b /. k) = (a * (() ~)) * (i,k) by ;
k in Seg (width (a * (() ~))) by D0, L2;
then Q4: (Line ((a * (() ~)),i)) . k = (a * (() ~)) * (i,k) by MATRIX_0:def 7;
k in Seg (len ()) by D0, L1;
then k in dom () by FINSEQ_1:def 3;
then Q5: (Col ((),i)) . k = () * (k,i) by MATRIX_0:def 8
.= () . ((b /. k),(b /. i)) by
.= <;(b /. k),(b /. i);>
.= <;(b /. i),(b /. k);> by ZMODLAT1:def 3
.= () . ((b /. i),(b /. k))
.= () * (i,k) by ;
Seg (len (mlt ((Line ((a * (() ~)),i)),(Col ((),i))))) = Seg (len b) by
.= dom b by FINSEQ_1:def 3 ;
then Q6: k in dom (mlt ((Line ((a * (() ~)),i)),(Col ((),i)))) by ;
<;(b /. i),((l . (b /. k)) * (b /. k));> = ((a * (() ~)) * (i,k)) * <;(b /. i),(b /. k);> by
.= ((a * (() ~)) * (i,k)) * (() . ((b /. i),(b /. k)))
.= ((a * (() ~)) * (i,k)) * (() * (i,k)) by
.= (mlt ((Line ((a * (() ~)),i)),(Col ((),i)))) . k by ;
hence (mlt ((Line ((a * (() ~)),i)),(Col ((),i)))) . k = (ScFS ((b /. i),l,b)) . k by ; :: thesis: verum
end;
then A32: mlt ((Line ((a * (() ~)),i)),(Col ((),i))) = ScFS ((b /. i),l,b) by A31;
set F = canFS ();
A303: ( canFS () is one-to-one & rng (canFS ()) = Carrier l ) by FUNCT_2:def 3;
then reconsider F = canFS () as FinSequence of () by FINSEQ_1:def 4;
A30: SumSc ((b /. i),l) = Sum (ScFS ((b /. i),l,F)) by ;
A302: Carrier l c= rng b
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Carrier l or x in rng b )
assume x in Carrier l ; :: thesis: x in rng b
then consider v being Element of () such that
B30: ( x = v & l . v <> 0. INT.Ring ) ;
assume not x in rng b ; :: thesis: contradiction
hence contradiction by A18, B30; :: thesis: verum
end;
b is one-to-one by ZMATRLIN:def 5;
then A20: SumSc ((b /. i),l) = a by A15, A30, A32, A302, LM1;
A21: for j being Nat st i <> j & j in dom b holds
<;(b /. j),(Sum l);> = 0
proof
let j be Nat; :: thesis: ( i <> j & j in dom b implies <;(b /. j),(Sum l);> = 0 )
assume BJ1: ( i <> j & j in dom b ) ; :: thesis: <;(b /. j),(Sum l);> = 0
Q7: len (Line ((a * (() ~)),i)) = len b by ;
Q8: len (Col ((),j)) = len b by ;
A31: len (ScFS ((b /. j),l,b)) = len b by defScFS
.= len (mlt ((Line ((a * (() ~)),i)),(Col ((),j)))) by ;
for k being Nat st 1 <= k & k <= len (ScFS ((b /. j),l,b)) holds
(mlt ((Line ((a * (() ~)),i)),(Col ((),j)))) . k = (ScFS ((b /. j),l,b)) . k
proof
let k be Nat; :: thesis: ( 1 <= k & k <= len (ScFS ((b /. j),l,b)) implies (mlt ((Line ((a * (() ~)),i)),(Col ((),j)))) . k = (ScFS ((b /. j),l,b)) . k )
assume AS1: ( 1 <= k & k <= len (ScFS ((b /. j),l,b)) ) ; :: thesis: (mlt ((Line ((a * (() ~)),i)),(Col ((),j)))) . k = (ScFS ((b /. j),l,b)) . k
then Q0: k in dom (ScFS ((b /. j),l,b)) by FINSEQ_3:25;
D0: ( 1 <= k & k <= len b ) by ;
then D1: k in dom b by FINSEQ_3:25;
then b . k in rng b by FUNCT_1:3;
then Q1: b /. k in I by ;
b is one-to-one by ZMATRLIN:def 5;
then k = (b ") . (b . k) by
.= (b ") . (b /. k) by ;
then Q3: l . (b /. k) = (a * (() ~)) * (i,k) by ;
k in Seg (width (a * (() ~))) by D0, L2;
then Q4: (Line ((a * (() ~)),i)) . k = (a * (() ~)) * (i,k) by MATRIX_0:def 7;
k in Seg (len ()) by D0, L1;
then k in dom () by FINSEQ_1:def 3;
then Q5: (Col ((),j)) . k = () * (k,j) by MATRIX_0:def 8
.= () . ((b /. k),(b /. j)) by
.= <;(b /. k),(b /. j);>
.= <;(b /. j),(b /. k);> by ZMODLAT1:def 3
.= () . ((b /. j),(b /. k))
.= () * (j,k) by ;
Seg (len (mlt ((Line ((a * (() ~)),i)),(Col ((),j))))) = Seg (len b) by
.= dom b by FINSEQ_1:def 3 ;
then Q6: k in dom (mlt ((Line ((a * (() ~)),i)),(Col ((),j)))) by ;
<;(b /. j),((l . (b /. k)) * (b /. k));> = ((a * (() ~)) * (i,k)) * <;(b /. j),(b /. k);> by
.= ((a * (() ~)) * (i,k)) * (() . ((b /. j),(b /. k)))
.= ((a * (() ~)) * (i,k)) * (() * (j,k)) by
.= (mlt ((Line ((a * (() ~)),i)),(Col ((),j)))) . k by ;
hence (mlt ((Line ((a * (() ~)),i)),(Col ((),j)))) . k = (ScFS ((b /. j),l,b)) . k by ; :: thesis: verum
end;
then mlt ((Line ((a * (() ~)),i)),(Col ((),j))) = ScFS ((b /. j),l,b) by A31;
then A32: Sum (ScFS ((b /. j),l,b)) = (Line ((a * (() ~)),i)) "*" (Col ((),j))
.= 0 by ;
A30: SumSc ((b /. j),l) = Sum (ScFS ((b /. j),l,F)) by ;
b is one-to-one by ZMATRLIN:def 5;
then Sum (ScFS ((b /. j),l,F)) = Sum (ScFS ((b /. j),l,b)) by ;
hence <;(b /. j),(Sum l);> = 0 by ; :: thesis: verum
end;
reconsider EL = EMLat L as Submodule of DivisibleMod L by ZMODLAT2:20;
Sum l in EL ;
then Sum l in DivisibleMod L by ZMODUL01:24;
then consider u being Vector of () such that
A22: ai * u = Sum l by ;
take u ; :: thesis: ( () . ((b /. i),u) = 1 & ( for j being Nat st i <> j & j in dom b holds
() . ((b /. j),u) = 0 ) )

b /. i in EMLat L ;
then b /. i in rng () by ZMODLAT2:def 4;
then A24: b /. i in EMbedding L by ZMODUL08:def 3;
Sum l in EMLat L ;
then Sum l in rng () by ZMODLAT2:def 4;
then A25: Sum l in EMbedding L by ZMODUL08:def 3;
b /. i in EL ;
then b /. i in DivisibleMod L by ZMODUL01:24;
then reconsider bi = b /. i as Element of () ;
A28: a <> 0. F_Real by A3;
A29: a * (() . (bi,u)) = () . (bi,(ai * u)) by ZMODLAT2:13
.= () . ((b /. i),(Sum l)) by
.= <;(b /. i),(Sum l);> by ZMODLAT2:def 4
.= a * () by ;
for j being Nat st i <> j & j in dom b holds
() . ((b /. j),u) = 0
proof
let j be Nat; :: thesis: ( i <> j & j in dom b implies () . ((b /. j),u) = 0 )
assume B1: ( i <> j & j in dom b ) ; :: thesis: () . ((b /. j),u) = 0
b /. j in EMLat L ;
then b /. j in rng () by ZMODLAT2:def 4;
then B2: b /. j in EMbedding L by ZMODUL08:def 3;
b /. j in EL ;
then b /. j in DivisibleMod L by ZMODUL01:24;
then reconsider bj = b /. j as Element of () ;
a * (() . (bj,u)) = () . (bj,(ai * u)) by ZMODLAT2:13
.= () . ((b /. j),(Sum l)) by
.= <;(b /. j),(Sum l);> by ZMODLAT2:def 4
.= a * () by ;
hence (ScProductDM L) . ((b /. j),u) = 0 by A3; :: thesis: verum
end;
hence ( (ScProductDM L) . ((b /. i),u) = 1 & ( for j being Nat st i <> j & j in dom b holds
() . ((b /. j),u) = 0 ) ) by ; :: thesis: verum