mmtheorems122 - Metamath Proof Explorer

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-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9500 96 9501-9600 97 9601-9700 98 9701-9800 99 9801-9900 100 9901-10000 101 10001-10100 102 10101-10200 103 10201-10300 104 10301-10400 105 10401-10500 106 10501-10600 107 10601-10700 108 10701-10800 109 10801-10900 110 10901-11000 111 11001-11100 112 11101-11200 113 11201-11300 114 11301-11400 115 11401-11500 116 11501-11600 117 11601-11700 118 11701-11800 119 11801-11900 120 11901-12000 121 12001-12100 122 12101-12200 123 12201-12229

Statement List for Metamath Proof Explorer - 12101-12200 - Page 122 of 123

Type	Label	Description
Statement
Theorem	isphtpc 12101	The relation "is path homotopic to".
|- ((J e. Top /\ F e. A /\ G e. B) -> (F(=~ph` J)G <-> (((F e. (II Cn J) /\ G e. (II Cn J)) /\ ((F` 0) = (G` 0) /\ (F` 1) = (G` 1))) /\ (F(PHtpy` J)G) =/= (/))))
Theorem	isphtpc2 12102	The relation "is path homotopic to".
|- ((J e. Top /\ G e. A) -> (F(=~ph` J)G <-> (((F e. (II Cn J) /\ G e. (II Cn J)) /\ ((F` 0) = (G` 0) /\ (F` 1) = (G` 1))) /\ (F(PHtpy` J)G) =/= (/))))
Theorem	phtpcdm 12103	The domain of the path homotopy relation.
|- (J e. Top -> dom (=~ph` J) = (II Cn J))
Theorem	phtpcer 12104	Path homotopy is an equivalence relation. Proposition 1.2 of Hatcher.
|- (J e. Top -> Er (=~ph` J))
Mathbox for Norm Megill
Axioms for quantum logic system Q3
Axiom	ax-q1 12105	Axiom for quantum logic system Q3. Note: This will be broken out as a separate database, but for now I am reusing the structure already in set.mm. All proofs should refer only to axioms in this section, and nothing outside of this section should make use of it since it will go away eventually. The purpose of this project is to try to simplify the axioms of Kalmbach's quantum logic using implication and negation as primitives. Kalmbach proved that this is the only quantum logic possible that has modus ponens as its sole inference rule. (Four other logics are possible with slightly different definitions of implication, but they all require inference rules other than modus ponens.) For the original system, see axioms QA1-QA16 and rule QR1 at http://us.metamath.org/qlegif/kalmbach.txt. I conjecture that the axioms here can be proved from that system and vice-versa, and the purpose of this project is to verify that. Eventually I'd like to find further simplifications to the axioms where possible, eliminate redundant axioms, and prove the independence of the remaining ones. (This axiom system doesn't make set.mm inconsistent, because each axiom here can be proved as a theorem of classical logic from ax-1 4 through ax-3 6. In addition, the definitions df-qora 12123, df-qorb 12124, df-qana 12125, and df-qanb 12126 are theorems of classical logic. Thus all theorems derived from the quantum logic system Q3 are also theorems of the classical propositional calculus. But the converse is false; for example ax-1 4 cannot be derived as a theorem inside system Q3.)
|- (ph -> (ps -> (ps -> ph)))
Axiom	ax-q2 12106	Axiom for quantum logic system Q3.
|- (-. ph -> (ph -> (ph -> ps)))
Axiom	ax-q3 12107	Axiom for quantum logic system Q3.
|- ((ph -> ps) -> (ph -> (ph -> ps)))
Axiom	ax-q4 12108	Axiom for quantum logic system Q3.
|- (-. -. ph -> ph)
Axiom	ax-q5 12109	Axiom for quantum logic system Q3.
|- (-. (-. ph -> ps) -> (ph -> ps))
Axiom	ax-q6 12110	Axiom for quantum logic system Q3.
|- (-. (ph -> (ph -> ps)) -> (ps -> ph))
Axiom	ax-q7 12111	Axiom for quantum logic system Q3.
|- (-. (ph -> -. (ph -> (ph -> ps))) -> (ph -> ps))
Axiom	ax-q8 12112	Axiom for quantum logic system Q3.
|- ((-. ph -> -. ps) -> ((-. ph -> -. ps) -> (ps -> ph)))
Axiom	ax-q9 12113	Axiom for quantum logic system Q3.
|- ((ph -> ps) -> ((ps -> (ps -> ph)) -> ((-. ph -> ps) -> ph)))
Axiom	ax-q10 12114	Axiom for quantum logic system Q3.
|- (((-. ph -> ps) -> ph) -> (((-. ph -> ps) -> ph) -> (ps -> ph)))
Axiom	ax-q11 12115	Axiom for quantum logic system Q3.
|- ((-. ph -> ps) -> ((-. ph -> ps) -> ((ph -> (ph -> ps)) -> ps)))
Axiom	ax-q12 12116	Axiom for quantum logic system Q3.
|- ((ph -> ps) -> ((ph -> ps) -> ((ps -> ch) -> ((ps -> ch) -> ((-. ch -> ph) -> ch)))))
Axiom	ax-q13 12117	Axiom for quantum logic system Q3.
|- ((ph -> ps) -> ((ph -> ps) -> ((-. (ch -> (ch -> ps)) -> (ch -> (ch -> ph))) -> (ch -> (ch -> ps)))))
Axiom	ax-qmp 12118	Modus-ponens rule for quantum logic system Q3.
|- ph   &   |- (ph -> ps)   =>   |- ps
Preliminary lemmas to justify definitions
Theorem	qsyl 12119	Transitive law for implication.
|- (ph -> ps)   &   |- (ps -> ch)   =>   |- (ph -> ch)
Theorem	qnotnot2 12120	Double negation.
|- (-. -. ph -> ph)
Theorem	qnotnot1 12121	Double negation.
|- (ph -> -. -. ph)
Theorem	qid 12122	Identity law for implication.
|- (ph -> ph)
Definitions
Definition	df-qora 12123	Define disjunction. The justification is provided by qid 12122.
|- ((ph \/ ps) -> (-. ph -> (-. ph -> ps)))
Definition	df-qorb 12124	Define disjunction.
|- ((-. ph -> (-. ph -> ps)) -> (ph \/ ps))
Definition	df-qana 12125	Define conjunction.
|- ((ph /\ ps) -> -. (-. ph \/ -. ps))
Definition	df-qanb 12126	Define conjunction.
|- (-. (-. ph \/ -. ps) -> (ph /\ ps))
Basic theorems
Theorem	q2th 12127	Add theorem antecedent to a theorem.
|- ph   &   |- ps   =>   |- (ps -> ph)
Theorem	qa1i 12128	Add an antecedent to a theorem.
|- ph   =>   |- (ps -> ph)
Theorem	qmpc 12129	Classical modus ponens.
|- ph   &   |- (-. ph \/ ps)   =>   |- ps
Theorem	qax8a 12130	An older axiom of quantum logic system Q3, proved from the others, so it is redundant.
|- ((ph -> ph) -> (ps -> (ph -> ph)))
Theorem	qax8b 12131	An older axiom of quantum logic system Q3, proved from the others, so it is redundant.
|- ((ps -> (ps -> (ph -> ph))) -> (ph -> ph))
Theorem	qcon4i 12132	Contraposition inference.
|- (-. ph -> -. ps)   =>   |- (ps -> ph)
Theorem	qcon3i 12133	Contraposition inference.
|- (ph -> ps)   =>   |- (-. ps -> -. ph)
Theorem	qcon1i 12134	Contraposition inference.
|- (-. ph -> ps)   =>   |- (-. ps -> ph)
Theorem	qcon2i 12135	Contraposition inference.
|- (ph -> -. ps)   =>   |- (ps -> -. ph)
Theorem	qorl 12136	Add disjunct to consequent.
|- (ph -> (ps \/ ph))
Theorem	q2imim2i 12137	Introduce an imbedded consequent into both sides of an implication.
|- (ph -> ps)   =>   |- ((ch -> (ch -> ph)) -> (ch -> (ch -> ps)))
Theorem	qor2lim 12138	Disjoin antecedents (implication version of qor2l 12139).
|- (-. ph -> ch)   &   |- (ps -> ch)   =>   |- ((ph -> (ph -> ps)) -> ch)
Theorem	qor2l 12139	Disjoin antecedents.
|- (ph -> ch)   &   |- (ps -> ch)   =>   |- ((ph \/ ps) -> ch)
Theorem	qan2r 12140	Conjoin consequents.
|- (ph -> ps)   &   |- (ph -> ch)   =>   |- (ph -> (ps /\ ch))
Theorem	qorcoma 12141	Disjunction is commutative.
|- ((ph \/ ps) -> (ps \/ ph))
Theorem	qancoma 12142	Conjunction is commutative. Note: see description of quantum logic system Q3 under ax-q1 12105 .
|- ((ph /\ ps) -> (ps /\ ph))
Theorem	qorr 12143	Add disjunct to consequent.
|- (ph -> (ph \/ ps))
Theorem	qanr 12144	Remove conjunct from antecent.
|- ((ph /\ ps) -> ph)
Theorem	qanl 12145	Remove conjunct from antecent.
|- ((ph /\ ps) -> ps)
Theorem	qorassa 12146	Associative law.
|- (((ph \/ ps) \/ ch) -> (ph \/ (ps \/ ch)))
Theorem	qorim2i 12147	Introduce a left disjunct to both sides of an implication.
|- (ph -> ps)   =>   |- ((ch \/ ph) -> (ch \/ ps))
Theorem	qorim1i 12148	Introduce a right disjunct to both sides of an implication.
|- (ph -> ps)   =>   |- ((ph \/ ch) -> (ps \/ ch))
Theorem	qor2a 12149	Disjunction in terms of implication.
|- ((-. ph \/ ps) -> (ph -> (ph -> ps)))
Theorem	qor2b 12150	Disjunction in terms of implication.
|- ((ph -> (ph -> ps)) -> (-. ph \/ ps))
Theorem	qdfan2a 12151	Expand definition of AND.
|- ((ph /\ ps) -> -. (ph -> (ph -> -. ps)))
Theorem	qdfan2b 12152	Expand definition of AND.
|- (-. (ph -> (ph -> -. ps)) -> (ph /\ ps))
Theorem	qanim1i 12153	Introduce a right conjunct to both sides of an implication.
|- (ph -> ps)   =>   |- ((ph /\ ch) -> (ps /\ ch))
Theorem	qanim2i 12154	Introduce a left conjunct to both sides of an implication.
|- (ph -> ps)   =>   |- ((ch /\ ph) -> (ch /\ ps))
Theorem	qanqan 12155	Conjunction implies "quantum conjunction".
|- ((ph /\ ps) -> -. (ph -> -. ps))
Theorem	qanim12i 12156	Join both sides with conjunct.
|- (ph -> ps)   &   |- (ch -> th)   =>   |- ((ph /\ ch) -> (ps /\ th))
Theorem	qorim12i 12157	Join both sides with disjunction.
|- (ph -> ps)   &   |- (ch -> th)   =>   |- ((ph \/ ch) -> (ps \/ th))
Theorem	qorana 12158	Disjunction in terms of conjunction.
|- ((ph \/ ps) -> -. (-. ph /\ -. ps))
Theorem	qoranb 12159	Disjunction in terms of conjunction.
|- (-. (-. ph /\ -. ps) -> (ph \/ ps))
Theorem	qiorana 12160	Negated disjunction in terms of conjunction (DeMorgan's law).
|- (-. (ph \/ ps) -> (-. ph /\ -. ps))
Theorem	qioranb 12161	Negated disjunction in terms of conjunction (DeMorgan's law).
|- ((-. ph /\ -. ps) -> -. (ph \/ ps))
Theorem	qianora 12162	Negated conjunction in terms of disjunction (DeMorgan's law).
|- (-. (ph /\ ps) -> (-. ph \/ -. ps))
Theorem	qianorb 12163	Negated conjunction in terms of disjunction (DeMorgan's law). Note: see description of quantum logic system Q3 under ax-q1 12105.
|- ((-. ph \/ -. ps) -> -. (ph /\ ps))
Theorem	qanor1a 12164	Conjunction in terms of disjunction.
|- ((ph /\ -. ps) -> -. (-. ph \/ ps))
Theorem	qanor1b 12165	Conjunction in terms of disjunction.
|- (-. (-. ph \/ ps) -> (ph /\ -. ps))
Theorem	qanor2a 12166	Relation between conjunction and disjunction.
|- ((-. ph /\ ps) -> -. (ph \/ -. ps))
Theorem	qanor2b 12167	Relation between conjunction and disjunction.
|- (-. (ph \/ -. ps) -> (-. ph /\ ps))
Theorem	qanabsa 12168	Absorption law. Note: see description of quantum logic system Q3 under ax-q1 12105.
|- ((ph \/ (ph /\ ps)) -> ph)
Theorem	qexclmid 12169	Law of excluded middle.
|- (ph \/ -. ph)
Theorem	qa8a 12170	One direction of Kalmbach's axiom 8.
|- ((-. ph /\ ph) -> ((-. ph /\ ph) /\ ps))
Theorem	qa8b 12171	The other direction of Kalmbach's axiom 8. Note: see description of quantum logic system Q3 under ax-q1 12105.
|- (((-. ph /\ ph) /\ ps) -> (-. ph /\ ph))
Theorem	qorabsa 12172	Absorption law.
|- ((ph /\ (ph \/ ps)) -> ph)
Theorem	qorabsb 12173	Absorption law.
|- (ph -> (ph /\ (ph \/ ps)))
Theorem	q0equiv0a 12174	Theorem justifying a definition of false (by showing that the expression for it is independent of the wff variable).
|- ((-. ph /\ ph) -> (-. ps /\ ps))
Theorem	q1equiv1a 12175	True is equivalent to true.
|- ((ph \/ -. ph) -> (ps \/ -. ps))
Theorem	qanidma 12176	Idempotent law.
|- ((ph /\ ph) -> ph)
Theorem	qanidmb 12177	Idempotent law.
|- (ph -> (ph /\ ph))
Theorem	qoridma 12178	Idempotent law.
|- ((ph \/ ph) -> ph)
Theorem	qoridmb 12179	Idempotent law.
|- (ph -> (ph \/ ph))
Theorem	qanabsb 12180	Absorption law.
|- (ph -> (ph \/ (ph /\ ps)))
Theorem	qorassb 12181	Associative law.
|- ((ph \/ (ps \/ ch)) -> ((ph \/ ps) \/ ch))
Theorem	qanassa 12182	Associative law.
|- (((ph /\ ps) /\ ch) -> (ph /\ (ps /\ ch)))
Theorem	qanassb 12183	Associative law.
|- ((ph /\ (ps /\ ch)) -> ((ph /\ ps) /\ ch))
Theorem	qor12a 12184	Swap disjuncts.
|- ((ph \/ (ps \/ ch)) -> (ps \/ (ph \/ ch)))
Theorem	qan12a 12185	Swap conjuncts.
|- ((ph /\ (ps /\ ch)) -> (ps /\ (ph /\ ch)))
Theorem	qor23a 12186	Swap disjuncts.
|- (((ph \/ ps) \/ ch) -> ((ph \/ ch) \/ ps))
Theorem	qan23a 12187	Swap conjuncts.
|- (((ph /\ ps) /\ ch) -> ((ph /\ ch) /\ ps))
Theorem	qor4a 12188	Swap disjuncts.
|- (((ph \/ ps) \/ (ch \/ th)) -> ((ph \/ ch) \/ (ps \/ th)))
Theorem	qan4a 12189	Swap conjuncts.
|- (((ph /\ ps) /\ (ch /\ th)) -> ((ph /\ ch) /\ (ps /\ th)))
Theorem	qleorana 12190	Discard a conjunct in the antecedent. Note: see description of quantum logic system Q3 under ax-q1 12105.
|- ((ph /\ ps) -> ph)
Mathbox for Steve Rodriguez
Hypergraphs
Syntax	chgra 12191	Extend class notation with the class of all hypergraphs.
class HypGrph
Definition	df-hgra 12192	Define the class of all hypergraphs. For a textbook definition of a hypergraph and more information, see ishgrag 12195.
|- HypGrph = {<.a, b>. | ((a i^i b) = (/) /\ b (_ (P~a \ {(/)}))}
Theorem	blkssatm 12193	Two ways of saying "the blocks in a hypergraph are each non-empty subsets of the set of atoms in the hypergraph."
|- (B (_ (P~A \ {(/)}) <-> A.b e. B (b (_ A /\ b =/= (/)))
Theorem	hgrarel 12194	The class of all hypergraphs is a relation.
|- Rel HypGrph
Theorem	ishgrag 12195	Express the predicate "H is a hypergraph." Definition of hypergraph in [Diestel] p. 28, which states "A hypergraph is a pair (V, E) of disjoint sets, where the elements of E are non-empty subsets (of any cardinality) of V." Because V and E are both used as symbols (for the universal class df-v 1858 and the epsilon relation df-eprel 2910, respectively) in Metamath, we instead use A to represent V, the set of vertices or atoms of the hypergraph, and B to represent E, the set of edges or blocks that each connect one or more atoms in A. (See Definition 2.1 in [McKMegPav] p. 2384 for an analogous use of atom and block in Greechie diagrams.)
|- H = <.A, B>.   =>   |- ((A e. C /\ B e. D) -> (H e. HypGrph <-> ((A i^i B) = (/) /\ A.b e. B (b (_ A /\ b =/= (/)))))
Theorem	hgralem 12196	Lemma for various hypergraph theorems.
Theorem	hgradj 12197	The sets of atoms and blocks in a hypergraph are disjoint.
|- A = (1st` H)   &   |- B = (2nd` H)   =>   |- (H e. HypGrph -> (A i^i B) = (/))
Theorem	hgrablkconn 12198	The blocks in a hypergraph each connect to one or more atoms.
|- A = (1st` H)   &   |- B = (2nd` H)   =>   |- (H e. HypGrph -> B (_ (P~A \ {(/)}))
Theorem	hgrablkne0 12199	The empty set cannot be a block in a hypergraph.
|- B = (2nd` H)   =>   |- (H e. HypGrph -> A.b e. B b =/= (/))
Theorem	hgrablkcard 12200	The number of atoms incident to each block of a hypergraph is greater than zero.
|- B = (2nd` H)   =>   |- (H e. HypGrph -> A.b e. B (/) e. (card` b))