Home Quantum Logic ExplorerTheorem List (p. 11 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 - 1001-1100   *Has distinct variable group(s)
TypeLabelDescription
Statement

Theoremoaliii 1001 Orthoarguesian law. Godowski/Greechie, Eq. III.

Theoremoalii 1002 Orthoarguesian law. Godowski/Greechie, Eq. II. This proof references oaliii 1001 only.

Theoremoaliv 1003 Orthoarguesian law. Godowski/Greechie, Eq. IV.

Theoremoath1 1004 OA theorem.

Theoremoalem1 1005 Lemma.

Theoremoalem2 1006 Lemma.

Theoremoadist2a 1007 Distributive inference derived from OA.

Theoremoadist2b 1008 Distributive inference derived from OA.

Theoremoadist2 1009 Distributive inference derived from OA.

Theoremoadist12 1010 Distributive law derived from OA.

Theoremoacom 1011 Commutation law requiring OA.

Theoremoacom2 1012 Commutation law requiring OA.

Theoremoacom3 1013 Commutation law requiring OA.

Theoremoagen1 1014 "Generalized" OA.

Theoremoagen1b 1015 "Generalized" OA.

Theoremoagen2 1016 "Generalized" OA.

Theoremoagen2b 1017 "Generalized" OA.

Theoremmloa 1018 Mladen's OA

Theoremoadist 1019 Distributive law derived from OAL.

Theoremoadistb 1020 Distributive law derived from OAL.

Theoremoadistc0 1021 Pre-distributive law.

Theoremoadistc 1022 Distributive law.

Theoremoadistd 1023 OA distributive law.

Theorem3oa2 1024 Alternate form for the 3-variable orthoarguesion law.

Theorem3oa3 1025 3-variable orthoarguesion law expressed with the 3OA identity abbreviation.

0.5.2  4-variable orthoarguesian law

Axiomax-oal4 1026 Orthoarguesian law (4-variable version).

Theoremoa4cl 1027 4-variable OA closed equational form)

Theoremoa43v 1028 Derivation of 3-variable OA from 4-variable OA.

Theoremoa3moa3 1029 4-variable 3OA to 5-variable Mayet's 3OA.

0.5.3  6-variable orthoarguesian law

Axiomax-oa6 1030 Orthoarguesian law (6-variable version).

Theoremoa64v 1031 Derivation of 4-variable OA from 6-variable OA.

Theoremoa63v 1032 Derivation of 3-variable OA from 6-variable OA.

0.5.4  The proper 4-variable orthoarguesian law

Axiomax-4oa 1033 The proper 4-variable OA law.

Theoremaxoa4 1034 The proper 4-variable OA law.

Theoremaxoa4b 1035 Proper 4-variable OA law variant.

Theoremoa6 1036 Derivation of 6-variable orthoarguesian law from 4-variable version.

Theoremaxoa4a 1037 Proper 4-variable OA law variant.

Theoremaxoa4d 1038 Proper 4-variable OA law variant.

Theorem4oa 1039 Variant of proper 4-OA.

Theorem4oaiii 1040 Proper OA analog to Godowski/Greechie, Eq. III.

Theorem4oath1 1041 Proper 4-OA theorem.

Theorem4oagen1 1042 "Generalized" 4-OA.

Theorem4oagen1b 1043 "Generalized" OA.

Theorem4oadist 1044 OA Distributive law. This is equivalent to the 6-variable OA law, as shown by theorem d6oa 997.

0.6  Other stronger-than-OML laws

0.6.1  New state-related equation

Axiomax-newstateeq 1045 New equation that holds in Hilbert space, discovered by Pavicic and Megill (unpublished).

0.7  Contributions of Roy Longton

0.7.1  Roy's first section

Theoremlem3.3.2 1046 Equation 3.2 of [PavMeg1999] p. 9. (Contributed by Roy F. Longton, 3-Jul-05.)

Definitiondf-id5 1047 Define asymmetrical identity (for "Non-Orthomodular Models..." paper).

Definitiondf-b1 1048 Define biconditional for .

Theoremlem3.3.3lem1 1049 Lemma for lem3.3.3 1052.

Theoremlem3.3.3lem2 1050 Lemma for lem3.3.3 1052.

Theoremlem3.3.3lem3 1051 Lemma for lem3.3.3 1052.

Theoremlem3.3.3 1052 Equation 3.3 of [PavMeg1999] p. 9. (Contributed by Roy F. Longton, 3-Jul-05.)

Theoremlem3.3.4 1053 Equation 3.4 of [PavMeg1999] p. 9. (Contributed by Roy F. Longton, 3-Jul-05.)

Theoremlem3.3.5lem 1054 A fundamental property in quantum logic. Lemma for lem3.3.5 1055.

Theoremlem3.3.5 1055 Equation 3.5 of [PavMeg1999] p. 9. (Contributed by Roy F. Longton, 3-Jul-05.)

Theoremlem3.3.6 1056 Equation 3.6 of [PavMeg1999] p. 9. (Contributed by Roy F. Longton, 3-Jul-05.)

Theoremlem3.3.7i0e1 1057 Equation 3.7 of [PavMeg1999] p. 9. The variable i in the paper is set to 0, and this is the first part of the equation. (Contributed by Roy F. Longton, 3-Jul-05.)

Theoremlem3.3.7i0e2 1058 Equation 3.7 of [PavMeg1999] p. 9. The variable i in the paper is set to 0, and this is the second part of the equation. (Contributed by Roy F. Longton, 3-Jul-05.)

Theoremlem3.3.7i0e3 1059 Equation 3.7 of [PavMeg1999] p. 9. The variable i in the paper is set to 0, and this is the third part of the equation. (Contributed by Roy F. Longton, 3-Jul-05.)

Theoremlem3.3.7i1e1 1060 Equation 3.7 of [PavMeg1999] p. 9. The variable i in the paper is set to 1, and this is the first part of the equation. (Contributed by Roy F. Longton, 3-Jul-05.)

Theoremlem3.3.7i1e2 1061 Equation 3.7 of [PavMeg1999] p. 9. The variable i in the paper is set to 1, and this is the second part of the equation. (Contributed by Roy F. Longton, 3-Jul-05.)

Theoremlem3.3.7i1e3 1062 Equation 3.7 of [PavMeg1999] p. 9. The variable i in the paper is set to 1, and this is the third part of the equation. (Contributed by Roy F. Longton, 3-Jul-05.)

Theoremlem3.3.7i2e1 1063 Equation 3.7 of [PavMeg1999] p. 9. The variable i in the paper is set to 2, and this is the first part of the equation. (Contributed by Roy F. Longton, 3-Jul-05.)

Theoremlem3.3.7i2e2 1064 Equation 3.7 of [PavMeg1999] p. 9. The variable i in the paper is set to 2, and this is the second part of the equation. (Contributed by Roy F. Longton, 3-Jul-05.)

Theoremlem3.3.7i2e3 1065 Equation 3.7 of [PavMeg1999] p. 9. The variable i in the paper is set to 2, and this is the third part of the equation. (Contributed by Roy F. Longton, 3-Jul-05.)

Theoremlem3.3.7i3e1 1066 Equation 3.7 of [PavMeg1999] p. 9. The variable i in the paper is set to 3, and this is the first part of the equation. (Contributed by Roy F. Longton, 3-Jul-05.)

Theoremlem3.3.7i3e2 1067 Equation 3.7 of [PavMeg1999] p. 9. The variable i in the paper is set to 3, and this is the second part of the equation. (Contributed by Roy F. Longton, 3-Jul-05.)

Theoremlem3.3.7i3e3 1068 Equation 3.7 of [PavMeg1999] p. 9. The variable i in the paper is set to 3, and this is the third part of the equation. (Contributed by Roy F. Longton, 3-Jul-05.)

Theoremlem3.3.7i4e1 1069 Equation 3.7 of [PavMeg1999] p. 9. The variable i in the paper is set to 4, and this is the first part of the equation. (Contributed by Roy F. Longton, 3-Jul-05.)

Theoremlem3.3.7i4e2 1070 Equation 3.7 of [PavMeg1999] p. 9. The variable i in the paper is set to 4, and this is the second part of the equation. (Contributed by Roy F. Longton, 3-Jul-05.)

Theoremlem3.3.7i4e3 1071 Equation 3.7 of [PavMeg1999] p. 9. The variable i in the paper is set to 4, and this is the third part of the equation. (Contributed by Roy F. Longton, 3-Jul-05.)

Theoremlem3.3.7i5e1 1072 Equation 3.7 of [PavMeg1999] p. 9. The variable i in the paper is set to 5, and this is the first part of the equation. (Contributed by Roy F. Longton, 3-Jul-05.)

Theoremlem3.3.7i5e2 1073 Equation 3.7 of [PavMeg1999] p. 9. The variable i in the paper is set to 5, and this is the second part of the equation. (Contributed by Roy F. Longton, 3-Jul-05.)

Theoremlem3.3.7i5e3 1074 Equation 3.7 of [PavMeg1999] p. 9. The variable i in the paper is set to 5, and this is the third part of the equation. (Contributed by Roy F. Longton, 3-Jul-05.)

0.7.2  Roy's second section

Theoremlem3.4.1 1075 Equation 3.9 of [PavMeg1999] p. 9. (Contributed by Roy F. Longton, 3-Jul-05.)

Theoremlem3.4.3 1076 Equation 3.11 of [PavMeg1999] p. 9. (Contributed by Roy F. Longton, 3-Jul-05.)

Theoremlem3.4.4 1077 Equation 3.12 of [PavMeg1999] p. 9. (Contributed by Roy F. Longton, 3-Jul-05.)

Theoremlem3.4.5 1078 Equation 3.13 of [PavMeg1999] p. 9. (Contributed by Roy F. Longton, 3-Jul-05.)

Theoremlem3.4.6 1079 Equation 3.14 of [PavMeg1999] p. 9. (Contributed by Roy F. Longton, 3-Jul-05.)

0.7.3  Roy's third section

Theoremlem4.6.2e1 1080 Equation 4.10 of [MegPav2000] p. 23. This is the first part of the equation. (Contributed by Roy F. Longton, 3-Jul-05.)

Theoremlem4.6.2e2 1081 Equation 4.10 of [MegPav2000] p. 23. This is the second part of the equation. (Contributed by Roy F. Longton, 3-Jul-05.)

Theoremlem4.6.3le1 1082 Equation 4.11 of [MegPav2000] p. 23. This is the first part of the equation. (Contributed by Roy F. Longton, 3-Jul-05.)

Theoremlem4.6.3le2 1083 Equation 4.11 of [MegPav2000] p. 23. This is the second part of the equation. (Contributed by Roy F. Longton, 3-Jul-05.)

Theoremlem4.6.4 1084 Equation 4.12 of [MegPav2000] p. 23. (Contributed by Roy F. Longton, 3-Jul-05.)

Theoremlem4.6.5 1085 Equation 4.13 of [MegPav2000] p. 23. (Contributed by Roy F. Longton, 3-Jul-05.)

Theoremlem4.6.6i0j1 1086 Equation 4.14 of [MegPav2000] p. 23. The variable i in the paper is set to 0, and j is set to 1. (Contributed by Roy F. Longton, 3-Jul-05.)

Theoremlem4.6.6i0j2 1087 Equation 4.14 of [MegPav2000] p. 23. The variable i in the paper is set to 0, and j is set to 2. (Contributed by Roy F. Longton, 3-Jul-05.)

Theoremlem4.6.6i0j3 1088 Equation 4.14 of [MegPav2000] p. 23. The variable i in the paper is set to 0, and j is set to 3. (Contributed by Roy F. Longton, 3-Jul-05.)

Theoremlem4.6.6i0j4 1089 Equation 4.14 of [MegPav2000] p. 23. The variable i in the paper is set to 0, and j is set to 4. (Contributed by Roy F. Longton, 3-Jul-05.)

Theoremlem4.6.6i1j0 1090 Equation 4.14 of [MegPav2000] p. 23. The variable i in the paper is set to 1, and j is set to 0. (Contributed by Roy F. Longton, 3-Jul-05.)

Theoremlem4.6.6i1j2 1091 Equation 4.14 of [MegPav2000] p. 23. The variable i in the paper is set to 1, and j is set to 2. (Contributed by Roy F. Longton, 3-Jul-05.)

Theoremlem4.6.6i1j3 1092 Equation 4.14 of [MegPav2000] p. 23. The variable i in the paper is set to 1, and j is set to 3. (Contributed by Roy F. Longton, 3-Jul-05.)

Theoremlem4.6.6i2j0 1093 Equation 4.14 of [MegPav2000] p. 23. The variable i in the paper is set to 2, and j is set to 0. (Contributed by Roy F. Longton, 3-Jul-05.)

Theoremlem4.6.6i2j1 1094 Equation 4.14 of [MegPav2000] p. 23. The variable i in the paper is set to 2, and j is set to 1. (Contributed by Roy F. Longton, 3-Jul-05.)

Theoremlem4.6.6i2j4 1095 Equation 4.14 of [MegPav2000] p. 23. The variable i in the paper is set to 2, and j is set to 4. (Contributed by Roy F. Longton, 3-Jul-05.)

Theoremlem4.6.6i3j0 1096 Equation 4.14 of [MegPav2000] p. 23. The variable i in the paper is set to 3, and j is set to 0. (Contributed by Roy F. Longton, 3-Jul-05.)

Theoremlem4.6.6i3j1 1097 Equation 4.14 of [MegPav2000] p. 23. The variable i in the paper is set to 3, and j is set to 1. (Contributed by Roy F. Longton, 3-Jul-05.)

Theoremlem4.6.6i4j0 1098 Equation 4.14 of [MegPav2000] p. 23. The variable i in the paper is set to 4, and j is set to 0. (Contributed by Roy F. Longton, 3-Jul-05.)

Theoremlem4.6.6i4j2 1099 Equation 4.14 of [MegPav2000] p. 23. The variable i in the paper is set to 4, and j is set to 2. (Contributed by Roy F. Longton, 3-Jul-05.)

Theoremcom3iia 1100 The dual of com3ii 457. (Contributed by Roy F. Longton, 3-Jul-05.)

Page List
Jump to page: Contents  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-1100 12 1101-1200 13 1201-1215
 Copyright terms: Public domain < Previous  Next >