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

defpred S_{1}[ 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_{1}[x,y]

A18: for x being Element of (EMLat L) holds S_{1}[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

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

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

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

(ScProductDM L) . ((b /. j),u) = 0 ) ) by A28, A29, VECTSP_1:5; :: thesis: verum

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

reconsider I = rng b as Basis of (EMLat L) by ZMATRLIN:def 5;
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;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

defpred S

$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

proof

consider l being Function of (EMLat L),INT.Ring such that
let x be Element of (EMLat L); :: thesis: ex y being Element of INT.Ring st S_{1}[x,y]

end;per cases
( x in I or not x in I )
;

end;

suppose B1:
x in I
; :: thesis: ex y being Element of INT.Ring st S_{1}[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_{1}[x,y]

thus S_{1}[x,y]
by B1; :: thesis: verum

end;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

thus S

A18: for x being Element of (EMLat L) holds S

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

then A32:
mlt ((Line ((a * ((GramMatrix b) ~)),i)),(Col ((GramMatrix b),i))) = ScFS ((b /. i),l,b)
by A31;
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;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

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

b is one-to-one
by ZMATRLIN:def 5;
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;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

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

reconsider EL = EMLat L as Submodule of DivisibleMod L by ZMODLAT2:20;
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

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;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

then
mlt ((Line ((a * ((GramMatrix b) ~)),i)),(Col ((GramMatrix b),j))) = ScFS ((b /. j),l,b)
by A31;
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;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

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

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

hence
( (ScProductDM L) . ((b /. i),u) = 1 & ( for j being Nat st i <> j & j in dom b holds
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;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

(ScProductDM L) . ((b /. j),u) = 0 ) ) by A28, A29, VECTSP_1:5; :: thesis: verum