[Lattice L46-7]Home PageHome Quantum Logic Explorer
Theorem List (p. 5 of 13)
< Previous  Next >
Browser slow? Try the
Unicode version.

Mirrors  >  Metamath Home Page  >  QLE Home Page  >  Theorem List Contents       This page: Page List

Theorem List for Quantum Logic Explorer - 401-500   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremwbile 401 Biconditional to l.e.
(a == b) = 1   =>   (a =<2 b) = 1
 
Theoremwlebi 402 L.e. to biconditional.
(a =<2 b) = 1   &   (b =<2 a) = 1   =>   (a == b) = 1
 
Theoremwle2or 403 Disjunction of 2 l.e.'s.
(a =<2 b) = 1   &   (c =<2 d) = 1   =>   ((a v c) =<2 (b v d)) = 1
 
Theoremwle2an 404 Conjunction of 2 l.e.'s.
(a =<2 b) = 1   &   (c =<2 d) = 1   =>   ((a ^ c) =<2 (b ^ d)) = 1
 
Theoremwledi 405 Half of distributive law.
(((a ^ b) v (a ^ c)) =<2 (a ^ (b v c))) = 1
 
Theoremwledio 406 Half of distributive law.
((a v (b ^ c)) =<2 ((a v b) ^ (a v c))) = 1
 
Theoremwcom0 407 Commutation with 0. Kalmbach 83 p. 20.
C (a, 0) = 1
 
Theoremwcom1 408 Commutation with 1. Kalmbach 83 p. 20.
C (1, a) = 1
 
Theoremwlecom 409 Comparable elements commute. Beran 84 2.3(iii) p. 40.
(a =<2 b) = 1   =>   C (a, b) = 1
 
Theoremwbctr 410 Transitive inference.
(a == b) = 1   &   C (b, c) = 1   =>   C (a, c) = 1
 
Theoremwcbtr 411 Transitive inference.
C (a, b) = 1   &   (b == c) = 1   =>   C (a, c) = 1
 
Theoremwcomorr 412 Weak commutation law.
C (a, (a v b)) = 1
 
Theoremwcoman1 413 Weak commutation law.
C ((a ^ b), a) = 1
 
Theoremwcomcom 414 Commutation is symmetric. Kalmbach 83 p. 22.
C (a, b) = 1   =>   C (b, a) = 1
 
Theoremwcomcom2 415 Commutation equivalence. Kalmbach 83 p. 23.
C (a, b) = 1   =>   C (a, b') = 1
 
Theoremwcomcom3 416 Commutation equivalence. Kalmbach 83 p. 23.
C (a, b) = 1   =>   C (a', b) = 1
 
Theoremwcomcom4 417 Commutation equivalence. Kalmbach 83 p. 23.
C (a, b) = 1   =>   C (a', b') = 1
 
Theoremwcomd 418 Commutation dual. Kalmbach 83 p. 23.
C (a, b) = 1   =>   (a == ((a v b) ^ (a v b'))) = 1
 
Theoremwcom3ii 419 Lemma 3(ii) of Kalmbach 83 p. 23.
C (a, b) = 1   =>   ((a ^ (a' v b)) == (a ^ b)) = 1
 
Theoremwcomcom5 420 Commutation equivalence. Kalmbach 83 p. 23.
C (a', b') = 1   =>   C (a, b) = 1
 
Theoremwcomdr 421 Commutation dual. Kalmbach 83 p. 23.
(a == ((a v b) ^ (a v b'))) = 1   =>   C (a, b) = 1
 
Theoremwcom3i 422 Lemma 3(i) of Kalmbach 83 p. 23.
((a ^ (a' v b)) == (a ^ b)) = 1   =>   C (a, b) = 1
 
Theoremwfh1 423 Weak structural analog of Foulis-Holland Theorem.
C (a, b) = 1   &   C (a, c) = 1   =>   ((a ^ (b v c)) == ((a ^ b) v (a ^ c))) = 1
 
Theoremwfh2 424 Weak structural analog of Foulis-Holland Theorem.
C (a, b) = 1   &   C (a, c) = 1   =>   ((b ^ (a v c)) == ((b ^ a) v (b ^ c))) = 1
 
Theoremwfh3 425 Weak structural analog of Foulis-Holland Theorem.
C (a, b) = 1   &   C (a, c) = 1   =>   ((a v (b ^ c)) == ((a v b) ^ (a v c))) = 1
 
Theoremwfh4 426 Weak structural analog of Foulis-Holland Theorem.
C (a, b) = 1   &   C (a, c) = 1   =>   ((b v (a ^ c)) == ((b v a) ^ (b v c))) = 1
 
Theoremwcom2or 427 Th. 4.2 Beran p. 49.
C (a, b) = 1   &   C (a, c) = 1   =>   C (a, (b v c)) = 1
 
Theoremwcom2an 428 Th. 4.2 Beran p. 49.
C (a, b) = 1   &   C (a, c) = 1   =>   C (a, (b ^ c)) = 1
 
Theoremwnbdi 429 Negated biconditional (distributive form)
((a == b)' == (((a v b) ^ a') v ((a v b) ^ b'))) = 1
 
Theoremwlem14 430 Lemma for KA14 soundness.
(((a ^ b') v a')' v ((a ^ b') v ((a' ^ ((a v b') ^ (a v b))) v (a' ^ ((a v b') ^ (a v b))')))) = 1
 
Theoremwr5 431 Proof of weak orthomodular law from weaker-looking equivalent, wom3 367, which in turn is derived from ax-wom 361.
(a == b) = 1   =>   ((a v c) == (b v c)) = 1
 
0.2.4  Kalmbach axioms (soundness proofs) that require WOML
 
Theoremska2 432 Soundness theorem for Kalmbach's quantum propositional logic axiom KA2.
((a == b)' v ((b == c)' v (a == c))) = 1
 
Theoremska4 433 Soundness theorem for Kalmbach's quantum propositional logic axiom KA4.
((a == b)' v ((a ^ c) == (b ^ c))) = 1
 
Theoremwom2 434 Weak orthomodular law for study of weakly orthomodular lattices.
a =< ((a == b)' v ((a v c) == (b v c)))
 
Theoremka4ot 435 3-variable version of weakly orthomodular law. It is proved from a weaker-looking equivalent, wom2 434, which in turn is proved from ax-wom 361.
((a == b)' v ((a v c) == (b v c))) = 1
 
0.2.5  Weak orthomodular law variants
 
Theoremwoml6 436 Variant of weakly orthomodular law.
((a ->1 b)' v (a ->2 b)) = 1
 
Theoremwoml7 437 Variant of weakly orthomodular law.
(((a ->2 b) ^ (b ->2 a))' v (a == b)) = 1
 
Theoremortha 438 Property of orthogonality.
a =< b'   =>   (a ^ b) = 0
 
0.3  Orthomodular lattices
 
0.3.1  Orthomodular law
 
Axiomax-r3 439 Orthomodular law - when added to an ortholattice, it makes the ortholattice an orthomodular lattice. See r3a 440 for a more compact version.
(c v c') = ((a' v b')' v (a v b)')   =>   a = b
 
Theoremr3a 440 Orthomodular law restated.
1 = (a == b)   =>   a = b
 
Theoremwed 441 Weak equivalential detachment (WBMP).
a = b   &   (a == b) = (c == d)   =>   c = d
 
Theoremr3b 442 Orthomodular law from weak equivalential detachment (WBMP).
(c v c') = (a == b)   =>   a = b
 
Theoremlem3.1 443 Lemma used in proof of Th. 3.1 of Pavicic 1993.
(a v b) = b   &   (b' v a) = 1   =>   a = b
 
Theoremlem3a.1 444 Lemma used in proof of Th. 3.1 of Pavicic 1993.
(a v b) = b   &   (b' v a) = 1   =>   (a v b) = a
 
Theoremoml 445 Orthomodular law. Compare Th. 1 of Pavicic 1987.
(a v (a' ^ (a v b))) = (a v b)
 
Theoremomln 446 Orthomodular law.
(a' v (a ^ (a' v b))) = (a' v b)
 
Theoremomla 447 Orthomodular law.
(a ^ (a' v (a ^ b))) = (a ^ b)
 
Theoremomlan 448 Orthomodular law.
(a' ^ (a v (a' ^ b))) = (a' ^ b)
 
Theoremoml5 449 Orthomodular law.
((a ^ b) v ((a ^ b)' ^ (b v c))) = (b v c)
 
Theoremoml5a 450 Orthomodular law.
((a v b) ^ ((a v b)' v (b ^ c))) = (b ^ c)
 
0.3.2  Relationship analogues using OML (ordering; commutation)
 
Theoremoml2 451 Orthomodular law. Kalmbach 83 p. 22.
a =< b   =>   (a v (a' ^ b)) = b
 
Theoremoml3 452 Orthomodular law. Kalmbach 83 p. 22.
a =< b   &   (b ^ a') = 0   =>   a = b
 
Theoremcomcom 453 Commutation is symmetric. Kalmbach 83 p. 22.
a C b   =>   b C a
 
Theoremcomcom3 454 Commutation equivalence. Kalmbach 83 p. 23.
a C b   =>   a' C b
 
Theoremcomcom4 455 Commutation equivalence. Kalmbach 83 p. 23.
a C b   =>   a' C b'
 
Theoremcomd 456 Commutation dual. Kalmbach 83 p. 23.
a C b   =>   a = ((a v b) ^ (a v b'))
 
Theoremcom3ii 457 Lemma 3(ii) of Kalmbach 83 p. 23.
a C b   =>   (a ^ (a' v b)) = (a ^ b)
 
Theoremcomcom5 458 Commutation equivalence. Kalmbach 83 p. 23.
a' C b'   =>   a C b
 
Theoremcomcom6 459 Commutation equivalence. Kalmbach 83 p. 23.
a' C b   =>   a C b
 
Theoremcomcom7 460 Commutation equivalence. Kalmbach 83 p. 23.
a C b'   =>   a C b
 
Theoremcomor1 461 Commutation law.
(a v b) C a
 
Theoremcomor2 462 Commutation law.
(a v b) C b
 
Theoremcomorr2 463 Commutation law.
b C (a v b)
 
Theoremcomanr1 464 Commutation law.
a C (a ^ b)
 
Theoremcomanr2 465 Commutation law.
b C (a ^ b)
 
Theoremcomdr 466 Commutation dual. Kalmbach 83 p. 23.
a = ((a v b) ^ (a v b'))   =>   a C b
 
Theoremcom3i 467 Lemma 3(i) of Kalmbach 83 p. 23.
(a ^ (a' v b)) = (a ^ b)   =>   a C b
 
Theoremdf2c1 468 Dual 'commutes' analogue for == analogue of =.
a = ((a v b) ^ (a v b'))   =>   a C b
 
Theoremfh1 469 Foulis-Holland Theorem.
a C b   &   a C c   =>   (a ^ (b v c)) = ((a ^ b) v (a ^ c))
 
Theoremfh2 470 Foulis-Holland Theorem.
a C b   &   a C c   =>   (b ^ (a v c)) = ((b ^ a) v (b ^ c))
 
Theoremfh3 471 Foulis-Holland Theorem.
a C b   &   a C c   =>   (a v (b ^ c)) = ((a v b) ^ (a v c))
 
Theoremfh4 472 Foulis-Holland Theorem.
a C b   &   a C c   =>   (b v (a ^ c)) = ((b v a) ^ (b v c))
 
Theoremfh1r 473 Foulis-Holland Theorem.
a C b   &   a C c   =>   ((b v c) ^ a) = ((b ^ a) v (c ^ a))
 
Theoremfh2r 474 Foulis-Holland Theorem.
a C b   &   a C c   =>   ((a v c) ^ b) = ((a ^ b) v (c ^ b))
 
Theoremfh3r 475 Foulis-Holland Theorem.
a C b   &   a C c   =>   ((b ^ c) v a) = ((b v a) ^ (c v a))
 
Theoremfh4r 476 Foulis-Holland Theorem.
a C b   &   a C c   =>   ((a ^ c) v b) = ((a v b) ^ (c v b))
 
Theoremfh2c 477 Foulis-Holland Theorem.
a C b   &   a C c   =>   (b ^ (c v a)) = ((b ^ c) v (b ^ a))
 
Theoremfh4c 478 Foulis-Holland Theorem.
a C b   &   a C c   =>   (b v (c ^ a)) = ((b v c) ^ (b v a))
 
Theoremfh1rc 479 Foulis-Holland Theorem.
a C b   &   a C c   =>   ((c v b) ^ a) = ((c ^ a) v (b ^ a))
 
Theoremfh2rc 480 Foulis-Holland Theorem.
a C b   &   a C c   =>   ((c v a) ^ b) = ((c ^ b) v (a ^ b))
 
Theoremfh3rc 481 Foulis-Holland Theorem.
a C b   &   a C c   =>   ((c ^ b) v a) = ((c v a) ^ (b v a))
 
Theoremfh4rc 482 Foulis-Holland Theorem.
a C b   &   a C c   =>   ((c ^ a) v b) = ((c v b) ^ (a v b))
 
Theoremcom2or 483 Th. 4.2 Beran p. 49.
a C b   &   a C c   =>   a C (b v c)
 
Theoremcom2an 484 Th. 4.2 Beran p. 49.
a C b   &   a C c   =>   a C (b ^ c)
 
Theoremcombi 485 Commutation theorem for Sasaki implication.
a C (a == b)
 
Theoremnbdi 486 Negated biconditional (distributive form)
(a == b)' = (((a v b) ^ a') v ((a v b) ^ b'))
 
Theoremoml4 487 Orthomodular law.
((a == b) ^ a) =< b
 
Theoremoml6 488 Orthomodular law.
(a v (b ^ (a' v b'))) = (a v b)
 
Theoremgsth 489 Gudder-Schelp's Theorem. Beran, p. 262, Th. 4.1.
a C b   &   b C c   &   a C (b ^ c)   =>   (a ^ b) C c
 
Theoremgsth2 490 Stronger version of Gudder-Schelp's Theorem. Beran, p. 263, Th. 4.2.
b C c   &   a C (b ^ c)   =>   (a ^ b) C c
 
Theoremgstho 491 "OR" version of Gudder-Schelp's Theorem.
b C c   &   a C (b v c)   =>   (a v b) C c
 
Theoremgt1 492 Part of Lemma 1 from Gaisi Takeuti, "Quantum Set Theory".
a = (b v c)   &   b =< d   &   c =< d'   =>   a C d
 
0.3.3  Commutator (orthomodular lattice theorems)
 
Theoremcmtr1com 493 Commutator equal to 1 commutes. Theorem 2.11 of Beran, p. 86.
C (a, b) = 1   =>   a C b
 
Theoremcomcmtr1 494 Commutation implies commutator equal to 1. Theorem 2.11 of Beran, p. 86.
a C b   =>   C (a, b) = 1
 
Theoremi0cmtrcom 495 Commutator element ->0 commutator implies commutation.
(a ->0 C (a, b)) = 1   =>   a C b
 
0.3.4  Kalmbach conditional
 
Theoremi3bi 496 Kalmbach implication and biconditional.
((a ->3 b) ^ (b ->3 a)) = (a == b)
 
Theoremi3or 497 Kalmbach implication OR builder.
((a == b)' v ((a v c) ->3 (b v c))) = 1
 
Theoremdf2i3 498 Alternate definition for Kalmbach implication.
(a ->3 b) = ((a' ^ b') v ((a' v b) ^ (a v (a' ^ b))))
 
Theoremdfi3b 499 Alternate Kalmbach conditional.
(a ->3 b) = ((a' v b) ^ ((a v (a' ^ b')) v (a' ^ b)))
 
Theoremdfi4b 500 Alternate non-tollens conditional.
(a ->4 b) = ((a' v b) ^ ((b' v (b ^ a')) v (b ^ a)))
    < Previous  Next >

Page List
Jump to page: Contents  1 1-100 2 101-200 3 201-300 4 301-400401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1215
  Copyright terms: Public domain < Previous  Next >