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 holds LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) is Lattice
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF; :: thesis: LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) is Lattice
set S = LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #);
A1: for A, B being Element of LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) holds A "/\" B = B "/\" A

proof

let A, B be Element of LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #); :: thesis: A "/\" B = B "/\" A
consider W1 being strict Subspace of M such that
A2: W1 = A by Def3;
consider W2 being strict Subspace of M such that
A3: W2 = B by Def3;
thus A "/\" B = (SubMeet M) . (A,B) by LATTICES:def 2
.= W1 /\ W2 by A2, A3, Def8
.= (SubMeet M) . (B,A) by A2, A3, Def8
.= B "/\" A by LATTICES:def 2 ; :: thesis: verum

end;

A4: for A, B being Element of LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) holds (A "/\" B) "\/" B = B

proof

let A, B be Element of LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #); :: thesis: (A "/\" B) "\/" B = B
consider W1 being strict Subspace of M such that
A5: W1 = A by Def3;
consider W2 being strict Subspace of M such that
A6: W2 = B by Def3;
reconsider AB = W1 /\ W2 as Element of LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) by Def3;
thus (A "/\" B) "\/" B = (SubJoin M) . ((A "/\" B),B) by LATTICES:def 1
.= (SubJoin M) . (((SubMeet M) . (A,B)),B) by LATTICES:def 2
.= (SubJoin M) . (AB,B) by A5, A6, Def8
.= (W1 /\ W2) + W2 by A6, Def7
.= B by A6, Lm10, VECTSP_4:29 ; :: thesis: verum

end;

A7: for A, B, C being Element of LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) holds A "/\" (B "/\" C) = (A "/\" B) "/\" C

proof

let A, B, C be Element of LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #); :: thesis: A "/\" (B "/\" C) = (A "/\" B) "/\" C
consider W1 being strict Subspace of M such that
A8: W1 = A by Def3;
consider W2 being strict Subspace of M such that
A9: W2 = B by Def3;
consider W3 being strict Subspace of M such that
A10: W3 = C by Def3;
reconsider AB = W1 /\ W2, BC = W2 /\ W3 as Element of LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) by Def3;
thus A "/\" (B "/\" C) = (SubMeet M) . (A,(B "/\" C)) by LATTICES:def 2
.= (SubMeet M) . (A,((SubMeet M) . (B,C))) by LATTICES:def 2
.= (SubMeet M) . (A,BC) by A9, A10, Def8
.= W1 /\ (W2 /\ W3) by A8, Def8
.= (W1 /\ W2) /\ W3 by Th14
.= (SubMeet M) . (AB,C) by A10, Def8
.= (SubMeet M) . (((SubMeet M) . (A,B)),C) by A8, A9, Def8
.= (SubMeet M) . ((A "/\" B),C) by LATTICES:def 2
.= (A "/\" B) "/\" C by LATTICES:def 2 ; :: thesis: verum

end;

A11: for A, B, C being Element of LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) holds A "\/" (B "\/" C) = (A "\/" B) "\/" C

proof

let A, B, C be Element of LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #); :: thesis: A "\/" (B "\/" C) = (A "\/" B) "\/" C
consider W1 being strict Subspace of M such that
A12: W1 = A by Def3;
consider W2 being strict Subspace of M such that
A13: W2 = B by Def3;
consider W3 being strict Subspace of M such that
A14: W3 = C by Def3;
reconsider AB = W1 + W2, BC = W2 + W3 as Element of LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) by Def3;
thus A "\/" (B "\/" C) = (SubJoin M) . (A,(B "\/" C)) by LATTICES:def 1
.= (SubJoin M) . (A,((SubJoin M) . (B,C))) by LATTICES:def 1
.= (SubJoin M) . (A,BC) by A13, A14, Def7
.= W1 + (W2 + W3) by A12, Def7
.= (W1 + W2) + W3 by Th6
.= (SubJoin M) . (AB,C) by A14, Def7
.= (SubJoin M) . (((SubJoin M) . (A,B)),C) by A12, A13, Def7
.= (SubJoin M) . ((A "\/" B),C) by LATTICES:def 1
.= (A "\/" B) "\/" C by LATTICES:def 1 ; :: thesis: verum

end;

A15: for A, B being Element of LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) holds A "/\" (A "\/" B) = A

proof

let A, B be Element of LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #); :: thesis: A "/\" (A "\/" B) = A
consider W1 being strict Subspace of M such that
A16: W1 = A by Def3;
consider W2 being strict Subspace of M such that
A17: W2 = B by Def3;
reconsider AB = W1 + W2 as Element of LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) by Def3;
thus A "/\" (A "\/" B) = (SubMeet M) . (A,(A "\/" B)) by LATTICES:def 2
.= (SubMeet M) . (A,((SubJoin M) . (A,B))) by LATTICES:def 1
.= (SubMeet M) . (A,AB) by A16, A17, Def7
.= W1 /\ (W1 + W2) by A16, Def8
.= A by A16, Lm11, VECTSP_4:29 ; :: thesis: verum

end;

for A, B being Element of LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) holds A "\/" B = B "\/" A

proof

let A, B be Element of LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #); :: thesis: A "\/" B = B "\/" A
consider W1 being strict Subspace of M such that
A18: W1 = A by Def3;
consider W2 being strict Subspace of M such that
A19: W2 = B by Def3;
thus A "\/" B = (SubJoin M) . (A,B) by LATTICES:def 1
.= W1 + W2 by A18, A19, Def7
.= W2 + W1 by Lm1
.= (SubJoin M) . (B,A) by A18, A19, Def7
.= B "\/" A by LATTICES:def 1 ; :: thesis: verum

end;

then ( LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) is join-commutative & LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) is join-associative & LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) is meet-absorbing & LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) is meet-commutative & LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) is meet-associative & LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) is join-absorbing ) by A11, A4, A1, A7, A15, LATTICES:def 4, LATTICES:def 5, LATTICES:def 6, LATTICES:def 7, LATTICES:def 8, LATTICES:def 9;
hence LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) is Lattice ; :: thesis: verum