Quantum Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  QLE Home  >  Th. List  >  oago3.21x GIF version

Theorem oago3.21x 890
 Description: 4-variable extension of Equation (3.21) of "Equations, states, and lattices..." paper. This shows that it holds in all OMLs, not just 4GO.
Assertion
Ref Expression
oago3.21x ((((a5 b) ∩ (b5 c)) ∩ (c5 d)) ∩ (d5 a)) = (((ab) ∩ (bc)) ∩ (cd))

Proof of Theorem oago3.21x
StepHypRef Expression
1 i5lei1 347 . . . . . 6 (a5 b) ≤ (a1 b)
2 i5lei2 348 . . . . . 6 (b5 c) ≤ (b2 c)
31, 2le2an 169 . . . . 5 ((a5 b) ∩ (b5 c)) ≤ ((a1 b) ∩ (b2 c))
4 i5lei1 347 . . . . 5 (c5 d) ≤ (c1 d)
53, 4le2an 169 . . . 4 (((a5 b) ∩ (b5 c)) ∩ (c5 d)) ≤ (((a1 b) ∩ (b2 c)) ∩ (c1 d))
6 i5lei2 348 . . . 4 (d5 a) ≤ (d2 a)
75, 6le2an 169 . . 3 ((((a5 b) ∩ (b5 c)) ∩ (c5 d)) ∩ (d5 a)) ≤ ((((a1 b) ∩ (b2 c)) ∩ (c1 d)) ∩ (d2 a))
8 mhcor1 888 . . 3 ((((a1 b) ∩ (b2 c)) ∩ (c1 d)) ∩ (d2 a)) = (((ab) ∩ (bc)) ∩ (cd))
97, 8lbtr 139 . 2 ((((a5 b) ∩ (b5 c)) ∩ (c5 d)) ∩ (d5 a)) ≤ (((ab) ∩ (bc)) ∩ (cd))
10 leid 148 . . . 4 (((ab) ∩ (bc)) ∩ (cd)) ≤ (((ab) ∩ (bc)) ∩ (cd))
11 eqtr4 834 . . . . 5 (((ab) ∩ (bc)) ∩ (cd)) ≤ (ad)
12 bicom 96 . . . . 5 (ad) = (da)
1311, 12lbtr 139 . . . 4 (((ab) ∩ (bc)) ∩ (cd)) ≤ (da)
1410, 13ler2an 173 . . 3 (((ab) ∩ (bc)) ∩ (cd)) ≤ ((((ab) ∩ (bc)) ∩ (cd)) ∩ (da))
15 u5lembi 725 . . . . . . . 8 ((a5 b) ∩ (b5 a)) = (ab)
1615ax-r1 35 . . . . . . 7 (ab) = ((a5 b) ∩ (b5 a))
17 lea 160 . . . . . . 7 ((a5 b) ∩ (b5 a)) ≤ (a5 b)
1816, 17bltr 138 . . . . . 6 (ab) ≤ (a5 b)
19 u5lembi 725 . . . . . . . 8 ((b5 c) ∩ (c5 b)) = (bc)
2019ax-r1 35 . . . . . . 7 (bc) = ((b5 c) ∩ (c5 b))
21 lea 160 . . . . . . 7 ((b5 c) ∩ (c5 b)) ≤ (b5 c)
2220, 21bltr 138 . . . . . 6 (bc) ≤ (b5 c)
2318, 22le2an 169 . . . . 5 ((ab) ∩ (bc)) ≤ ((a5 b) ∩ (b5 c))
24 u5lembi 725 . . . . . . 7 ((c5 d) ∩ (d5 c)) = (cd)
2524ax-r1 35 . . . . . 6 (cd) = ((c5 d) ∩ (d5 c))
26 lea 160 . . . . . 6 ((c5 d) ∩ (d5 c)) ≤ (c5 d)
2725, 26bltr 138 . . . . 5 (cd) ≤ (c5 d)
2823, 27le2an 169 . . . 4 (((ab) ∩ (bc)) ∩ (cd)) ≤ (((a5 b) ∩ (b5 c)) ∩ (c5 d))
29 u5lembi 725 . . . . . 6 ((d5 a) ∩ (a5 d)) = (da)
3029ax-r1 35 . . . . 5 (da) = ((d5 a) ∩ (a5 d))
31 lea 160 . . . . 5 ((d5 a) ∩ (a5 d)) ≤ (d5 a)
3230, 31bltr 138 . . . 4 (da) ≤ (d5 a)
3328, 32le2an 169 . . 3 ((((ab) ∩ (bc)) ∩ (cd)) ∩ (da)) ≤ ((((a5 b) ∩ (b5 c)) ∩ (c5 d)) ∩ (d5 a))
3414, 33letr 137 . 2 (((ab) ∩ (bc)) ∩ (cd)) ≤ ((((a5 b) ∩ (b5 c)) ∩ (c5 d)) ∩ (d5 a))
359, 34lebi 145 1 ((((a5 b) ∩ (b5 c)) ∩ (c5 d)) ∩ (d5 a)) = (((ab) ∩ (bc)) ∩ (cd))
 Colors of variables: term Syntax hints:   = wb 1   ≡ tb 5   ∩ wa 7   →1 wi1 12   →2 wi2 13   →5 wi5 16 This theorem was proved from axioms:  ax-a1 30  ax-a2 31  ax-a3 32  ax-a4 33  ax-a5 34  ax-r1 35  ax-r2 36  ax-r4 37  ax-r5 38  ax-r3 439 This theorem depends on definitions:  df-b 39  df-a 40  df-t 41  df-f 42  df-i1 44  df-i2 45  df-i5 48  df-le1 130  df-le2 131  df-c1 132  df-c2 133 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator