P. 5 of Theorem List - Quantum Logic Explorer

Theorem List for Quantum Logic Explorer - 401-500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	wbile 401	Biconditional to l.e. (Contributed by NM, 13-Oct-1997.)
(a ≡ b) = 1    ⇒   (a ≤2 b) = 1
Theorem	wlebi 402	L.e. to biconditional. (Contributed by NM, 13-Oct-1997.)
(a ≤2 b) = 1    &   (b ≤2 a) = 1    ⇒   (a ≡ b) = 1
Theorem	wle2or 403	Disjunction of 2 l.e.'s. (Contributed by NM, 13-Oct-1997.)
(a ≤2 b) = 1    &   (c ≤2 d) = 1    ⇒   ((a ∪ c) ≤2 (b ∪ d)) = 1
Theorem	wle2an 404	Conjunction of 2 l.e.'s. (Contributed by NM, 13-Oct-1997.)
(a ≤2 b) = 1    &   (c ≤2 d) = 1    ⇒   ((a ∩ c) ≤2 (b ∩ d)) = 1
Theorem	wledi 405	Half of distributive law. (Contributed by NM, 13-Oct-1997.)
(((a ∩ b) ∪ (a ∩ c)) ≤2 (a ∩ (b ∪ c))) = 1
Theorem	wledio 406	Half of distributive law. (Contributed by NM, 13-Oct-1997.)
((a ∪ (b ∩ c)) ≤2 ((a ∪ b) ∩ (a ∪ c))) = 1
Theorem	wcom0 407	Commutation with 0. Kalmbach 83 p. 20. (Contributed by NM, 13-Oct-1997.)
C (a, 0) = 1
Theorem	wcom1 408	Commutation with 1. Kalmbach 83 p. 20. (Contributed by NM, 13-Oct-1997.)
C (1, a) = 1
Theorem	wlecom 409	Comparable elements commute. Beran 84 2.3(iii) p. 40. (Contributed by NM, 13-Oct-1997.)
(a ≤2 b) = 1    ⇒    C (a, b) = 1
Theorem	wbctr 410	Transitive inference. (Contributed by NM, 13-Oct-1997.)
(a ≡ b) = 1    &    C (b, c) = 1    ⇒    C (a, c) = 1
Theorem	wcbtr 411	Transitive inference. (Contributed by NM, 13-Oct-1997.)
C (a, b) = 1    &   (b ≡ c) = 1    ⇒    C (a, c) = 1
Theorem	wcomorr 412	Weak commutation law. (Contributed by NM, 13-Oct-1997.)
C (a, (a ∪ b)) = 1
Theorem	wcoman1 413	Weak commutation law. (Contributed by NM, 13-Oct-1997.)
C ((a ∩ b), a) = 1
Theorem	wcomcom 414	Commutation is symmetric. Kalmbach 83 p. 22. (Contributed by NM, 13-Oct-1997.)
C (a, b) = 1    ⇒    C (b, a) = 1
Theorem	wcomcom2 415	Commutation equivalence. Kalmbach 83 p. 23. (Contributed by NM, 13-Oct-1997.)
C (a, b) = 1    ⇒    C (a, b⊥ ) = 1
Theorem	wcomcom3 416	Commutation equivalence. Kalmbach 83 p. 23. (Contributed by NM, 13-Oct-1997.)
C (a, b) = 1    ⇒    C (a⊥ , b) = 1
Theorem	wcomcom4 417	Commutation equivalence. Kalmbach 83 p. 23. (Contributed by NM, 13-Oct-1997.)
C (a, b) = 1    ⇒    C (a⊥ , b⊥ ) = 1
Theorem	wcomd 418	Commutation dual. Kalmbach 83 p. 23. (Contributed by NM, 13-Oct-1997.)
C (a, b) = 1    ⇒   (a ≡ ((a ∪ b) ∩ (a ∪ b⊥ ))) = 1
Theorem	wcom3ii 419	Lemma 3(ii) of Kalmbach 83 p. 23. (Contributed by NM, 13-Oct-1997.)
C (a, b) = 1    ⇒   ((a ∩ (a⊥ ∪ b)) ≡ (a ∩ b)) = 1
Theorem	wcomcom5 420	Commutation equivalence. Kalmbach 83 p. 23. (Contributed by NM, 13-Oct-1997.)
C (a⊥ , b⊥ ) = 1    ⇒    C (a, b) = 1
Theorem	wcomdr 421	Commutation dual. Kalmbach 83 p. 23. (Contributed by NM, 13-Oct-1997.)
(a ≡ ((a ∪ b) ∩ (a ∪ b⊥ ))) = 1    ⇒    C (a, b) = 1
Theorem	wcom3i 422	Lemma 3(i) of Kalmbach 83 p. 23. (Contributed by NM, 13-Oct-1997.)
((a ∩ (a⊥ ∪ b)) ≡ (a ∩ b)) = 1    ⇒    C (a, b) = 1
Theorem	wfh1 423	Weak structural analog of Foulis-Holland Theorem. (Contributed by NM, 13-Oct-1997.)
C (a, b) = 1    &    C (a, c) = 1    ⇒   ((a ∩ (b ∪ c)) ≡ ((a ∩ b) ∪ (a ∩ c))) = 1
Theorem	wfh2 424	Weak structural analog of Foulis-Holland Theorem. (Contributed by NM, 13-Oct-1997.)
C (a, b) = 1    &    C (a, c) = 1    ⇒   ((b ∩ (a ∪ c)) ≡ ((b ∩ a) ∪ (b ∩ c))) = 1
Theorem	wfh3 425	Weak structural analog of Foulis-Holland Theorem. (Contributed by NM, 13-Oct-1997.)
C (a, b) = 1    &    C (a, c) = 1    ⇒   ((a ∪ (b ∩ c)) ≡ ((a ∪ b) ∩ (a ∪ c))) = 1
Theorem	wfh4 426	Weak structural analog of Foulis-Holland Theorem. (Contributed by NM, 13-Oct-1997.)
C (a, b) = 1    &    C (a, c) = 1    ⇒   ((b ∪ (a ∩ c)) ≡ ((b ∪ a) ∩ (b ∪ c))) = 1
Theorem	wcom2or 427	Thm. 4.2 Beran p. 49. (Contributed by NM, 10-Nov-1998.)
C (a, b) = 1    &    C (a, c) = 1    ⇒    C (a, (b ∪ c)) = 1
Theorem	wcom2an 428	Thm. 4.2 Beran p. 49. (Contributed by NM, 10-Nov-1998.)
C (a, b) = 1    &    C (a, c) = 1    ⇒    C (a, (b ∩ c)) = 1
Theorem	wnbdi 429	Negated biconditional (distributive form). (Contributed by NM, 13-Oct-1997.)
((a ≡ b)⊥ ≡ (((a ∪ b) ∩ a⊥ ) ∪ ((a ∪ b) ∩ b⊥ ))) = 1
Theorem	wlem14 430	Lemma for KA14 soundness. (Contributed by NM, 25-Oct-1997.)
(((a ∩ b⊥ ) ∪ a⊥ )⊥ ∪ ((a ∩ b⊥ ) ∪ ((a⊥ ∩ ((a ∪ b⊥ ) ∩ (a ∪ b))) ∪ (a⊥ ∩ ((a ∪ b⊥ ) ∩ (a ∪ b))⊥ )))) = 1
Theorem	wr5 431	Proof of weak orthomodular law from weaker-looking equivalent, wom3 367, which in turn is derived from ax-wom 361. (Contributed by NM, 25-Oct-1997.)
(a ≡ b) = 1    ⇒   ((a ∪ c) ≡ (b ∪ c)) = 1
0.2.4  Kalmbach axioms (soundness proofs) that require WOML
Theorem	ska2 432	Soundness theorem for Kalmbach's quantum propositional logic axiom KA2. (Contributed by NM, 10-Nov-1998.)
((a ≡ b)⊥ ∪ ((b ≡ c)⊥ ∪ (a ≡ c))) = 1
Theorem	ska4 433	Soundness theorem for Kalmbach's quantum propositional logic axiom KA4. (Contributed by NM, 9-Nov-1998.)
((a ≡ b)⊥ ∪ ((a ∩ c) ≡ (b ∩ c))) = 1
Theorem	wom2 434	Weak orthomodular law for study of weakly orthomodular lattices. (Contributed by NM, 13-Nov-1998.)
a ≤ ((a ≡ b)⊥ ∪ ((a ∪ c) ≡ (b ∪ c)))
Theorem	ka4ot 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. (Contributed by NM, 25-Oct-1997.)
((a ≡ b)⊥ ∪ ((a ∪ c) ≡ (b ∪ c))) = 1
0.2.5  Weak orthomodular law variants
Theorem	woml6 436	Variant of weakly orthomodular law. (Contributed by NM, 14-Nov-1998.)
((a →1 b)⊥ ∪ (a →2 b)) = 1
Theorem	woml7 437	Variant of weakly orthomodular law. (Contributed by NM, 14-Nov-1998.)
(((a →2 b) ∩ (b →2 a))⊥ ∪ (a ≡ b)) = 1
Theorem	ortha 438	Property of orthogonality. (Contributed by NM, 10-Mar-2002.)
a ≤ b⊥    ⇒   (a ∩ b) = 0
0.3  Orthomodular lattices
0.3.1  Orthomodular law
Axiom	ax-r3 439	Orthomodular law - when added to an ortholattice, it makes the ortholattice an orthomodular lattice. See r3a 440 for a more compact version. (Contributed by NM, 12-Aug-1997.)
(c ∪ c⊥ ) = ((a⊥ ∪ b⊥ )⊥ ∪ (a ∪ b)⊥ )    ⇒   a = b
Theorem	r3a 440	Orthomodular law restated. (Contributed by NM, 12-Aug-1997.)
1 = (a ≡ b)    ⇒   a = b
Theorem	wed 441	Weak equivalential detachment (WBMP). (Contributed by NM, 10-Aug-1997.)
a = b    &   (a ≡ b) = (c ≡ d)    ⇒   c = d
Theorem	r3b 442	Orthomodular law from weak equivalential detachment (WBMP). (Contributed by NM, 10-Aug-1997.)
(c ∪ c⊥ ) = (a ≡ b)    ⇒   a = b
Theorem	lem3.1 443	Lemma used in proof of Thm. 3.1 of Pavicic 1993. (Contributed by NM, 12-Aug-1997.)
(a ∪ b) = b    &   (b⊥ ∪ a) = 1    ⇒   a = b
Theorem	lem3a.1 444	Lemma used in proof of Thm. 3.1 of Pavicic 1993. (Contributed by NM, 12-Aug-1997.)
(a ∪ b) = b    &   (b⊥ ∪ a) = 1    ⇒   (a ∪ b) = a
Theorem	oml 445	Orthomodular law. Compare Thm. 1 of Pavicic 1987. (Contributed by NM, 12-Aug-1997.)
(a ∪ (a⊥ ∩ (a ∪ b))) = (a ∪ b)
Theorem	omln 446	Orthomodular law. (Contributed by NM, 2-Nov-1997.)
(a⊥ ∪ (a ∩ (a⊥ ∪ b))) = (a⊥ ∪ b)
Theorem	omla 447	Orthomodular law. (Contributed by NM, 7-Nov-1997.)
(a ∩ (a⊥ ∪ (a ∩ b))) = (a ∩ b)
Theorem	omlan 448	Orthomodular law. (Contributed by NM, 7-Nov-1997.)
(a⊥ ∩ (a ∪ (a⊥ ∩ b))) = (a⊥ ∩ b)
Theorem	oml5 449	Orthomodular law. (Contributed by NM, 16-Nov-1997.)
((a ∩ b) ∪ ((a ∩ b)⊥ ∩ (b ∪ c))) = (b ∪ c)
Theorem	oml5a 450	Orthomodular law. (Contributed by NM, 16-Nov-1997.)
((a ∪ b) ∩ ((a ∪ b)⊥ ∪ (b ∩ c))) = (b ∩ c)
0.3.2  Relationship analogues using OML (ordering; commutation)
Theorem	oml2 451	Orthomodular law. Kalmbach 83 p. 22. (Contributed by NM, 27-Aug-1997.)
a ≤ b    ⇒   (a ∪ (a⊥ ∩ b)) = b
Theorem	oml3 452	Orthomodular law. Kalmbach 83 p. 22. (Contributed by NM, 27-Aug-1997.)
a ≤ b    &   (b ∩ a⊥ ) = 0    ⇒   a = b
Theorem	comcom 453	Commutation is symmetric. Kalmbach 83 p. 22. (Contributed by NM, 27-Aug-1997.)
a C b    ⇒   b C a
Theorem	comcom3 454	Commutation equivalence. Kalmbach 83 p. 23. (Contributed by NM, 27-Aug-1997.)
a C b    ⇒   a⊥ C b
Theorem	comcom4 455	Commutation equivalence. Kalmbach 83 p. 23. (Contributed by NM, 27-Aug-1997.)
a C b    ⇒   a⊥ C b⊥
Theorem	comd 456	Commutation dual. Kalmbach 83 p. 23. (Contributed by NM, 27-Aug-1997.)
a C b    ⇒   a = ((a ∪ b) ∩ (a ∪ b⊥ ))
Theorem	com3ii 457	Lemma 3(ii) of Kalmbach 83 p. 23. (Contributed by NM, 27-Aug-1997.)
a C b    ⇒   (a ∩ (a⊥ ∪ b)) = (a ∩ b)
Theorem	comcom5 458	Commutation equivalence. Kalmbach 83 p. 23. (Contributed by NM, 27-Aug-1997.)
a⊥ C b⊥    ⇒   a C b
Theorem	comcom6 459	Commutation equivalence. Kalmbach 83 p. 23. (Contributed by NM, 26-Nov-1997.)
a⊥ C b    ⇒   a C b
Theorem	comcom7 460	Commutation equivalence. Kalmbach 83 p. 23. (Contributed by NM, 26-Nov-1997.)
a C b⊥    ⇒   a C b
Theorem	comor1 461	Commutation law. (Contributed by NM, 9-Nov-1997.)
(a ∪ b) C a
Theorem	comor2 462	Commutation law. (Contributed by NM, 9-Nov-1997.)
(a ∪ b) C b
Theorem	comorr2 463	Commutation law. (Contributed by NM, 26-Nov-1997.)
b C (a ∪ b)
Theorem	comanr1 464	Commutation law. (Contributed by NM, 26-Nov-1997.)
a C (a ∩ b)
Theorem	comanr2 465	Commutation law. (Contributed by NM, 26-Nov-1997.)
b C (a ∩ b)
Theorem	comdr 466	Commutation dual. Kalmbach 83 p. 23. (Contributed by NM, 27-Aug-1997.)
a = ((a ∪ b) ∩ (a ∪ b⊥ ))    ⇒   a C b
Theorem	com3i 467	Lemma 3(i) of Kalmbach 83 p. 23. (Contributed by NM, 28-Aug-1997.)
(a ∩ (a⊥ ∪ b)) = (a ∩ b)    ⇒   a C b
Theorem	df2c1 468	Dual 'commutes' analogue for ≡ analogue of =. (Contributed by NM, 20-Sep-1998.)
a = ((a ∪ b) ∩ (a ∪ b⊥ ))    ⇒   a C b
Theorem	fh1 469	Foulis-Holland Theorem. (Contributed by NM, 29-Aug-1997.)
a C b    &   a C c    ⇒   (a ∩ (b ∪ c)) = ((a ∩ b) ∪ (a ∩ c))
Theorem	fh2 470	Foulis-Holland Theorem. (Contributed by NM, 29-Aug-1997.)
a C b    &   a C c    ⇒   (b ∩ (a ∪ c)) = ((b ∩ a) ∪ (b ∩ c))
Theorem	fh3 471	Foulis-Holland Theorem. (Contributed by NM, 29-Aug-1997.)
a C b    &   a C c    ⇒   (a ∪ (b ∩ c)) = ((a ∪ b) ∩ (a ∪ c))
Theorem	fh4 472	Foulis-Holland Theorem. (Contributed by NM, 29-Aug-1997.)
a C b    &   a C c    ⇒   (b ∪ (a ∩ c)) = ((b ∪ a) ∩ (b ∪ c))
Theorem	fh1r 473	Foulis-Holland Theorem. (Contributed by NM, 23-Nov-1997.)
a C b    &   a C c    ⇒   ((b ∪ c) ∩ a) = ((b ∩ a) ∪ (c ∩ a))
Theorem	fh2r 474	Foulis-Holland Theorem. (Contributed by NM, 23-Nov-1997.)
a C b    &   a C c    ⇒   ((a ∪ c) ∩ b) = ((a ∩ b) ∪ (c ∩ b))
Theorem	fh3r 475	Foulis-Holland Theorem. (Contributed by NM, 23-Nov-1997.)
a C b    &   a C c    ⇒   ((b ∩ c) ∪ a) = ((b ∪ a) ∩ (c ∪ a))
Theorem	fh4r 476	Foulis-Holland Theorem. (Contributed by NM, 23-Nov-1997.)
a C b    &   a C c    ⇒   ((a ∩ c) ∪ b) = ((a ∪ b) ∩ (c ∪ b))
Theorem	fh2c 477	Foulis-Holland Theorem. (Contributed by NM, 20-Sep-1998.)
a C b    &   a C c    ⇒   (b ∩ (c ∪ a)) = ((b ∩ c) ∪ (b ∩ a))
Theorem	fh4c 478	Foulis-Holland Theorem. (Contributed by NM, 20-Sep-1998.)
a C b    &   a C c    ⇒   (b ∪ (c ∩ a)) = ((b ∪ c) ∩ (b ∪ a))
Theorem	fh1rc 479	Foulis-Holland Theorem. (Contributed by NM, 10-Mar-2002.)
a C b    &   a C c    ⇒   ((c ∪ b) ∩ a) = ((c ∩ a) ∪ (b ∩ a))
Theorem	fh2rc 480	Foulis-Holland Theorem. (Contributed by NM, 20-Sep-1998.)
a C b    &   a C c    ⇒   ((c ∪ a) ∩ b) = ((c ∩ b) ∪ (a ∩ b))
Theorem	fh3rc 481	Foulis-Holland Theorem. (Contributed by NM, 6-Aug-2001.)
a C b    &   a C c    ⇒   ((c ∩ b) ∪ a) = ((c ∪ a) ∩ (b ∪ a))
Theorem	fh4rc 482	Foulis-Holland Theorem. (Contributed by NM, 20-Sep-1998.)
a C b    &   a C c    ⇒   ((c ∩ a) ∪ b) = ((c ∪ b) ∩ (a ∪ b))
Theorem	com2or 483	Thm. 4.2 Beran p. 49. (Contributed by NM, 7-Nov-1997.)
a C b    &   a C c    ⇒   a C (b ∪ c)
Theorem	com2an 484	Thm. 4.2 Beran p. 49. (Contributed by NM, 7-Nov-1997.)
a C b    &   a C c    ⇒   a C (b ∩ c)
Theorem	combi 485	Commutation theorem for Sasaki implication. (Contributed by NM, 25-Oct-1998.)
a C (a ≡ b)
Theorem	nbdi 486	Negated biconditional (distributive form). (Contributed by NM, 30-Aug-1997.)
(a ≡ b)⊥ = (((a ∪ b) ∩ a⊥ ) ∪ ((a ∪ b) ∩ b⊥ ))
Theorem	oml4 487	Orthomodular law. (Contributed by NM, 25-Oct-1997.)
((a ≡ b) ∩ a) ≤ b
Theorem	oml6 488	Orthomodular law. (Contributed by NM, 3-Jan-1999.)
(a ∪ (b ∩ (a⊥ ∪ b⊥ ))) = (a ∪ b)
Theorem	gsth 489	Gudder-Schelp's Theorem. Beran, p. 262, Thm. 4.1. (Contributed by NM, 20-Sep-1998.)
a C b    &   b C c    &   a C (b ∩ c)    ⇒   (a ∩ b) C c
Theorem	gsth2 490	Stronger version of Gudder-Schelp's Theorem. Beran, p. 263, Thm. 4.2. (Contributed by NM, 20-Sep-1998.)
b C c    &   a C (b ∩ c)    ⇒   (a ∩ b) C c
Theorem	gstho 491	"OR" version of Gudder-Schelp's Theorem. (Contributed by NM, 19-Oct-1998.)
b C c    &   a C (b ∪ c)    ⇒   (a ∪ b) C c
Theorem	gt1 492	Part of Lemma 1 from Gaisi Takeuti, "Quantum Set Theory". (Contributed by NM, 2-Dec-1998.)
a = (b ∪ c)    &   b ≤ d    &   c ≤ d⊥    ⇒   a C d
0.3.3  Commutator (orthomodular lattice theorems)
Theorem	cmtr1com 493	Commutator equal to 1 commutes. Theorem 2.11 of Beran, p. 86. (Contributed by NM, 24-Jan-1999.)
C (a, b) = 1    ⇒   a C b
Theorem	comcmtr1 494	Commutation implies commutator equal to 1. Theorem 2.11 of Beran, p. 86. (Contributed by NM, 24-Jan-1999.)
a C b    ⇒    C (a, b) = 1
Theorem	i0cmtrcom 495	Commutator element →0 commutator implies commutation. (Contributed by NM, 24-Jan-1999.)
(a →0 C (a, b)) = 1    ⇒   a C b
0.3.4  Kalmbach conditional
Theorem	i3bi 496	Kalmbach implication and biconditional. (Contributed by NM, 5-Nov-1997.)
((a →3 b) ∩ (b →3 a)) = (a ≡ b)
Theorem	i3or 497	Kalmbach implication OR builder. (Contributed by NM, 26-Dec-1997.)
((a ≡ b)⊥ ∪ ((a ∪ c) →3 (b ∪ c))) = 1
Theorem	df2i3 498	Alternate definition for Kalmbach implication. (Contributed by NM, 7-Nov-1997.)
(a →3 b) = ((a⊥ ∩ b⊥ ) ∪ ((a⊥ ∪ b) ∩ (a ∪ (a⊥ ∩ b))))
Theorem	dfi3b 499	Alternate Kalmbach conditional. (Contributed by NM, 6-Aug-2001.)
(a →3 b) = ((a⊥ ∪ b) ∩ ((a ∪ (a⊥ ∩ b⊥ )) ∪ (a⊥ ∩ b)))
Theorem	dfi4b 500	Alternate non-tollens conditional. (Contributed by NM, 6-Aug-2001.)
(a →4 b) = ((a⊥ ∪ b) ∩ ((b⊥ ∪ (b ∩ a⊥ )) ∪ (b ∩ a)))