Home | Metamath
Proof Explorer Theorem List (p. 263 of 454) | < 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-28701) |
Hilbert Space Explorer
(28702-30224) |
Users' Mathboxes
(30225-45333) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | padicval 26201* | Value of the p-adic absolute value. (Contributed by Mario Carneiro, 8-Sep-2014.) |
⊢ 𝐽 = (𝑞 ∈ ℙ ↦ (𝑥 ∈ ℚ ↦ if(𝑥 = 0, 0, (𝑞↑-(𝑞 pCnt 𝑥))))) ⇒ ⊢ ((𝑃 ∈ ℙ ∧ 𝑋 ∈ ℚ) → ((𝐽‘𝑃)‘𝑋) = if(𝑋 = 0, 0, (𝑃↑-(𝑃 pCnt 𝑋)))) | ||
Theorem | ostth2lem1 26202* | Lemma for ostth2 26221, although it is just a simple statement about exponentials which does not involve any specifics of ostth2 26221. If a power is upper bounded by a linear term, the exponent must be less than one. Or in big-O notation, 𝑛 ∈ 𝑜(𝐴↑𝑛) for any 1 < 𝐴. (Contributed by Mario Carneiro, 10-Sep-2014.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐴↑𝑛) ≤ (𝑛 · 𝐵)) ⇒ ⊢ (𝜑 → 𝐴 ≤ 1) | ||
Theorem | qrngbas 26203 | The base set of the field of rationals. (Contributed by Mario Carneiro, 8-Sep-2014.) |
⊢ 𝑄 = (ℂfld ↾s ℚ) ⇒ ⊢ ℚ = (Base‘𝑄) | ||
Theorem | qdrng 26204 | The rationals form a division ring. (Contributed by Mario Carneiro, 8-Sep-2014.) |
⊢ 𝑄 = (ℂfld ↾s ℚ) ⇒ ⊢ 𝑄 ∈ DivRing | ||
Theorem | qrng0 26205 | The zero element of the field of rationals. (Contributed by Mario Carneiro, 8-Sep-2014.) |
⊢ 𝑄 = (ℂfld ↾s ℚ) ⇒ ⊢ 0 = (0g‘𝑄) | ||
Theorem | qrng1 26206 | The unit element of the field of rationals. (Contributed by Mario Carneiro, 8-Sep-2014.) |
⊢ 𝑄 = (ℂfld ↾s ℚ) ⇒ ⊢ 1 = (1r‘𝑄) | ||
Theorem | qrngneg 26207 | The additive inverse in the field of rationals. (Contributed by Mario Carneiro, 8-Sep-2014.) |
⊢ 𝑄 = (ℂfld ↾s ℚ) ⇒ ⊢ (𝑋 ∈ ℚ → ((invg‘𝑄)‘𝑋) = -𝑋) | ||
Theorem | qrngdiv 26208 | The division operation in the field of rationals. (Contributed by Mario Carneiro, 8-Sep-2014.) |
⊢ 𝑄 = (ℂfld ↾s ℚ) ⇒ ⊢ ((𝑋 ∈ ℚ ∧ 𝑌 ∈ ℚ ∧ 𝑌 ≠ 0) → (𝑋(/r‘𝑄)𝑌) = (𝑋 / 𝑌)) | ||
Theorem | qabvle 26209 | By using induction on 𝑁, we show a long-range inequality coming from the triangle inequality. (Contributed by Mario Carneiro, 10-Sep-2014.) |
⊢ 𝑄 = (ℂfld ↾s ℚ) & ⊢ 𝐴 = (AbsVal‘𝑄) ⇒ ⊢ ((𝐹 ∈ 𝐴 ∧ 𝑁 ∈ ℕ0) → (𝐹‘𝑁) ≤ 𝑁) | ||
Theorem | qabvexp 26210 | Induct the product rule abvmul 19593 to find the absolute value of a power. (Contributed by Mario Carneiro, 10-Sep-2014.) |
⊢ 𝑄 = (ℂfld ↾s ℚ) & ⊢ 𝐴 = (AbsVal‘𝑄) ⇒ ⊢ ((𝐹 ∈ 𝐴 ∧ 𝑀 ∈ ℚ ∧ 𝑁 ∈ ℕ0) → (𝐹‘(𝑀↑𝑁)) = ((𝐹‘𝑀)↑𝑁)) | ||
Theorem | ostthlem1 26211* | Lemma for ostth 26223. If two absolute values agree on the positive integers greater than one, then they agree for all rational numbers and thus are equal as functions. (Contributed by Mario Carneiro, 9-Sep-2014.) |
⊢ 𝑄 = (ℂfld ↾s ℚ) & ⊢ 𝐴 = (AbsVal‘𝑄) & ⊢ (𝜑 → 𝐹 ∈ 𝐴) & ⊢ (𝜑 → 𝐺 ∈ 𝐴) & ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘2)) → (𝐹‘𝑛) = (𝐺‘𝑛)) ⇒ ⊢ (𝜑 → 𝐹 = 𝐺) | ||
Theorem | ostthlem2 26212* | Lemma for ostth 26223. Refine ostthlem1 26211 so that it is sufficient to only show equality on the primes. (Contributed by Mario Carneiro, 9-Sep-2014.) (Revised by Mario Carneiro, 20-Jun-2015.) |
⊢ 𝑄 = (ℂfld ↾s ℚ) & ⊢ 𝐴 = (AbsVal‘𝑄) & ⊢ (𝜑 → 𝐹 ∈ 𝐴) & ⊢ (𝜑 → 𝐺 ∈ 𝐴) & ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝐹‘𝑝) = (𝐺‘𝑝)) ⇒ ⊢ (𝜑 → 𝐹 = 𝐺) | ||
Theorem | qabsabv 26213 | The regular absolute value function on the rationals is in fact an absolute value under our definition. (Contributed by Mario Carneiro, 9-Sep-2014.) |
⊢ 𝑄 = (ℂfld ↾s ℚ) & ⊢ 𝐴 = (AbsVal‘𝑄) ⇒ ⊢ (abs ↾ ℚ) ∈ 𝐴 | ||
Theorem | padicabv 26214* | The p-adic absolute value (with arbitrary base) is an absolute value. (Contributed by Mario Carneiro, 9-Sep-2014.) |
⊢ 𝑄 = (ℂfld ↾s ℚ) & ⊢ 𝐴 = (AbsVal‘𝑄) & ⊢ 𝐹 = (𝑥 ∈ ℚ ↦ if(𝑥 = 0, 0, (𝑁↑(𝑃 pCnt 𝑥)))) ⇒ ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) → 𝐹 ∈ 𝐴) | ||
Theorem | padicabvf 26215* | The p-adic absolute value is an absolute value. (Contributed by Mario Carneiro, 9-Sep-2014.) |
⊢ 𝑄 = (ℂfld ↾s ℚ) & ⊢ 𝐴 = (AbsVal‘𝑄) & ⊢ 𝐽 = (𝑞 ∈ ℙ ↦ (𝑥 ∈ ℚ ↦ if(𝑥 = 0, 0, (𝑞↑-(𝑞 pCnt 𝑥))))) ⇒ ⊢ 𝐽:ℙ⟶𝐴 | ||
Theorem | padicabvcxp 26216* | All positive powers of the p-adic absolute value are absolute values. (Contributed by Mario Carneiro, 9-Sep-2014.) |
⊢ 𝑄 = (ℂfld ↾s ℚ) & ⊢ 𝐴 = (AbsVal‘𝑄) & ⊢ 𝐽 = (𝑞 ∈ ℙ ↦ (𝑥 ∈ ℚ ↦ if(𝑥 = 0, 0, (𝑞↑-(𝑞 pCnt 𝑥))))) ⇒ ⊢ ((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+) → (𝑦 ∈ ℚ ↦ (((𝐽‘𝑃)‘𝑦)↑𝑐𝑅)) ∈ 𝐴) | ||
Theorem | ostth1 26217* | - Lemma for ostth 26223: trivial case. (Not that the proof is trivial, but that we are proving that the function is trivial.) If 𝐹 is equal to 1 on the primes, then by complete induction and the multiplicative property abvmul 19593 of the absolute value, 𝐹 is equal to 1 on all the integers, and ostthlem1 26211 extends this to the other rational numbers. (Contributed by Mario Carneiro, 10-Sep-2014.) |
⊢ 𝑄 = (ℂfld ↾s ℚ) & ⊢ 𝐴 = (AbsVal‘𝑄) & ⊢ 𝐽 = (𝑞 ∈ ℙ ↦ (𝑥 ∈ ℚ ↦ if(𝑥 = 0, 0, (𝑞↑-(𝑞 pCnt 𝑥))))) & ⊢ 𝐾 = (𝑥 ∈ ℚ ↦ if(𝑥 = 0, 0, 1)) & ⊢ (𝜑 → 𝐹 ∈ 𝐴) & ⊢ (𝜑 → ∀𝑛 ∈ ℕ ¬ 1 < (𝐹‘𝑛)) & ⊢ (𝜑 → ∀𝑛 ∈ ℙ ¬ (𝐹‘𝑛) < 1) ⇒ ⊢ (𝜑 → 𝐹 = 𝐾) | ||
Theorem | ostth2lem2 26218* | Lemma for ostth2 26221. (Contributed by Mario Carneiro, 10-Sep-2014.) |
⊢ 𝑄 = (ℂfld ↾s ℚ) & ⊢ 𝐴 = (AbsVal‘𝑄) & ⊢ 𝐽 = (𝑞 ∈ ℙ ↦ (𝑥 ∈ ℚ ↦ if(𝑥 = 0, 0, (𝑞↑-(𝑞 pCnt 𝑥))))) & ⊢ 𝐾 = (𝑥 ∈ ℚ ↦ if(𝑥 = 0, 0, 1)) & ⊢ (𝜑 → 𝐹 ∈ 𝐴) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘2)) & ⊢ (𝜑 → 1 < (𝐹‘𝑁)) & ⊢ 𝑅 = ((log‘(𝐹‘𝑁)) / (log‘𝑁)) & ⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘2)) & ⊢ 𝑆 = ((log‘(𝐹‘𝑀)) / (log‘𝑀)) & ⊢ 𝑇 = if((𝐹‘𝑀) ≤ 1, 1, (𝐹‘𝑀)) ⇒ ⊢ ((𝜑 ∧ 𝑋 ∈ ℕ0 ∧ 𝑌 ∈ (0...((𝑀↑𝑋) − 1))) → (𝐹‘𝑌) ≤ ((𝑀 · 𝑋) · (𝑇↑𝑋))) | ||
Theorem | ostth2lem3 26219* | Lemma for ostth2 26221. (Contributed by Mario Carneiro, 10-Sep-2014.) |
⊢ 𝑄 = (ℂfld ↾s ℚ) & ⊢ 𝐴 = (AbsVal‘𝑄) & ⊢ 𝐽 = (𝑞 ∈ ℙ ↦ (𝑥 ∈ ℚ ↦ if(𝑥 = 0, 0, (𝑞↑-(𝑞 pCnt 𝑥))))) & ⊢ 𝐾 = (𝑥 ∈ ℚ ↦ if(𝑥 = 0, 0, 1)) & ⊢ (𝜑 → 𝐹 ∈ 𝐴) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘2)) & ⊢ (𝜑 → 1 < (𝐹‘𝑁)) & ⊢ 𝑅 = ((log‘(𝐹‘𝑁)) / (log‘𝑁)) & ⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘2)) & ⊢ 𝑆 = ((log‘(𝐹‘𝑀)) / (log‘𝑀)) & ⊢ 𝑇 = if((𝐹‘𝑀) ≤ 1, 1, (𝐹‘𝑀)) & ⊢ 𝑈 = ((log‘𝑁) / (log‘𝑀)) ⇒ ⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (((𝐹‘𝑁) / (𝑇↑𝑐𝑈))↑𝑋) ≤ (𝑋 · ((𝑀 · 𝑇) · (𝑈 + 1)))) | ||
Theorem | ostth2lem4 26220* | Lemma for ostth2 26221. (Contributed by Mario Carneiro, 10-Sep-2014.) |
⊢ 𝑄 = (ℂfld ↾s ℚ) & ⊢ 𝐴 = (AbsVal‘𝑄) & ⊢ 𝐽 = (𝑞 ∈ ℙ ↦ (𝑥 ∈ ℚ ↦ if(𝑥 = 0, 0, (𝑞↑-(𝑞 pCnt 𝑥))))) & ⊢ 𝐾 = (𝑥 ∈ ℚ ↦ if(𝑥 = 0, 0, 1)) & ⊢ (𝜑 → 𝐹 ∈ 𝐴) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘2)) & ⊢ (𝜑 → 1 < (𝐹‘𝑁)) & ⊢ 𝑅 = ((log‘(𝐹‘𝑁)) / (log‘𝑁)) & ⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘2)) & ⊢ 𝑆 = ((log‘(𝐹‘𝑀)) / (log‘𝑀)) & ⊢ 𝑇 = if((𝐹‘𝑀) ≤ 1, 1, (𝐹‘𝑀)) & ⊢ 𝑈 = ((log‘𝑁) / (log‘𝑀)) ⇒ ⊢ (𝜑 → (1 < (𝐹‘𝑀) ∧ 𝑅 ≤ 𝑆)) | ||
Theorem | ostth2 26221* | - Lemma for ostth 26223: regular case. (Contributed by Mario Carneiro, 10-Sep-2014.) |
⊢ 𝑄 = (ℂfld ↾s ℚ) & ⊢ 𝐴 = (AbsVal‘𝑄) & ⊢ 𝐽 = (𝑞 ∈ ℙ ↦ (𝑥 ∈ ℚ ↦ if(𝑥 = 0, 0, (𝑞↑-(𝑞 pCnt 𝑥))))) & ⊢ 𝐾 = (𝑥 ∈ ℚ ↦ if(𝑥 = 0, 0, 1)) & ⊢ (𝜑 → 𝐹 ∈ 𝐴) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘2)) & ⊢ (𝜑 → 1 < (𝐹‘𝑁)) & ⊢ 𝑅 = ((log‘(𝐹‘𝑁)) / (log‘𝑁)) ⇒ ⊢ (𝜑 → ∃𝑎 ∈ (0(,]1)𝐹 = (𝑦 ∈ ℚ ↦ ((abs‘𝑦)↑𝑐𝑎))) | ||
Theorem | ostth3 26222* | - Lemma for ostth 26223: p-adic case. (Contributed by Mario Carneiro, 10-Sep-2014.) |
⊢ 𝑄 = (ℂfld ↾s ℚ) & ⊢ 𝐴 = (AbsVal‘𝑄) & ⊢ 𝐽 = (𝑞 ∈ ℙ ↦ (𝑥 ∈ ℚ ↦ if(𝑥 = 0, 0, (𝑞↑-(𝑞 pCnt 𝑥))))) & ⊢ 𝐾 = (𝑥 ∈ ℚ ↦ if(𝑥 = 0, 0, 1)) & ⊢ (𝜑 → 𝐹 ∈ 𝐴) & ⊢ (𝜑 → ∀𝑛 ∈ ℕ ¬ 1 < (𝐹‘𝑛)) & ⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ (𝜑 → (𝐹‘𝑃) < 1) & ⊢ 𝑅 = -((log‘(𝐹‘𝑃)) / (log‘𝑃)) & ⊢ 𝑆 = if((𝐹‘𝑃) ≤ (𝐹‘𝑝), (𝐹‘𝑝), (𝐹‘𝑃)) ⇒ ⊢ (𝜑 → ∃𝑎 ∈ ℝ+ 𝐹 = (𝑦 ∈ ℚ ↦ (((𝐽‘𝑃)‘𝑦)↑𝑐𝑎))) | ||
Theorem | ostth 26223* | Ostrowski's theorem, which classifies all absolute values on ℚ. Any such absolute value must either be the trivial absolute value 𝐾, a constant exponent 0 < 𝑎 ≤ 1 times the regular absolute value, or a positive exponent times the p-adic absolute value. (Contributed by Mario Carneiro, 10-Sep-2014.) |
⊢ 𝑄 = (ℂfld ↾s ℚ) & ⊢ 𝐴 = (AbsVal‘𝑄) & ⊢ 𝐽 = (𝑞 ∈ ℙ ↦ (𝑥 ∈ ℚ ↦ if(𝑥 = 0, 0, (𝑞↑-(𝑞 pCnt 𝑥))))) & ⊢ 𝐾 = (𝑥 ∈ ℚ ↦ if(𝑥 = 0, 0, 1)) ⇒ ⊢ (𝐹 ∈ 𝐴 ↔ (𝐹 = 𝐾 ∨ ∃𝑎 ∈ (0(,]1)𝐹 = (𝑦 ∈ ℚ ↦ ((abs‘𝑦)↑𝑐𝑎)) ∨ ∃𝑎 ∈ ℝ+ ∃𝑔 ∈ ran 𝐽 𝐹 = (𝑦 ∈ ℚ ↦ ((𝑔‘𝑦)↑𝑐𝑎)))) | ||
This part develops elementary geometry based on Tarski's axioms, following [Schwabhauser]. Tarski's geometry is a first-order theory with one sort, the "points". It has two primitive notions, the ternary predicate of "betweenness" and the quaternary predicate of "congruence". To adapt this theory to the framework of set.mm, and to be able to talk of *a* Tarski structure as a space satisfying the given axioms, we use the following definition, stated informally: A Tarski structure 𝑓 is a set (of points) (Base‘𝑓) together with functions (Itv‘𝑓) and (dist‘𝑓) on ((Base‘𝑓) × (Base‘𝑓)) satisfying certain axioms (given in the definitions df-trkg 26247 et sequentes). This allows us to treat a Tarski structure as a special kind of extensible structure (see df-struct 16477). The translation to and from Tarski's treatment is as follows (given, again, informally). Suppose that one is given an extensible structure 𝑓. One defines a betweenness ternary predicate Btw by positing that, for any 𝑥, 𝑦, 𝑧 ∈ (Base‘𝑓), one has "Btw 𝑥𝑦𝑧 " if and only if 𝑦 ∈ 𝑥(Itv‘𝑓)𝑧, and a congruence quaternary predicate Congr by positing that, for any 𝑥, 𝑦, 𝑧, 𝑡 ∈ (Base‘𝑓), one has "Congr 𝑥𝑦𝑧𝑡 " if and only if 𝑥(dist‘𝑓)𝑦 = 𝑧(dist‘𝑓)𝑡. It is easy to check that if 𝑓 satisfies our Tarski axioms, then Btw and Congr satisfy Tarski's Tarski axioms when (Base‘𝑓) is interpreted as the universe of discourse. Conversely, suppose that one is given a set 𝑎, a ternary predicate Btw, and a quaternary predicate Congr. One defines the extensible structure 𝑓 such that (Base‘𝑓) is 𝑎, and (Itv‘𝑓) is the function which associates with each 〈𝑥, 𝑦〉 ∈ (𝑎 × 𝑎) the set of points 𝑧 ∈ 𝑎 such that "Btw 𝑥𝑧𝑦", and (dist‘𝑓) is the function which associates with each 〈𝑥, 𝑦〉 ∈ (𝑎 × 𝑎) the set of ordered pairs 〈𝑧, 𝑡〉 ∈ (𝑎 × 𝑎) such that "Congr 𝑥𝑦𝑧𝑡". It is easy to check that if Btw and Congr satisfy Tarski's Tarski axioms when 𝑎 is interpreted as the universe of discourse, then 𝑓 satisfies our Tarski axioms. We intentionally choose to represent congruence (without loss of generality) as 𝑥(dist‘𝑓)𝑦 = 𝑧(dist‘𝑓)𝑡 instead of "Congr 𝑥𝑦𝑧𝑡", as it is more convenient. It is always possible to define dist for any particular geometry to produce equal results when conguence is desired, and in many cases there is an obvious interpretation of "distance" between two points that can be useful in other situations. Encoding congruence as an equality of distances makes it easier to use these theorems in cases where there is a preferred distance function. We prove that representing a congruence relationship using a distance in the form 𝑥(dist‘𝑓)𝑦 = 𝑧(dist‘𝑓)𝑡 causes no loss of generality in tgjustc1 26269 and tgjustc2 26270, which in turn are supported by tgjustf 26267 and tgjustr 26268. A similar representation of congruence (using a "distance" function) is used in Axiom A1 of [Beeson2016] p. 5, which discusses how a large number of formalized proofs were found in Tarskian Geometry using OTTER. Their detailed proofs in Tarski Geometry, along with other information, are available at http://www.michaelbeeson.com/research/FormalTarski/ 26268. Most theorems are in deduction form, as this is a very general, simple, and convenient format to use in Metamath. An assertion in deduction form can be easily converted into an assertion in inference form (removing the antecedents 𝜑 →) by insert a ⊤ → in each hypothesis, using a1i 11, then using mptru 1545 to remove the final ⊤ → prefix. In some cases we represent, without loss of generality, an implication antecedent in [Schwabhauser] as a hypothesis. The implication can be retrieved from the by using simpr 488, the theorem as stated, and ex 416. For descriptions of individual axioms, we refer to the specific definitions below. A particular feature of Tarski's axioms is modularity, so by using various subsets of the set of axioms, we can define the classes of "absolute dimensionless Tarski structures" (df-trkg 26247), of "Euclidean dimensionless Tarski structures" (df-trkge 26245) and of "Tarski structures of dimension no less than N" (df-trkgld 26246). In this system, angles are not a primitive notion, but instead a derived notion (see df-cgra 26602 and iscgra 26603). To maintain its simplicity, in this system congruence between shapes (a finite sequence of points) is the case where corresponding segments between all corresponding points are congruent. This includes triangles (a shape of 3 distinct points). Note that this definition has no direct regard for angles. For more details and rationale, see df-cgrg 26305. The first section is devoted to the definitions of these various structures. The second section ("Tarskian geometry") develops the synthetic treatment of geometry. The remaining sections prove that real Euclidean spaces and complex Hilbert spaces, with intended interpretations, are Euclidean Tarski structures. Most of the work in this part is due to Thierry Arnoux, with earlier work by Mario Carneiro and Scott Fenton. See also the credits in the comment of each statement. | ||
Syntax | cstrkg 26224 | Extends class notation with the class of Tarski geometries. |
class TarskiG | ||
Syntax | cstrkgc 26225 | Extends class notation with the class of geometries fulfilling the congruence axioms. |
class TarskiGC | ||
Syntax | cstrkgb 26226 | Extends class notation with the class of geometries fulfilling the betweenness axioms. |
class TarskiGB | ||
Syntax | cstrkgcb 26227 | Extends class notation with the class of geometries fulfilling the congruence and betweenness axioms. |
class TarskiGCB | ||
Syntax | cstrkgld 26228 | Extends class notation with the relation for geometries fulfilling the lower dimension axioms. |
class DimTarskiG≥ | ||
Syntax | cstrkge 26229 | Extends class notation with the class of geometries fulfilling Euclid's axiom. |
class TarskiGE | ||
Syntax | citv 26230 | Declare the syntax for the Interval (segment) index extractor. |
class Itv | ||
Syntax | clng 26231 | Declare the syntax for the Line function. |
class LineG | ||
Definition | df-itv 26232 | Define the Interval (segment) index extractor for Tarski geometries. (Contributed by Thierry Arnoux, 24-Aug-2017.) |
⊢ Itv = Slot ;16 | ||
Definition | df-lng 26233 | Define the line index extractor for geometries. (Contributed by Thierry Arnoux, 27-Mar-2019.) |
⊢ LineG = Slot ;17 | ||
Theorem | itvndx 26234 | Index value of the Interval (segment) slot. Use ndxarg 16500. (Contributed by Thierry Arnoux, 24-Aug-2017.) |
⊢ (Itv‘ndx) = ;16 | ||
Theorem | lngndx 26235 | Index value of the "line" slot. Use ndxarg 16500. (Contributed by Thierry Arnoux, 27-Mar-2019.) |
⊢ (LineG‘ndx) = ;17 | ||
Theorem | itvid 26236 | Utility theorem: index-independent form of df-itv 26232. (Contributed by Thierry Arnoux, 24-Aug-2017.) |
⊢ Itv = Slot (Itv‘ndx) | ||
Theorem | lngid 26237 | Utility theorem: index-independent form of df-lng 26233. (Contributed by Thierry Arnoux, 27-Mar-2019.) |
⊢ LineG = Slot (LineG‘ndx) | ||
Theorem | trkgstr 26238 | Functionality of a Tarski geometry. (Contributed by Thierry Arnoux, 24-Aug-2017.) |
⊢ 𝑊 = {〈(Base‘ndx), 𝑈〉, 〈(dist‘ndx), 𝐷〉, 〈(Itv‘ndx), 𝐼〉} ⇒ ⊢ 𝑊 Struct 〈1, ;16〉 | ||
Theorem | trkgbas 26239 | The base set of a Tarski geometry. (Contributed by Thierry Arnoux, 24-Aug-2017.) |
⊢ 𝑊 = {〈(Base‘ndx), 𝑈〉, 〈(dist‘ndx), 𝐷〉, 〈(Itv‘ndx), 𝐼〉} ⇒ ⊢ (𝑈 ∈ 𝑉 → 𝑈 = (Base‘𝑊)) | ||
Theorem | trkgdist 26240 | The measure of a distance in a Tarski geometry. (Contributed by Thierry Arnoux, 24-Aug-2017.) |
⊢ 𝑊 = {〈(Base‘ndx), 𝑈〉, 〈(dist‘ndx), 𝐷〉, 〈(Itv‘ndx), 𝐼〉} ⇒ ⊢ (𝐷 ∈ 𝑉 → 𝐷 = (dist‘𝑊)) | ||
Theorem | trkgitv 26241 | The congruence relation in a Tarski geometry. (Contributed by Thierry Arnoux, 24-Aug-2017.) |
⊢ 𝑊 = {〈(Base‘ndx), 𝑈〉, 〈(dist‘ndx), 𝐷〉, 〈(Itv‘ndx), 𝐼〉} ⇒ ⊢ (𝐼 ∈ 𝑉 → 𝐼 = (Itv‘𝑊)) | ||
Definition | df-trkgc 26242* | Define the class of geometries fulfilling the congruence axioms of reflexivity, identity and transitivity. These are axioms A1 to A3 of [Schwabhauser] p. 10. With our distance based notation for congruence, transitivity of congruence boils down to transitivity of equality and is already given by eqtr 2818, so it is not listed in this definition. (Contributed by Thierry Arnoux, 24-Aug-2017.) |
⊢ TarskiGC = {𝑓 ∣ [(Base‘𝑓) / 𝑝][(dist‘𝑓) / 𝑑](∀𝑥 ∈ 𝑝 ∀𝑦 ∈ 𝑝 (𝑥𝑑𝑦) = (𝑦𝑑𝑥) ∧ ∀𝑥 ∈ 𝑝 ∀𝑦 ∈ 𝑝 ∀𝑧 ∈ 𝑝 ((𝑥𝑑𝑦) = (𝑧𝑑𝑧) → 𝑥 = 𝑦))} | ||
Definition | df-trkgb 26243* | Define the class of geometries fulfilling the 3 betweenness axioms in Tarski's Axiomatization of Geometry: identity, Axiom A6 of [Schwabhauser] p. 11, axiom of Pasch, Axiom A7 of [Schwabhauser] p. 12, and continuity, Axiom A11 of [Schwabhauser] p. 13. (Contributed by Thierry Arnoux, 24-Aug-2017.) |
⊢ TarskiGB = {𝑓 ∣ [(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](∀𝑥 ∈ 𝑝 ∀𝑦 ∈ 𝑝 (𝑦 ∈ (𝑥𝑖𝑥) → 𝑥 = 𝑦) ∧ ∀𝑥 ∈ 𝑝 ∀𝑦 ∈ 𝑝 ∀𝑧 ∈ 𝑝 ∀𝑢 ∈ 𝑝 ∀𝑣 ∈ 𝑝 ((𝑢 ∈ (𝑥𝑖𝑧) ∧ 𝑣 ∈ (𝑦𝑖𝑧)) → ∃𝑎 ∈ 𝑝 (𝑎 ∈ (𝑢𝑖𝑦) ∧ 𝑎 ∈ (𝑣𝑖𝑥))) ∧ ∀𝑠 ∈ 𝒫 𝑝∀𝑡 ∈ 𝒫 𝑝(∃𝑎 ∈ 𝑝 ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝑖𝑦) → ∃𝑏 ∈ 𝑝 ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑏 ∈ (𝑥𝑖𝑦)))} | ||
Definition | df-trkgcb 26244* | Define the class of geometries fulfilling the five segment axiom, Axiom A5 of [Schwabhauser] p. 11, and segment construction axiom, Axiom A4 of [Schwabhauser] p. 11. (Contributed by Thierry Arnoux, 14-Mar-2019.) |
⊢ TarskiGCB = {𝑓 ∣ [(Base‘𝑓) / 𝑝][(dist‘𝑓) / 𝑑][(Itv‘𝑓) / 𝑖](∀𝑥 ∈ 𝑝 ∀𝑦 ∈ 𝑝 ∀𝑧 ∈ 𝑝 ∀𝑢 ∈ 𝑝 ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑝 ∀𝑐 ∈ 𝑝 ∀𝑣 ∈ 𝑝 (((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝑖𝑧) ∧ 𝑏 ∈ (𝑎𝑖𝑐)) ∧ (((𝑥𝑑𝑦) = (𝑎𝑑𝑏) ∧ (𝑦𝑑𝑧) = (𝑏𝑑𝑐)) ∧ ((𝑥𝑑𝑢) = (𝑎𝑑𝑣) ∧ (𝑦𝑑𝑢) = (𝑏𝑑𝑣)))) → (𝑧𝑑𝑢) = (𝑐𝑑𝑣)) ∧ ∀𝑥 ∈ 𝑝 ∀𝑦 ∈ 𝑝 ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑝 ∃𝑧 ∈ 𝑝 (𝑦 ∈ (𝑥𝑖𝑧) ∧ (𝑦𝑑𝑧) = (𝑎𝑑𝑏)))} | ||
Definition | df-trkge 26245* | Define the class of geometries fulfilling Euclid's axiom, Axiom A10 of [Schwabhauser] p. 13. (Contributed by Thierry Arnoux, 14-Mar-2019.) |
⊢ TarskiGE = {𝑓 ∣ [(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖]∀𝑥 ∈ 𝑝 ∀𝑦 ∈ 𝑝 ∀𝑧 ∈ 𝑝 ∀𝑢 ∈ 𝑝 ∀𝑣 ∈ 𝑝 ((𝑢 ∈ (𝑥𝑖𝑣) ∧ 𝑢 ∈ (𝑦𝑖𝑧) ∧ 𝑥 ≠ 𝑢) → ∃𝑎 ∈ 𝑝 ∃𝑏 ∈ 𝑝 (𝑦 ∈ (𝑥𝑖𝑎) ∧ 𝑧 ∈ (𝑥𝑖𝑏) ∧ 𝑣 ∈ (𝑎𝑖𝑏)))} | ||
Definition | df-trkgld 26246* | Define the class of geometries fulfilling the lower dimension axiom for dimension 𝑛. For such geometries, there are three non-colinear points that are equidistant from 𝑛 − 1 distinct points. Derived from remarks in Tarski's System of Geometry, Alfred Tarski and Steven Givant, Bulletin of Symbolic Logic, Volume 5, Number 2 (1999), 175-214. (Contributed by Scott Fenton, 22-Apr-2013.) (Revised by Thierry Arnoux, 23-Nov-2019.) |
⊢ DimTarskiG≥ = {〈𝑔, 𝑛〉 ∣ [(Base‘𝑔) / 𝑝][(dist‘𝑔) / 𝑑][(Itv‘𝑔) / 𝑖]∃𝑓(𝑓:(1..^𝑛)–1-1→𝑝 ∧ ∃𝑥 ∈ 𝑝 ∃𝑦 ∈ 𝑝 ∃𝑧 ∈ 𝑝 (∀𝑗 ∈ (2..^𝑛)(((𝑓‘1)𝑑𝑥) = ((𝑓‘𝑗)𝑑𝑥) ∧ ((𝑓‘1)𝑑𝑦) = ((𝑓‘𝑗)𝑑𝑦) ∧ ((𝑓‘1)𝑑𝑧) = ((𝑓‘𝑗)𝑑𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))))} | ||
Definition | df-trkg 26247* |
Define the class of Tarski geometries. A Tarski geometry is a set of
points, equipped with a betweenness relation (denoting that a point lies
on a line segment between two other points) and a congruence relation
(denoting equality of line segment lengths).
Here, we are using the following:
Tarski originally had more axioms, but later reduced his list to 11:
So our definition of a Tarskian Geometry includes the 3 axioms for the quaternary congruence relation (A1, A2, A3), the 3 axioms for the ternary betweenness relation (A6, A7, A11), and the 2 axioms of compatibility of the congruence and the betweenness relations (A4,A5). It does not include Euclid's axiom A10, nor the 2-dimensional axioms A8 (Lower dimension axiom) and A9 (Upper dimension axiom) so the number of dimensions of the geometry it formalizes is not constrained. Considering A2 as one of the 3 axioms for the quaternary congruence relation is somewhat conventional, because the transitivity of the congruence relation is automatically given by our choice to take the distance as this congruence relation in our definition of Tarski geometries. (Contributed by Thierry Arnoux, 24-Aug-2017.) (Revised by Thierry Arnoux, 27-Apr-2019.) |
⊢ TarskiG = ((TarskiGC ∩ TarskiGB) ∩ (TarskiGCB ∩ {𝑓 ∣ [(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥 ∈ 𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})})) | ||
Theorem | istrkgc 26248* | Property of being a Tarski geometry - congruence part. (Contributed by Thierry Arnoux, 14-Mar-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) ⇒ ⊢ (𝐺 ∈ TarskiGC ↔ (𝐺 ∈ V ∧ (∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 (𝑥 − 𝑦) = (𝑦 − 𝑥) ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ∀𝑧 ∈ 𝑃 ((𝑥 − 𝑦) = (𝑧 − 𝑧) → 𝑥 = 𝑦)))) | ||
Theorem | istrkgb 26249* | Property of being a Tarski geometry - betweenness part. (Contributed by Thierry Arnoux, 14-Mar-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) ⇒ ⊢ (𝐺 ∈ TarskiGB ↔ (𝐺 ∈ V ∧ (∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 (𝑦 ∈ (𝑥𝐼𝑥) → 𝑥 = 𝑦) ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ∀𝑧 ∈ 𝑃 ∀𝑢 ∈ 𝑃 ∀𝑣 ∈ 𝑃 ((𝑢 ∈ (𝑥𝐼𝑧) ∧ 𝑣 ∈ (𝑦𝐼𝑧)) → ∃𝑎 ∈ 𝑃 (𝑎 ∈ (𝑢𝐼𝑦) ∧ 𝑎 ∈ (𝑣𝐼𝑥))) ∧ ∀𝑠 ∈ 𝒫 𝑃∀𝑡 ∈ 𝒫 𝑃(∃𝑎 ∈ 𝑃 ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐼𝑦) → ∃𝑏 ∈ 𝑃 ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑏 ∈ (𝑥𝐼𝑦))))) | ||
Theorem | istrkgcb 26250* | Property of being a Tarski geometry - congruence and betweenness part. (Contributed by Thierry Arnoux, 14-Mar-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) ⇒ ⊢ (𝐺 ∈ TarskiGCB ↔ (𝐺 ∈ V ∧ (∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ∀𝑧 ∈ 𝑃 ∀𝑢 ∈ 𝑃 ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑥 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑥 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣)) ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ∃𝑧 ∈ 𝑃 (𝑦 ∈ (𝑥𝐼𝑧) ∧ (𝑦 − 𝑧) = (𝑎 − 𝑏))))) | ||
Theorem | istrkge 26251* | Property of fulfilling Euclid's axiom. (Contributed by Thierry Arnoux, 14-Mar-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) ⇒ ⊢ (𝐺 ∈ TarskiGE ↔ (𝐺 ∈ V ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ∀𝑧 ∈ 𝑃 ∀𝑢 ∈ 𝑃 ∀𝑣 ∈ 𝑃 ((𝑢 ∈ (𝑥𝐼𝑣) ∧ 𝑢 ∈ (𝑦𝐼𝑧) ∧ 𝑥 ≠ 𝑢) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑦 ∈ (𝑥𝐼𝑎) ∧ 𝑧 ∈ (𝑥𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏))))) | ||
Theorem | istrkgl 26252* | Building lines from the segment property. (Contributed by Thierry Arnoux, 14-Mar-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) ⇒ ⊢ (𝐺 ∈ {𝑓 ∣ [(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥 ∈ 𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})} ↔ (𝐺 ∈ V ∧ (LineG‘𝐺) = (𝑥 ∈ 𝑃, 𝑦 ∈ (𝑃 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑃 ∣ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))}))) | ||
Theorem | istrkgld 26253* | Property of fulfilling the lower dimension 𝑁 axiom. (Contributed by Thierry Arnoux, 20-Nov-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) ⇒ ⊢ ((𝐺 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2)) → (𝐺DimTarskiG≥𝑁 ↔ ∃𝑓(𝑓:(1..^𝑁)–1-1→𝑃 ∧ ∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 ∃𝑧 ∈ 𝑃 (∀𝑗 ∈ (2..^𝑁)(((𝑓‘1) − 𝑥) = ((𝑓‘𝑗) − 𝑥) ∧ ((𝑓‘1) − 𝑦) = ((𝑓‘𝑗) − 𝑦) ∧ ((𝑓‘1) − 𝑧) = ((𝑓‘𝑗) − 𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧)))))) | ||
Theorem | istrkg2ld 26254* | Property of fulfilling the lower dimension 2 axiom. (Contributed by Thierry Arnoux, 20-Nov-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) ⇒ ⊢ (𝐺 ∈ 𝑉 → (𝐺DimTarskiG≥2 ↔ ∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 ∃𝑧 ∈ 𝑃 ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧)))) | ||
Theorem | istrkg3ld 26255* | Property of fulfilling the lower dimension 3 axiom. (Contributed by Thierry Arnoux, 12-Jul-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) ⇒ ⊢ (𝐺 ∈ 𝑉 → (𝐺DimTarskiG≥3 ↔ ∃𝑢 ∈ 𝑃 ∃𝑣 ∈ 𝑃 (𝑢 ≠ 𝑣 ∧ ∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 ∃𝑧 ∈ 𝑃 (((𝑢 − 𝑥) = (𝑣 − 𝑥) ∧ (𝑢 − 𝑦) = (𝑣 − 𝑦) ∧ (𝑢 − 𝑧) = (𝑣 − 𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧)))))) | ||
Theorem | axtgcgrrflx 26256 | Axiom of reflexivity of congruence, Axiom A1 of [Schwabhauser] p. 10. (Contributed by Thierry Arnoux, 14-Mar-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) ⇒ ⊢ (𝜑 → (𝑋 − 𝑌) = (𝑌 − 𝑋)) | ||
Theorem | axtgcgrid 26257 | Axiom of identity of congruence, Axiom A3 of [Schwabhauser] p. 10. (Contributed by Thierry Arnoux, 14-Mar-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ (𝜑 → 𝑍 ∈ 𝑃) & ⊢ (𝜑 → (𝑋 − 𝑌) = (𝑍 − 𝑍)) ⇒ ⊢ (𝜑 → 𝑋 = 𝑌) | ||
Theorem | axtgsegcon 26258* | Axiom of segment construction, Axiom A4 of [Schwabhauser] p. 11. As discussed in Axiom 4 of [Tarski1999] p. 178, "The intuitive content [is that] given any line segment 𝐴𝐵, one can construct a line segment congruent to it, starting at any point 𝑌 and going in the direction of any ray containing 𝑌. The ray is determined by the point 𝑌 and a second point 𝑋, the endpoint of the ray. The other endpoint of the line segment to be constructed is just the point 𝑧 whose existence is asserted." (Contributed by Thierry Arnoux, 15-Mar-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) ⇒ ⊢ (𝜑 → ∃𝑧 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑧) ∧ (𝑌 − 𝑧) = (𝐴 − 𝐵))) | ||
Theorem | axtg5seg 26259 | Five segments axiom, Axiom A5 of [Schwabhauser] p. 11. Take two triangles 𝑋𝑍𝑈 and 𝐴𝐶𝑉, a point 𝑌 on 𝑋𝑍, and a point 𝐵 on 𝐴𝐶. If all corresponding line segments except for 𝑍𝑈 and 𝐶𝑉 are congruent ( i.e., 𝑋𝑌 ∼ 𝐴𝐵, 𝑌𝑍 ∼ 𝐵𝐶, 𝑋𝑈 ∼ 𝐴𝑉, and 𝑌𝑈 ∼ 𝐵𝑉), then 𝑍𝑈 and 𝐶𝑉 are also congruent. As noted in Axiom 5 of [Tarski1999] p. 178, "this axiom is similar in character to the well-known theorems of Euclidean geometry that allow one to conclude, from hypotheses about the congruence of certain corresponding sides and angles in two triangles, the congruence of other corresponding sides and angles." (Contributed by Thierry Arnoux, 14-Mar-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ (𝜑 → 𝑍 ∈ 𝑃) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝑈 ∈ 𝑃) & ⊢ (𝜑 → 𝑉 ∈ 𝑃) & ⊢ (𝜑 → 𝑋 ≠ 𝑌) & ⊢ (𝜑 → 𝑌 ∈ (𝑋𝐼𝑍)) & ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐶)) & ⊢ (𝜑 → (𝑋 − 𝑌) = (𝐴 − 𝐵)) & ⊢ (𝜑 → (𝑌 − 𝑍) = (𝐵 − 𝐶)) & ⊢ (𝜑 → (𝑋 − 𝑈) = (𝐴 − 𝑉)) & ⊢ (𝜑 → (𝑌 − 𝑈) = (𝐵 − 𝑉)) ⇒ ⊢ (𝜑 → (𝑍 − 𝑈) = (𝐶 − 𝑉)) | ||
Theorem | axtgbtwnid 26260 | Identity of Betweenness. Axiom A6 of [Schwabhauser] p. 11. (Contributed by Thierry Arnoux, 15-Mar-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ (𝑋𝐼𝑋)) ⇒ ⊢ (𝜑 → 𝑋 = 𝑌) | ||
Theorem | axtgpasch 26261* | Axiom of (Inner) Pasch, Axiom A7 of [Schwabhauser] p. 12. Given triangle 𝑋𝑌𝑍, point 𝑈 in segment 𝑋𝑍, and point 𝑉 in segment 𝑌𝑍, there exists a point 𝑎 on both the segment 𝑈𝑌 and the segment 𝑉𝑋. This axiom is essentially a subset of the general Pasch axiom. The general Pasch axiom asserts that on a plane "a line intersecting a triangle in one of its sides, and not intersecting any of the vertices, must intersect one of the other two sides" (per the discussion about Axiom 7 of [Tarski1999] p. 179). The (general) Pasch axiom was used implicitly by Euclid, but never stated; Moritz Pasch discovered its omission in 1882. As noted in the Metamath book, this means that the omission of Pasch's axiom from Euclid went unnoticed for 2000 years. Only the inner Pasch algorithm is included as an axiom; the "outer" form of the Pasch axiom can be proved using the inner form (see theorem 9.6 of [Schwabhauser] p. 69 and the brief discussion in axiom 7.1 of [Tarski1999] p. 180). (Contributed by Thierry Arnoux, 15-Mar-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ (𝜑 → 𝑍 ∈ 𝑃) & ⊢ (𝜑 → 𝑈 ∈ 𝑃) & ⊢ (𝜑 → 𝑉 ∈ 𝑃) & ⊢ (𝜑 → 𝑈 ∈ (𝑋𝐼𝑍)) & ⊢ (𝜑 → 𝑉 ∈ (𝑌𝐼𝑍)) ⇒ ⊢ (𝜑 → ∃𝑎 ∈ 𝑃 (𝑎 ∈ (𝑈𝐼𝑌) ∧ 𝑎 ∈ (𝑉𝐼𝑋))) | ||
Theorem | axtgcont1 26262* | Axiom of Continuity. Axiom A11 of [Schwabhauser] p. 13. This axiom (scheme) asserts that any two sets 𝑆 and 𝑇 (of points) such that the elements of 𝑆 precede the elements of 𝑇 with respect to some point 𝑎 (that is, 𝑥 is between 𝑎 and 𝑦 whenever 𝑥 is in 𝑋 and 𝑦 is in 𝑌) are separated by some point 𝑏; this is explained in Axiom 11 of [Tarski1999] p. 185. (Contributed by Thierry Arnoux, 16-Mar-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝑆 ⊆ 𝑃) & ⊢ (𝜑 → 𝑇 ⊆ 𝑃) ⇒ ⊢ (𝜑 → (∃𝑎 ∈ 𝑃 ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑇 𝑥 ∈ (𝑎𝐼𝑦) → ∃𝑏 ∈ 𝑃 ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑇 𝑏 ∈ (𝑥𝐼𝑦))) | ||
Theorem | axtgcont 26263* | Axiom of Continuity. Axiom A11 of [Schwabhauser] p. 13. For more information see axtgcont1 26262. (Contributed by Thierry Arnoux, 16-Mar-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝑆 ⊆ 𝑃) & ⊢ (𝜑 → 𝑇 ⊆ 𝑃) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑇) → 𝑢 ∈ (𝐴𝐼𝑣)) ⇒ ⊢ (𝜑 → ∃𝑏 ∈ 𝑃 ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑇 𝑏 ∈ (𝑥𝐼𝑦)) | ||
Theorem | axtglowdim2 26264* | Lower dimension axiom for dimension 2, Axiom A8 of [Schwabhauser] p. 13. There exist 3 non-colinear points. (Contributed by Thierry Arnoux, 20-Nov-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ 𝑉) & ⊢ (𝜑 → 𝐺DimTarskiG≥2) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 ∃𝑧 ∈ 𝑃 ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))) | ||
Theorem | axtgupdim2 26265 | Upper dimension axiom for dimension 2, Axiom A9 of [Schwabhauser] p. 13. Three points 𝑋, 𝑌 and 𝑍 equidistant to two given two points 𝑈 and 𝑉 must be colinear. (Contributed by Thierry Arnoux, 29-May-2019.) (Revised by Thierry Arnoux, 11-Jul-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ (𝜑 → 𝑍 ∈ 𝑃) & ⊢ (𝜑 → 𝑈 ∈ 𝑃) & ⊢ (𝜑 → 𝑉 ∈ 𝑃) & ⊢ (𝜑 → 𝑈 ≠ 𝑉) & ⊢ (𝜑 → (𝑈 − 𝑋) = (𝑉 − 𝑋)) & ⊢ (𝜑 → (𝑈 − 𝑌) = (𝑉 − 𝑌)) & ⊢ (𝜑 → (𝑈 − 𝑍) = (𝑉 − 𝑍)) & ⊢ (𝜑 → 𝐺 ∈ 𝑉) & ⊢ (𝜑 → ¬ 𝐺DimTarskiG≥3) ⇒ ⊢ (𝜑 → (𝑍 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑍𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑍))) | ||
Theorem | axtgeucl 26266* | Euclid's Axiom. Axiom A10 of [Schwabhauser] p. 13. This is equivalent to Euclid's parallel postulate when combined with other axioms. (Contributed by Thierry Arnoux, 16-Mar-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiGE) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ (𝜑 → 𝑍 ∈ 𝑃) & ⊢ (𝜑 → 𝑈 ∈ 𝑃) & ⊢ (𝜑 → 𝑉 ∈ 𝑃) & ⊢ (𝜑 → 𝑈 ∈ (𝑋𝐼𝑉)) & ⊢ (𝜑 → 𝑈 ∈ (𝑌𝐼𝑍)) & ⊢ (𝜑 → 𝑋 ≠ 𝑈) ⇒ ⊢ (𝜑 → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑎) ∧ 𝑍 ∈ (𝑋𝐼𝑏) ∧ 𝑉 ∈ (𝑎𝐼𝑏))) | ||
Theorem | tgjustf 26267* | Given any function 𝐹, equality of the image by 𝐹 is an equivalence relation. (Contributed by Thierry Arnoux, 25-Jan-2023.) |
⊢ (𝐴 ∈ 𝑉 → ∃𝑟(𝑟 Er 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑟𝑦 ↔ (𝐹‘𝑥) = (𝐹‘𝑦)))) | ||
Theorem | tgjustr 26268* | Given any equivalence relation 𝑅, one can define a function 𝑓 such that all elements of an equivalence classe of 𝑅 have the same image by 𝑓. (Contributed by Thierry Arnoux, 25-Jan-2023.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 Er 𝐴) → ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝑓‘𝑥) = (𝑓‘𝑦)))) | ||
Theorem | tgjustc1 26269* | A justification for using distance equality instead of the textbook relation on pairs of points for congruence. (Contributed by Thierry Arnoux, 29-Jan-2023.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) ⇒ ⊢ ∃𝑟(𝑟 Er (𝑃 × 𝑃) ∧ ∀𝑤 ∈ 𝑃 ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ∀𝑧 ∈ 𝑃 (〈𝑤, 𝑥〉𝑟〈𝑦, 𝑧〉 ↔ (𝑤 − 𝑥) = (𝑦 − 𝑧))) | ||
Theorem | tgjustc2 26270* | A justification for using distance equality instead of the textbook relation on pairs of points for congruence. (Contributed by Thierry Arnoux, 29-Jan-2023.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝑅 Er (𝑃 × 𝑃) ⇒ ⊢ ∃𝑑(𝑑 Fn (𝑃 × 𝑃) ∧ ∀𝑤 ∈ 𝑃 ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ∀𝑧 ∈ 𝑃 (〈𝑤, 𝑥〉𝑅〈𝑦, 𝑧〉 ↔ (𝑤𝑑𝑥) = (𝑦𝑑𝑧))) | ||
Theorem | tgcgrcomimp 26271 | Congruence commutes on the RHS. Theorem 2.5 of [Schwabhauser] p. 27. (Contributed by David A. Wheeler, 29-Jun-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) ⇒ ⊢ (𝜑 → ((𝐴 − 𝐵) = (𝐶 − 𝐷) → (𝐴 − 𝐵) = (𝐷 − 𝐶))) | ||
Theorem | tgcgrcomr 26272 | Congruence commutes on the RHS. Variant of Theorem 2.5 of [Schwabhauser] p. 27, but in a convenient form for a common case. (Contributed by David A. Wheeler, 29-Jun-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → (𝐴 − 𝐵) = (𝐶 − 𝐷)) ⇒ ⊢ (𝜑 → (𝐴 − 𝐵) = (𝐷 − 𝐶)) | ||
Theorem | tgcgrcoml 26273 | Congruence commutes on the LHS. Variant of Theorem 2.5 of [Schwabhauser] p. 27, but in a convenient form for a common case. (Contributed by David A. Wheeler, 29-Jun-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → (𝐴 − 𝐵) = (𝐶 − 𝐷)) ⇒ ⊢ (𝜑 → (𝐵 − 𝐴) = (𝐶 − 𝐷)) | ||
Theorem | tgcgrcomlr 26274 | Congruence commutes on both sides. (Contributed by Thierry Arnoux, 23-Mar-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → (𝐴 − 𝐵) = (𝐶 − 𝐷)) ⇒ ⊢ (𝜑 → (𝐵 − 𝐴) = (𝐷 − 𝐶)) | ||
Theorem | tgcgreqb 26275 | Congruence and equality. (Contributed by Thierry Arnoux, 27-Aug-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → (𝐴 − 𝐵) = (𝐶 − 𝐷)) ⇒ ⊢ (𝜑 → (𝐴 = 𝐵 ↔ 𝐶 = 𝐷)) | ||
Theorem | tgcgreq 26276 | Congruence and equality. (Contributed by Thierry Arnoux, 27-Aug-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → (𝐴 − 𝐵) = (𝐶 − 𝐷)) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → 𝐶 = 𝐷) | ||
Theorem | tgcgrneq 26277 | Congruence and equality. (Contributed by Thierry Arnoux, 27-Aug-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → (𝐴 − 𝐵) = (𝐶 − 𝐷)) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) ⇒ ⊢ (𝜑 → 𝐶 ≠ 𝐷) | ||
Theorem | tgcgrtriv 26278 | Degenerate segments are congruent. Theorem 2.8 of [Schwabhauser] p. 28. (Contributed by Thierry Arnoux, 23-Mar-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) ⇒ ⊢ (𝜑 → (𝐴 − 𝐴) = (𝐵 − 𝐵)) | ||
Theorem | tgcgrextend 26279 | Link congruence over a pair of line segments. Theorem 2.11 of [Schwabhauser] p. 29. (Contributed by Thierry Arnoux, 23-Mar-2019.) (Shortened by David A. Wheeler and Thierry Arnoux, 22-Apr-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐶)) & ⊢ (𝜑 → 𝐸 ∈ (𝐷𝐼𝐹)) & ⊢ (𝜑 → (𝐴 − 𝐵) = (𝐷 − 𝐸)) & ⊢ (𝜑 → (𝐵 − 𝐶) = (𝐸 − 𝐹)) ⇒ ⊢ (𝜑 → (𝐴 − 𝐶) = (𝐷 − 𝐹)) | ||
Theorem | tgsegconeq 26280 | Two points that satisfy the conclusion of axtgsegcon 26258 are identical. Uniqueness portion of Theorem 2.12 of [Schwabhauser] p. 29. (Contributed by Thierry Arnoux, 23-Mar-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ≠ 𝐴) & ⊢ (𝜑 → 𝐴 ∈ (𝐷𝐼𝐸)) & ⊢ (𝜑 → 𝐴 ∈ (𝐷𝐼𝐹)) & ⊢ (𝜑 → (𝐴 − 𝐸) = (𝐵 − 𝐶)) & ⊢ (𝜑 → (𝐴 − 𝐹) = (𝐵 − 𝐶)) ⇒ ⊢ (𝜑 → 𝐸 = 𝐹) | ||
Theorem | tgbtwntriv2 26281 | Betweenness always holds for the second endpoint. Theorem 3.1 of [Schwabhauser] p. 30. (Contributed by Thierry Arnoux, 15-Mar-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) ⇒ ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐵)) | ||
Theorem | tgbtwncom 26282 | Betweenness commutes. Theorem 3.2 of [Schwabhauser] p. 30. (Contributed by Thierry Arnoux, 15-Mar-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐶)) ⇒ ⊢ (𝜑 → 𝐵 ∈ (𝐶𝐼𝐴)) | ||
Theorem | tgbtwncomb 26283 | Betweenness commutes, biconditional version. (Contributed by Thierry Arnoux, 3-Apr-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) ⇒ ⊢ (𝜑 → (𝐵 ∈ (𝐴𝐼𝐶) ↔ 𝐵 ∈ (𝐶𝐼𝐴))) | ||
Theorem | tgbtwnne 26284 | Betweenness and inequality. (Contributed by Thierry Arnoux, 1-Dec-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐶)) & ⊢ (𝜑 → 𝐵 ≠ 𝐴) ⇒ ⊢ (𝜑 → 𝐴 ≠ 𝐶) | ||
Theorem | tgbtwntriv1 26285 | Betweenness always holds for the first endpoint. Theorem 3.3 of [Schwabhauser] p. 30. (Contributed by Thierry Arnoux, 15-Mar-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) ⇒ ⊢ (𝜑 → 𝐴 ∈ (𝐴𝐼𝐵)) | ||
Theorem | tgbtwnswapid 26286 | 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 Thierry Arnoux, 16-Mar-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐴 ∈ (𝐵𝐼𝐶)) & ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐶)) ⇒ ⊢ (𝜑 → 𝐴 = 𝐵) | ||
Theorem | tgbtwnintr 26287 | Inner transitivity law for betweenness. Left-hand side of Theorem 3.5 of [Schwabhauser] p. 30. (Contributed by Thierry Arnoux, 18-Mar-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐴 ∈ (𝐵𝐼𝐷)) & ⊢ (𝜑 → 𝐵 ∈ (𝐶𝐼𝐷)) ⇒ ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐶)) | ||
Theorem | tgbtwnexch3 26288 | Exchange the first endpoint in betweenness. Left-hand side of Theorem 3.6 of [Schwabhauser] p. 30. (Contributed by Thierry Arnoux, 18-Mar-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐶)) & ⊢ (𝜑 → 𝐶 ∈ (𝐴𝐼𝐷)) ⇒ ⊢ (𝜑 → 𝐶 ∈ (𝐵𝐼𝐷)) | ||
Theorem | tgbtwnouttr2 26289 | Outer transitivity law for betweenness. Left-hand side of Theorem 3.7 of [Schwabhauser] p. 30. (Contributed by Thierry Arnoux, 18-Mar-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ≠ 𝐶) & ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐶)) & ⊢ (𝜑 → 𝐶 ∈ (𝐵𝐼𝐷)) ⇒ ⊢ (𝜑 → 𝐶 ∈ (𝐴𝐼𝐷)) | ||
Theorem | tgbtwnexch2 26290 | Exchange the outer point of two betweenness statements. Right-hand side of Theorem 3.5 of [Schwabhauser] p. 30. (Contributed by Thierry Arnoux, 23-Mar-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐷)) & ⊢ (𝜑 → 𝐶 ∈ (𝐵𝐼𝐷)) ⇒ ⊢ (𝜑 → 𝐶 ∈ (𝐴𝐼𝐷)) | ||
Theorem | tgbtwnouttr 26291 | Outer transitivity law for betweenness. Right-hand side of Theorem 3.7 of [Schwabhauser] p. 30. (Contributed by Thierry Arnoux, 23-Mar-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ≠ 𝐶) & ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐶)) & ⊢ (𝜑 → 𝐶 ∈ (𝐵𝐼𝐷)) ⇒ ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐷)) | ||
Theorem | tgbtwnexch 26292 | Outer transitivity law for betweenness. Right-hand side of Theorem 3.6 of [Schwabhauser] p. 30. (Contributed by Thierry Arnoux, 23-Mar-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐶)) & ⊢ (𝜑 → 𝐶 ∈ (𝐴𝐼𝐷)) ⇒ ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐷)) | ||
Theorem | tgtrisegint 26293* | 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 Thierry Arnoux, 23-Mar-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐶)) & ⊢ (𝜑 → 𝐸 ∈ (𝐷𝐼𝐶)) & ⊢ (𝜑 → 𝐹 ∈ (𝐴𝐼𝐷)) ⇒ ⊢ (𝜑 → ∃𝑞 ∈ 𝑃 (𝑞 ∈ (𝐹𝐼𝐶) ∧ 𝑞 ∈ (𝐵𝐼𝐸))) | ||
Theorem | tglowdim1 26294* | Lower dimension axiom for one dimension. In dimension at least 1, there are at least two distinct points. The condition "the space is of dimension 1 or more" is written here as 2 ≤ (♯‘𝑃) to avoid a new definition, but a different convention could be chosen. (Contributed by Thierry Arnoux, 23-Mar-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 2 ≤ (♯‘𝑃)) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 𝑥 ≠ 𝑦) | ||
Theorem | tglowdim1i 26295* | Lower dimension axiom for one dimension. (Contributed by Thierry Arnoux, 28-May-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 2 ≤ (♯‘𝑃)) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) ⇒ ⊢ (𝜑 → ∃𝑦 ∈ 𝑃 𝑋 ≠ 𝑦) | ||
Theorem | tgldimor 26296 | Excluded-middle like statement allowing to treat dimension zero as a special case. (Contributed by Thierry Arnoux, 11-Apr-2019.) |
⊢ 𝑃 = (𝐸‘𝐹) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) ⇒ ⊢ (𝜑 → ((♯‘𝑃) = 1 ∨ 2 ≤ (♯‘𝑃))) | ||
Theorem | tgldim0eq 26297 | In dimension zero, any two points are equal. (Contributed by Thierry Arnoux, 11-Apr-2019.) |
⊢ 𝑃 = (𝐸‘𝐹) & ⊢ (𝜑 → (♯‘𝑃) = 1) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) ⇒ ⊢ (𝜑 → 𝐴 = 𝐵) | ||
Theorem | tgldim0itv 26298 | In dimension zero, any two points are equal. (Contributed by Thierry Arnoux, 12-Apr-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → (♯‘𝑃) = 1) ⇒ ⊢ (𝜑 → 𝐴 ∈ (𝐵𝐼𝐶)) | ||
Theorem | tgldim0cgr 26299 | In dimension zero, any two pairs of points are congruent. (Contributed by Thierry Arnoux, 12-Apr-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → (♯‘𝑃) = 1) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) ⇒ ⊢ (𝜑 → (𝐴 − 𝐵) = (𝐶 − 𝐷)) | ||
Theorem | tgbtwndiff 26300* | There is always a 𝑐 distinct from 𝐵 such that 𝐵 lies between 𝐴 and 𝑐. Theorem 3.14 of [Schwabhauser] p. 32. The condition "the space is of dimension 1 or more" is written here as 2 ≤ (♯‘𝑃) for simplicity. (Contributed by Thierry Arnoux, 23-Mar-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 2 ≤ (♯‘𝑃)) ⇒ ⊢ (𝜑 → ∃𝑐 ∈ 𝑃 (𝐵 ∈ (𝐴𝐼𝑐) ∧ 𝐵 ≠ 𝑐)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |