P. 4 of Theorem List - Quantum Logic Explorer

Theorem List for Quantum Logic Explorer - 301-400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	nomcon0 301	Lemma for "Non-Orthomodular Models..." paper. (Contributed by NM, 7-Feb-1999.)
(a ≡0 b) = (b⊥ ≡0 a⊥ )
Theorem	nomcon1 302	Lemma for "Non-Orthomodular Models..." paper. (Contributed by NM, 7-Feb-1999.)
(a ≡1 b) = (b⊥ ≡2 a⊥ )
Theorem	nomcon2 303	Lemma for "Non-Orthomodular Models..." paper. (Contributed by NM, 7-Feb-1999.)
(a ≡2 b) = (b⊥ ≡1 a⊥ )
Theorem	nomcon3 304	Lemma for "Non-Orthomodular Models..." paper. (Contributed by NM, 7-Feb-1999.)
(a ≡3 b) = (b⊥ ≡4 a⊥ )
Theorem	nomcon4 305	Lemma for "Non-Orthomodular Models..." paper. (Contributed by NM, 7-Feb-1999.)
(a ≡4 b) = (b⊥ ≡3 a⊥ )
Theorem	nomcon5 306	Lemma for "Non-Orthomodular Models..." paper. (Contributed by NM, 7-Feb-1999.)
(a ≡ b) = (b⊥ ≡ a⊥ )
Theorem	nom10 307	Part of Lemma 3.3(14) from "Non-Orthomodular Models..." paper. (Contributed by NM, 7-Feb-1999.)
(a →0 (a ∩ b)) = (a →1 b)
Theorem	nom11 308	Part of Lemma 3.3(14) from "Non-Orthomodular Models..." paper. (Contributed by NM, 7-Feb-1999.)
(a →1 (a ∩ b)) = (a →1 b)
Theorem	nom12 309	Part of Lemma 3.3(14) from "Non-Orthomodular Models..." paper. (Contributed by NM, 7-Feb-1999.)
(a →2 (a ∩ b)) = (a →1 b)
Theorem	nom13 310	Part of Lemma 3.3(14) from "Non-Orthomodular Models..." paper. (Contributed by NM, 7-Feb-1999.)
(a →3 (a ∩ b)) = (a →1 b)
Theorem	nom14 311	Part of Lemma 3.3(14) from "Non-Orthomodular Models..." paper. (Contributed by NM, 7-Feb-1999.)
(a →4 (a ∩ b)) = (a →1 b)
Theorem	nom15 312	Part of Lemma 3.3(14) from "Non-Orthomodular Models..." paper. (Contributed by NM, 7-Feb-1999.)
(a →5 (a ∩ b)) = (a →1 b)
Theorem	nom20 313	Part of Lemma 3.3(14) from "Non-Orthomodular Models..." paper. (Contributed by NM, 7-Feb-1999.)
(a ≡0 (a ∩ b)) = (a →1 b)
Theorem	nom21 314	Part of Lemma 3.3(14) from "Non-Orthomodular Models..." paper. (Contributed by NM, 7-Feb-1999.)
(a ≡1 (a ∩ b)) = (a →1 b)
Theorem	nom22 315	Part of Lemma 3.3(14) from "Non-Orthomodular Models..." paper. (Contributed by NM, 7-Feb-1999.)
(a ≡2 (a ∩ b)) = (a →1 b)
Theorem	nom23 316	Part of Lemma 3.3(14) from "Non-Orthomodular Models..." paper. (Contributed by NM, 7-Feb-1999.)
(a ≡3 (a ∩ b)) = (a →1 b)
Theorem	nom24 317	Part of Lemma 3.3(14) from "Non-Orthomodular Models..." paper. (Contributed by NM, 7-Feb-1999.)
(a ≡4 (a ∩ b)) = (a →1 b)
Theorem	nom25 318	Part of Lemma 3.3(14) from "Non-Orthomodular Models..." paper. (Contributed by NM, 7-Feb-1999.)
(a ≡ (a ∩ b)) = (a →1 b)
Theorem	nom30 319	Part of Lemma 3.3(14) from "Non-Orthomodular Models..." paper. (Contributed by NM, 7-Feb-1999.)
((a ∩ b) ≡0 a) = (a →1 b)
Theorem	nom31 320	Part of Lemma 3.3(14) from "Non-Orthomodular Models..." paper. (Contributed by NM, 7-Feb-1999.)
((a ∩ b) ≡1 a) = (a →1 b)
Theorem	nom32 321	Part of Lemma 3.3(14) from "Non-Orthomodular Models..." paper. (Contributed by NM, 7-Feb-1999.)
((a ∩ b) ≡2 a) = (a →1 b)
Theorem	nom33 322	Part of Lemma 3.3(14) from "Non-Orthomodular Models..." paper. (Contributed by NM, 7-Feb-1999.)
((a ∩ b) ≡3 a) = (a →1 b)
Theorem	nom34 323	Part of Lemma 3.3(14) from "Non-Orthomodular Models..." paper. (Contributed by NM, 7-Feb-1999.)
((a ∩ b) ≡4 a) = (a →1 b)
Theorem	nom35 324	Part of Lemma 3.3(14) from "Non-Orthomodular Models..." paper. (Contributed by NM, 7-Feb-1999.)
((a ∩ b) ≡ a) = (a →1 b)
Theorem	nom40 325	Part of Lemma 3.3(15) from "Non-Orthomodular Models..." paper. (Contributed by NM, 7-Feb-1999.)
((a ∪ b) →0 b) = (a →2 b)
Theorem	nom41 326	Part of Lemma 3.3(15) from "Non-Orthomodular Models..." paper. (Contributed by NM, 7-Feb-1999.)
((a ∪ b) →1 b) = (a →2 b)
Theorem	nom42 327	Part of Lemma 3.3(15) from "Non-Orthomodular Models..." paper. (Contributed by NM, 7-Feb-1999.)
((a ∪ b) →2 b) = (a →2 b)
Theorem	nom43 328	Part of Lemma 3.3(15) from "Non-Orthomodular Models..." paper. (Contributed by NM, 7-Feb-1999.)
((a ∪ b) →3 b) = (a →2 b)
Theorem	nom44 329	Part of Lemma 3.3(15) from "Non-Orthomodular Models..." paper. (Contributed by NM, 7-Feb-1999.)
((a ∪ b) →4 b) = (a →2 b)
Theorem	nom45 330	Part of Lemma 3.3(15) from "Non-Orthomodular Models..." paper. (Contributed by NM, 7-Feb-1999.)
((a ∪ b) →5 b) = (a →2 b)
Theorem	nom50 331	Part of Lemma 3.3(15) from "Non-Orthomodular Models..." paper. (Contributed by NM, 7-Feb-1999.)
((a ∪ b) ≡0 b) = (a →2 b)
Theorem	nom51 332	Part of Lemma 3.3(15) from "Non-Orthomodular Models..." paper. (Contributed by NM, 7-Feb-1999.)
((a ∪ b) ≡1 b) = (a →2 b)
Theorem	nom52 333	Part of Lemma 3.3(15) from "Non-Orthomodular Models..." paper. (Contributed by NM, 7-Feb-1999.)
((a ∪ b) ≡2 b) = (a →2 b)
Theorem	nom53 334	Part of Lemma 3.3(15) from "Non-Orthomodular Models..." paper. (Contributed by NM, 7-Feb-1999.)
((a ∪ b) ≡3 b) = (a →2 b)
Theorem	nom54 335	Part of Lemma 3.3(15) from "Non-Orthomodular Models..." paper. (Contributed by NM, 7-Feb-1999.)
((a ∪ b) ≡4 b) = (a →2 b)
Theorem	nom55 336	Part of Lemma 3.3(15) from "Non-Orthomodular Models..." paper. (Contributed by NM, 7-Feb-1999.)
((a ∪ b) ≡ b) = (a →2 b)
Theorem	nom60 337	Part of Lemma 3.3(15) from "Non-Orthomodular Models..." paper. (Contributed by NM, 7-Feb-1999.)
(b ≡0 (a ∪ b)) = (a →2 b)
Theorem	nom61 338	Part of Lemma 3.3(15) from "Non-Orthomodular Models..." paper. (Contributed by NM, 7-Feb-1999.)
(b ≡1 (a ∪ b)) = (a →2 b)
Theorem	nom62 339	Part of Lemma 3.3(15) from "Non-Orthomodular Models..." paper. (Contributed by NM, 7-Feb-1999.)
(b ≡2 (a ∪ b)) = (a →2 b)
Theorem	nom63 340	Part of Lemma 3.3(15) from "Non-Orthomodular Models..." paper. (Contributed by NM, 7-Feb-1999.)
(b ≡3 (a ∪ b)) = (a →2 b)
Theorem	nom64 341	Part of Lemma 3.3(15) from "Non-Orthomodular Models..." paper. (Contributed by NM, 7-Feb-1999.)
(b ≡4 (a ∪ b)) = (a →2 b)
Theorem	nom65 342	Part of Lemma 3.3(15) from "Non-Orthomodular Models..." paper. (Contributed by NM, 7-Feb-1999.)
(b ≡ (a ∪ b)) = (a →2 b)
Theorem	go1 343	Lemma for proof of Mayet 8-variable "full" equation from 4-variable Godowski equation. (Contributed by NM, 19-Nov-1999.)
((a ∩ b) ∩ (a →1 b⊥ )) = 0
Theorem	i2or 344	Lemma for disjunction of →2 . (Contributed by NM, 5-Jul-2000.)
((a →2 c) ∪ (b →2 c)) ≤ ((a ∩ b) →2 c)
Theorem	i1or 345	Lemma for disjunction of →1 . (Contributed by NM, 5-Jul-2000.)
((c →1 a) ∪ (c →1 b)) ≤ (c →1 (a ∪ b))
Theorem	lei2 346	"Less than" analogue is equal to →2 implication. (Contributed by NM, 28-Jan-2002.)
(a ≤2 b) = (a →2 b)
Theorem	i5lei1 347	Relevance implication is less than or equal to Sasaki implication. (Contributed by NM, 26-Jun-2003.)
(a →5 b) ≤ (a →1 b)
Theorem	i5lei2 348	Relevance implication is less than or equal to Dishkant implication. (Contributed by NM, 26-Jun-2003.)
(a →5 b) ≤ (a →2 b)
Theorem	i5lei3 349	Relevance implication is less than or equal to Kalmbach implication. (Contributed by NM, 26-Jun-2003.)
(a →5 b) ≤ (a →3 b)
Theorem	i5lei4 350	Relevance implication is less than or equal to non-tollens implication. (Contributed by NM, 26-Jun-2003.)
(a →5 b) ≤ (a →4 b)
Theorem	id5leid0 351	Quantum identity is less than classical identity. (Contributed by NM, 4-Mar-2006.)
(a ≡ b) ≤ (a ≡0 b)
Theorem	id5id0 352	Show that classical identity follows from quantum identity in OL. (Contributed by NM, 4-Mar-2006.)
(a ≡ b) = 1    ⇒   (a ≡0 b) = 1
Theorem	k1-6 353	Statement (6) in proof of Theorem 1 of Kalmbach, Orthomodular Lattices, p. 21. (Contributed by NM, 26-May-2008.)
x = ((x ∩ c) ∪ (x ∩ c⊥ ))    ⇒   (x⊥ ∩ c) = ((x⊥ ∪ c⊥ ) ∩ c)
Theorem	k1-7 354	Statement (7) in proof of Theorem 1 of Kalmbach, Orthomodular Lattices, p. 21. (Contributed by NM, 26-May-2008.)
x = ((x ∩ c) ∪ (x ∩ c⊥ ))    ⇒   (x⊥ ∩ c⊥ ) = ((x⊥ ∪ c) ∩ c⊥ )
Theorem	k1-8a 355	First part of statement (8) in proof of Theorem 1 of Kalmbach, Orthomodular Lattices, p. 21. (Contributed by NM, 27-May-2008.)
x⊥ = ((x⊥ ∩ c) ∪ (x⊥ ∩ c⊥ ))    &   x ≤ c    &   y ≤ c⊥    ⇒   x = ((x ∪ y) ∩ c)
Theorem	k1-8b 356	Second part of statement (8) in proof of Theorem 1 of Kalmbach, Orthomodular Lattices, p. 21. (Contributed by NM, 27-May-2008.)
y⊥ = ((y⊥ ∩ c) ∪ (y⊥ ∩ c⊥ ))    &   x ≤ c    &   y ≤ c⊥    ⇒   y = ((x ∪ y) ∩ c⊥ )
Theorem	k1-2 357	Statement (2) in proof of Theorem 1 of Kalmbach, Orthomodular Lattices, p. 21. (Contributed by NM, 27-May-2008.)
x = ((x ∩ c) ∪ (x ∩ c⊥ ))    &   y = ((y ∩ c) ∪ (y ∩ c⊥ ))    &   ((x ∩ c) ∪ (y ∩ c))⊥ = ((((x ∩ c) ∪ (y ∩ c))⊥ ∩ c) ∪ (((x ∩ c) ∪ (y ∩ c))⊥ ∩ c⊥ ))    ⇒   ((x ∪ y) ∩ c) = ((x ∩ c) ∪ (y ∩ c))
Theorem	k1-3 358	Statement (3) in proof of Theorem 1 of Kalmbach, Orthomodular Lattices, p. 21. (Contributed by NM, 27-May-2008.)
x = ((x ∩ c) ∪ (x ∩ c⊥ ))    &   y = ((y ∩ c) ∪ (y ∩ c⊥ ))    &   ((x ∩ c⊥ ) ∪ (y ∩ c⊥ ))⊥ = ((((x ∩ c⊥ ) ∪ (y ∩ c⊥ ))⊥ ∩ c) ∪ (((x ∩ c⊥ ) ∪ (y ∩ c⊥ ))⊥ ∩ c⊥ ))    ⇒   ((x ∪ y) ∩ c⊥ ) = ((x ∩ c⊥ ) ∪ (y ∩ c⊥ ))
Theorem	k1-4 359	Statement (4) in proof of Theorem 1 of Kalmbach, Orthomodular Lattices, p. 21. (Contributed by NM, 27-May-2008.)
(x⊥ ∩ (x ∪ c⊥ )) = (((x⊥ ∩ (x ∪ c⊥ )) ∩ c) ∪ ((x⊥ ∩ (x ∪ c⊥ )) ∩ c⊥ ))    &   x ≤ c    ⇒   (x ∪ (x⊥ ∩ c)) = c
Theorem	k1-5 360	Statement (5) in proof of Theorem 1 of Kalmbach, Orthomodular Lattices, p. 21. (Contributed by NM, 27-May-2008.)
(x⊥ ∩ (x ∪ c)) = (((x⊥ ∩ (x ∪ c)) ∩ c) ∪ ((x⊥ ∩ (x ∪ c)) ∩ c⊥ ))    &   x ≤ c⊥    ⇒   (x ∪ (x⊥ ∩ c⊥ )) = c⊥
0.2  Weakly orthomodular lattices
0.2.1  Weak orthomodular law
Axiom	ax-wom 361	2-variable WOML rule. (Contributed by NM, 13-Nov-1998.)
(a⊥ ∪ (a ∩ b)) = 1    ⇒   (b ∪ (a⊥ ∩ b⊥ )) = 1
Theorem	2vwomr2 362	2-variable WOML rule. (Contributed by NM, 13-Nov-1998.)
(b ∪ (a⊥ ∩ b⊥ )) = 1    ⇒   (a⊥ ∪ (a ∩ b)) = 1
Theorem	2vwomr1a 363	2-variable WOML rule. (Contributed by NM, 13-Nov-1998.)
(a →1 b) = 1    ⇒   (a →2 b) = 1
Theorem	2vwomr2a 364	2-variable WOML rule. (Contributed by NM, 13-Nov-1998.)
(a →2 b) = 1    ⇒   (a →1 b) = 1
Theorem	2vwomlem 365	Lemma from 2-variable WOML rule. (Contributed by NM, 13-Nov-1998.)
(a →2 b) = 1    &   (b →2 a) = 1    ⇒   (a ≡ b) = 1
Theorem	wr5-2v 366	WOML derived from 2-variable axioms. (Contributed by NM, 11-Nov-1998.)
(a ≡ b) = 1    ⇒   ((a ∪ c) ≡ (b ∪ c)) = 1
0.2.2  Weakly orthomodular lattices
Theorem	wom3 367	Weak orthomodular law for study of weakly orthomodular lattices. (Contributed by NM, 13-Nov-1998.)
(a ≡ b) = 1    ⇒   a ≤ ((a ∪ c) ≡ (b ∪ c))
Theorem	wlor 368	Weak orthomodular law. (Contributed by NM, 24-Sep-1997.)
(a ≡ b) = 1    ⇒   ((c ∪ a) ≡ (c ∪ b)) = 1
Theorem	wran 369	Weak orthomodular law. (Contributed by NM, 24-Sep-1997.)
(a ≡ b) = 1    ⇒   ((a ∩ c) ≡ (b ∩ c)) = 1
Theorem	wlan 370	Weak orthomodular law. (Contributed by NM, 24-Sep-1997.)
(a ≡ b) = 1    ⇒   ((c ∩ a) ≡ (c ∩ b)) = 1
Theorem	wr2 371	Inference rule of AUQL. (Contributed by NM, 24-Sep-1997.)
(a ≡ b) = 1    &   (b ≡ c) = 1    ⇒   (a ≡ c) = 1
Theorem	w2or 372	Join both sides with disjunction. (Contributed by NM, 13-Oct-1997.)
(a ≡ b) = 1    &   (c ≡ d) = 1    ⇒   ((a ∪ c) ≡ (b ∪ d)) = 1
Theorem	w2an 373	Join both sides with conjunction. (Contributed by NM, 13-Oct-1997.)
(a ≡ b) = 1    &   (c ≡ d) = 1    ⇒   ((a ∩ c) ≡ (b ∩ d)) = 1
Theorem	w3tr1 374	Transitive inference useful for introducing definitions. (Contributed by NM, 13-Oct-1997.)
(a ≡ b) = 1    &   (c ≡ a) = 1    &   (d ≡ b) = 1    ⇒   (c ≡ d) = 1
Theorem	w3tr2 375	Transitive inference useful for eliminating definitions. (Contributed by NM, 13-Oct-1997.)
(a ≡ b) = 1    &   (a ≡ c) = 1    &   (b ≡ d) = 1    ⇒   (c ≡ d) = 1
0.2.3  Relationship analogues (ordering; commutation) in WOML
Theorem	wleoa 376	Relation between two methods of expressing "less than or equal to". (Contributed by NM, 27-Sep-1997.)
((a ∪ c) ≡ b) = 1    ⇒   ((a ∩ b) ≡ a) = 1
Theorem	wleao 377	Relation between two methods of expressing "less than or equal to". (Contributed by NM, 27-Sep-1997.)
((c ∩ b) ≡ a) = 1    ⇒   ((a ∪ b) ≡ b) = 1
Theorem	wdf-le1 378	Define "less than or equal to" analogue for ≡ analogue of =. (Contributed by NM, 27-Sep-1997.)
((a ∪ b) ≡ b) = 1    ⇒   (a ≤2 b) = 1
Theorem	wdf-le2 379	Define "less than or equal to" analogue for ≡ analogue of =. (Contributed by NM, 27-Sep-1997.)
(a ≤2 b) = 1    ⇒   ((a ∪ b) ≡ b) = 1
Theorem	wom4 380	Orthomodular law. Kalmbach 83 p. 22. (Contributed by NM, 13-Oct-1997.)
(a ≤2 b) = 1    ⇒   ((a ∪ (a⊥ ∩ b)) ≡ b) = 1
Theorem	wom5 381	Orthomodular law. Kalmbach 83 p. 22. (Contributed by NM, 13-Oct-1997.)
(a ≤2 b) = 1    &   ((b ∩ a⊥ ) ≡ 0) = 1    ⇒   (a ≡ b) = 1
Theorem	wcomlem 382	Analogue of commutation is symmetric. Similar to Kalmbach 83 p. 22. (Contributed by NM, 27-Jan-2002.)
(a ≡ ((a ∩ b) ∪ (a ∩ b⊥ ))) = 1    ⇒   (b ≡ ((b ∩ a) ∪ (b ∩ a⊥ ))) = 1
Theorem	wdf-c1 383	Show that commutator is a 'commutes' analogue for ≡ analogue of =. (Contributed by NM, 27-Jan-2002.)
(a ≡ ((a ∩ b) ∪ (a ∩ b⊥ ))) = 1    ⇒    C (a, b) = 1
Theorem	wdf-c2 384	Show that commutator is a 'commutes' analogue for ≡ analogue of =. (Contributed by NM, 27-Jan-2002.)
C (a, b) = 1    ⇒   (a ≡ ((a ∩ b) ∪ (a ∩ b⊥ ))) = 1
Theorem	wdf2le1 385	Alternate definition of "less than or equal to". (Contributed by NM, 27-Sep-1997.)
((a ∩ b) ≡ a) = 1    ⇒   (a ≤2 b) = 1
Theorem	wdf2le2 386	Alternate definition of "less than or equal to". (Contributed by NM, 27-Sep-1997.)
(a ≤2 b) = 1    ⇒   ((a ∩ b) ≡ a) = 1
Theorem	wleo 387	L.e. absorption. (Contributed by NM, 27-Sep-1997.)
(a ≤2 (a ∪ b)) = 1
Theorem	wlea 388	L.e. absorption. (Contributed by NM, 27-Sep-1997.)
((a ∩ b) ≤2 a) = 1
Theorem	wle1 389	Anything is less than or equal to 1. (Contributed by NM, 27-Sep-1997.)
(a ≤2 1) = 1
Theorem	wle0 390	0 is less than or equal to anything. (Contributed by NM, 11-Oct-1997.)
(0 ≤2 a) = 1
Theorem	wler 391	Add disjunct to right of l.e. (Contributed by NM, 13-Oct-1997.)
(a ≤2 b) = 1    ⇒   (a ≤2 (b ∪ c)) = 1
Theorem	wlel 392	Add conjunct to left of l.e. (Contributed by NM, 13-Oct-1997.)
(a ≤2 b) = 1    ⇒   ((a ∩ c) ≤2 b) = 1
Theorem	wleror 393	Add disjunct to right of both sides. (Contributed by NM, 13-Oct-1997.)
(a ≤2 b) = 1    ⇒   ((a ∪ c) ≤2 (b ∪ c)) = 1
Theorem	wleran 394	Add conjunct to right of both sides. (Contributed by NM, 13-Oct-1997.)
(a ≤2 b) = 1    ⇒   ((a ∩ c) ≤2 (b ∩ c)) = 1
Theorem	wlecon 395	Contrapositive for l.e. (Contributed by NM, 13-Oct-1997.)
(a ≤2 b) = 1    ⇒   (b⊥ ≤2 a⊥ ) = 1
Theorem	wletr 396	Transitive law for l.e. (Contributed by NM, 13-Oct-1997.)
(a ≤2 b) = 1    &   (b ≤2 c) = 1    ⇒   (a ≤2 c) = 1
Theorem	wbltr 397	Transitive inference. (Contributed by NM, 13-Oct-1997.)
(a ≡ b) = 1    &   (b ≤2 c) = 1    ⇒   (a ≤2 c) = 1
Theorem	wlbtr 398	Transitive inference. (Contributed by NM, 13-Oct-1997.)
(a ≤2 b) = 1    &   (b ≡ c) = 1    ⇒   (a ≤2 c) = 1
Theorem	wle3tr1 399	Transitive inference useful for introducing definitions. (Contributed by NM, 13-Oct-1997.)
(a ≤2 b) = 1    &   (c ≡ a) = 1    &   (d ≡ b) = 1    ⇒   (c ≤2 d) = 1
Theorem	wle3tr2 400	Transitive inference useful for eliminating definitions. (Contributed by NM, 13-Oct-1997.)
(a ≤2 b) = 1    &   (a ≡ c) = 1    &   (b ≡ d) = 1    ⇒   (c ≤2 d) = 1