QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  oago3.21x Unicode 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 ((((a ->5 b) ^ (b ->5 c)) ^ (c ->5 d)) ^ (d ->5 a)) = (((a == b) ^ (b == c)) ^ (c == d))
Proof of Theorem oago3.21x
StepHypRef Expression
1 i5lei1 347 . . . . . 6 (a ->5 b) =< (a ->1 b)
2 i5lei2 348 . . . . . 6 (b ->5 c) =< (b ->2 c)
31, 2le2an 169 . . . . 5 ((a ->5 b) ^ (b ->5 c)) =< ((a ->1 b) ^ (b ->2 c))
4 i5lei1 347 . . . . 5 (c ->5 d) =< (c ->1 d)
53, 4le2an 169 . . . 4 (((a ->5 b) ^ (b ->5 c)) ^ (c ->5 d)) =< (((a ->1 b) ^ (b ->2 c)) ^ (c ->1 d))
6 i5lei2 348 . . . 4 (d ->5 a) =< (d ->2 a)
75, 6le2an 169 . . 3 ((((a ->5 b) ^ (b ->5 c)) ^ (c ->5 d)) ^ (d ->5 a)) =< ((((a ->1 b) ^ (b ->2 c)) ^ (c ->1 d)) ^ (d ->2 a))
8 mhcor1 888 . . 3 ((((a ->1 b) ^ (b ->2 c)) ^ (c ->1 d)) ^ (d ->2 a)) = (((a == b) ^ (b == c)) ^ (c == d))
97, 8lbtr 139 . 2 ((((a ->5 b) ^ (b ->5 c)) ^ (c ->5 d)) ^ (d ->5 a)) =< (((a == b) ^ (b == c)) ^ (c == d))
10 leid 148 . . . 4 (((a == b) ^ (b == c)) ^ (c == d)) =< (((a == b) ^ (b == c)) ^ (c == d))
11 eqtr4 834 . . . . 5 (((a == b) ^ (b == c)) ^ (c == d)) =< (a == d)
12 bicom 96 . . . . 5 (a == d) = (d == a)
1311, 12lbtr 139 . . . 4 (((a == b) ^ (b == c)) ^ (c == d)) =< (d == a)
1410, 13ler2an 173 . . 3 (((a == b) ^ (b == c)) ^ (c == d)) =< ((((a == b) ^ (b == c)) ^ (c == d)) ^ (d == a))
15 u5lembi 725 . . . . . . . 8 ((a ->5 b) ^ (b ->5 a)) = (a == b)
1615ax-r1 35 . . . . . . 7 (a == b) = ((a ->5 b) ^ (b ->5 a))
17 lea 160 . . . . . . 7 ((a ->5 b) ^ (b ->5 a)) =< (a ->5 b)
1816, 17bltr 138 . . . . . 6 (a == b) =< (a ->5 b)
19 u5lembi 725 . . . . . . . 8 ((b ->5 c) ^ (c ->5 b)) = (b == c)
2019ax-r1 35 . . . . . . 7 (b == c) = ((b ->5 c) ^ (c ->5 b))
21 lea 160 . . . . . . 7 ((b ->5 c) ^ (c ->5 b)) =< (b ->5 c)
2220, 21bltr 138 . . . . . 6 (b == c) =< (b ->5 c)
2318, 22le2an 169 . . . . 5 ((a == b) ^ (b == c)) =< ((a ->5 b) ^ (b ->5 c))
24 u5lembi 725 . . . . . . 7 ((c ->5 d) ^ (d ->5 c)) = (c == d)
2524ax-r1 35 . . . . . 6 (c == d) = ((c ->5 d) ^ (d ->5 c))
26 lea 160 . . . . . 6 ((c ->5 d) ^ (d ->5 c)) =< (c ->5 d)
2725, 26bltr 138 . . . . 5 (c == d) =< (c ->5 d)
2823, 27le2an 169 . . . 4 (((a == b) ^ (b == c)) ^ (c == d)) =< (((a ->5 b) ^ (b ->5 c)) ^ (c ->5 d))
29 u5lembi 725 . . . . . 6 ((d ->5 a) ^ (a ->5 d)) = (d == a)
3029ax-r1 35 . . . . 5 (d == a) = ((d ->5 a) ^ (a ->5 d))
31 lea 160 . . . . 5 ((d ->5 a) ^ (a ->5 d)) =< (d ->5 a)
3230, 31bltr 138 . . . 4 (d == a) =< (d ->5 a)
3328, 32le2an 169 . . 3 ((((a == b) ^ (b == c)) ^ (c == d)) ^ (d == a)) =< ((((a ->5 b) ^ (b ->5 c)) ^ (c ->5 d)) ^ (d ->5 a))
3414, 33letr 137 . 2 (((a == b) ^ (b == c)) ^ (c == d)) =< ((((a ->5 b) ^ (b ->5 c)) ^ (c ->5 d)) ^ (d ->5 a))
359, 34lebi 145 1 ((((a ->5 b) ^ (b ->5 c)) ^ (c ->5 d)) ^ (d ->5 a)) = (((a == b) ^ (b == c)) ^ (c == d))
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