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

hence LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) is Lattice ; :: thesis: verum

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

A4:
for A, B being Element of LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) holds (A "/\" B) "\/" B = B
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;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

proof

A7:
for A, B, C being Element of LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) holds A "/\" (B "/\" C) = (A "/\" B) "/\" C
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;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

proof

A11:
for A, B, C being Element of LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) holds A "\/" (B "\/" C) = (A "\/" B) "\/" C
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;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

proof

A15:
for A, B being Element of LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) holds A "/\" (A "\/" B) = A
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;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

proof

for A, B being Element of LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) holds A "\/" B = B "\/" A
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;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

proof

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;
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;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

hence LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) is Lattice ; :: thesis: verum