let L be Z_Lattice; :: thesis: for b being FinSequence of L holds
( b is OrdBasis of L iff (MorphsZQ L) * b is OrdBasis of EMbedding L )
let b be FinSequence of L; :: thesis: ( b is OrdBasis of L iff (MorphsZQ L) * b is OrdBasis of EMbedding L )
E1: ex T being linear-transformation of L,(EMbedding L) st
( T is bijective & T = MorphsZQ L & ( for v being Vector of L holds T . v = Class ((EQRZM L),[v,1]) ) ) by ZMODUL08:21;
E4: (MorphsZQ L) * b is FinSequence of (EMbedding L) by E1, FINSEQ_2:32;
P3: rng ((MorphsZQ L) * b) = (MorphsZQ L) .: (rng b) by RELAT_1:127;
hereby :: thesis: ( (MorphsZQ L) * b is OrdBasis of EMbedding L implies b is OrdBasis of L )
assume b is OrdBasis of L ; :: thesis: (MorphsZQ L) * b is OrdBasis of EMbedding L
then P1: ( b is one-to-one & rng b is Basis of L ) by ZMATRLIN:def 5;
then (MorphsZQ L) .: (rng b) is Basis of (EMbedding L) by LmEMDetX6;
hence (MorphsZQ L) * b is OrdBasis of EMbedding L by E1, E4, P1, P3, ZMATRLIN:def 5; :: thesis: verum
end;
assume (MorphsZQ L) * b is OrdBasis of EMbedding L ; :: thesis: b is OrdBasis of L
then P1: ( (MorphsZQ L) * b is one-to-one & rng ((MorphsZQ L) * b) is Basis of (EMbedding L) ) by ZMATRLIN:def 5;
dom (MorphsZQ L) = the carrier of L by FUNCT_2:def 1;
then rng b c= dom (MorphsZQ L) ;
then P2: b is one-to-one by P1, FUNCT_1:25;
rng b is Basis of L by LmEMDetX6, P1, P3;
hence b is OrdBasis of L by ZMATRLIN:def 5, P2; :: thesis: verum