Home | Metamath
Proof Explorer Theorem List (p. 322 of 426) | < Previous Next > |
Browser slow? Try the
Unicode version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | cgrtr3 32101 | Transitivity law for congruence. (Contributed by Scott Fenton, 7-Oct-2013.) |
Cgr Cgr Cgr | ||
Theorem | cgrtr3and 32102 | Deduction form of cgrtr3 32101. (Contributed by Scott Fenton, 13-Oct-2013.) |
Cgr Cgr Cgr | ||
Theorem | cgrcoml 32103 | Congruence commutes on the left. Biconditional version of Theorem 2.4 of [Schwabhauser] p. 27. (Contributed by Scott Fenton, 12-Jun-2013.) |
Cgr Cgr | ||
Theorem | cgrcomr 32104 | Congruence commutes on the right. Biconditional version of Theorem 2.5 of [Schwabhauser] p. 27. (Contributed by Scott Fenton, 12-Jun-2013.) |
Cgr Cgr | ||
Theorem | cgrcomlr 32105 | Congruence commutes on both sides. (Contributed by Scott Fenton, 12-Jun-2013.) |
Cgr Cgr | ||
Theorem | cgrcomland 32106 | Deduction form of cgrcoml 32103. (Contributed by Scott Fenton, 14-Oct-2013.) |
Cgr Cgr | ||
Theorem | cgrcomrand 32107 | Deduction form of cgrcoml 32103. (Contributed by Scott Fenton, 14-Oct-2013.) |
Cgr Cgr | ||
Theorem | cgrcomlrand 32108 | Deduction form of cgrcomlr 32105. (Contributed by Scott Fenton, 14-Oct-2013.) |
Cgr Cgr | ||
Theorem | cgrtriv 32109 | Degenerate segments are congruent. Theorem 2.8 of [Schwabhauser] p. 28. (Contributed by Scott Fenton, 12-Jun-2013.) |
Cgr | ||
Theorem | cgrid2 32110 | Identity law for congruence. (Contributed by Scott Fenton, 12-Jun-2013.) |
Cgr | ||
Theorem | cgrdegen 32111 | Two congruent segments are either both degenerate or both non-degenerate. (Contributed by Scott Fenton, 12-Jun-2013.) |
Cgr | ||
Theorem | brofs 32112 | Binary relation form of the outer five segment predicate. (Contributed by Scott Fenton, 21-Sep-2013.) |
Cgr Cgr Cgr Cgr | ||
Theorem | 5segofs 32113 | Rephrase ax5seg 25818 using the outer five segment predicate. Theorem 2.10 of [Schwabhauser] p. 28. (Contributed by Scott Fenton, 21-Sep-2013.) |
Cgr | ||
Theorem | ofscom 32114 | The outer five segment predicate commutes. (Contributed by Scott Fenton, 26-Sep-2013.) |
Theorem | cgrextend 32115 | Link congruence over a pair of line segments. Theorem 2.11 of [Schwabhauser] p. 29. (Contributed by Scott Fenton, 12-Jun-2013.) |
Cgr Cgr Cgr | ||
Theorem | cgrextendand 32116 | Deduction form of cgrextend 32115. (Contributed by Scott Fenton, 14-Oct-2013.) |
Cgr Cgr Cgr | ||
Theorem | segconeq 32117 | Two points that satsify the conclusion of axsegcon 25807 are identical. Uniqueness portion of Theorem 2.12 of [Schwabhauser] p. 29. (Contributed by Scott Fenton, 12-Jun-2013.) |
Cgr Cgr | ||
Theorem | segconeu 32118* | Existential uniqueness version of segconeq 32117. (Contributed by Scott Fenton, 19-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
Cgr | ||
Theorem | btwntriv2 32119 | Betweenness always holds for the second endpoint. Theorem 3.1 of [Schwabhauser] p. 30. (Contributed by Scott Fenton, 12-Jun-2013.) |
Theorem | btwncomim 32120 | Betweenness commutes. Implication version. Theorem 3.2 of [Schwabhauser] p. 30. (Contributed by Scott Fenton, 12-Jun-2013.) |
Theorem | btwncom 32121 | Betweenness commutes. (Contributed by Scott Fenton, 12-Jun-2013.) |
Theorem | btwncomand 32122 | Deduction form of btwncom 32121. (Contributed by Scott Fenton, 14-Oct-2013.) |
Theorem | btwntriv1 32123 | Betweenness always holds for the first endpoint. Theorem 3.3 of [Schwabhauser] p. 30. (Contributed by Scott Fenton, 12-Jun-2013.) |
Theorem | btwnswapid 32124 | If you can swap the first two arguments of a betweenness statement, then those arguments are identical. Theorem 3.4 of [Schwabhauser] p. 30. (Contributed by Scott Fenton, 12-Jun-2013.) |
Theorem | btwnswapid2 32125 | If you can swap arguments one and three of a betweenness statement, then those arguments are identical. (Contributed by Scott Fenton, 7-Oct-2013.) |
Theorem | btwnintr 32126 | Inner transitivity law for betweenness. Left-hand side of Theorem 3.5 of [Schwabhauser] p. 30. (Contributed by Scott Fenton, 12-Jun-2013.) |
Theorem | btwnexch3 32127 | Exchange the first endpoint in betweenness. Left-hand side of Theorem 3.6 of [Schwabhauser] p. 30. (Contributed by Scott Fenton, 12-Jun-2013.) |
Theorem | btwnexch3and 32128 | Deduction form of btwnexch3 32127. (Contributed by Scott Fenton, 13-Oct-2013.) |
Theorem | btwnouttr2 32129 | Outer transitivity law for betweenness. Left-hand side of Theorem 3.1 of [Schwabhauser] p. 30. (Contributed by Scott Fenton, 12-Jun-2013.) |
Theorem | btwnexch2 32130 | Exchange the outer point of two betweenness statements. Right-hand side of Theorem 3.5 of [Schwabhauser] p. 30. (Contributed by Scott Fenton, 14-Jun-2013.) |
Theorem | btwnouttr 32131 | Outer transitivity law for betweenness. Right-hand side of Theorem 3.7 of [Schwabhauser] p. 30. (Contributed by Scott Fenton, 14-Jun-2013.) |
Theorem | btwnexch 32132 | Outer transitivity law for betweenness. Right-hand side of Theorem 3.6 of [Schwabhauser] p. 30. (Contributed by Scott Fenton, 24-Sep-2013.) |
Theorem | btwnexchand 32133 | Deduction form of btwnexch 32132. (Contributed by Scott Fenton, 13-Oct-2013.) |
Theorem | btwndiff 32134* | There is always a distinct from such that lies between and . Theorem 3.14 of [Schwabhauser] p. 32. (Contributed by Scott Fenton, 24-Sep-2013.) |
Theorem | trisegint 32135* | A line segment between two sides of a triange intersects a segment crossing from the remaining side to the opposite vertex. Theorem 3.17 of [Schwabhauser] p. 33. (Contributed by Scott Fenton, 24-Sep-2013.) |
Syntax | ctransport 32136 | Declare the syntax for the segment transport function. |
TransportTo | ||
Definition | df-transport 32137* | Define the segment transport function. See fvtransport 32139 for an explanation of the function. (Contributed by Scott Fenton, 18-Oct-2013.) |
TransportTo Cgr | ||
Theorem | funtransport 32138 | The TransportTo relationship is a function. (Contributed by Scott Fenton, 18-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
TransportTo | ||
Theorem | fvtransport 32139* | Calculate the value of the TransportTo function. This function takes four points, through , where and are distinct. It then returns the point that extends by the length of . (Contributed by Scott Fenton, 18-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
TransportTo Cgr | ||
Theorem | transportcl 32140 | Closure law for segment transport. (Contributed by Scott Fenton, 19-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
TransportTo | ||
Theorem | transportprops 32141 | Calculate the defining properties of the transport function. (Contributed by Scott Fenton, 19-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
TransportTo TransportTo Cgr | ||
Syntax | cifs 32142 | Declare the syntax for the inner five segment predicate. |
Syntax | ccgr3 32143 | Declare the syntax for the three place congruence predicate. |
Cgr3 | ||
Syntax | ccolin 32144 | Declare the syntax for the colinearity predicate. |
Syntax | cfs 32145 | Declare the syntax for the five segment predicate. |
Definition | df-colinear 32146* | The colinearity predicate states that the three points in its arguments sit on one line. Definition 4.10 of [Schwabhauser] p. 36. (Contributed by Scott Fenton, 25-Oct-2013.) |
Definition | df-ifs 32147* | The inner five segment configuration is an abbreviation for another congruence condition. See brifs 32150 and ifscgr 32151 for how it is used. Definition 4.1 of [Schwabhauser] p. 34. (Contributed by Scott Fenton, 26-Sep-2013.) |
Cgr Cgr Cgr Cgr | ||
Definition | df-cgr3 32148* | The three place congruence predicate. This is an abbreviation for saying that all three pair in a triple are congruent with each other. Three place form of Definition 4.4 of [Schwabhauser] p. 35. (Contributed by Scott Fenton, 4-Oct-2013.) |
Cgr3 Cgr Cgr Cgr | ||
Definition | df-fs 32149* | The general five segment configuration is a generalization of the outer and inner five segment configurations. See brfs 32186 and fscgr 32187 for its use. Definition 4.15 of [Schwabhauser] p. 37. (Contributed by Scott Fenton, 5-Oct-2013.) |
Cgr3 Cgr Cgr | ||
Theorem | brifs 32150 | Binary relation form of the inner five segment predicate. (Contributed by Scott Fenton, 26-Sep-2013.) |
Cgr Cgr Cgr Cgr | ||
Theorem | ifscgr 32151 | Inner five segment congruence. Take two triangles, and , with between and and between and . If the other components of the triangles are congruent, then so are and . Theorem 4.2 of [Schwabhauser] p. 34. (Contributed by Scott Fenton, 27-Sep-2013.) |
Cgr | ||
Theorem | cgrsub 32152 | Removing identical parts from the end of a line segment preserves congruence. Theorem 4.3 of [Schwabhauser] p. 35. (Contributed by Scott Fenton, 4-Oct-2013.) |
Cgr Cgr Cgr | ||
Theorem | brcgr3 32153 | Binary relation form of the three-place congruence predicate. (Contributed by Scott Fenton, 4-Oct-2013.) |
Cgr3 Cgr Cgr Cgr | ||
Theorem | cgr3permute3 32154 | Permutation law for three-place congruence. (Contributed by Scott Fenton, 5-Oct-2013.) |
Cgr3 Cgr3 | ||
Theorem | cgr3permute1 32155 | Permutation law for three-place congruence. (Contributed by Scott Fenton, 5-Oct-2013.) |
Cgr3 Cgr3 | ||
Theorem | cgr3permute2 32156 | Permutation law for three-place congruence. (Contributed by Scott Fenton, 5-Oct-2013.) |
Cgr3 Cgr3 | ||
Theorem | cgr3permute4 32157 | Permutation law for three-place congruence. (Contributed by Scott Fenton, 5-Oct-2013.) |
Cgr3 Cgr3 | ||
Theorem | cgr3permute5 32158 | Permutation law for three-place congruence. (Contributed by Scott Fenton, 5-Oct-2013.) |
Cgr3 Cgr3 | ||
Theorem | cgr3tr4 32159 | Transitivity law for three-place congruence. (Contributed by Scott Fenton, 5-Oct-2013.) |
Cgr3 Cgr3 Cgr3 | ||
Theorem | cgr3com 32160 | Commutativity law for three-place congruence. (Contributed by Scott Fenton, 5-Oct-2013.) |
Cgr3 Cgr3 | ||
Theorem | cgr3rflx 32161 | Identity law for three-place congruence. (Contributed by Scott Fenton, 6-Oct-2013.) |
Cgr3 | ||
Theorem | cgrxfr 32162* | A line segment can be divided at the same place as a congruent line segment is divided. Theorem 4.5 of [Schwabhauser] p. 35. (Contributed by Scott Fenton, 4-Oct-2013.) |
Cgr Cgr3 | ||
Theorem | btwnxfr 32163 | A condition for extending betweenness to a new set of points based on congruence with another set of points. Theorem 4.6 of [Schwabhauser] p. 36. (Contributed by Scott Fenton, 4-Oct-2013.) |
Cgr3 | ||
Theorem | colinrel 32164 | Colinearity is a relationship. (Contributed by Scott Fenton, 7-Nov-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
Theorem | brcolinear2 32165* | Alternate colinearity binary relation. (Contributed by Scott Fenton, 7-Nov-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
Theorem | brcolinear 32166 | The binary relation form of the colinearity predicate. (Contributed by Scott Fenton, 5-Oct-2013.) |
Theorem | colinearex 32167 | The colinear predicate exists. (Contributed by Scott Fenton, 25-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
Theorem | colineardim1 32168 | If is colinear with and , then is in the same space as . (Contributed by Scott Fenton, 25-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
Theorem | colinearperm1 32169 | Permutation law for colinearity. Part of theorem 4.11 of [Schwabhauser] p. 36. (Contributed by Scott Fenton, 5-Oct-2013.) |
Theorem | colinearperm3 32170 | Permutation law for colinearity. Part of theorem 4.11 of [Schwabhauser] p. 36. (Contributed by Scott Fenton, 5-Oct-2013.) |
Theorem | colinearperm2 32171 | Permutation law for colinearity. Part of theorem 4.11 of [Schwabhauser] p. 36. (Contributed by Scott Fenton, 5-Oct-2013.) |
Theorem | colinearperm4 32172 | Permutation law for colinearity. Part of theorem 4.11 of [Schwabhauser] p. 36. (Contributed by Scott Fenton, 5-Oct-2013.) |
Theorem | colinearperm5 32173 | Permutation law for colinearity. Part of theorem 4.11 of [Schwabhauser] p. 36. (Contributed by Scott Fenton, 5-Oct-2013.) |
Theorem | colineartriv1 32174 | Trivial case of colinearity. Theorem 4.12 of [Schwabhauser] p. 37. (Contributed by Scott Fenton, 5-Oct-2013.) |
Theorem | colineartriv2 32175 | Trivial case of colinearity. (Contributed by Scott Fenton, 18-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
Theorem | btwncolinear1 32176 | Betweenness implies colinearity. (Contributed by Scott Fenton, 7-Oct-2013.) |
Theorem | btwncolinear2 32177 | Betweenness implies colinearity. (Contributed by Scott Fenton, 15-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
Theorem | btwncolinear3 32178 | Betweenness implies colinearity. (Contributed by Scott Fenton, 15-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
Theorem | btwncolinear4 32179 | Betweenness implies colinearity. (Contributed by Scott Fenton, 15-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
Theorem | btwncolinear5 32180 | Betweenness implies colinearity. (Contributed by Scott Fenton, 15-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
Theorem | btwncolinear6 32181 | Betweenness implies colinearity. (Contributed by Scott Fenton, 15-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
Theorem | colinearxfr 32182 | Transfer law for colinearity. Theorem 4.13 of [Schwabhauser] p. 37. (Contributed by Scott Fenton, 5-Oct-2013.) |
Cgr3 | ||
Theorem | lineext 32183* | Extend a line with a missing point. Theorem 4.14 of [Schwabhauser] p. 37. (Contributed by Scott Fenton, 6-Oct-2013.) |
Cgr Cgr3 | ||
Theorem | brofs2 32184 | Change some conditions for outer five segment predicate. (Contributed by Scott Fenton, 6-Oct-2013.) |
Cgr3 Cgr Cgr | ||
Theorem | brifs2 32185 | Change some conditions for inner five segment predicate. (Contributed by Scott Fenton, 6-Oct-2013.) |
Cgr3 Cgr Cgr | ||
Theorem | brfs 32186 | Binary relation form of the general five segment predicate. (Contributed by Scott Fenton, 5-Oct-2013.) |
Cgr3 Cgr Cgr | ||
Theorem | fscgr 32187 | Congruence law for the general five segment configuration. Theorem 4.16 of [Schwabhauser] p. 37. (Contributed by Scott Fenton, 5-Oct-2013.) |
Cgr | ||
Theorem | linecgr 32188 | Congruence rule for lines. Theorem 4.17 of [Schwabhauser] p. 37. (Contributed by Scott Fenton, 6-Oct-2013.) |
Cgr Cgr Cgr | ||
Theorem | linecgrand 32189 | Deduction form of linecgr 32188. (Contributed by Scott Fenton, 14-Oct-2013.) |
Cgr Cgr Cgr | ||
Theorem | lineid 32190 | Identity law for points on lines. Theorem 4.18 of [Schwabhauser] p. 38. (Contributed by Scott Fenton, 7-Oct-2013.) |
Cgr Cgr | ||
Theorem | idinside 32191 | Law for finding a point inside a segment. Theorem 4.19 of [Schwabhauser] p. 38. (Contributed by Scott Fenton, 7-Oct-2013.) |
Cgr Cgr | ||
Theorem | endofsegid 32192 | If , , and fall in order on a line, and and are congruent, then . (Contributed by Scott Fenton, 7-Oct-2013.) |
Cgr | ||
Theorem | endofsegidand 32193 | Deduction form of endofsegid 32192. (Contributed by Scott Fenton, 15-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
Cgr | ||
Theorem | btwnconn1lem1 32194 | Lemma for btwnconn1 32208. The next several lemmas introduce various properties of hypothetical points that end up eliminating alternatives to connectivity. We begin by showing a congruence property of those hypothetical points. (Contributed by Scott Fenton, 8-Oct-2013.) |
Cgr Cgr Cgr Cgr Cgr | ||
Theorem | btwnconn1lem2 32195 | Lemma for btwnconn1 32208. Now, we show that two of the hypotheticals we introduced in the first lemma are identical. (Contributed by Scott Fenton, 8-Oct-2013.) |
Cgr Cgr Cgr Cgr | ||
Theorem | btwnconn1lem3 32196 | Lemma for btwnconn1 32208. Establish the next congruence in the series. (Contributed by Scott Fenton, 8-Oct-2013.) |
Cgr Cgr Cgr Cgr Cgr | ||
Theorem | btwnconn1lem4 32197 | Lemma for btwnconn1 32208. Assuming , we now attempt to force from here out via a series of congruences. (Contributed by Scott Fenton, 8-Oct-2013.) |
Cgr Cgr Cgr Cgr Cgr | ||
Theorem | btwnconn1lem5 32198 | Lemma for btwnconn1 32208. Now, we introduce , the intersection of and . We begin by showing that it is the midpoint of and . (Contributed by Scott Fenton, 8-Oct-2013.) |
Cgr Cgr Cgr Cgr Cgr | ||
Theorem | btwnconn1lem6 32199 | Lemma for btwnconn1 32208. Next, we show that is the midpoint of and . (Contributed by Scott Fenton, 8-Oct-2013.) |
Cgr Cgr Cgr Cgr Cgr | ||
Theorem | btwnconn1lem7 32200 | Lemma for btwnconn1 32208. Under our assumptions, and are distinct. (Contributed by Scott Fenton, 8-Oct-2013.) |
Cgr Cgr Cgr Cgr |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |