let GF be non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr ; :: thesis: for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W1, W2 being Subspace of M

for C1 being Coset of W1

for C2 being Coset of W2 st C1 meets C2 holds

C1 /\ C2 is Coset of W1 /\ W2

let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF; :: thesis: for W1, W2 being Subspace of M

for C1 being Coset of W1

for C2 being Coset of W2 st C1 meets C2 holds

C1 /\ C2 is Coset of W1 /\ W2

let W1, W2 be Subspace of M; :: thesis: for C1 being Coset of W1

for C2 being Coset of W2 st C1 meets C2 holds

C1 /\ C2 is Coset of W1 /\ W2

let C1 be Coset of W1; :: thesis: for C2 being Coset of W2 st C1 meets C2 holds

C1 /\ C2 is Coset of W1 /\ W2

let C2 be Coset of W2; :: thesis: ( C1 meets C2 implies C1 /\ C2 is Coset of W1 /\ W2 )

set v = the Element of C1 /\ C2;

set C = C1 /\ C2;

assume A1: C1 /\ C2 <> {} ; :: according to XBOOLE_0:def 7 :: thesis: C1 /\ C2 is Coset of W1 /\ W2

then reconsider v = the Element of C1 /\ C2 as Element of M by TARSKI:def 3;

v in C2 by A1, XBOOLE_0:def 4;

then A2: C2 = v + W2 by VECTSP_4:77;

v in C1 by A1, XBOOLE_0:def 4;

then A3: C1 = v + W1 by VECTSP_4:77;

C1 /\ C2 is Coset of W1 /\ W2

for W1, W2 being Subspace of M

for C1 being Coset of W1

for C2 being Coset of W2 st C1 meets C2 holds

C1 /\ C2 is Coset of W1 /\ W2

let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF; :: thesis: for W1, W2 being Subspace of M

for C1 being Coset of W1

for C2 being Coset of W2 st C1 meets C2 holds

C1 /\ C2 is Coset of W1 /\ W2

let W1, W2 be Subspace of M; :: thesis: for C1 being Coset of W1

for C2 being Coset of W2 st C1 meets C2 holds

C1 /\ C2 is Coset of W1 /\ W2

let C1 be Coset of W1; :: thesis: for C2 being Coset of W2 st C1 meets C2 holds

C1 /\ C2 is Coset of W1 /\ W2

let C2 be Coset of W2; :: thesis: ( C1 meets C2 implies C1 /\ C2 is Coset of W1 /\ W2 )

set v = the Element of C1 /\ C2;

set C = C1 /\ C2;

assume A1: C1 /\ C2 <> {} ; :: according to XBOOLE_0:def 7 :: thesis: C1 /\ C2 is Coset of W1 /\ W2

then reconsider v = the Element of C1 /\ C2 as Element of M by TARSKI:def 3;

v in C2 by A1, XBOOLE_0:def 4;

then A2: C2 = v + W2 by VECTSP_4:77;

v in C1 by A1, XBOOLE_0:def 4;

then A3: C1 = v + W1 by VECTSP_4:77;

C1 /\ C2 is Coset of W1 /\ W2

proof

hence
C1 /\ C2 is Coset of W1 /\ W2
; :: thesis: verum
take
v
; :: according to VECTSP_4:def 6 :: thesis: C1 /\ C2 = v + (W1 /\ W2)

thus C1 /\ C2 c= v + (W1 /\ W2) :: according to XBOOLE_0:def 10 :: thesis: v + (W1 /\ W2) c= C1 /\ C2

assume x in v + (W1 /\ W2) ; :: thesis: x in C1 /\ C2

then consider u being Element of M such that

A9: u in W1 /\ W2 and

A10: x = v + u by VECTSP_4:42;

u in W2 by A9, Th3;

then A11: x in { (v + u2) where u2 is Element of M : u2 in W2 } by A10;

u in W1 by A9, Th3;

then x in { (v + u1) where u1 is Element of M : u1 in W1 } by A10;

hence x in C1 /\ C2 by A3, A2, A11, XBOOLE_0:def 4; :: thesis: verum

end;thus C1 /\ C2 c= v + (W1 /\ W2) :: according to XBOOLE_0:def 10 :: thesis: v + (W1 /\ W2) c= C1 /\ C2

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in v + (W1 /\ W2) or x in C1 /\ C2 )
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in C1 /\ C2 or x in v + (W1 /\ W2) )

assume A4: x in C1 /\ C2 ; :: thesis: x in v + (W1 /\ W2)

then x in C1 by XBOOLE_0:def 4;

then consider u1 being Element of M such that

A5: u1 in W1 and

A6: x = v + u1 by A3, VECTSP_4:42;

x in C2 by A4, XBOOLE_0:def 4;

then consider u2 being Element of M such that

A7: u2 in W2 and

A8: x = v + u2 by A2, VECTSP_4:42;

u1 = u2 by A6, A8, RLVECT_1:8;

then u1 in W1 /\ W2 by A5, A7, Th3;

hence x in v + (W1 /\ W2) by A6; :: thesis: verum

end;assume A4: x in C1 /\ C2 ; :: thesis: x in v + (W1 /\ W2)

then x in C1 by XBOOLE_0:def 4;

then consider u1 being Element of M such that

A5: u1 in W1 and

A6: x = v + u1 by A3, VECTSP_4:42;

x in C2 by A4, XBOOLE_0:def 4;

then consider u2 being Element of M such that

A7: u2 in W2 and

A8: x = v + u2 by A2, VECTSP_4:42;

u1 = u2 by A6, A8, RLVECT_1:8;

then u1 in W1 /\ W2 by A5, A7, Th3;

hence x in v + (W1 /\ W2) by A6; :: thesis: verum

assume x in v + (W1 /\ W2) ; :: thesis: x in C1 /\ C2

then consider u being Element of M such that

A9: u in W1 /\ W2 and

A10: x = v + u by VECTSP_4:42;

u in W2 by A9, Th3;

then A11: x in { (v + u2) where u2 is Element of M : u2 in W2 } by A10;

u in W1 by A9, Th3;

then x in { (v + u1) where u1 is Element of M : u1 in W1 } by A10;

hence x in C1 /\ C2 by A3, A2, A11, XBOOLE_0:def 4; :: thesis: verum