![]() |
Metamath
Proof Explorer Theorem List (p. 267 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: | ![]() (1-28701) |
![]() (28702-30224) |
![]() (30225-45333) |
Type | Label | Description |
---|---|---|
Statement | ||
Syntax | ccgra 26601 | Declare the constant for the congruence between angles relation. |
class cgrA | ||
Definition | df-cgra 26602* | Define the congruence relation between angles. As for triangles we use "words of points". See iscgra 26603 for a more human readable version. (Contributed by Thierry Arnoux, 30-Jul-2020.) |
⊢ cgrA = (𝑔 ∈ V ↦ {〈𝑎, 𝑏〉 ∣ [(Base‘𝑔) / 𝑝][(hlG‘𝑔) / 𝑘]((𝑎 ∈ (𝑝 ↑m (0..^3)) ∧ 𝑏 ∈ (𝑝 ↑m (0..^3))) ∧ ∃𝑥 ∈ 𝑝 ∃𝑦 ∈ 𝑝 (𝑎(cgrG‘𝑔)〈“𝑥(𝑏‘1)𝑦”〉 ∧ 𝑥(𝑘‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝑘‘(𝑏‘1))(𝑏‘2)))}) | ||
Theorem | iscgra 26603* | Property for two angles ABC and DEF to be congruent. This is a modified version of the definition 11.3 of [Schwabhauser] p. 95. where the number of constructed points has been reduced to two. We chose this version rather than the textbook version because it is shorter and therefore simpler to work with. Theorem dfcgra2 26624 shows that those definitions are indeed equivalent. (Contributed by Thierry Arnoux, 31-Jul-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐾 = (hlG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) ⇒ ⊢ (𝜑 → (〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉 ↔ ∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑥𝐸𝑦”〉 ∧ 𝑥(𝐾‘𝐸)𝐷 ∧ 𝑦(𝐾‘𝐸)𝐹))) | ||
Theorem | iscgra1 26604* | A special version of iscgra 26603 where one distance is known to be equal. In this case, angle congruence can be written with only one quantifier. (Contributed by Thierry Arnoux, 9-Aug-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐾 = (hlG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ − = (dist‘𝐺) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) & ⊢ (𝜑 → (𝐴 − 𝐵) = (𝐷 − 𝐸)) ⇒ ⊢ (𝜑 → (〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉 ↔ ∃𝑥 ∈ 𝑃 (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝐷𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝐹))) | ||
Theorem | iscgrad 26605 | Sufficient conditions for angle congruence, deduction version. (Contributed by Thierry Arnoux, 1-Aug-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐾 = (hlG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑋𝐸𝑌”〉) & ⊢ (𝜑 → 𝑋(𝐾‘𝐸)𝐷) & ⊢ (𝜑 → 𝑌(𝐾‘𝐸)𝐹) ⇒ ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) | ||
Theorem | cgrane1 26606 | Angles imply inequality. (Contributed by Thierry Arnoux, 1-Aug-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐾 = (hlG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) ⇒ ⊢ (𝜑 → 𝐴 ≠ 𝐵) | ||
Theorem | cgrane2 26607 | Angles imply inequality. (Contributed by Thierry Arnoux, 1-Aug-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐾 = (hlG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) ⇒ ⊢ (𝜑 → 𝐵 ≠ 𝐶) | ||
Theorem | cgrane3 26608 | Angles imply inequality. (Contributed by Thierry Arnoux, 1-Aug-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐾 = (hlG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) ⇒ ⊢ (𝜑 → 𝐸 ≠ 𝐷) | ||
Theorem | cgrane4 26609 | Angles imply inequality. (Contributed by Thierry Arnoux, 1-Aug-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐾 = (hlG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) ⇒ ⊢ (𝜑 → 𝐸 ≠ 𝐹) | ||
Theorem | cgrahl1 26610 | Angle congruence is independent of the choice of points on the rays. Proposition 11.10 of [Schwabhauser] p. 95. (Contributed by Thierry Arnoux, 1-Aug-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐾 = (hlG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑋(𝐾‘𝐸)𝐷) ⇒ ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝑋𝐸𝐹”〉) | ||
Theorem | cgrahl2 26611 | Angle congruence is independent of the choice of points on the rays. Proposition 11.10 of [Schwabhauser] p. 95. (Contributed by Thierry Arnoux, 1-Aug-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐾 = (hlG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑋(𝐾‘𝐸)𝐹) ⇒ ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝑋”〉) | ||
Theorem | cgracgr 26612 | First direction of proposition 11.4 of [Schwabhauser] p. 95. Again, this is "half" of the proposition, i.e. only two additional points are used, while Schwabhauser has four. (Contributed by Thierry Arnoux, 31-Jul-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐾 = (hlG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ − = (dist‘𝐺) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ (𝜑 → 𝑋(𝐾‘𝐵)𝐴) & ⊢ (𝜑 → 𝑌(𝐾‘𝐵)𝐶) & ⊢ (𝜑 → (𝐵 − 𝑋) = (𝐸 − 𝐷)) & ⊢ (𝜑 → (𝐵 − 𝑌) = (𝐸 − 𝐹)) ⇒ ⊢ (𝜑 → (𝑋 − 𝑌) = (𝐷 − 𝐹)) | ||
Theorem | cgraid 26613 | Angle congruence is reflexive. Theorem 11.6 of [Schwabhauser] p. 96. (Contributed by Thierry Arnoux, 31-Jul-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ 𝐾 = (hlG‘𝐺) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) & ⊢ (𝜑 → 𝐵 ≠ 𝐶) ⇒ ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐴𝐵𝐶”〉) | ||
Theorem | cgraswap 26614 | Swap rays in a congruence relation. Theorem 11.9 of [Schwabhauser] p. 96. (Contributed by Thierry Arnoux, 5-Mar-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ 𝐾 = (hlG‘𝐺) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) & ⊢ (𝜑 → 𝐵 ≠ 𝐶) ⇒ ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐶𝐵𝐴”〉) | ||
Theorem | cgrcgra 26615 | Triangle congruence implies angle congruence. This is a portion of CPCTC, focusing on a specific angle. (Contributed by Arnoux, 2-Aug-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ 𝐾 = (hlG‘𝐺) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) & ⊢ (𝜑 → 𝐵 ≠ 𝐶) & ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝐷𝐸𝐹”〉) ⇒ ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) | ||
Theorem | cgracom 26616 | Angle congruence commutes. Theorem 11.7 of [Schwabhauser] p. 97. (Contributed by Thierry Arnoux, 5-Mar-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ 𝐾 = (hlG‘𝐺) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) ⇒ ⊢ (𝜑 → 〈“𝐷𝐸𝐹”〉(cgrA‘𝐺)〈“𝐴𝐵𝐶”〉) | ||
Theorem | cgratr 26617 | Angle congruence is transitive. Theorem 11.8 of [Schwabhauser] p. 97. (Contributed by Thierry Arnoux, 5-Mar-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ 𝐾 = (hlG‘𝐺) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) & ⊢ (𝜑 → 𝐻 ∈ 𝑃) & ⊢ (𝜑 → 𝑈 ∈ 𝑃) & ⊢ (𝜑 → 𝐽 ∈ 𝑃) & ⊢ (𝜑 → 〈“𝐷𝐸𝐹”〉(cgrA‘𝐺)〈“𝐻𝑈𝐽”〉) ⇒ ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐻𝑈𝐽”〉) | ||
Theorem | flatcgra 26618 | Flat angles are congruent. (Contributed by Thierry Arnoux, 13-Feb-2023.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐶)) & ⊢ (𝜑 → 𝐸 ∈ (𝐷𝐼𝐹)) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) & ⊢ (𝜑 → 𝐶 ≠ 𝐵) & ⊢ (𝜑 → 𝐷 ≠ 𝐸) & ⊢ (𝜑 → 𝐹 ≠ 𝐸) ⇒ ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) | ||
Theorem | cgraswaplr 26619 | Swap both side of angle congruence. (Contributed by Thierry Arnoux, 5-Oct-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) ⇒ ⊢ (𝜑 → 〈“𝐶𝐵𝐴”〉(cgrA‘𝐺)〈“𝐹𝐸𝐷”〉) | ||
Theorem | cgrabtwn 26620 | Angle congruence preserves flat angles. Part of Theorem 11.21 of [Schwabhauser] p. 97. (Contributed by Thierry Arnoux, 9-Aug-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) & ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐶)) ⇒ ⊢ (𝜑 → 𝐸 ∈ (𝐷𝐼𝐹)) | ||
Theorem | cgrahl 26621 | Angle congruence preserves null angles. Part of Theorem 11.21 of [Schwabhauser] p. 97. (Contributed by Thierry Arnoux, 9-Aug-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) & ⊢ 𝐾 = (hlG‘𝐺) & ⊢ (𝜑 → 𝐴(𝐾‘𝐵)𝐶) ⇒ ⊢ (𝜑 → 𝐷(𝐾‘𝐸)𝐹) | ||
Theorem | cgracol 26622 | Angle congruence preserves colinearity. (Contributed by Thierry Arnoux, 9-Aug-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ⇒ ⊢ (𝜑 → (𝐹 ∈ (𝐷𝐿𝐸) ∨ 𝐷 = 𝐸)) | ||
Theorem | cgrancol 26623 | Angle congruence preserves non-colinearity. (Contributed by Thierry Arnoux, 9-Aug-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ⇒ ⊢ (𝜑 → ¬ (𝐹 ∈ (𝐷𝐿𝐸) ∨ 𝐷 = 𝐸)) | ||
Theorem | dfcgra2 26624* | This is the full statement of definition 11.2 of [Schwabhauser] p. 95. This proof serves to confirm that the definition we have chosen, df-cgra 26602 is indeed equivalent to the textbook's definition. (Contributed by Thierry Arnoux, 2-Aug-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) ⇒ ⊢ (𝜑 → (〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉 ↔ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸) ∧ ∃𝑎 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝑎 − 𝑐) = (𝑑 − 𝑓))))) | ||
Theorem | sacgr 26625 | Supplementary angles of congruent angles are themselves congruent. Theorem 11.13 of [Schwabhauser] p. 98. (Contributed by Thierry Arnoux, 30-Sep-2020.) (Proof shortened by Igor Ieskov, 16-Feb-2023.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) & ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝑋)) & ⊢ (𝜑 → 𝐸 ∈ (𝐷𝐼𝑌)) & ⊢ (𝜑 → 𝐵 ≠ 𝑋) & ⊢ (𝜑 → 𝐸 ≠ 𝑌) ⇒ ⊢ (𝜑 → 〈“𝑋𝐵𝐶”〉(cgrA‘𝐺)〈“𝑌𝐸𝐹”〉) | ||
Theorem | oacgr 26626 | Vertical angle theorem. Vertical, or opposite angles are the facing pair of angles formed when two lines intersect. Eudemus of Rhodes attributed the proof to Thales of Miletus. The proposition showed that since both of a pair of vertical angles are supplementary to both of the adjacent angles, the vertical angles are equal in measure. We follow the same path. Theorem 11.14 of [Schwabhauser] p. 98. (Contributed by Thierry Arnoux, 27-Sep-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐷)) & ⊢ (𝜑 → 𝐵 ∈ (𝐶𝐼𝐹)) & ⊢ (𝜑 → 𝐵 ≠ 𝐴) & ⊢ (𝜑 → 𝐵 ≠ 𝐶) & ⊢ (𝜑 → 𝐵 ≠ 𝐷) & ⊢ (𝜑 → 𝐵 ≠ 𝐹) ⇒ ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐵𝐹”〉) | ||
Theorem | acopy 26627* | Angle construction. Theorem 11.15 of [Schwabhauser] p. 98. This is Hilbert's axiom III.4 for geometry. (Contributed by Thierry Arnoux, 9-Aug-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → ¬ (𝐴 ∈ (𝐵𝐿𝐶) ∨ 𝐵 = 𝐶)) & ⊢ (𝜑 → ¬ (𝐷 ∈ (𝐸𝐿𝐹) ∨ 𝐸 = 𝐹)) ⇒ ⊢ (𝜑 → ∃𝑓 ∈ 𝑃 (〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝑓”〉 ∧ 𝑓((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) | ||
Theorem | acopyeu 26628 | Angle construction. Theorem 11.15 of [Schwabhauser] p. 98. This is Hilbert's axiom III.4 for geometry. Akin to a uniqueness theorem, this states that if two points 𝑋 and 𝑌 both fulfill the conditions, then they are on the same half-line. (Contributed by Thierry Arnoux, 9-Aug-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → ¬ (𝐴 ∈ (𝐵𝐿𝐶) ∨ 𝐵 = 𝐶)) & ⊢ (𝜑 → ¬ (𝐷 ∈ (𝐸𝐿𝐹) ∨ 𝐸 = 𝐹)) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ 𝐾 = (hlG‘𝐺) & ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝑋”〉) & ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝑌”〉) & ⊢ (𝜑 → 𝑋((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹) & ⊢ (𝜑 → 𝑌((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹) ⇒ ⊢ (𝜑 → 𝑋(𝐾‘𝐸)𝑌) | ||
Syntax | cinag 26629 | Extend class relation with the geometrical "point in angle" relation. |
class inA | ||
Syntax | cleag 26630 | Extend class relation with the "angle less than" relation. |
class ≤∠ | ||
Definition | df-inag 26631* | Definition of the geometrical "in angle" relation. (Contributed by Thierry Arnoux, 15-Aug-2020.) |
⊢ inA = (𝑔 ∈ V ↦ {〈𝑝, 𝑡〉 ∣ ((𝑝 ∈ (Base‘𝑔) ∧ 𝑡 ∈ ((Base‘𝑔) ↑m (0..^3))) ∧ (((𝑡‘0) ≠ (𝑡‘1) ∧ (𝑡‘2) ≠ (𝑡‘1) ∧ 𝑝 ≠ (𝑡‘1)) ∧ ∃𝑥 ∈ (Base‘𝑔)(𝑥 ∈ ((𝑡‘0)(Itv‘𝑔)(𝑡‘2)) ∧ (𝑥 = (𝑡‘1) ∨ 𝑥((hlG‘𝑔)‘(𝑡‘1))𝑝))))}) | ||
Theorem | isinag 26632* | Property for point 𝑋 to lie in the angle 〈“𝐴𝐵𝐶”〉. Definition 11.23 of [Schwabhauser] p. 101. (Contributed by Thierry Arnoux, 15-Aug-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐾 = (hlG‘𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐺 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝑋(inA‘𝐺)〈“𝐴𝐵𝐶”〉 ↔ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ∧ 𝑋 ≠ 𝐵) ∧ ∃𝑥 ∈ 𝑃 (𝑥 ∈ (𝐴𝐼𝐶) ∧ (𝑥 = 𝐵 ∨ 𝑥(𝐾‘𝐵)𝑋))))) | ||
Theorem | isinagd 26633 | Sufficient conditions for in-angle relation, deduction version. (Contributed by Thierry Arnoux, 20-Oct-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐾 = (hlG‘𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐺 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) & ⊢ (𝜑 → 𝐶 ≠ 𝐵) & ⊢ (𝜑 → 𝑋 ≠ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ (𝐴𝐼𝐶)) & ⊢ (𝜑 → (𝑌 = 𝐵 ∨ 𝑌(𝐾‘𝐵)𝑋)) ⇒ ⊢ (𝜑 → 𝑋(inA‘𝐺)〈“𝐴𝐵𝐶”〉) | ||
Theorem | inagflat 26634 | Any point lies in a flat angle. (Contributed by Thierry Arnoux, 13-Feb-2023.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐾 = (hlG‘𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) & ⊢ (𝜑 → 𝐶 ≠ 𝐵) & ⊢ (𝜑 → 𝑋 ≠ 𝐵) & ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐶)) ⇒ ⊢ (𝜑 → 𝑋(inA‘𝐺)〈“𝐴𝐵𝐶”〉) | ||
Theorem | inagswap 26635 | Swap the order of the half lines delimiting the angle. Theorem 11.24 of [Schwabhauser] p. 101. (Contributed by Thierry Arnoux, 15-Aug-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐾 = (hlG‘𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝑋(inA‘𝐺)〈“𝐴𝐵𝐶”〉) ⇒ ⊢ (𝜑 → 𝑋(inA‘𝐺)〈“𝐶𝐵𝐴”〉) | ||
Theorem | inagne1 26636 | Deduce inequality from the in-angle relation. (Contributed by Thierry Arnoux, 29-Oct-2021.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐾 = (hlG‘𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝑋(inA‘𝐺)〈“𝐴𝐵𝐶”〉) ⇒ ⊢ (𝜑 → 𝐴 ≠ 𝐵) | ||
Theorem | inagne2 26637 | Deduce inequality from the in-angle relation. (Contributed by Thierry Arnoux, 29-Oct-2021.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐾 = (hlG‘𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝑋(inA‘𝐺)〈“𝐴𝐵𝐶”〉) ⇒ ⊢ (𝜑 → 𝐶 ≠ 𝐵) | ||
Theorem | inagne3 26638 | Deduce inequality from the in-angle relation. (Contributed by Thierry Arnoux, 29-Oct-2021.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐾 = (hlG‘𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝑋(inA‘𝐺)〈“𝐴𝐵𝐶”〉) ⇒ ⊢ (𝜑 → 𝑋 ≠ 𝐵) | ||
Theorem | inaghl 26639 | The "point lie in angle" relation is independent of the points chosen on the half lines starting from 𝐵. Theorem 11.25 of [Schwabhauser] p. 101. (Contributed by Thierry Arnoux, 27-Sep-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐾 = (hlG‘𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝑋(inA‘𝐺)〈“𝐴𝐵𝐶”〉) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ (𝜑 → 𝐷(𝐾‘𝐵)𝐴) & ⊢ (𝜑 → 𝐹(𝐾‘𝐵)𝐶) & ⊢ (𝜑 → 𝑌(𝐾‘𝐵)𝑋) ⇒ ⊢ (𝜑 → 𝑌(inA‘𝐺)〈“𝐷𝐵𝐹”〉) | ||
Definition | df-leag 26640* | Definition of the geometrical "angle less than" relation. Definition 11.27 of [Schwabhauser] p. 102. (Contributed by Thierry Arnoux, 7-Oct-2020.) |
⊢ ≤∠ = (𝑔 ∈ V ↦ {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ ((Base‘𝑔) ↑m (0..^3)) ∧ 𝑏 ∈ ((Base‘𝑔) ↑m (0..^3))) ∧ ∃𝑥 ∈ (Base‘𝑔)(𝑥(inA‘𝑔)〈“(𝑏‘0)(𝑏‘1)(𝑏‘2)”〉 ∧ 〈“(𝑎‘0)(𝑎‘1)(𝑎‘2)”〉(cgrA‘𝑔)〈“(𝑏‘0)(𝑏‘1)𝑥”〉))}) | ||
Theorem | isleag 26641* | Geometrical "less than" property for angles. Definition 11.27 of [Schwabhauser] p. 102. (Contributed by Thierry Arnoux, 7-Oct-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) ⇒ ⊢ (𝜑 → (〈“𝐴𝐵𝐶”〉(≤∠‘𝐺)〈“𝐷𝐸𝐹”〉 ↔ ∃𝑥 ∈ 𝑃 (𝑥(inA‘𝐺)〈“𝐷𝐸𝐹”〉 ∧ 〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝑥”〉))) | ||
Theorem | isleagd 26642 | Sufficient condition for "less than" angle relation, deduction version (Contributed by Thierry Arnoux, 12-Oct-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ ≤ = (≤∠‘𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑋(inA‘𝐺)〈“𝐷𝐸𝐹”〉) & ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝑋”〉) ⇒ ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉 ≤ 〈“𝐷𝐸𝐹”〉) | ||
Theorem | leagne1 26643 | Deduce inequality from the less-than angle relation. (Contributed by Thierry Arnoux, 25-Feb-2023.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉(≤∠‘𝐺)〈“𝐷𝐸𝐹”〉) ⇒ ⊢ (𝜑 → 𝐴 ≠ 𝐵) | ||
Theorem | leagne2 26644 | Deduce inequality from the less-than angle relation. (Contributed by Thierry Arnoux, 25-Feb-2023.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉(≤∠‘𝐺)〈“𝐷𝐸𝐹”〉) ⇒ ⊢ (𝜑 → 𝐶 ≠ 𝐵) | ||
Theorem | leagne3 26645 | Deduce inequality from the less-than angle relation. (Contributed by Thierry Arnoux, 25-Feb-2023.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉(≤∠‘𝐺)〈“𝐷𝐸𝐹”〉) ⇒ ⊢ (𝜑 → 𝐷 ≠ 𝐸) | ||
Theorem | leagne4 26646 | Deduce inequality from the less-than angle relation. (Contributed by Thierry Arnoux, 25-Feb-2023.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉(≤∠‘𝐺)〈“𝐷𝐸𝐹”〉) ⇒ ⊢ (𝜑 → 𝐹 ≠ 𝐸) | ||
Theorem | cgrg3col4 26647* | Lemma 11.28 of [Schwabhauser] p. 102. Extend a congruence of three points with a fourth colinear point. (Contributed by Thierry Arnoux, 8-Oct-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝐷𝐸𝐹”〉) & ⊢ (𝜑 → (𝑋 ∈ (𝐴𝐿𝐶) ∨ 𝐴 = 𝐶)) ⇒ ⊢ (𝜑 → ∃𝑦 ∈ 𝑃 〈“𝐴𝐵𝐶𝑋”〉(cgrG‘𝐺)〈“𝐷𝐸𝐹𝑦”〉) | ||
Theorem | tgsas1 26648 | First congruence theorem: SAS (Side-Angle-Side): If two pairs of sides of two triangles are equal in length, and the included angles are equal in measurement, then third sides are equal in length. Theorem 11.49 of [Schwabhauser] p. 107. (Contributed by Thierry Arnoux, 1-Aug-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ (𝜑 → (𝐴 − 𝐵) = (𝐷 − 𝐸)) & ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) & ⊢ (𝜑 → (𝐵 − 𝐶) = (𝐸 − 𝐹)) ⇒ ⊢ (𝜑 → (𝐶 − 𝐴) = (𝐹 − 𝐷)) | ||
Theorem | tgsas 26649 | First congruence theorem: SAS (Side-Angle-Side): If two pairs of sides of two triangles are equal in length, and the included angles are equal in measurement, then the triangles are congruent. Theorem 11.49 of [Schwabhauser] p. 107. (Contributed by Thierry Arnoux, 1-Aug-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ (𝜑 → (𝐴 − 𝐵) = (𝐷 − 𝐸)) & ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) & ⊢ (𝜑 → (𝐵 − 𝐶) = (𝐸 − 𝐹)) ⇒ ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝐷𝐸𝐹”〉) | ||
Theorem | tgsas2 26650 | First congruence theorem: SAS. Theorem 11.49 of [Schwabhauser] p. 107. (Contributed by Thierry Arnoux, 1-Aug-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ (𝜑 → (𝐴 − 𝐵) = (𝐷 − 𝐸)) & ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) & ⊢ (𝜑 → (𝐵 − 𝐶) = (𝐸 − 𝐹)) & ⊢ (𝜑 → 𝐴 ≠ 𝐶) ⇒ ⊢ (𝜑 → 〈“𝐶𝐴𝐵”〉(cgrA‘𝐺)〈“𝐹𝐷𝐸”〉) | ||
Theorem | tgsas3 26651 | First congruence theorem: SAS. Theorem 11.49 of [Schwabhauser] p. 107. (Contributed by Thierry Arnoux, 1-Aug-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ (𝜑 → (𝐴 − 𝐵) = (𝐷 − 𝐸)) & ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) & ⊢ (𝜑 → (𝐵 − 𝐶) = (𝐸 − 𝐹)) & ⊢ (𝜑 → 𝐴 ≠ 𝐶) ⇒ ⊢ (𝜑 → 〈“𝐵𝐶𝐴”〉(cgrA‘𝐺)〈“𝐸𝐹𝐷”〉) | ||
Theorem | tgasa1 26652 | Second congruence theorem: ASA. (Angle-Side-Angle): If two pairs of angles of two triangles are equal in measurement, and the included sides are equal in length, then the triangles are congruent. Theorem 11.50 of [Schwabhauser] p. 108. (Contributed by Thierry Arnoux, 15-Aug-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) & ⊢ (𝜑 → (𝐴 − 𝐵) = (𝐷 − 𝐸)) & ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) & ⊢ (𝜑 → 〈“𝐶𝐴𝐵”〉(cgrA‘𝐺)〈“𝐹𝐷𝐸”〉) ⇒ ⊢ (𝜑 → (𝐵 − 𝐶) = (𝐸 − 𝐹)) | ||
Theorem | tgasa 26653 | Second congruence theorem: ASA. (Angle-Side-Angle): If two pairs of angles of two triangles are equal in measurement, and the included sides are equal in length, then the triangles are congruent. Theorem 11.50 of [Schwabhauser] p. 108. (Contributed by Thierry Arnoux, 15-Aug-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) & ⊢ (𝜑 → (𝐴 − 𝐵) = (𝐷 − 𝐸)) & ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) & ⊢ (𝜑 → 〈“𝐶𝐴𝐵”〉(cgrA‘𝐺)〈“𝐹𝐷𝐸”〉) ⇒ ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝐷𝐸𝐹”〉) | ||
Theorem | tgsss1 26654 | Third congruence theorem: SSS (Side-Side-Side): If the three pairs of sides of two triangles are equal in length, then the triangles are congruent. Theorem 11.51 of [Schwabhauser] p. 109. (Contributed by Thierry Arnoux, 1-Aug-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ (𝜑 → (𝐴 − 𝐵) = (𝐷 − 𝐸)) & ⊢ (𝜑 → (𝐵 − 𝐶) = (𝐸 − 𝐹)) & ⊢ (𝜑 → (𝐶 − 𝐴) = (𝐹 − 𝐷)) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) & ⊢ (𝜑 → 𝐵 ≠ 𝐶) & ⊢ (𝜑 → 𝐶 ≠ 𝐴) ⇒ ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) | ||
Theorem | tgsss2 26655 | Third congruence theorem: SSS. Theorem 11.51 of [Schwabhauser] p. 109. (Contributed by Thierry Arnoux, 1-Aug-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ (𝜑 → (𝐴 − 𝐵) = (𝐷 − 𝐸)) & ⊢ (𝜑 → (𝐵 − 𝐶) = (𝐸 − 𝐹)) & ⊢ (𝜑 → (𝐶 − 𝐴) = (𝐹 − 𝐷)) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) & ⊢ (𝜑 → 𝐵 ≠ 𝐶) & ⊢ (𝜑 → 𝐶 ≠ 𝐴) ⇒ ⊢ (𝜑 → 〈“𝐶𝐴𝐵”〉(cgrA‘𝐺)〈“𝐹𝐷𝐸”〉) | ||
Theorem | tgsss3 26656 | Third congruence theorem: SSS. Theorem 11.51 of [Schwabhauser] p. 109. (Contributed by Thierry Arnoux, 1-Aug-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ (𝜑 → (𝐴 − 𝐵) = (𝐷 − 𝐸)) & ⊢ (𝜑 → (𝐵 − 𝐶) = (𝐸 − 𝐹)) & ⊢ (𝜑 → (𝐶 − 𝐴) = (𝐹 − 𝐷)) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) & ⊢ (𝜑 → 𝐵 ≠ 𝐶) & ⊢ (𝜑 → 𝐶 ≠ 𝐴) ⇒ ⊢ (𝜑 → 〈“𝐵𝐶𝐴”〉(cgrA‘𝐺)〈“𝐸𝐹𝐷”〉) | ||
Theorem | dfcgrg2 26657 | Congruence for two triangles can also be defined as congruence of sides and angles (6 parts). This is often the actual textbook definition of triangle congruence, see for example https://en.wikipedia.org/wiki/Congruence_(geometry)#Congruence_of_triangles. With this definition, the "SSS" congruence theorem has an additional part, namely, that triangle congruence implies congruence of the sides (which means equality of the lengths). Because our development of elementary geometry strives to closely follow Schwabhaeuser's, our original definition of shape congruence, df-cgrg 26305, already covers that part: see trgcgr 26310. This theorem is also named "CPCTC", which stands for "Corresponding Parts of Congruent Triangles are Congruent", see https://en.wikipedia.org/wiki/Congruence_(geometry)#CPCTC 26310. (Contributed by Thierry Arnoux, 18-Jan-2023.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) & ⊢ (𝜑 → 𝐵 ≠ 𝐶) & ⊢ (𝜑 → 𝐶 ≠ 𝐴) ⇒ ⊢ (𝜑 → (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝐷𝐸𝐹”〉 ↔ (((𝐴 − 𝐵) = (𝐷 − 𝐸) ∧ (𝐵 − 𝐶) = (𝐸 − 𝐹) ∧ (𝐶 − 𝐴) = (𝐹 − 𝐷)) ∧ (〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉 ∧ 〈“𝐶𝐴𝐵”〉(cgrA‘𝐺)〈“𝐹𝐷𝐸”〉 ∧ 〈“𝐵𝐶𝐴”〉(cgrA‘𝐺)〈“𝐸𝐹𝐷”〉)))) | ||
Theorem | isoas 26658 | Congruence theorem for isocele triangles: if two angles of a triangle are congruent, then the corresponding sides also are. (Contributed by Thierry Arnoux, 5-Oct-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) & ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐴𝐶𝐵”〉) ⇒ ⊢ (𝜑 → (𝐴 − 𝐵) = (𝐴 − 𝐶)) | ||
Syntax | ceqlg 26659 | Declare the class of equilateral triangles. |
class eqltrG | ||
Definition | df-eqlg 26660* | Define the class of equilateral triangles. (Contributed by Thierry Arnoux, 27-Nov-2019.) |
⊢ eqltrG = (𝑔 ∈ V ↦ {𝑥 ∈ ((Base‘𝑔) ↑m (0..^3)) ∣ 𝑥(cgrG‘𝑔)〈“(𝑥‘1)(𝑥‘2)(𝑥‘0)”〉}) | ||
Theorem | iseqlg 26661 | Property of a triangle being equilateral. (Contributed by Thierry Arnoux, 5-Oct-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) ⇒ ⊢ (𝜑 → (〈“𝐴𝐵𝐶”〉 ∈ (eqltrG‘𝐺) ↔ 〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝐵𝐶𝐴”〉)) | ||
Theorem | iseqlgd 26662 | Condition for a triangle to be equilateral. (Contributed by Thierry Arnoux, 5-Oct-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → (𝐴 − 𝐵) = (𝐵 − 𝐶)) & ⊢ (𝜑 → (𝐵 − 𝐶) = (𝐶 − 𝐴)) & ⊢ (𝜑 → (𝐶 − 𝐴) = (𝐴 − 𝐵)) ⇒ ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉 ∈ (eqltrG‘𝐺)) | ||
Theorem | f1otrgds 26663* | Convenient lemma for f1otrg 26665. (Contributed by Thierry Arnoux, 19-Mar-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐷 = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐵 = (Base‘𝐻) & ⊢ 𝐸 = (dist‘𝐻) & ⊢ 𝐽 = (Itv‘𝐻) & ⊢ (𝜑 → 𝐹:𝐵–1-1-onto→𝑃) & ⊢ ((𝜑 ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) → (𝑒𝐸𝑓) = ((𝐹‘𝑒)𝐷(𝐹‘𝑓))) & ⊢ ((𝜑 ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹‘𝑔) ∈ ((𝐹‘𝑒)𝐼(𝐹‘𝑓)))) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋𝐸𝑌) = ((𝐹‘𝑋)𝐷(𝐹‘𝑌))) | ||
Theorem | f1otrgitv 26664* | Convenient lemma for f1otrg 26665. (Contributed by Thierry Arnoux, 19-Mar-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐷 = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐵 = (Base‘𝐻) & ⊢ 𝐸 = (dist‘𝐻) & ⊢ 𝐽 = (Itv‘𝐻) & ⊢ (𝜑 → 𝐹:𝐵–1-1-onto→𝑃) & ⊢ ((𝜑 ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) → (𝑒𝐸𝑓) = ((𝐹‘𝑒)𝐷(𝐹‘𝑓))) & ⊢ ((𝜑 ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹‘𝑔) ∈ ((𝐹‘𝑒)𝐼(𝐹‘𝑓)))) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑍 ∈ (𝑋𝐽𝑌) ↔ (𝐹‘𝑍) ∈ ((𝐹‘𝑋)𝐼(𝐹‘𝑌)))) | ||
Theorem | f1otrg 26665* | A bijection between bases which conserves distances and intervals conserves also geometries. (Contributed by Thierry Arnoux, 23-Mar-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐷 = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐵 = (Base‘𝐻) & ⊢ 𝐸 = (dist‘𝐻) & ⊢ 𝐽 = (Itv‘𝐻) & ⊢ (𝜑 → 𝐹:𝐵–1-1-onto→𝑃) & ⊢ ((𝜑 ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) → (𝑒𝐸𝑓) = ((𝐹‘𝑒)𝐷(𝐹‘𝑓))) & ⊢ ((𝜑 ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹‘𝑔) ∈ ((𝐹‘𝑒)𝐼(𝐹‘𝑓)))) & ⊢ (𝜑 → 𝐻 ∈ 𝑉) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → (LineG‘𝐻) = (𝑥 ∈ 𝐵, 𝑦 ∈ (𝐵 ∖ {𝑥}) ↦ {𝑧 ∈ 𝐵 ∣ (𝑧 ∈ (𝑥𝐽𝑦) ∨ 𝑥 ∈ (𝑧𝐽𝑦) ∨ 𝑦 ∈ (𝑥𝐽𝑧))})) ⇒ ⊢ (𝜑 → 𝐻 ∈ TarskiG) | ||
Theorem | f1otrge 26666* | A bijection between bases which conserves distances and intervals conserves also the property of being a Euclidean geometry. (Contributed by Thierry Arnoux, 23-Mar-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐷 = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐵 = (Base‘𝐻) & ⊢ 𝐸 = (dist‘𝐻) & ⊢ 𝐽 = (Itv‘𝐻) & ⊢ (𝜑 → 𝐹:𝐵–1-1-onto→𝑃) & ⊢ ((𝜑 ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) → (𝑒𝐸𝑓) = ((𝐹‘𝑒)𝐷(𝐹‘𝑓))) & ⊢ ((𝜑 ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹‘𝑔) ∈ ((𝐹‘𝑒)𝐼(𝐹‘𝑓)))) & ⊢ (𝜑 → 𝐻 ∈ 𝑉) & ⊢ (𝜑 → 𝐺 ∈ TarskiGE) ⇒ ⊢ (𝜑 → 𝐻 ∈ TarskiGE) | ||
Syntax | cttg 26667 | Function to convert an algebraic structure to a Tarski geometry. |
class toTG | ||
Definition | df-ttg 26668* | Define a function converting a subcomplex Hilbert space to a Tarski Geometry. It does so by equipping the structure with a betweenness operation. Note that because the scalar product is applied over the interval (0[,]1), only spaces whose scalar field is a superset of that interval can be considered. (Contributed by Thierry Arnoux, 24-Mar-2019.) |
⊢ toTG = (𝑤 ∈ V ↦ ⦋(𝑥 ∈ (Base‘𝑤), 𝑦 ∈ (Base‘𝑤) ↦ {𝑧 ∈ (Base‘𝑤) ∣ ∃𝑘 ∈ (0[,]1)(𝑧(-g‘𝑤)𝑥) = (𝑘( ·𝑠 ‘𝑤)(𝑦(-g‘𝑤)𝑥))}) / 𝑖⦌((𝑤 sSet 〈(Itv‘ndx), 𝑖〉) sSet 〈(LineG‘ndx), (𝑥 ∈ (Base‘𝑤), 𝑦 ∈ (Base‘𝑤) ↦ {𝑧 ∈ (Base‘𝑤) ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})〉)) | ||
Theorem | ttgval 26669* | Define a function to augment a subcomplex Hilbert space with betweenness and a line definition. (Contributed by Thierry Arnoux, 25-Mar-2019.) |
⊢ 𝐺 = (toTG‘𝐻) & ⊢ 𝐵 = (Base‘𝐻) & ⊢ − = (-g‘𝐻) & ⊢ · = ( ·𝑠 ‘𝐻) & ⊢ 𝐼 = (Itv‘𝐺) ⇒ ⊢ (𝐻 ∈ 𝑉 → (𝐺 = ((𝐻 sSet 〈(Itv‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})〉) sSet 〈(LineG‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))})〉) ∧ 𝐼 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))}))) | ||
Theorem | ttglem 26670 | Lemma for ttgbas 26671 and ttgvsca 26674. (Contributed by Thierry Arnoux, 15-Apr-2019.) |
⊢ 𝐺 = (toTG‘𝐻) & ⊢ 𝐸 = Slot 𝑁 & ⊢ 𝑁 ∈ ℕ & ⊢ 𝑁 < ;16 ⇒ ⊢ (𝐸‘𝐻) = (𝐸‘𝐺) | ||
Theorem | ttgbas 26671 | The base set of a subcomplex Hilbert space augmented with betweenness. (Contributed by Thierry Arnoux, 25-Mar-2019.) |
⊢ 𝐺 = (toTG‘𝐻) & ⊢ 𝐵 = (Base‘𝐻) ⇒ ⊢ 𝐵 = (Base‘𝐺) | ||
Theorem | ttgplusg 26672 | The addition operation of a subcomplex Hilbert space augmented with betweenness. (Contributed by Thierry Arnoux, 25-Mar-2019.) |
⊢ 𝐺 = (toTG‘𝐻) & ⊢ + = (+g‘𝐻) ⇒ ⊢ + = (+g‘𝐺) | ||
Theorem | ttgsub 26673 | The subtraction operation of a subcomplex Hilbert space augmented with betweenness. (Contributed by Thierry Arnoux, 25-Mar-2019.) |
⊢ 𝐺 = (toTG‘𝐻) & ⊢ − = (-g‘𝐻) ⇒ ⊢ − = (-g‘𝐺) | ||
Theorem | ttgvsca 26674 | The scalar product of a subcomplex Hilbert space augmented with betweenness. (Contributed by Thierry Arnoux, 25-Mar-2019.) |
⊢ 𝐺 = (toTG‘𝐻) & ⊢ · = ( ·𝑠 ‘𝐻) ⇒ ⊢ · = ( ·𝑠 ‘𝐺) | ||
Theorem | ttgds 26675 | The metric of a subcomplex Hilbert space augmented with betweenness. (Contributed by Thierry Arnoux, 25-Mar-2019.) |
⊢ 𝐺 = (toTG‘𝐻) & ⊢ 𝐷 = (dist‘𝐻) ⇒ ⊢ 𝐷 = (dist‘𝐺) | ||
Theorem | ttgitvval 26676* | Betweenness for a subcomplex Hilbert space augmented with betweenness. (Contributed by Thierry Arnoux, 25-Mar-2019.) |
⊢ 𝐺 = (toTG‘𝐻) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝑃 = (Base‘𝐻) & ⊢ − = (-g‘𝐻) & ⊢ · = ( ·𝑠 ‘𝐻) ⇒ ⊢ ((𝐻 ∈ 𝑉 ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃) → (𝑋𝐼𝑌) = {𝑧 ∈ 𝑃 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑋) = (𝑘 · (𝑌 − 𝑋))}) | ||
Theorem | ttgelitv 26677* | Betweenness for a subcomplex Hilbert space augmented with betweenness. (Contributed by Thierry Arnoux, 25-Mar-2019.) |
⊢ 𝐺 = (toTG‘𝐻) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝑃 = (Base‘𝐻) & ⊢ − = (-g‘𝐻) & ⊢ · = ( ·𝑠 ‘𝐻) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ (𝜑 → 𝐻 ∈ 𝑉) & ⊢ (𝜑 → 𝑍 ∈ 𝑃) ⇒ ⊢ (𝜑 → (𝑍 ∈ (𝑋𝐼𝑌) ↔ ∃𝑘 ∈ (0[,]1)(𝑍 − 𝑋) = (𝑘 · (𝑌 − 𝑋)))) | ||
Theorem | ttgbtwnid 26678 | Any subcomplex module equipped with the betweenness operation fulfills the identity of betweenness (Axiom A6). (Contributed by Thierry Arnoux, 26-Mar-2019.) |
⊢ 𝐺 = (toTG‘𝐻) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝑃 = (Base‘𝐻) & ⊢ − = (-g‘𝐻) & ⊢ · = ( ·𝑠 ‘𝐻) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ 𝑅 = (Base‘(Scalar‘𝐻)) & ⊢ (𝜑 → (0[,]1) ⊆ 𝑅) & ⊢ (𝜑 → 𝐻 ∈ ℂMod) & ⊢ (𝜑 → 𝑌 ∈ (𝑋𝐼𝑋)) ⇒ ⊢ (𝜑 → 𝑋 = 𝑌) | ||
Theorem | ttgcontlem1 26679 | Lemma for % ttgcont . (Contributed by Thierry Arnoux, 24-May-2019.) |
⊢ 𝐺 = (toTG‘𝐻) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝑃 = (Base‘𝐻) & ⊢ − = (-g‘𝐻) & ⊢ · = ( ·𝑠 ‘𝐻) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ 𝑅 = (Base‘(Scalar‘𝐻)) & ⊢ (𝜑 → (0[,]1) ⊆ 𝑅) & ⊢ + = (+g‘𝐻) & ⊢ (𝜑 → 𝐻 ∈ ℂVec) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝑁 ∈ 𝑃) & ⊢ (𝜑 → 𝑀 ≠ 0) & ⊢ (𝜑 → 𝐾 ≠ 0) & ⊢ (𝜑 → 𝐾 ≠ 1) & ⊢ (𝜑 → 𝐿 ≠ 𝑀) & ⊢ (𝜑 → 𝐿 ≤ (𝑀 / 𝐾)) & ⊢ (𝜑 → 𝐿 ∈ (0[,]1)) & ⊢ (𝜑 → 𝐾 ∈ (0[,]1)) & ⊢ (𝜑 → 𝑀 ∈ (0[,]𝐿)) & ⊢ (𝜑 → (𝑋 − 𝐴) = (𝐾 · (𝑌 − 𝐴))) & ⊢ (𝜑 → (𝑋 − 𝐴) = (𝑀 · (𝑁 − 𝐴))) & ⊢ (𝜑 → 𝐵 = (𝐴 + (𝐿 · (𝑁 − 𝐴)))) ⇒ ⊢ (𝜑 → 𝐵 ∈ (𝑋𝐼𝑌)) | ||
Theorem | xmstrkgc 26680 | Any metric space fulfills Tarski's geometry axioms of congruence. (Contributed by Thierry Arnoux, 13-Mar-2019.) |
⊢ (𝐺 ∈ ∞MetSp → 𝐺 ∈ TarskiGC) | ||
Theorem | cchhllem 26681* | Lemma for chlbas and chlvsca . (Contributed by Thierry Arnoux, 15-Apr-2019.) |
⊢ 𝐶 = (((subringAlg ‘ℂfld)‘ℝ) sSet 〈(·𝑖‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · (∗‘𝑦)))〉) & ⊢ 𝐸 = Slot 𝑁 & ⊢ 𝑁 ∈ ℕ & ⊢ (𝑁 < 5 ∨ 8 < 𝑁) ⇒ ⊢ (𝐸‘ℂfld) = (𝐸‘𝐶) | ||
Syntax | cee 26682 | Declare the syntax for the Euclidean space generator. |
class 𝔼 | ||
Syntax | cbtwn 26683 | Declare the syntax for the Euclidean betweenness predicate. |
class Btwn | ||
Syntax | ccgr 26684 | Declare the syntax for the Euclidean congruence predicate. |
class Cgr | ||
Definition | df-ee 26685 | Define the Euclidean space generator. For details, see elee 26688. (Contributed by Scott Fenton, 3-Jun-2013.) |
⊢ 𝔼 = (𝑛 ∈ ℕ ↦ (ℝ ↑m (1...𝑛))) | ||
Definition | df-btwn 26686* | Define the Euclidean betweenness predicate. For details, see brbtwn 26693. (Contributed by Scott Fenton, 3-Jun-2013.) |
⊢ Btwn = ◡{〈〈𝑥, 𝑧〉, 𝑦〉 ∣ ∃𝑛 ∈ ℕ ((𝑥 ∈ (𝔼‘𝑛) ∧ 𝑧 ∈ (𝔼‘𝑛) ∧ 𝑦 ∈ (𝔼‘𝑛)) ∧ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑛)(𝑦‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑧‘𝑖))))} | ||
Definition | df-cgr 26687* | Define the Euclidean congruence predicate. For details, see brcgr 26694. (Contributed by Scott Fenton, 3-Jun-2013.) |
⊢ Cgr = {〈𝑥, 𝑦〉 ∣ ∃𝑛 ∈ ℕ ((𝑥 ∈ ((𝔼‘𝑛) × (𝔼‘𝑛)) ∧ 𝑦 ∈ ((𝔼‘𝑛) × (𝔼‘𝑛))) ∧ Σ𝑖 ∈ (1...𝑛)((((1st ‘𝑥)‘𝑖) − ((2nd ‘𝑥)‘𝑖))↑2) = Σ𝑖 ∈ (1...𝑛)((((1st ‘𝑦)‘𝑖) − ((2nd ‘𝑦)‘𝑖))↑2))} | ||
Theorem | elee 26688 | Membership in a Euclidean space. We define Euclidean space here using Cartesian coordinates over 𝑁 space. We later abstract away from this using Tarski's geometry axioms, so this exact definition is unimportant. (Contributed by Scott Fenton, 3-Jun-2013.) |
⊢ (𝑁 ∈ ℕ → (𝐴 ∈ (𝔼‘𝑁) ↔ 𝐴:(1...𝑁)⟶ℝ)) | ||
Theorem | mptelee 26689* | A condition for a mapping to be an element of a Euclidean space. (Contributed by Scott Fenton, 7-Jun-2013.) |
⊢ (𝑁 ∈ ℕ → ((𝑘 ∈ (1...𝑁) ↦ (𝐴𝐹𝐵)) ∈ (𝔼‘𝑁) ↔ ∀𝑘 ∈ (1...𝑁)(𝐴𝐹𝐵) ∈ ℝ)) | ||
Theorem | eleenn 26690 | If 𝐴 is in (𝔼‘𝑁), then 𝑁 is a natural. (Contributed by Scott Fenton, 1-Jul-2013.) |
⊢ (𝐴 ∈ (𝔼‘𝑁) → 𝑁 ∈ ℕ) | ||
Theorem | eleei 26691 | The forward direction of elee 26688. (Contributed by Scott Fenton, 1-Jul-2013.) |
⊢ (𝐴 ∈ (𝔼‘𝑁) → 𝐴:(1...𝑁)⟶ℝ) | ||
Theorem | eedimeq 26692 | A point belongs to at most one Euclidean space. (Contributed by Scott Fenton, 1-Jul-2013.) |
⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑀)) → 𝑁 = 𝑀) | ||
Theorem | brbtwn 26693* | The binary relation form of the betweenness predicate. The statement 𝐴 Btwn 〈𝐵, 𝐶〉 should be informally read as "𝐴 lies on a line segment between 𝐵 and 𝐶. This exact definition is abstracted away by Tarski's geometry axioms later on. (Contributed by Scott Fenton, 3-Jun-2013.) |
⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → (𝐴 Btwn 〈𝐵, 𝐶〉 ↔ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐴‘𝑖) = (((1 − 𝑡) · (𝐵‘𝑖)) + (𝑡 · (𝐶‘𝑖))))) | ||
Theorem | brcgr 26694* | The binary relation form of the congruence predicate. The statement 〈𝐴, 𝐵〉Cgr〈𝐶, 𝐷〉 should be read informally as "the 𝑁 dimensional point 𝐴 is as far from 𝐵 as 𝐶 is from 𝐷, or "the line segment 𝐴𝐵 is congruent to the line segment 𝐶𝐷. This particular definition is encapsulated by Tarski's axioms later on. (Contributed by Scott Fenton, 3-Jun-2013.) |
⊢ (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → (〈𝐴, 𝐵〉Cgr〈𝐶, 𝐷〉 ↔ Σ𝑖 ∈ (1...𝑁)(((𝐴‘𝑖) − (𝐵‘𝑖))↑2) = Σ𝑖 ∈ (1...𝑁)(((𝐶‘𝑖) − (𝐷‘𝑖))↑2))) | ||
Theorem | fveere 26695 | The function value of a point is a real. (Contributed by Scott Fenton, 10-Jun-2013.) |
⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐼 ∈ (1...𝑁)) → (𝐴‘𝐼) ∈ ℝ) | ||
Theorem | fveecn 26696 | The function value of a point is a complex. (Contributed by Scott Fenton, 10-Jun-2013.) |
⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐼 ∈ (1...𝑁)) → (𝐴‘𝐼) ∈ ℂ) | ||
Theorem | eqeefv 26697* | Two points are equal iff they agree in all dimensions. (Contributed by Scott Fenton, 10-Jun-2013.) |
⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) → (𝐴 = 𝐵 ↔ ∀𝑖 ∈ (1...𝑁)(𝐴‘𝑖) = (𝐵‘𝑖))) | ||
Theorem | eqeelen 26698* | Two points are equal iff the square of the distance between them is zero. (Contributed by Scott Fenton, 10-Jun-2013.) (Revised by Mario Carneiro, 22-May-2014.) |
⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) → (𝐴 = 𝐵 ↔ Σ𝑖 ∈ (1...𝑁)(((𝐴‘𝑖) − (𝐵‘𝑖))↑2) = 0)) | ||
Theorem | brbtwn2 26699* | Alternate characterization of betweenness, with no existential quantifiers. (Contributed by Scott Fenton, 24-Jun-2013.) |
⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → (𝐴 Btwn 〈𝐵, 𝐶〉 ↔ (∀𝑖 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑖) − (𝐴‘𝑖))) ≤ 0 ∧ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑗) − (𝐴‘𝑗))) = (((𝐵‘𝑗) − (𝐴‘𝑗)) · ((𝐶‘𝑖) − (𝐴‘𝑖)))))) | ||
Theorem | colinearalglem1 26700 | Lemma for colinearalg 26704. Expand out a multiplication. (Contributed by Scott Fenton, 24-Jun-2013.) |
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ)) → (((𝐵 − 𝐴) · (𝐹 − 𝐷)) = ((𝐸 − 𝐷) · (𝐶 − 𝐴)) ↔ ((𝐵 · 𝐹) − ((𝐴 · 𝐹) + (𝐵 · 𝐷))) = ((𝐶 · 𝐸) − ((𝐴 · 𝐸) + (𝐶 · 𝐷))))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |