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

Type | Label | Description |
---|---|---|

Statement | ||

Theorem | oaliii 1001 | Orthoarguesian law. Godowski/Greechie, Eq. III. |

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

Theorem | oaliv 1003 | Orthoarguesian law. Godowski/Greechie, Eq. IV. |

Theorem | oath1 1004 | OA theorem. |

Theorem | oalem1 1005 | Lemma. |

Theorem | oalem2 1006 | Lemma. |

Theorem | oadist2a 1007 | Distributive inference derived from OA. |

Theorem | oadist2b 1008 | Distributive inference derived from OA. |

Theorem | oadist2 1009 | Distributive inference derived from OA. |

Theorem | oadist12 1010 | Distributive law derived from OA. |

Theorem | oacom 1011 | Commutation law requiring OA. |

Theorem | oacom2 1012 | Commutation law requiring OA. |

Theorem | oacom3 1013 | Commutation law requiring OA. |

Theorem | oagen1 1014 | "Generalized" OA. |

Theorem | oagen1b 1015 | "Generalized" OA. |

Theorem | oagen2 1016 | "Generalized" OA. |

Theorem | oagen2b 1017 | "Generalized" OA. |

Theorem | mloa 1018 | Mladen's OA |

Theorem | oadist 1019 | Distributive law derived from OAL. |

Theorem | oadistb 1020 | Distributive law derived from OAL. |

Theorem | oadistc0 1021 | Pre-distributive law. |

Theorem | oadistc 1022 | Distributive law. |

Theorem | oadistd 1023 | OA distributive law. |

Theorem | 3oa2 1024 | Alternate form for the 3-variable orthoarguesion law. |

Theorem | 3oa3 1025 | 3-variable orthoarguesion law expressed with the 3OA identity abbreviation. |

0.5.2 4-variable orthoarguesian law | ||

Axiom | ax-oal4 1026 | Orthoarguesian law (4-variable version). |

Theorem | oa4cl 1027 | 4-variable OA closed equational form) |

Theorem | oa43v 1028 | Derivation of 3-variable OA from 4-variable OA. |

Theorem | oa3moa3 1029 | 4-variable 3OA to 5-variable Mayet's 3OA. |

0.5.3 6-variable orthoarguesian law | ||

Axiom | ax-oa6 1030 | Orthoarguesian law (6-variable version). |

Theorem | oa64v 1031 | Derivation of 4-variable OA from 6-variable OA. |

Theorem | oa63v 1032 | Derivation of 3-variable OA from 6-variable OA. |

0.5.4 The proper 4-variable orthoarguesian
law | ||

Axiom | ax-4oa 1033 | The proper 4-variable OA law. |

Theorem | axoa4 1034 | The proper 4-variable OA law. |

Theorem | axoa4b 1035 | Proper 4-variable OA law variant. |

Theorem | oa6 1036 | Derivation of 6-variable orthoarguesian law from 4-variable version. |

Theorem | axoa4a 1037 | Proper 4-variable OA law variant. |

Theorem | axoa4d 1038 | Proper 4-variable OA law variant. |

Theorem | 4oa 1039 | Variant of proper 4-OA. |

Theorem | 4oaiii 1040 | Proper OA analog to Godowski/Greechie, Eq. III. |

Theorem | 4oath1 1041 | Proper 4-OA theorem. |

Theorem | 4oagen1 1042 | "Generalized" 4-OA. |

Theorem | 4oagen1b 1043 | "Generalized" OA. |

Theorem | 4oadist 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 | ||

Axiom | ax-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 | ||

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

Definition | df-id5 1047 | Define asymmetrical identity (for "Non-Orthomodular Models..." paper). |

Definition | df-b1 1048 | Define biconditional for . |

Theorem | lem3.3.3lem1 1049 | Lemma for lem3.3.3 1052. |

Theorem | lem3.3.3lem2 1050 | Lemma for lem3.3.3 1052. |

Theorem | lem3.3.3lem3 1051 | Lemma for lem3.3.3 1052. |

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

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

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

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

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

Theorem | lem3.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.) |

Theorem | lem3.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.) |

Theorem | lem3.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.) |

Theorem | lem3.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.) |

Theorem | lem3.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.) |

Theorem | lem3.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.) |

Theorem | lem3.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.) |

Theorem | lem3.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.) |

Theorem | lem3.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.) |

Theorem | lem3.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.) |

Theorem | lem3.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.) |

Theorem | lem3.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.) |

Theorem | lem3.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.) |

Theorem | lem3.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.) |

Theorem | lem3.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.) |

Theorem | lem3.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.) |

Theorem | lem3.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.) |

Theorem | lem3.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 | ||

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

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

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

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

Theorem | lem3.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 | ||

Theorem | lem4.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.) |

Theorem | lem4.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.) |

Theorem | lem4.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.) |

Theorem | lem4.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.) |

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

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

Theorem | lem4.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.) |

Theorem | lem4.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.) |

Theorem | lem4.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.) |

Theorem | lem4.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.) |

Theorem | lem4.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.) |

Theorem | lem4.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.) |

Theorem | lem4.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.) |

Theorem | lem4.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.) |

Theorem | lem4.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.) |

Theorem | lem4.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.) |

Theorem | lem4.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.) |

Theorem | lem4.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.) |

Theorem | lem4.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.) |

Theorem | lem4.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.) |

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

< Previous Next > |

Copyright terms: Public domain | < Previous Next > |