let V be RealLinearSpace; :: thesis: LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) is Lattice

set S = LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #);

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

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

set S = LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #);

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

proof

A2:
for A, B being Element of LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) holds (A "/\" B) "\/" B = B
let A, B be Element of LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #); :: thesis: A "/\" B = B "/\" A

reconsider W1 = A, W2 = B as Subspace of V by Def3;

thus A "/\" B = W1 /\ W2 by Def8

.= W2 /\ W1 by Th14

.= B "/\" A by Def8 ; :: thesis: verum

end;reconsider W1 = A, W2 = B as Subspace of V by Def3;

thus A "/\" B = W1 /\ W2 by Def8

.= W2 /\ W1 by Th14

.= B "/\" A by Def8 ; :: thesis: verum

proof

A3:
for A, B, C being Element of LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) holds A "\/" (B "\/" C) = (A "\/" B) "\/" C
let A, B be Element of LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #); :: thesis: (A "/\" B) "\/" B = B

reconsider W1 = A, W2 = B as strict Subspace of V by Def3;

reconsider AB = W1 /\ W2 as Element of LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) by Def3;

thus (A "/\" B) "\/" B = (SubJoin V) . (AB,B) by Def8

.= (W1 /\ W2) + W2 by Def7

.= B by Lm6, RLSUB_1:30 ; :: thesis: verum

end;reconsider W1 = A, W2 = B as strict Subspace of V by Def3;

reconsider AB = W1 /\ W2 as Element of LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) by Def3;

thus (A "/\" B) "\/" B = (SubJoin V) . (AB,B) by Def8

.= (W1 /\ W2) + W2 by Def7

.= B by Lm6, RLSUB_1:30 ; :: thesis: verum

proof

A4:
for A, B being Element of LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) holds A "/\" (A "\/" B) = A
let A, B, C be Element of LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #); :: thesis: A "\/" (B "\/" C) = (A "\/" B) "\/" C

reconsider W1 = A, W2 = B, W3 = C as Subspace of V by Def3;

reconsider AB = W1 + W2, BC = W2 + W3 as Element of LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) by Def3;

thus A "\/" (B "\/" C) = (SubJoin V) . (A,BC) by Def7

.= W1 + (W2 + W3) by Def7

.= (W1 + W2) + W3 by Th6

.= (SubJoin V) . (AB,C) by Def7

.= (A "\/" B) "\/" C by Def7 ; :: thesis: verum

end;reconsider W1 = A, W2 = B, W3 = C as Subspace of V by Def3;

reconsider AB = W1 + W2, BC = W2 + W3 as Element of LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) by Def3;

thus A "\/" (B "\/" C) = (SubJoin V) . (A,BC) by Def7

.= W1 + (W2 + W3) by Def7

.= (W1 + W2) + W3 by Th6

.= (SubJoin V) . (AB,C) by Def7

.= (A "\/" B) "\/" C by Def7 ; :: thesis: verum

proof

A5:
for A, B, C being Element of LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) holds A "/\" (B "/\" C) = (A "/\" B) "/\" C
let A, B be Element of LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #); :: thesis: A "/\" (A "\/" B) = A

reconsider W1 = A, W2 = B as strict Subspace of V by Def3;

reconsider AB = W1 + W2 as Element of LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) by Def3;

thus A "/\" (A "\/" B) = (SubMeet V) . (A,AB) by Def7

.= W1 /\ (W1 + W2) by Def8

.= A by Lm7, RLSUB_1:30 ; :: thesis: verum

end;reconsider W1 = A, W2 = B as strict Subspace of V by Def3;

reconsider AB = W1 + W2 as Element of LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) by Def3;

thus A "/\" (A "\/" B) = (SubMeet V) . (A,AB) by Def7

.= W1 /\ (W1 + W2) by Def8

.= A by Lm7, RLSUB_1:30 ; :: thesis: verum

proof

for A, B being Element of LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) holds A "\/" B = B "\/" A
let A, B, C be Element of LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #); :: thesis: A "/\" (B "/\" C) = (A "/\" B) "/\" C

reconsider W1 = A, W2 = B, W3 = C as Subspace of V by Def3;

reconsider AB = W1 /\ W2, BC = W2 /\ W3 as Element of LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) by Def3;

thus A "/\" (B "/\" C) = (SubMeet V) . (A,BC) by Def8

.= W1 /\ (W2 /\ W3) by Def8

.= (W1 /\ W2) /\ W3 by Th15

.= (SubMeet V) . (AB,C) by Def8

.= (A "/\" B) "/\" C by Def8 ; :: thesis: verum

end;reconsider W1 = A, W2 = B, W3 = C as Subspace of V by Def3;

reconsider AB = W1 /\ W2, BC = W2 /\ W3 as Element of LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) by Def3;

thus A "/\" (B "/\" C) = (SubMeet V) . (A,BC) by Def8

.= W1 /\ (W2 /\ W3) by Def8

.= (W1 /\ W2) /\ W3 by Th15

.= (SubMeet V) . (AB,C) by Def8

.= (A "/\" B) "/\" C by Def8 ; :: thesis: verum

proof

then
( LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) is join-commutative & LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) is join-associative & LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) is meet-absorbing & LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) is meet-commutative & LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) is meet-associative & LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) is join-absorbing )
by A3, A2, A1, A5, A4;
let A, B be Element of LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #); :: thesis: A "\/" B = B "\/" A

reconsider W1 = A, W2 = B as Subspace of V by Def3;

thus A "\/" B = W1 + W2 by Def7

.= W2 + W1 by Lm1

.= B "\/" A by Def7 ; :: thesis: verum

end;reconsider W1 = A, W2 = B as Subspace of V by Def3;

thus A "\/" B = W1 + W2 by Def7

.= W2 + W1 by Lm1

.= B "\/" A by Def7 ; :: thesis: verum

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