Theorem LT-2. SAM’s lemma. Let L be a modular lattice with 0 and 1. For all x, y ∈ L, if z_{1} is a complement of x ∨ y, and if z_{2} is a complement of x ∧ y, then

(z_{1} ∨ (x ∧ z_{2})) ∧ (z_{1} ∨ (y ∧ z_{2})) = z_{1}.

To help Otter find a short and quick proof, we reformulate the conclusion, from α = β into α = x, β = y → x = y. Also, in keeping with the theme of this work, we use an equational form of modularity,

(x ∧ y) ∨ (x ∧ z) = x ∧ (y ∨ (x ∧ z)),

instead of the more usual implicational form. Proof (found by Otter 3.0.4 on

gyro at 23.51 seconds).

4 x ∧ y = y ∧ x 6,5 (x ∧ y) ∧ z = x ∧ (y ∧ z) 9 x ∨ y = y ∨ x 11,10 (x ∨ y) ∨ z = x ∨ (y ∨ z) 12 x ∧ (x ∨ y) = x 14 x ∨ (x ∧ y) = x 17,16 0 ∧ x = 0 19,18 0 ∨ x = x 20 1 ∧ x = x 25,24 (x ∧ y) ∨ (x ∧ z) = x ∧ (y ∨ (x ∧ z)) 28 C_{1} ∧ (A ∨ B) = 0 30 C_{2} ∨ (A ∧ B) = 1 32 C_{2} ∧ (A ∧ B) = 0 34 C_{1} ∨ (A ∧ C_{2}) = D 37,36 C_{1} ∨ (B ∧ C_{2}) = E 38 D ∧ E ≠ C_{1}

39  E ∧ D ≠ C_{1}  [4 → 38]
40  C_{1} ∨ (C_{2} ∧ B) = E  [4 → 36]
44  (A ∨ B) ∧ C_{1} = 0  [4 → 28]
46  C_{1} ∧ ((A ∨ B) ∧ x) = 0  [28 → 5 :17, flip]
51  x ∧ (y ∧ z) = y ∧ (z ∧ x)  [4 → 5]
54  x ∧ (y ∧ z) = z ∧ (x ∧ y)  [flip 51]
55  C_{2} ∨ (B ∧ A) = 1  [4 → 30]
60,59  A ∧ (B ∧ C_{2}) = 0  [4 → 32 :6]
88,87  (A ∧ C_{2}) ∨ C_{1} = D  [34 → 9, flip]
156  C_{1} ∧ E = C_{1}  [40 → 12]
166  (x ∨ y) ∧ x = x  [4 → 12]
168  x ∧ ((x ∨ y) ∧ z) = x ∧ z  [12 → 5, flip]
175,174 E ∧ C_{1} = C_{1}  [4 → 156]
196 x ∨ (y ∧ x) = x [4 → 14]
201,200 (x ∧ y) ∨ x = x  [9 → 14]

217,216 x ∧ 0 = 0  [4 → 16]
219,218 x ∨ 0 = x  [9 → 18]
231,230 x ∧ 1 = x  [4 → 20]
296  (A ∨ B) ∧ (C_{1} ∨ ((A ∨ B) ∧ x)) = (A ∨ B) ∧ x [44 → 24 :19, flip]
306  (E ∧ x) ∨ C_{1} = E ∧ (x ∨ C_{1})  [174 → 24 :175]
312  x ∧ (y ∨ (x ∧ z)) = x ∧ (z ∨ (x ∧ y))  [9 → 24 :25]
349  C_{1} ∧ (x ∧ (A ∨ B)) = 0  [4 → 46]
1295  C_{1} ∧ A = 0  [12 → 349]
1300,1299 A ∧ C_{1} = 0  [4 → 1295]
3663  B ∧ (A ∨ (B ∧ C_{2})) = B  [55 → 312 :231, flip]
3671  A ∧ D = A ∧ C_{2}  [34 → 312 :1300,219]
3801  D ∧ A = A ∧ C_{2}  [4 → 3671]
3854  A ∨ (B ∧ C_{2}) = A ∨ B  [3663 → 196 :11,201, flip]
3916  (B ∧ C_{2}) ∨ A = A ∨ B  [9 → 3854]
4122,4121 (A ∨ B) ∧ (B ∧ C_{2}) = B ∧ C_{2}  [3916 → 166]
4395  (A ∨ B) ∧ E = B ∧ C_{2}  [4121 → 296 :37,4122]
4420  A ∧ E = 0  [4395 → 168 :60, flip]
4468  E ∧ (x ∧ A) = 0  [4420 → 54 :217, flip]
4721  E ∧ ((x ∧ A) ∨ C_{1}) = C_{1}  [4468 → 306 :19, flip]
4972  E ∧ D = C_{1}  [3801 → 4721 :88]
4974  □  [4972,39]