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
proof
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;
A2: for A, B being Element of LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) holds (A "/\" B) "\/" B = B
proof
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;
A3: for A, B, C being Element of LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) holds A "\/" (B "\/" C) = (A "\/" B) "\/" C
proof
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;
A4: for A, B being Element of LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) holds A "/\" (A "\/" B) = A
proof
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;
A5: for A, B, C being Element of LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) holds A "/\" (B "/\" C) = (A "/\" B) "/\" C
proof
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;
for A, B being Element of LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) holds A "\/" B = B "\/" A
proof
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;
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;
hence LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) is Lattice ; :: thesis: verum