let C1, C2 be Subset of (DivisibleMod L); :: thesis: ( ( for v being Vector of (DivisibleMod L) holds
( v in C1 iff ex u being Vector of (EMLat L) st
( u in I & (ScProductDM L) . (u,v) = 1 & ( for w being Vector of (EMLat L) st w in I & u <> w holds
(ScProductDM L) . (w,v) = 0 ) ) ) ) & ( for v being Vector of (DivisibleMod L) holds
( v in C2 iff ex u being Vector of (EMLat L) st
( u in I & (ScProductDM L) . (u,v) = 1 & ( for w being Vector of (EMLat L) st w in I & u <> w holds
(ScProductDM L) . (w,v) = 0 ) ) ) ) implies C1 = C2 )
assume that
A1: for v being Vector of (DivisibleMod L) holds
( v in C1 iff ex u being Vector of (EMLat L) st
( u in I & (ScProductDM L) . (u,v) = 1 & ( for w being Vector of (EMLat L) st w in I & u <> w holds
(ScProductDM L) . (w,v) = 0 ) ) ) and
A2: for v being Vector of (DivisibleMod L) holds
( v in C2 iff ex u being Vector of (EMLat L) st
( u in I & (ScProductDM L) . (u,v) = 1 & ( for w being Vector of (EMLat L) st w in I & u <> w holds
(ScProductDM L) . (w,v) = 0 ) ) ) ; :: thesis: C1 = C2
for v being Vector of (DivisibleMod L) st v in C1 holds
v in C2
proof
let v be Vector of (DivisibleMod L); :: thesis: ( v in C1 implies v in C2 )
assume B1: v in C1 ; :: thesis: v in C2
ex u being Vector of (EMLat L) st
( u in I & (ScProductDM L) . (u,v) = 1 & ( for w being Vector of (EMLat L) st w in I & u <> w holds
(ScProductDM L) . (w,v) = 0 ) ) by A1, B1;
hence v in C2 by A2; :: thesis: verum
end;
then A3: C1 c= C2 ;
for v being Vector of (DivisibleMod L) st v in C2 holds
v in C1
proof
let v be Vector of (DivisibleMod L); :: thesis: ( v in C2 implies v in C1 )
assume B1: v in C2 ; :: thesis: v in C1
ex u being Vector of (EMLat L) st
( u in I & (ScProductDM L) . (u,v) = 1 & ( for w being Vector of (EMLat L) st w in I & u <> w holds
(ScProductDM L) . (w,v) = 0 ) ) by A2, B1;
hence v in C1 by A1; :: thesis: verum
end;
then C2 c= C1 ;
hence C1 = C2 by A3; :: thesis: verum