Quantum Logic Explorer - mmtheorems11

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 - 1001-1024 - Page 11 of 11

Type	Label	Description
Statement
Theorem	oadistc0 1001	Pre-distributive law.
d =< ((a ->2 b) ^ (a ->2 c))   &   ((a ->2 c) ^ ((a ->2 b) ^ ((b v c)_|_ v d))) =< (((a ->2 b) ^ (b v c)_|_) v d)   =>   ((a ->2 b) ^ ((b v c)_|_ v d)) = (((a ->2 b) ^ (b v c)_|_) v d)
Theorem	oadistc 1002	Distributive law.
d =< ((a ->2 b) ^ (a ->2 c))   &   ((a ->2 b) ^ ((b v c)_|_ v d)) =< (((a ->2 b) ^ (b v c)_|_) v d)   =>   ((a ->2 b) ^ ((b v c)_|_ v d)) = (((a ->2 b) ^ (b v c)_|_) v ((a ->2 b) ^ d))
Theorem	oadistd 1003	OA distributive law.
d =< (a ->2 b)   &   e =< ((b v c) ->0 ((a ->2 b) ^ (a ->2 c)))   &   f =< ((b v c) ->0 ((a ->2 b) ^ (a ->2 c)))   &   (d ^ (a ->2 c)) =< f   =>   (d ^ (e v f)) = ((d ^ e) v (d ^ f))
Theorem	3oa2 1004	Alternate form for the 3-variable orthoarguesion law.
((a ->1 c) ^ (((a ->1 c) ^ (b ->1 c)) v ((a_|_ ->1 c) ^ (b_|_ ->1 c)))) =< (b ->1 c)
Theorem	3oa3 1005	3-variable orthoarguesion law expressed with the 3OA identity abbreviation.
((a ->1 c) ^ (a == c ==OA b)) =< (b ->1 c)
Axiom	ax-oal4 1006	Orthoarguesian law (4-variable version).
a =< b_|_   &   c =< d_|_   =>   ((a v b) ^ (c v d)) =< (b v (a ^ (c v ((a v c) ^ (b v d)))))
Theorem	oa4cl 1007	4-variable OA closed equational form)
((a v (b ^ a_|_)) ^ (c v (d ^ c_|_))) =< ((b ^ a_|_) v (a ^ (c v ((a v c) ^ ((b ^ a_|_) v (d ^ c_|_))))))
Theorem	oa43v 1008	Derivation of 3-variable OA from 4-variable OA.
((a ->2 b) ^ ((b v c)_|_ v ((a ->2 b) ^ (a ->2 c)))) =< (a ->2 c)
Axiom	ax-oa6 1009	Orthoarguesian law (6-variable version).
a =< b_|_   &   c =< d_|_   &   e =< f_|_   =>   (((a v b) ^ (c v d)) ^ (e v f)) =< (b v (a ^ (c v (((a v c) ^ (b v d)) ^ (((a v e) ^ (b v f)) v ((c v e) ^ (d v f)))))))
Theorem	oa64v 1010	Derivation of 4-variable OA from 6-variable OA.
a =< b_|_   &   c =< d_|_   =>   ((a v b) ^ (c v d)) =< (b v (a ^ (c v ((a v c) ^ (b v d)))))
Theorem	oa63v 1011	Derivation of 3-variable OA from 6-variable OA.
((a ->2 b) ^ ((b v c)_|_ v ((a ->2 b) ^ (a ->2 c)))) =< (a ->2 c)
Axiom	ax-4oa 1012	The proper 4-variable OA law.
((a ->1 d) ^ (((a ^ b) v ((a ->1 d) ^ (b ->1 d))) v (((a ^ c) v ((a ->1 d) ^ (c ->1 d))) ^ ((b ^ c) v ((b ->1 d) ^ (c ->1 d)))))) =< (b ->1 d)
Theorem	axoa4 1013	The proper 4-variable OA law.
(a_|_ ^ (a v (b ^ (((a ^ b) v ((a ->1 d) ^ (b ->1 d))) v (((a ^ c) v ((a ->1 d) ^ (c ->1 d))) ^ ((b ^ c) v ((b ->1 d) ^ (c ->1 d)))))))) =< d
Theorem	axoa4b 1014	Proper 4-variable OA law variant.
((a ->1 d) ^ (a v (b ^ (((a ^ b) v ((a ->1 d) ^ (b ->1 d))) v (((a ^ c) v ((a ->1 d) ^ (c ->1 d))) ^ ((b ^ c) v ((b ->1 d) ^ (c ->1 d)))))))) =< d
Theorem	oa6 1015	Derivation of 6-variable orthoarguesian law from 4-variable version.
a =< b_|_   &   c =< d_|_   &   e =< f_|_   =>   (((a v b) ^ (c v d)) ^ (e v f)) =< (b v (a ^ (c v (((a v c) ^ (b v d)) ^ (((a v e) ^ (b v f)) v ((c v e) ^ (d v f)))))))
Theorem	axoa4a 1016	Proper 4-variable OA law variant.
((a ->1 d) ^ (a v (b ^ (((a ^ b) v ((a ->1 d) ^ (b ->1 d))) v (((a ^ c) v ((a ->1 d) ^ (c ->1 d))) ^ ((b ^ c) v ((b ->1 d) ^ (c ->1 d)))))))) =< (((a ^ d) v (b ^ d)) v (c ^ d))
Theorem	axoa4d 1017	Proper 4-variable OA law variant.
(a ^ (((a ^ b) v ((a ->1 d) ^ (b ->1 d))) v (((a ^ c) v ((a ->1 d) ^ (c ->1 d))) ^ ((b ^ c) v ((b ->1 d) ^ (c ->1 d)))))) =< (b_|_ ->1 d)
Theorem	4oa 1018	Variant of proper 4-OA.
e = (((a ^ c) v ((a ->1 d) ^ (c ->1 d))) ^ ((b ^ c) v ((b ->1 d) ^ (c ->1 d))))   &   f = (((a ^ b) v ((a ->1 d) ^ (b ->1 d))) v e)   =>   ((a ->1 d) ^ f) =< (b ->1 d)
Theorem	4oaiii 1019	Proper OA analog to Godowski/Greechie, Eq. III.
e = (((a ^ c) v ((a ->1 d) ^ (c ->1 d))) ^ ((b ^ c) v ((b ->1 d) ^ (c ->1 d))))   &   f = (((a ^ b) v ((a ->1 d) ^ (b ->1 d))) v e)   =>   ((a ->1 d) ^ f) = ((b ->1 d) ^ f)
Theorem	4oath1 1020	Proper 4-OA theorem.
e = (((a ^ c) v ((a ->1 d) ^ (c ->1 d))) ^ ((b ^ c) v ((b ->1 d) ^ (c ->1 d))))   &   f = (((a ^ b) v ((a ->1 d) ^ (b ->1 d))) v e)   =>   ((a ->1 d) ^ f) = ((a ->1 d) ^ (b ->1 d))
Theorem	4oagen1 1021	"Generalized" 4-OA.
e = (((a ^ c) v ((a ->1 d) ^ (c ->1 d))) ^ ((b ^ c) v ((b ->1 d) ^ (c ->1 d))))   &   f = (((a ^ b) v ((a ->1 d) ^ (b ->1 d))) v e)   &   g =< f   =>   ((a ->1 d) ^ (g v ((a ->1 d) ^ (b ->1 d)))) = ((a ->1 d) ^ (b ->1 d))
Theorem	4oagen1b 1022	"Generalized" OA.
e = (((a ^ c) v ((a ->1 d) ^ (c ->1 d))) ^ ((b ^ c) v ((b ->1 d) ^ (c ->1 d))))   &   f = (((a ^ b) v ((a ->1 d) ^ (b ->1 d))) v e)   &   g =< f   &   h =< (a ->1 d)   =>   (h ^ (g v ((a ->1 d) ^ (b ->1 d)))) = (h ^ (b ->1 d))
Theorem	4oadist 1023	OA Distributive law. This is equivalent to the 6-variable OA law, as shown by theorem d6oa 977.
e = (((a ^ c) v ((a ->1 d) ^ (c ->1 d))) ^ ((b ^ c) v ((b ->1 d) ^ (c ->1 d))))   &   f = (((a ^ b) v ((a ->1 d) ^ (b ->1 d))) v e)   &   h =< (a ->1 d)   &   j =< f   &   k =< f   &   (h ^ (b ->1 d)) =< k   =>   (h ^ (j v k)) = ((h ^ j) v (h ^ k))
Axiom	ax-newstateeq 1024	New equation that holds in Hilbert space, discovered by Pavicic and Megill (unpublished).
(((a ->1 b) ->1 (c ->1 b)) ^ ((a ->1 c) ^ (b ->1 a))) =< (c ->1 a)

metamath.org

< Previous  Wrap >