let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; :: thesis: for M being non empty right_complementable VectSp-like Abelian add-associative right_zeroed VectSpStr of GF holds LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) is Lattice
let M be non empty right_complementable VectSp-like Abelian add-associative right_zeroed VectSpStr of 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 = (SubJoin M) . A,B by LATTICES:def 1
.= W1 + W2 by A2, A3, Def7
.= W2 + W1 by Lm1
.= (SubJoin M) . B,A by A2, A3, Def7
.= B "\/" A by LATTICES:def 1 ; :: thesis: verum

end;

A4: 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
A5: W1 = A by Def3;
consider W2 being strict Subspace of M such that
A6: W2 = B by Def3;
consider W3 being strict Subspace of M such that
A7: 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 A6, A7, Def7
.= W1 + (W2 + W3) by A5, Def7
.= (W1 + W2) + W3 by Th10
.= (SubJoin M) . AB,C by A7, Def7
.= (SubJoin M) . ((SubJoin M) . A,B),C by A5, A6, Def7
.= (SubJoin M) . (A "\/" B),C by LATTICES:def 1
.= (A "\/" B) "\/" C by LATTICES:def 1 ; :: thesis: verum

end;

A8: 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
A9: W1 = A by Def3;
consider W2 being strict Subspace of M such that
A10: 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 A9, A10, Def8
.= (W1 /\ W2) + W2 by A10, Def7
.= B by A10, Lm10, VECTSP_4:37 ; :: thesis: verum

end;

A11: 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
A12: W1 = A by Def3;
consider W2 being strict Subspace of M such that
A13: W2 = B by Def3;
thus A "/\" B = (SubMeet M) . A,B by LATTICES:def 2
.= W1 /\ W2 by A12, A13, Def8
.= (SubMeet M) . B,A by A12, A13, Def8
.= B "/\" A by LATTICES:def 2 ; :: thesis: verum

end;

A14: 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
A15: W1 = A by Def3;
consider W2 being strict Subspace of M such that
A16: W2 = B by Def3;
consider W3 being strict Subspace of M such that
A17: 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 A16, A17, Def8
.= W1 /\ (W2 /\ W3) by A15, Def8
.= (W1 /\ W2) /\ W3 by Th19
.= (SubMeet M) . AB,C by A17, Def8
.= (SubMeet M) . ((SubMeet M) . A,B),C by A15, A16, Def8
.= (SubMeet M) . (A "/\" B),C by LATTICES:def 2
.= (A "/\" B) "/\" C by LATTICES:def 2 ; :: thesis: verum

end;

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
A18: W1 = A by Def3;
consider W2 being strict Subspace of M such that
A19: 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 A18, A19, Def7
.= W1 /\ (W1 + W2) by A18, Def8
.= A by A18, Lm11, VECTSP_4:37 ; :: 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 A1, A4, A8, A11, A14, 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