Home | Metamath
Proof Explorer Theorem List (p. 313 of 424) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-27159) |
Hilbert Space Explorer
(27160-28684) |
Users' Mathboxes
(28685-42360) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | dffv5 31201 | Another quantifier free definition of function value. (Contributed by Scott Fenton, 19-Feb-2013.) |
⊢ (𝐹‘𝐴) = ∪ ∪ ({(𝐹 “ {𝐴})} ∩ Singletons ) | ||
Theorem | unisnif 31202 | Express union of singleton in terms of if. (Contributed by Scott Fenton, 27-Mar-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ ∪ {𝐴} = if(𝐴 ∈ V, 𝐴, ∅) | ||
Theorem | brimage 31203 | Binary relationship form of the Image functor. (Contributed by Scott Fenton, 4-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴Image𝑅𝐵 ↔ 𝐵 = (𝑅 “ 𝐴)) | ||
Theorem | brimageg 31204 | Closed form of brimage 31203. (Contributed by Scott Fenton, 4-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴Image𝑅𝐵 ↔ 𝐵 = (𝑅 “ 𝐴))) | ||
Theorem | funimage 31205 | Image𝐴 is a function. (Contributed by Scott Fenton, 27-Mar-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ Fun Image𝐴 | ||
Theorem | fnimage 31206* | Image𝑅 is a function over the set-like portion of 𝑅. (Contributed by Scott Fenton, 4-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ Image𝑅 Fn {𝑥 ∣ (𝑅 “ 𝑥) ∈ V} | ||
Theorem | imageval 31207* | The image functor in maps-to notation. (Contributed by Scott Fenton, 4-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ Image𝑅 = (𝑥 ∈ V ↦ (𝑅 “ 𝑥)) | ||
Theorem | fvimage 31208 | The value of the image functor. (Contributed by Scott Fenton, 4-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑅 “ 𝐴) ∈ 𝑊) → (Image𝑅‘𝐴) = (𝑅 “ 𝐴)) | ||
Theorem | brcart 31209 | Binary relationship form of the cartesian product operator. (Contributed by Scott Fenton, 11-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V ⇒ ⊢ (〈𝐴, 𝐵〉Cart𝐶 ↔ 𝐶 = (𝐴 × 𝐵)) | ||
Theorem | brdomain 31210 | The binary relationship form of the domain function. (Contributed by Scott Fenton, 11-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴Domain𝐵 ↔ 𝐵 = dom 𝐴) | ||
Theorem | brrange 31211 | The binary relationship form of the range function. (Contributed by Scott Fenton, 11-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴Range𝐵 ↔ 𝐵 = ran 𝐴) | ||
Theorem | brdomaing 31212 | Closed form of brdomain 31210. (Contributed by Scott Fenton, 2-May-2014.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴Domain𝐵 ↔ 𝐵 = dom 𝐴)) | ||
Theorem | brrangeg 31213 | Closed form of brrange 31211. (Contributed by Scott Fenton, 3-May-2014.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴Range𝐵 ↔ 𝐵 = ran 𝐴)) | ||
Theorem | brimg 31214 | The binary relationship form of the Img function. (Contributed by Scott Fenton, 12-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V ⇒ ⊢ (〈𝐴, 𝐵〉Img𝐶 ↔ 𝐶 = (𝐴 “ 𝐵)) | ||
Theorem | brapply 31215 | The binary relationship form of the Apply function. (Contributed by Scott Fenton, 12-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V ⇒ ⊢ (〈𝐴, 𝐵〉Apply𝐶 ↔ 𝐶 = (𝐴‘𝐵)) | ||
Theorem | brcup 31216 | Binary relationship form of the Cup function. (Contributed by Scott Fenton, 14-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V ⇒ ⊢ (〈𝐴, 𝐵〉Cup𝐶 ↔ 𝐶 = (𝐴 ∪ 𝐵)) | ||
Theorem | brcap 31217 | Binary relationship form of the Cap function. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V ⇒ ⊢ (〈𝐴, 𝐵〉Cap𝐶 ↔ 𝐶 = (𝐴 ∩ 𝐵)) | ||
Theorem | brsuccf 31218 | Binary relationship form of the Succ function. (Contributed by Scott Fenton, 14-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴Succ𝐵 ↔ 𝐵 = suc 𝐴) | ||
Theorem | funpartlem 31219* | Lemma for funpartfun 31220. Show membership in the restriction. (Contributed by Scott Fenton, 4-Dec-2017.) |
⊢ (𝐴 ∈ dom ((Image𝐹 ∘ Singleton) ∩ (V × Singletons )) ↔ ∃𝑥(𝐹 “ {𝐴}) = {𝑥}) | ||
Theorem | funpartfun 31220 | The functional part of 𝐹 is a function. (Contributed by Scott Fenton, 16-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ Fun Funpart𝐹 | ||
Theorem | funpartss 31221 | The functional part of 𝐹 is a subset of 𝐹. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ Funpart𝐹 ⊆ 𝐹 | ||
Theorem | funpartfv 31222 | The function value of the functional part is identical to the original functional value. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ (Funpart𝐹‘𝐴) = (𝐹‘𝐴) | ||
Theorem | fullfunfnv 31223 | The full functional part of 𝐹 is a function over V. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ FullFun𝐹 Fn V | ||
Theorem | fullfunfv 31224 | The function value of the full function of 𝐹 agrees with 𝐹. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ (FullFun𝐹‘𝐴) = (𝐹‘𝐴) | ||
Theorem | brfullfun 31225 | A binary relationship form condition for the full function. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴FullFun𝐹𝐵 ↔ 𝐵 = (𝐹‘𝐴)) | ||
Theorem | brrestrict 31226 | The binary relationship form of the Restrict function. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V ⇒ ⊢ (〈𝐴, 𝐵〉Restrict𝐶 ↔ 𝐶 = (𝐴 ↾ 𝐵)) | ||
Theorem | dfrecs2 31227 | A quantifier-free definition of recs. (Contributed by Scott Fenton, 17-Jul-2020.) |
⊢ recs(𝐹) = ∪ (( Funs ∩ (◡Domain “ On)) ∖ dom ((◡ E ∘ Domain) ∖ Fix (◡Apply ∘ (FullFun𝐹 ∘ Restrict)))) | ||
Theorem | dfrdg4 31228 | A quantifier-free definition of the recursive definition generator. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ rec(𝐹, 𝐴) = ∪ (( Funs ∩ (◡Domain “ On)) ∖ dom ((◡ E ∘ Domain) ∖ Fix (◡Apply ∘ (((V × {∅}) × {∪ {𝐴}}) ∪ ((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ))))))) | ||
Theorem | dfint3 31229 | Quantifier-free definition of class intersection. (Contributed by Scott Fenton, 13-Apr-2018.) |
⊢ ∩ 𝐴 = (V ∖ (◡(V ∖ E ) “ 𝐴)) | ||
Theorem | imagesset 31230 | The Image functor applied to the converse of the subset relationship yields a subset of the subset relationship. (Contributed by Scott Fenton, 14-Apr-2018.) |
⊢ Image◡ SSet ⊆ SSet | ||
Theorem | brub 31231* | Binary relationship form of the upper bound functor. (Contributed by Scott Fenton, 3-May-2018.) |
⊢ 𝑆 ∈ V & ⊢ 𝐴 ∈ V ⇒ ⊢ (𝑆UB𝑅𝐴 ↔ ∀𝑥 ∈ 𝑆 𝑥𝑅𝐴) | ||
Theorem | brlb 31232* | Binary relationship form of the lower bound functor. (Contributed by Scott Fenton, 3-May-2018.) |
⊢ 𝑆 ∈ V & ⊢ 𝐴 ∈ V ⇒ ⊢ (𝑆LB𝑅𝐴 ↔ ∀𝑥 ∈ 𝑆 𝐴𝑅𝑥) | ||
Syntax | caltop 31233 | Declare the syntax for an alternate ordered pair. |
class ⟪𝐴, 𝐵⟫ | ||
Syntax | caltxp 31234 | Declare the syntax for an alternate Cartesian product. |
class (𝐴 ×× 𝐵) | ||
Definition | df-altop 31235 | An alternative definition of ordered pairs. This definition removes a hypothesis from its defining theorem (see altopth 31246), making it more convenient in some circumstances. (Contributed by Scott Fenton, 22-Mar-2012.) |
⊢ ⟪𝐴, 𝐵⟫ = {{𝐴}, {𝐴, {𝐵}}} | ||
Definition | df-altxp 31236* | Define Cartesian products of alternative ordered pairs. (Contributed by Scott Fenton, 23-Mar-2012.) |
⊢ (𝐴 ×× 𝐵) = {𝑧 ∣ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑧 = ⟪𝑥, 𝑦⟫} | ||
Theorem | altopex 31237 | Alternative ordered pairs always exist. (Contributed by Scott Fenton, 22-Mar-2012.) |
⊢ ⟪𝐴, 𝐵⟫ ∈ V | ||
Theorem | altopthsn 31238 | Two alternate ordered pairs are equal iff the singletons of their respective elements are equal. Note that this holds regardless of sethood of any of the elements. (Contributed by Scott Fenton, 16-Apr-2012.) |
⊢ (⟪𝐴, 𝐵⟫ = ⟪𝐶, 𝐷⟫ ↔ ({𝐴} = {𝐶} ∧ {𝐵} = {𝐷})) | ||
Theorem | altopeq12 31239 | Equality for alternate ordered pairs. (Contributed by Scott Fenton, 22-Mar-2012.) |
⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → ⟪𝐴, 𝐶⟫ = ⟪𝐵, 𝐷⟫) | ||
Theorem | altopeq1 31240 | Equality for alternate ordered pairs. (Contributed by Scott Fenton, 22-Mar-2012.) |
⊢ (𝐴 = 𝐵 → ⟪𝐴, 𝐶⟫ = ⟪𝐵, 𝐶⟫) | ||
Theorem | altopeq2 31241 | Equality for alternate ordered pairs. (Contributed by Scott Fenton, 22-Mar-2012.) |
⊢ (𝐴 = 𝐵 → ⟪𝐶, 𝐴⟫ = ⟪𝐶, 𝐵⟫) | ||
Theorem | altopth1 31242 | Equality of the first members of equal alternate ordered pairs, which holds regardless of the second members' sethood. (Contributed by Scott Fenton, 22-Mar-2012.) |
⊢ (𝐴 ∈ 𝑉 → (⟪𝐴, 𝐵⟫ = ⟪𝐶, 𝐷⟫ → 𝐴 = 𝐶)) | ||
Theorem | altopth2 31243 | Equality of the second members of equal alternate ordered pairs, which holds regardless of the first members' sethood. (Contributed by Scott Fenton, 22-Mar-2012.) |
⊢ (𝐵 ∈ 𝑉 → (⟪𝐴, 𝐵⟫ = ⟪𝐶, 𝐷⟫ → 𝐵 = 𝐷)) | ||
Theorem | altopthg 31244 | Alternate ordered pair theorem. (Contributed by Scott Fenton, 22-Mar-2012.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (⟪𝐴, 𝐵⟫ = ⟪𝐶, 𝐷⟫ ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))) | ||
Theorem | altopthbg 31245 | Alternate ordered pair theorem. (Contributed by Scott Fenton, 14-Apr-2012.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐷 ∈ 𝑊) → (⟪𝐴, 𝐵⟫ = ⟪𝐶, 𝐷⟫ ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))) | ||
Theorem | altopth 31246 | The alternate ordered pair theorem. If two alternate ordered pairs are equal, their first elements are equal and their second elements are equal. Note that 𝐶 and 𝐷 are not required to be a set due to a peculiarity of our specific ordered pair definition, as opposed to the regular ordered pairs used here, which (as in opth 4871), requires 𝐷 to be a set. (Contributed by Scott Fenton, 23-Mar-2012.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (⟪𝐴, 𝐵⟫ = ⟪𝐶, 𝐷⟫ ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)) | ||
Theorem | altopthb 31247 | Alternate ordered pair theorem with different sethood requirements. See altopth 31246 for more comments. (Contributed by Scott Fenton, 14-Apr-2012.) |
⊢ 𝐴 ∈ V & ⊢ 𝐷 ∈ V ⇒ ⊢ (⟪𝐴, 𝐵⟫ = ⟪𝐶, 𝐷⟫ ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)) | ||
Theorem | altopthc 31248 | Alternate ordered pair theorem with different sethood requirements. See altopth 31246 for more comments. (Contributed by Scott Fenton, 14-Apr-2012.) |
⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V ⇒ ⊢ (⟪𝐴, 𝐵⟫ = ⟪𝐶, 𝐷⟫ ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)) | ||
Theorem | altopthd 31249 | Alternate ordered pair theorem with different sethood requirements. See altopth 31246 for more comments. (Contributed by Scott Fenton, 14-Apr-2012.) |
⊢ 𝐶 ∈ V & ⊢ 𝐷 ∈ V ⇒ ⊢ (⟪𝐴, 𝐵⟫ = ⟪𝐶, 𝐷⟫ ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)) | ||
Theorem | altxpeq1 31250 | Equality for alternate Cartesian products. (Contributed by Scott Fenton, 24-Mar-2012.) |
⊢ (𝐴 = 𝐵 → (𝐴 ×× 𝐶) = (𝐵 ×× 𝐶)) | ||
Theorem | altxpeq2 31251 | Equality for alternate Cartesian products. (Contributed by Scott Fenton, 24-Mar-2012.) |
⊢ (𝐴 = 𝐵 → (𝐶 ×× 𝐴) = (𝐶 ×× 𝐵)) | ||
Theorem | elaltxp 31252* | Membership in alternate Cartesian products. (Contributed by Scott Fenton, 23-Mar-2012.) |
⊢ (𝑋 ∈ (𝐴 ×× 𝐵) ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑋 = ⟪𝑥, 𝑦⟫) | ||
Theorem | altopelaltxp 31253 | Alternate ordered pair membership in a Cartesian product. Note that, unlike opelxp 5070, there is no sethood requirement here. (Contributed by Scott Fenton, 22-Mar-2012.) |
⊢ (⟪𝑋, 𝑌⟫ ∈ (𝐴 ×× 𝐵) ↔ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵)) | ||
Theorem | altxpsspw 31254 | An inclusion rule for alternate Cartesian products. (Contributed by Scott Fenton, 24-Mar-2012.) |
⊢ (𝐴 ×× 𝐵) ⊆ 𝒫 𝒫 (𝐴 ∪ 𝒫 𝐵) | ||
Theorem | altxpexg 31255 | The alternate Cartesian product of two sets is a set. (Contributed by Scott Fenton, 24-Mar-2012.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ×× 𝐵) ∈ V) | ||
Theorem | rankaltopb 31256 | Compute the rank of an alternate ordered pair. (Contributed by Scott Fenton, 18-Dec-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ ((𝐴 ∈ ∪ (𝑅1 “ On) ∧ 𝐵 ∈ ∪ (𝑅1 “ On)) → (rank‘⟪𝐴, 𝐵⟫) = suc suc ((rank‘𝐴) ∪ suc (rank‘𝐵))) | ||
Theorem | nfaltop 31257 | Bound-variable hypothesis builder for alternate ordered pairs. (Contributed by Scott Fenton, 25-Sep-2015.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥⟪𝐴, 𝐵⟫ | ||
Theorem | sbcaltop 31258* | Distribution of class substitution over alternate ordered pairs. (Contributed by Scott Fenton, 25-Sep-2015.) |
⊢ (𝐴 ∈ V → ⦋𝐴 / 𝑥⦌⟪𝐶, 𝐷⟫ = ⟪⦋𝐴 / 𝑥⦌𝐶, ⦋𝐴 / 𝑥⦌𝐷⟫) | ||
Syntax | cofs 31259 | Declare the syntax for the outer five segment configuration. |
class OuterFiveSeg | ||
Definition | df-ofs 31260* | The outer five segment configuration is an abbreviation for the conditions of the Five Segment Axiom (ax5seg 25618). See brofs 31282 and 5segofs 31283 for how it is used. Definition 2.10 of [Schwabhauser] p. 28. (Contributed by Scott Fenton, 21-Sep-2013.) |
⊢ OuterFiveSeg = {〈𝑝, 𝑞〉 ∣ ∃𝑛 ∈ ℕ ∃𝑎 ∈ (𝔼‘𝑛)∃𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)∃𝑥 ∈ (𝔼‘𝑛)∃𝑦 ∈ (𝔼‘𝑛)∃𝑧 ∈ (𝔼‘𝑛)∃𝑤 ∈ (𝔼‘𝑛)(𝑝 = 〈〈𝑎, 𝑏〉, 〈𝑐, 𝑑〉〉 ∧ 𝑞 = 〈〈𝑥, 𝑦〉, 〈𝑧, 𝑤〉〉 ∧ ((𝑏 Btwn 〈𝑎, 𝑐〉 ∧ 𝑦 Btwn 〈𝑥, 𝑧〉) ∧ (〈𝑎, 𝑏〉Cgr〈𝑥, 𝑦〉 ∧ 〈𝑏, 𝑐〉Cgr〈𝑦, 𝑧〉) ∧ (〈𝑎, 𝑑〉Cgr〈𝑥, 𝑤〉 ∧ 〈𝑏, 𝑑〉Cgr〈𝑦, 𝑤〉)))} | ||
Theorem | cgrrflx2d 31261 | Deduction form of axcgrrflx 25594. (Contributed by Scott Fenton, 13-Oct-2013.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐴 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐵 ∈ (𝔼‘𝑁)) ⇒ ⊢ (𝜑 → 〈𝐴, 𝐵〉Cgr〈𝐵, 𝐴〉) | ||
Theorem | cgrtr4d 31262 | Deduction form of axcgrtr 25595. (Contributed by Scott Fenton, 13-Oct-2013.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐴 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐵 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐶 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐷 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐸 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐹 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 〈𝐴, 𝐵〉Cgr〈𝐶, 𝐷〉) & ⊢ (𝜑 → 〈𝐴, 𝐵〉Cgr〈𝐸, 𝐹〉) ⇒ ⊢ (𝜑 → 〈𝐶, 𝐷〉Cgr〈𝐸, 𝐹〉) | ||
Theorem | cgrtr4and 31263 | Deduction form of axcgrtr 25595. (Contributed by Scott Fenton, 13-Oct-2013.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐴 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐵 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐶 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐷 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐸 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐹 ∈ (𝔼‘𝑁)) & ⊢ ((𝜑 ∧ 𝜓) → 〈𝐴, 𝐵〉Cgr〈𝐶, 𝐷〉) & ⊢ ((𝜑 ∧ 𝜓) → 〈𝐴, 𝐵〉Cgr〈𝐸, 𝐹〉) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 〈𝐶, 𝐷〉Cgr〈𝐸, 𝐹〉) | ||
Theorem | cgrrflx 31264 | Reflexivity law for congruence. Theorem 2.1 of [Schwabhauser] p. 27. (Contributed by Scott Fenton, 12-Jun-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) → 〈𝐴, 𝐵〉Cgr〈𝐴, 𝐵〉) | ||
Theorem | cgrrflxd 31265 | Deduction form of cgrrflx 31264. (Contributed by Scott Fenton, 13-Oct-2013.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐴 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐵 ∈ (𝔼‘𝑁)) ⇒ ⊢ (𝜑 → 〈𝐴, 𝐵〉Cgr〈𝐴, 𝐵〉) | ||
Theorem | cgrcomim 31266 | Congruence commutes on the two sides. Implication version. Theorem 2.2 of [Schwabhauser] p. 27. (Contributed by Scott Fenton, 12-Jun-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → (〈𝐴, 𝐵〉Cgr〈𝐶, 𝐷〉 → 〈𝐶, 𝐷〉Cgr〈𝐴, 𝐵〉)) | ||
Theorem | cgrcom 31267 | Congruence commutes between the two sides. (Contributed by Scott Fenton, 12-Jun-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → (〈𝐴, 𝐵〉Cgr〈𝐶, 𝐷〉 ↔ 〈𝐶, 𝐷〉Cgr〈𝐴, 𝐵〉)) | ||
Theorem | cgrcomand 31268 | Deduction form of cgrcom 31267. (Contributed by Scott Fenton, 13-Oct-2013.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐴 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐵 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐶 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐷 ∈ (𝔼‘𝑁)) & ⊢ ((𝜑 ∧ 𝜓) → 〈𝐴, 𝐵〉Cgr〈𝐶, 𝐷〉) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 〈𝐶, 𝐷〉Cgr〈𝐴, 𝐵〉) | ||
Theorem | cgrtr 31269 | Transitivity law for congruence. Theorem 2.3 of [Schwabhauser] p. 27. (Contributed by Scott Fenton, 24-Sep-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) → ((〈𝐴, 𝐵〉Cgr〈𝐶, 𝐷〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐸, 𝐹〉) → 〈𝐴, 𝐵〉Cgr〈𝐸, 𝐹〉)) | ||
Theorem | cgrtrand 31270 | Deduction form of cgrtr 31269. (Contributed by Scott Fenton, 13-Oct-2013.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐴 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐵 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐶 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐷 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐸 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐹 ∈ (𝔼‘𝑁)) & ⊢ ((𝜑 ∧ 𝜓) → 〈𝐴, 𝐵〉Cgr〈𝐶, 𝐷〉) & ⊢ ((𝜑 ∧ 𝜓) → 〈𝐶, 𝐷〉Cgr〈𝐸, 𝐹〉) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 〈𝐴, 𝐵〉Cgr〈𝐸, 𝐹〉) | ||
Theorem | cgrtr3 31271 | Transitivity law for congruence. (Contributed by Scott Fenton, 7-Oct-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) → ((〈𝐴, 𝐵〉Cgr〈𝐸, 𝐹〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐸, 𝐹〉) → 〈𝐴, 𝐵〉Cgr〈𝐶, 𝐷〉)) | ||
Theorem | cgrtr3and 31272 | Deduction form of cgrtr3 31271. (Contributed by Scott Fenton, 13-Oct-2013.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐴 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐵 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐶 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐷 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐸 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐹 ∈ (𝔼‘𝑁)) & ⊢ ((𝜑 ∧ 𝜓) → 〈𝐴, 𝐵〉Cgr〈𝐸, 𝐹〉) & ⊢ ((𝜑 ∧ 𝜓) → 〈𝐶, 𝐷〉Cgr〈𝐸, 𝐹〉) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 〈𝐴, 𝐵〉Cgr〈𝐶, 𝐷〉) | ||
Theorem | cgrcoml 31273 | 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 31274 | 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 31275 | Congruence commutes on both sides. (Contributed by Scott Fenton, 12-Jun-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → (〈𝐴, 𝐵〉Cgr〈𝐶, 𝐷〉 ↔ 〈𝐵, 𝐴〉Cgr〈𝐷, 𝐶〉)) | ||
Theorem | cgrcomland 31276 | Deduction form of cgrcoml 31273. (Contributed by Scott Fenton, 14-Oct-2013.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐴 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐵 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐶 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐷 ∈ (𝔼‘𝑁)) & ⊢ ((𝜑 ∧ 𝜓) → 〈𝐴, 𝐵〉Cgr〈𝐶, 𝐷〉) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 〈𝐵, 𝐴〉Cgr〈𝐶, 𝐷〉) | ||
Theorem | cgrcomrand 31277 | Deduction form of cgrcoml 31273. (Contributed by Scott Fenton, 14-Oct-2013.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐴 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐵 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐶 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐷 ∈ (𝔼‘𝑁)) & ⊢ ((𝜑 ∧ 𝜓) → 〈𝐴, 𝐵〉Cgr〈𝐶, 𝐷〉) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 〈𝐴, 𝐵〉Cgr〈𝐷, 𝐶〉) | ||
Theorem | cgrcomlrand 31278 | Deduction form of cgrcomlr 31275. (Contributed by Scott Fenton, 14-Oct-2013.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐴 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐵 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐶 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐷 ∈ (𝔼‘𝑁)) & ⊢ ((𝜑 ∧ 𝜓) → 〈𝐴, 𝐵〉Cgr〈𝐶, 𝐷〉) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 〈𝐵, 𝐴〉Cgr〈𝐷, 𝐶〉) | ||
Theorem | cgrtriv 31279 | Degenerate segments are congruent. Theorem 2.8 of [Schwabhauser] p. 28. (Contributed by Scott Fenton, 12-Jun-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) → 〈𝐴, 𝐴〉Cgr〈𝐵, 𝐵〉) | ||
Theorem | cgrid2 31280 | Identity law for congruence. (Contributed by Scott Fenton, 12-Jun-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → (〈𝐴, 𝐴〉Cgr〈𝐵, 𝐶〉 → 𝐵 = 𝐶)) | ||
Theorem | cgrdegen 31281 | Two congruent segments are either both degenrate or both non-degenerate. (Contributed by Scott Fenton, 12-Jun-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → (〈𝐴, 𝐵〉Cgr〈𝐶, 𝐷〉 → (𝐴 = 𝐵 ↔ 𝐶 = 𝐷))) | ||
Theorem | brofs 31282 | Binary relationship form of the outer five segment predicate. (Contributed by Scott Fenton, 21-Sep-2013.) |
⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → (〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 OuterFiveSeg 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 ↔ ((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐹 Btwn 〈𝐸, 𝐺〉) ∧ (〈𝐴, 𝐵〉Cgr〈𝐸, 𝐹〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝐹, 𝐺〉) ∧ (〈𝐴, 𝐷〉Cgr〈𝐸, 𝐻〉 ∧ 〈𝐵, 𝐷〉Cgr〈𝐹, 𝐻〉)))) | ||
Theorem | 5segofs 31283 | Rephrase ax5seg 25618 using the outer five segment predicate. Theorem 2.10 of [Schwabhauser] p. 28. (Contributed by Scott Fenton, 21-Sep-2013.) |
⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → ((〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 OuterFiveSeg 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 ∧ 𝐴 ≠ 𝐵) → 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉)) | ||
Theorem | ofscom 31284 | The outer five segment predicate commutes. (Contributed by Scott Fenton, 26-Sep-2013.) |
⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → (〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 OuterFiveSeg 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 ↔ 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 OuterFiveSeg 〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉)) | ||
Theorem | cgrextend 31285 | Link congruence over a pair of line segments. Theorem 2.11 of [Schwabhauser] p. 29. (Contributed by Scott Fenton, 12-Jun-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) → (((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐸 Btwn 〈𝐷, 𝐹〉) ∧ (〈𝐴, 𝐵〉Cgr〈𝐷, 𝐸〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝐸, 𝐹〉)) → 〈𝐴, 𝐶〉Cgr〈𝐷, 𝐹〉)) | ||
Theorem | cgrextendand 31286 | Deduction form of cgrextend 31285. (Contributed by Scott Fenton, 14-Oct-2013.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐴 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐵 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐶 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐷 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐸 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐹 ∈ (𝔼‘𝑁)) & ⊢ ((𝜑 ∧ 𝜓) → 𝐵 Btwn 〈𝐴, 𝐶〉) & ⊢ ((𝜑 ∧ 𝜓) → 𝐸 Btwn 〈𝐷, 𝐹〉) & ⊢ ((𝜑 ∧ 𝜓) → 〈𝐴, 𝐵〉Cgr〈𝐷, 𝐸〉) & ⊢ ((𝜑 ∧ 𝜓) → 〈𝐵, 𝐶〉Cgr〈𝐸, 𝐹〉) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 〈𝐴, 𝐶〉Cgr〈𝐷, 𝐹〉) | ||
Theorem | segconeq 31287 | Two points that satsify the conclusion of axsegcon 25607 are identical. Uniqueness portion of Theorem 2.12 of [Schwabhauser] p. 29. (Contributed by Scott Fenton, 12-Jun-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑄 ∈ (𝔼‘𝑁) ∧ 𝑋 ∈ (𝔼‘𝑁) ∧ 𝑌 ∈ (𝔼‘𝑁))) → ((𝑄 ≠ 𝐴 ∧ (𝐴 Btwn 〈𝑄, 𝑋〉 ∧ 〈𝐴, 𝑋〉Cgr〈𝐵, 𝐶〉) ∧ (𝐴 Btwn 〈𝑄, 𝑌〉 ∧ 〈𝐴, 𝑌〉Cgr〈𝐵, 𝐶〉)) → 𝑋 = 𝑌)) | ||
Theorem | segconeu 31288* | Existential uniqueness version of segconeq 31287. (Contributed by Scott Fenton, 19-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ ((𝑁 ∈ ℕ ∧ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)) ∧ 𝐶 ≠ 𝐷)) → ∃!𝑟 ∈ (𝔼‘𝑁)(𝐷 Btwn 〈𝐶, 𝑟〉 ∧ 〈𝐷, 𝑟〉Cgr〈𝐴, 𝐵〉)) | ||
Theorem | btwntriv2 31289 | Betweenness always holds for the second endpoint. Theorem 3.1 of [Schwabhauser] p. 30. (Contributed by Scott Fenton, 12-Jun-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) → 𝐵 Btwn 〈𝐴, 𝐵〉) | ||
Theorem | btwncomim 31290 | Betweenness commutes. Implication version. Theorem 3.2 of [Schwabhauser] p. 30. (Contributed by Scott Fenton, 12-Jun-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → (𝐴 Btwn 〈𝐵, 𝐶〉 → 𝐴 Btwn 〈𝐶, 𝐵〉)) | ||
Theorem | btwncom 31291 | Betweenness commutes. (Contributed by Scott Fenton, 12-Jun-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → (𝐴 Btwn 〈𝐵, 𝐶〉 ↔ 𝐴 Btwn 〈𝐶, 𝐵〉)) | ||
Theorem | btwncomand 31292 | Deduction form of btwncom 31291. (Contributed by Scott Fenton, 14-Oct-2013.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐴 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐵 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐶 ∈ (𝔼‘𝑁)) & ⊢ ((𝜑 ∧ 𝜓) → 𝐴 Btwn 〈𝐵, 𝐶〉) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝐴 Btwn 〈𝐶, 𝐵〉) | ||
Theorem | btwntriv1 31293 | Betweenness always holds for the first endpoint. Theorem 3.3 of [Schwabhauser] p. 30. (Contributed by Scott Fenton, 12-Jun-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) → 𝐴 Btwn 〈𝐴, 𝐵〉) | ||
Theorem | btwnswapid 31294 | 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.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → ((𝐴 Btwn 〈𝐵, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐶〉) → 𝐴 = 𝐵)) | ||
Theorem | btwnswapid2 31295 | If you can swap arguments one and three of a betweenness statement, then those arguments are identical. (Contributed by Scott Fenton, 7-Oct-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → ((𝐴 Btwn 〈𝐵, 𝐶〉 ∧ 𝐶 Btwn 〈𝐵, 𝐴〉) → 𝐴 = 𝐶)) | ||
Theorem | btwnintr 31296 | Inner transitivity law for betweenness. Left-hand side of Theorem 3.5 of [Schwabhauser] p. 30. (Contributed by Scott Fenton, 12-Jun-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → ((𝐵 Btwn 〈𝐴, 𝐷〉 ∧ 𝐶 Btwn 〈𝐵, 𝐷〉) → 𝐵 Btwn 〈𝐴, 𝐶〉)) | ||
Theorem | btwnexch3 31297 | Exchange the first endpoint in betweenness. Left-hand side of Theorem 3.6 of [Schwabhauser] p. 30. (Contributed by Scott Fenton, 12-Jun-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → ((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐶 Btwn 〈𝐴, 𝐷〉) → 𝐶 Btwn 〈𝐵, 𝐷〉)) | ||
Theorem | btwnexch3and 31298 | Deduction form of btwnexch3 31297. (Contributed by Scott Fenton, 13-Oct-2013.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐴 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐵 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐶 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐷 ∈ (𝔼‘𝑁)) & ⊢ ((𝜑 ∧ 𝜓) → 𝐵 Btwn 〈𝐴, 𝐶〉) & ⊢ ((𝜑 ∧ 𝜓) → 𝐶 Btwn 〈𝐴, 𝐷〉) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝐶 Btwn 〈𝐵, 𝐷〉) | ||
Theorem | btwnouttr2 31299 | Outer transitivity law for betweenness. Left-hand side of Theorem 3.1 of [Schwabhauser] p. 30. (Contributed by Scott Fenton, 12-Jun-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → ((𝐵 ≠ 𝐶 ∧ 𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐶 Btwn 〈𝐵, 𝐷〉) → 𝐶 Btwn 〈𝐴, 𝐷〉)) | ||
Theorem | btwnexch2 31300 | 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.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → ((𝐵 Btwn 〈𝐴, 𝐷〉 ∧ 𝐶 Btwn 〈𝐵, 𝐷〉) → 𝐶 Btwn 〈𝐴, 𝐷〉)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |