Quantum Logic Explorer - mmtheorems5

Jump to page: 1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1024

Statement List for Quantum Logic Explorer - 401-500 - Page 5 of 11

Type	Label	Description
Statement
Theorem	wcom3ii 401	Lemma 3(ii) of Kalmbach 83 p. 23.
C (a, b) = 1   =>   ((a ^ (a_|_ v b)) == (a ^ b)) = 1
Theorem	wcomcom5 402	Commutation equivalence. Kalmbach 83 p. 23.
C (a_|_, b_|_) = 1   =>   C (a, b) = 1
Theorem	wcomdr 403	Commutation dual. Kalmbach 83 p. 23.
(a == ((a v b) ^ (a v b_|_))) = 1   =>   C (a, b) = 1
Theorem	wcom3i 404	Lemma 3(i) of Kalmbach 83 p. 23.
((a ^ (a_|_ v b)) == (a ^ b)) = 1   =>   C (a, b) = 1
Theorem	wfh1 405	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
Theorem	wfh2 406	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
Theorem	wfh3 407	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
Theorem	wfh4 408	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
Theorem	wcom2or 409	Th. 4.2 Beran p. 49.
C (a, b) = 1   &   C (a, c) = 1   =>   C (a, (b v c)) = 1
Theorem	wcom2an 410	Th. 4.2 Beran p. 49.
C (a, b) = 1   &   C (a, c) = 1   =>   C (a, (b ^ c)) = 1
Theorem	wnbdi 411	Negated biconditional (distributive form)
((a == b)_|_ == (((a v b) ^ a_|_) v ((a v b) ^ b_|_))) = 1
Theorem	wlem14 412	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
Theorem	wr5 413	Proof of weak orthomodular law from weaker-looking equivalent, wom3 349, which in turn is derived from ax-wom 343.
(a == b) = 1   =>   ((a v c) == (b v c)) = 1
Theorem	ska2 414	Soundness theorem for Kalmbach's quantum propositional logic axiom KA2.
((a == b)_|_ v ((b == c)_|_ v (a == c))) = 1
Theorem	ska4 415	Soundness theorem for Kalmbach's quantum propositional logic axiom KA4.
((a == b)_|_ v ((a ^ c) == (b ^ c))) = 1
Theorem	wom2 416	Weak orthomodular law for study of weakly orthomodular lattices.
a =< ((a == b)_|_ v ((a v c) == (b v c)))
Theorem	ka4ot 417	3-variable version of weakly orthomodular law. It is proved from a weaker-looking equivalent, wom2 416, which in turn is proved from ax-wom 343.
((a == b)_|_ v ((a v c) == (b v c))) = 1
Theorem	woml6 418	Variant of weakly orthomodular law.
((a ->1 b)_|_ v (a ->2 b)) = 1
Theorem	woml7 419	Variant of weakly orthomodular law.
(((a ->2 b) ^ (b ->2 a))_|_ v (a == b)) = 1
Theorem	ortha 420	Property of orthogonality
a =< b_|_   =>   (a ^ b) = 0
Axiom	ax-r3 421	Orthomodular law - when added to an ortholattice, it makes the ortholattice an orthomodular lattice. See r3a 422 for a more compact version.
(c v c_|_) = ((a_|_ v b_|_)_|_ v (a v b)_|_)   =>   a = b
Theorem	r3a 422	Orthomodular law restated.
1 = (a == b)   =>   a = b
Theorem	wed 423	Weak equivalential detachment (WBMP).
a = b   &   (a == b) = (c == d)   =>   c = d
Theorem	r3b 424	Orthomodular law from weak equivalential detachment (WBMP).
(c v c_|_) = (a == b)   =>   a = b
Theorem	lem3.1 425	Lemma used in proof of Th. 3.1 of Pavicic 1993.
(a v b) = b   &   (b_|_ v a) = 1   =>   a = b
Theorem	lem3a.1 426	Lemma used in proof of Th. 3.1 of Pavicic 1993.
(a v b) = b   &   (b_|_ v a) = 1   =>   (a v b) = a
Theorem	oml 427	Orthomodular law. Compare Th. 1 of Pavicic 1987.
(a v (a_|_ ^ (a v b))) = (a v b)
Theorem	omln 428	Orthomodular law.
(a_|_ v (a ^ (a_|_ v b))) = (a_|_ v b)
Theorem	omla 429	Orthomodular law.
(a ^ (a_|_ v (a ^ b))) = (a ^ b)
Theorem	omlan 430	Orthomodular law.
(a_|_ ^ (a v (a_|_ ^ b))) = (a_|_ ^ b)
Theorem	oml5 431	Orthomodular law.
((a ^ b) v ((a ^ b)_|_ ^ (b v c))) = (b v c)
Theorem	oml5a 432	Orthomodular law.
((a v b) ^ ((a v b)_|_ v (b ^ c))) = (b ^ c)
Theorem	oml2 433	Orthomodular law. Kalmbach 83 p. 22.
a =< b   =>   (a v (a_|_ ^ b)) = b
Theorem	oml3 434	Orthomodular law. Kalmbach 83 p. 22.
a =< b   &   (b ^ a_|_) = 0   =>   a = b
Theorem	comcom 435	Commutation is symmetric. Kalmbach 83 p. 22.
a C b   =>   b C a
Theorem	comcom3 436	Commutation equivalence. Kalmbach 83 p. 23.
a C b   =>   a_|_ C b
Theorem	comcom4 437	Commutation equivalence. Kalmbach 83 p. 23.
a C b   =>   a_|_ C b_|_
Theorem	comd 438	Commutation dual. Kalmbach 83 p. 23.
a C b   =>   a = ((a v b) ^ (a v b_|_))
Theorem	com3ii 439	Lemma 3(ii) of Kalmbach 83 p. 23.
a C b   =>   (a ^ (a_|_ v b)) = (a ^ b)
Theorem	comcom5 440	Commutation equivalence. Kalmbach 83 p. 23.
a_|_ C b_|_   =>   a C b
Theorem	comcom6 441	Commutation equivalence. Kalmbach 83 p. 23.
a_|_ C b   =>   a C b
Theorem	comcom7 442	Commutation equivalence. Kalmbach 83 p. 23.
a C b_|_   =>   a C b
Theorem	comor1 443	Commutation law.
(a v b) C a
Theorem	comor2 444	Commutation law.
(a v b) C b
Theorem	comorr2 445	Commutation law.
b C (a v b)
Theorem	comanr1 446	Commutation law.
a C (a ^ b)
Theorem	comanr2 447	Commutation law.
b C (a ^ b)
Theorem	comdr 448	Commutation dual. Kalmbach 83 p. 23.
a = ((a v b) ^ (a v b_|_))   =>   a C b
Theorem	com3i 449	Lemma 3(i) of Kalmbach 83 p. 23.
(a ^ (a_|_ v b)) = (a ^ b)   =>   a C b
Theorem	df2c1 450	Dual 'commutes' analogue for == analogue of =.
a = ((a v b) ^ (a v b_|_))   =>   a C b
Theorem	fh1 451	Foulis-Holland Theorem.
a C b   &   a C c   =>   (a ^ (b v c)) = ((a ^ b) v (a ^ c))
Theorem	fh2 452	Foulis-Holland Theorem.
a C b   &   a C c   =>   (b ^ (a v c)) = ((b ^ a) v (b ^ c))
Theorem	fh3 453	Foulis-Holland Theorem.
a C b   &   a C c   =>   (a v (b ^ c)) = ((a v b) ^ (a v c))
Theorem	fh4 454	Foulis-Holland Theorem.
a C b   &   a C c   =>   (b v (a ^ c)) = ((b v a) ^ (b v c))
Theorem	fh1r 455	Foulis-Holland Theorem.
a C b   &   a C c   =>   ((b v c) ^ a) = ((b ^ a) v (c ^ a))
Theorem	fh2r 456	Foulis-Holland Theorem.
a C b   &   a C c   =>   ((a v c) ^ b) = ((a ^ b) v (c ^ b))
Theorem	fh3r 457	Foulis-Holland Theorem.
a C b   &   a C c   =>   ((b ^ c) v a) = ((b v a) ^ (c v a))
Theorem	fh4r 458	Foulis-Holland Theorem.
a C b   &   a C c   =>   ((a ^ c) v b) = ((a v b) ^ (c v b))
Theorem	fh2c 459	Foulis-Holland Theorem.
a C b   &   a C c   =>   (b ^ (c v a)) = ((b ^ c) v (b ^ a))
Theorem	fh4c 460	Foulis-Holland Theorem.
a C b   &   a C c   =>   (b v (c ^ a)) = ((b v c) ^ (b v a))
Theorem	fh1rc 461	Foulis-Holland Theorem.
a C b   &   a C c   =>   ((c v b) ^ a) = ((c ^ a) v (b ^ a))
Theorem	fh2rc 462	Foulis-Holland Theorem.
a C b   &   a C c   =>   ((c v a) ^ b) = ((c ^ b) v (a ^ b))
Theorem	fh3rc 463	Foulis-Holland Theorem.
a C b   &   a C c   =>   ((c ^ b) v a) = ((c v a) ^ (b v a))
Theorem	fh4rc 464	Foulis-Holland Theorem.
a C b   &   a C c   =>   ((c ^ a) v b) = ((c v b) ^ (a v b))
Theorem	com2or 465	Th. 4.2 Beran p. 49.
a C b   &   a C c   =>   a C (b v c)
Theorem	com2an 466	Th. 4.2 Beran p. 49.
a C b   &   a C c   =>   a C (b ^ c)
Theorem	combi 467	Commutation theorem for Sasaki implication.
a C (a == b)
Theorem	nbdi 468	Negated biconditional (distributive form)
(a == b)_|_ = (((a v b) ^ a_|_) v ((a v b) ^ b_|_))
Theorem	oml4 469	Orthomodular law.
((a == b) ^ a) =< b
Theorem	oml6 470	Orthomodular law.
(a v (b ^ (a_|_ v b_|_))) = (a v b)
Theorem	gsth 471	Gudder-Schelp's Theorem. Beran, p. 262, Th. 4.1.
a C b   &   b C c   &   a C (b ^ c)   =>   (a ^ b) C c
Theorem	gsth2 472	Stronger version of Gudder-Schelp's Theorem. Beran, p. 263, Th. 4.2.
b C c   &   a C (b ^ c)   =>   (a ^ b) C c
Theorem	gstho 473	"OR" version of Gudder-Schelp's Theorem.
b C c   &   a C (b v c)   =>   (a v b) C c
Theorem	gt1 474	Part of Lemma 1 from Gaisi Takeuti, "Quantum Set Theory".
a = (b v c)   &   b =< d   &   c =< d_|_   =>   a C d
Theorem	cmtr1com 475	Commutator equal to 1 commutes. Theorem 2.11 of Beran, p. 86.
C (a, b) = 1   =>   a C b
Theorem	comcmtr1 476	Commutation implies commutator equal to 1. Theorem 2.11 of Beran, p. 86.
a C b   =>   C (a, b) = 1
Theorem	i0cmtrcom 477	Commutator element ->0 commutator implies commutation.
(a ->0 C