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 (DivisibleMod L) st
( (ScProductDM L) . ((b /. i),v) = 1 & ( for j being Nat st i <> j & j in dom b holds
(ScProductDM L) . ((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 (DivisibleMod L) st
( (ScProductDM L) . ((b /. i),v) = 1 & ( for j being Nat st i <> j & j in dom b holds
(ScProductDM L) . ((b /. j),v) = 0 ) )
let i be Nat; :: thesis: ( i in dom b implies ex v being Vector of (DivisibleMod L) st
( (ScProductDM L) . ((b /. i),v) = 1 & ( for j being Nat st i <> j & j in dom b holds
(ScProductDM L) . ((b /. j),v) = 0 ) ) )
assume A1: i in dom b ; :: thesis: ex v being Vector of (DivisibleMod L) st
( (ScProductDM L) . ((b /. i),v) = 1 & ( for j being Nat st i <> j & j in dom b holds
(ScProductDM L) . ((b /. j),v) = 0 ) )
A2: dim L = dim (EMLat L) by ZMODLAT2:42;
consider a being Element of F_Real such that
A3: ( a is Element of INT.Ring & a <> 0 & a * ((GramMatrix b) ~) is Matrix of dim L,INT.Ring ) by A2, LmDE311;
(GramMatrix b) ~ is_reverse_of GramMatrix b by MATRIX_6:def 4;
then A5: ((GramMatrix b) ~) * (GramMatrix b) = 1. (F_Real,(dim (EMLat L))) by MATRIX_6:def 2
.= 1. (F_Real,(dim L)) by ZMODLAT2:42 ;
len ((GramMatrix b) ~) = dim (EMLat L) by MATRIX_0:def 2;
then width ((GramMatrix b) ~) = dim (EMLat L) by MATRIX_0:20
.= len (GramMatrix b) by MATRIX_0:def 2 ;
then A8: (a * ((GramMatrix b) ~)) * (GramMatrix b) = a * (1. (F_Real,(dim L))) by A5, MATRIX15:1;
AX1: len b = dim (EMLat L) by ZMATRLIN:49;
then A9: i in Seg (dim L) by A1, A2, FINSEQ_1:def 3;
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 A9, ZFMISC_1:87;
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 * ((GramMatrix b) ~)) * (GramMatrix b)) by A8, A9, ZFMISC_1:87;
AX3: width (a * ((GramMatrix b) ~)) = dim (EMLat L) by MATRIX_0:23
.= len (GramMatrix b) by MATRIX_0:def 2 ;
A15: (Line ((a * ((GramMatrix b) ~)),i)) "*" (Col ((GramMatrix b),i)) = ((a * ((GramMatrix b) ~)) * (GramMatrix b)) * (i,i) by A14, AX3, MATRIX_3:def 4
.= a * ((1. (F_Real,(dim L))) * (i,i)) by A8, A11, MATRIX_3:def 5
.= a * (1. F_Real) by A11, MATRIX_1:def 3
.= a ;
A16: for j being Nat st i <> j & j in dom b holds
(Line ((a * ((GramMatrix b) ~)),i)) "*" (Col ((GramMatrix b),j)) = 0

proof

let j be Nat; :: thesis: ( i <> j & j in dom b implies (Line ((a * ((GramMatrix b) ~)),i)) "*" (Col ((GramMatrix b),j)) = 0 )
assume B1: ( i <> j & j in dom b ) ; :: thesis: (Line ((a * ((GramMatrix b) ~)),i)) "*" (Col ((GramMatrix b),j)) = 0
B2: j in Seg (dim L) by A2, AX1, B1, FINSEQ_1:def 3;
then B3: [i,j] in Indices (1. (F_Real,(dim L))) by A9, A10, ZFMISC_1:87;
[i,j] in Indices ((a * ((GramMatrix b) ~)) * (GramMatrix b)) by A8, A9, A12, B2, ZFMISC_1:87;
hence (Line ((a * ((GramMatrix b) ~)),i)) "*" (Col ((GramMatrix b),j)) = ((a * ((GramMatrix b) ~)) * (GramMatrix b)) * (i,j) by AX3, MATRIX_3:def 4
.= a * ((1. (F_Real,(dim L))) * (i,j)) by A8, B3, MATRIX_3:def 5
.= a * (0. F_Real) by B1, B3, MATRIX_1:def 3
.= 0 ;
:: thesis: verum

end;

reconsider I = rng b as Basis of (EMLat L) by ZMATRLIN:def 5;
defpred S₁[ object , object ] means ( ( $1 in I implies for n being Nat st n = (b ") . $1 & n in dom b holds
$2 = (a * ((GramMatrix b) ~)) * (i,n) ) & ( not $1 in I implies $2 = 0. INT.Ring ) );
A17: for x being Element of (EMLat L) ex y being Element of INT.Ring st S₁[x,y]

proof

let x be Element of (EMLat L); :: thesis: ex y being Element of INT.Ring st S₁[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 S₁[x,y]

b is one-to-one by ZMATRLIN:def 5;
then B3: (b ") . x in dom b by B1, FUNCT_1:32;
then reconsider n = (b ") . x as Nat ;
reconsider aG = a * ((GramMatrix b) ~) 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 A2, AX1, B3, FINSEQ_1:def 3;
then B5: [i,n] in Indices aG by A9, B4, ZFMISC_1:87;
aG * (i,n) is Element of INT.Ring ;
then reconsider y = (a * ((GramMatrix b) ~)) * (i,n) as Element of INT.Ring by B5, ZMATRLIN:1;
take y ; :: thesis: S₁[x,y]
thus S₁[x,y] by B1; :: thesis: verum

end;

suppose B1: not x in I ; :: thesis: ex y being Element of INT.Ring st S₁[x,y]

take 0. INT.Ring ; :: thesis: S₁[x, 0. INT.Ring]
thus S₁[x, 0. INT.Ring] by B1; :: thesis: verum

end;

end;

end;

consider l being Function of (EMLat L),INT.Ring such that
A18: for x being Element of (EMLat L) holds S₁[x,l . x] from FUNCT_2:sch 3(A17);
l is Element of Funcs ( the carrier of (EMLat L), the carrier of INT.Ring) by FUNCT_2:8;
then reconsider l = l as Linear_Combination of EMLat L by A18, VECTSP_6:def 1;
reconsider ai = a as Element of INT.Ring by A3;
L1: len (GramMatrix b) = len b by MATRIX_0:24;
L2: width (a * ((GramMatrix b) ~)) = dim (EMLat L) by MATRIX_0:23
.= len b by ZMATRLIN:49 ;
Q7: len (Line ((a * ((GramMatrix b) ~)),i)) = len b by L2, MATRIX_0:def 7;
Q8: len (Col ((GramMatrix b),i)) = len b by L1, MATRIX_0:def 8;
A31: len (ScFS ((b /. i),l,b)) = len b by defScFS
.= len (mlt ((Line ((a * ((GramMatrix b) ~)),i)),(Col ((GramMatrix b),i)))) by Q7, Q8, FINSEQ_2:72 ;
for k being Nat st 1 <= k & k <= len (ScFS ((b /. i),l,b)) holds
(mlt ((Line ((a * ((GramMatrix b) ~)),i)),(Col ((GramMatrix b),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 * ((GramMatrix b) ~)),i)),(Col ((GramMatrix b),i)))) . k = (ScFS ((b /. i),l,b)) . k )
assume AS1: ( 1 <= k & k <= len (ScFS ((b /. i),l,b)) ) ; :: thesis: (mlt ((Line ((a * ((GramMatrix b) ~)),i)),(Col ((GramMatrix b),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 AS1, defScFS;
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 PARTFUN1:def 6, D1;
b is one-to-one by ZMATRLIN:def 5;
then Q2: k = (b ") . (b . k) by FUNCT_1:34, D1
.= (b ") . (b /. k) by PARTFUN1:def 6, D1 ;
Q3: l . (b /. k) = (a * ((GramMatrix b) ~)) * (i,k) by Q1, Q2, D0, A18, FINSEQ_3:25;
k in Seg (width (a * ((GramMatrix b) ~))) by D0, L2;
then Q4: (Line ((a * ((GramMatrix b) ~)),i)) . k = (a * ((GramMatrix b) ~)) * (i,k) by MATRIX_0:def 7;
k in Seg (len (GramMatrix b)) by D0, L1;
then k in dom (GramMatrix b) by FINSEQ_1:def 3;
then Q5: (Col ((GramMatrix b),i)) . k = (GramMatrix b) * (k,i) by MATRIX_0:def 8
.= (InnerProduct (EMLat L)) . ((b /. k),(b /. i)) by D1, A1, ZMODLAT1:def 32
.= <;(b /. k),(b /. i);>
.= <;(b /. i),(b /. k);> by ZMODLAT1:def 3
.= (InnerProduct (EMLat L)) . ((b /. i),(b /. k))
.= (GramMatrix b) * (i,k) by D1, A1, ZMODLAT1:def 32 ;
Seg (len (mlt ((Line ((a * ((GramMatrix b) ~)),i)),(Col ((GramMatrix b),i))))) = Seg (len b) by Q7, Q8, FINSEQ_2:72
.= dom b by FINSEQ_1:def 3 ;
then Q6: k in dom (mlt ((Line ((a * ((GramMatrix b) ~)),i)),(Col ((GramMatrix b),i)))) by D1, FINSEQ_1:def 3;
<;(b /. i),((l . (b /. k)) * (b /. k));> = ((a * ((GramMatrix b) ~)) * (i,k)) * <;(b /. i),(b /. k);> by Q3, ZMODLAT1:9
.= ((a * ((GramMatrix b) ~)) * (i,k)) * ((InnerProduct (EMLat L)) . ((b /. i),(b /. k)))
.= ((a * ((GramMatrix b) ~)) * (i,k)) * ((GramMatrix b) * (i,k)) by D1, A1, ZMODLAT1:def 32
.= (mlt ((Line ((a * ((GramMatrix b) ~)),i)),(Col ((GramMatrix b),i)))) . k by Q4, Q5, Q6, FVSUM_1:60 ;
hence (mlt ((Line ((a * ((GramMatrix b) ~)),i)),(Col ((GramMatrix b),i)))) . k = (ScFS ((b /. i),l,b)) . k by Q0, defScFS; :: thesis: verum

end;

then A32: mlt ((Line ((a * ((GramMatrix b) ~)),i)),(Col ((GramMatrix b),i))) = ScFS ((b /. i),l,b) by A31;
set F = canFS (Carrier l);
A303: ( canFS (Carrier l) is one-to-one & rng (canFS (Carrier l)) = Carrier l ) by FUNCT_2:def 3;
then reconsider F = canFS (Carrier l) as FinSequence of (EMLat L) by FINSEQ_1:def 4;
A30: SumSc ((b /. i),l) = Sum (ScFS ((b /. i),l,F)) by A303, defSumSc;
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 (EMLat L) 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 * ((GramMatrix b) ~)),i)) = len b by L2, MATRIX_0:def 7;
Q8: len (Col ((GramMatrix b),j)) = len b by L1, MATRIX_0:def 8;
A31: len (ScFS ((b /. j),l,b)) = len b by defScFS
.= len (mlt ((Line ((a * ((GramMatrix b) ~)),i)),(Col ((GramMatrix b),j)))) by Q7, Q8, FINSEQ_2:72 ;
for k being Nat st 1 <= k & k <= len (ScFS ((b /. j),l,b)) holds
(mlt ((Line ((a * ((GramMatrix b) ~)),i)),(Col ((GramMatrix b),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 * ((GramMatrix b) ~)),i)),(Col ((GramMatrix b),j)))) . k = (ScFS ((b /. j),l,b)) . k )
assume AS1: ( 1 <= k & k <= len (ScFS ((b /. j),l,b)) ) ; :: thesis: (mlt ((Line ((a * ((GramMatrix b) ~)),i)),(Col ((GramMatrix b),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 AS1, defScFS;
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 PARTFUN1:def 6, D1;
b is one-to-one by ZMATRLIN:def 5;
then k = (b ") . (b . k) by FUNCT_1:34, D1
.= (b ") . (b /. k) by PARTFUN1:def 6, D1 ;
then Q3: l . (b /. k) = (a * ((GramMatrix b) ~)) * (i,k) by Q1, D0, A18, FINSEQ_3:25;
k in Seg (width (a * ((GramMatrix b) ~))) by D0, L2;
then Q4: (Line ((a * ((GramMatrix b) ~)),i)) . k = (a * ((GramMatrix b) ~)) * (i,k) by MATRIX_0:def 7;
k in Seg (len (GramMatrix b)) by D0, L1;
then k in dom (GramMatrix b) by FINSEQ_1:def 3;
then Q5: (Col ((GramMatrix b),j)) . k = (GramMatrix b) * (k,j) by MATRIX_0:def 8
.= (InnerProduct (EMLat L)) . ((b /. k),(b /. j)) by D1, BJ1, ZMODLAT1:def 32
.= <;(b /. k),(b /. j);>
.= <;(b /. j),(b /. k);> by ZMODLAT1:def 3
.= (InnerProduct (EMLat L)) . ((b /. j),(b /. k))
.= (GramMatrix b) * (j,k) by D1, BJ1, ZMODLAT1:def 32 ;
Seg (len (mlt ((Line ((a * ((GramMatrix b) ~)),i)),(Col ((GramMatrix b),j))))) = Seg (len b) by Q7, Q8, FINSEQ_2:72
.= dom b by FINSEQ_1:def 3 ;
then Q6: k in dom (mlt ((Line ((a * ((GramMatrix b) ~)),i)),(Col ((GramMatrix b),j)))) by D1, FINSEQ_1:def 3;
<;(b /. j),((l . (b /. k)) * (b /. k));> = ((a * ((GramMatrix b) ~)) * (i,k)) * <;(b /. j),(b /. k);> by Q3, ZMODLAT1:9
.= ((a * ((GramMatrix b) ~)) * (i,k)) * ((InnerProduct (EMLat L)) . ((b /. j),(b /. k)))
.= ((a * ((GramMatrix b) ~)) * (i,k)) * ((GramMatrix b) * (j,k)) by D1, BJ1, ZMODLAT1:def 32
.= (mlt ((Line ((a * ((GramMatrix b) ~)),i)),(Col ((GramMatrix b),j)))) . k by Q4, Q5, Q6, FVSUM_1:60 ;
hence (mlt ((Line ((a * ((GramMatrix b) ~)),i)),(Col ((GramMatrix b),j)))) . k = (ScFS ((b /. j),l,b)) . k by Q0, defScFS; :: thesis: verum

end;

then mlt ((Line ((a * ((GramMatrix b) ~)),i)),(Col ((GramMatrix b),j))) = ScFS ((b /. j),l,b) by A31;
then A32: Sum (ScFS ((b /. j),l,b)) = (Line ((a * ((GramMatrix b) ~)),i)) "*" (Col ((GramMatrix b),j))
.= 0 by A16, BJ1 ;
A30: SumSc ((b /. j),l) = Sum (ScFS ((b /. j),l,F)) by A303, defSumSc;
b is one-to-one by ZMATRLIN:def 5;
then Sum (ScFS ((b /. j),l,F)) = Sum (ScFS ((b /. j),l,b)) by LM1, A302;
hence <;(b /. j),(Sum l);> = 0 by A30, A32, ThSumSc1; :: 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 (DivisibleMod L) such that
A22: ai * u = Sum l by A3, ZMODUL08:23;
take u ; :: thesis: ( (ScProductDM L) . ((b /. i),u) = 1 & ( for j being Nat st i <> j & j in dom b holds
(ScProductDM L) . ((b /. j),u) = 0 ) )
b /. i in EMLat L ;
then b /. i in rng (MorphsZQ L) 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 (MorphsZQ L) 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 (DivisibleMod L) ;
A28: a <> 0. F_Real by A3;
A29: a * ((ScProductDM L) . (bi,u)) = (ScProductDM L) . (bi,(ai * u)) by ZMODLAT2:13
.= (ScProductEM L) . ((b /. i),(Sum l)) by A22, A24, A25, ZMODLAT2:8
.= <;(b /. i),(Sum l);> by ZMODLAT2:def 4
.= a * (1. F_Real) by A20, ThSumSc1 ;
for j being Nat st i <> j & j in dom b holds
(ScProductDM L) . ((b /. j),u) = 0

proof

let j be Nat; :: thesis: ( i <> j & j in dom b implies (ScProductDM L) . ((b /. j),u) = 0 )
assume B1: ( i <> j & j in dom b ) ; :: thesis: (ScProductDM L) . ((b /. j),u) = 0
b /. j in EMLat L ;
then b /. j in rng (MorphsZQ L) 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 (DivisibleMod L) ;
a * ((ScProductDM L) . (bj,u)) = (ScProductDM L) . (bj,(ai * u)) by ZMODLAT2:13
.= (ScProductEM L) . ((b /. j),(Sum l)) by A22, A25, B2, ZMODLAT2:8
.= <;(b /. j),(Sum l);> by ZMODLAT2:def 4
.= a * (0. F_Real) by A21, B1 ;
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
(ScProductDM L) . ((b /. j),u) = 0 ) ) by A28, A29, VECTSP_1:5; :: thesis: verum