Home | Metamath
Proof Explorer Theorem List (p. 266 of 449) | < 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-28623) |
Hilbert Space Explorer
(28624-30146) |
Users' Mathboxes
(30147-44804) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | islmib 26501 | Property of the line mirror. (Contributed by Thierry Arnoux, 11-Dec-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐺DimTarskiG≥2) & ⊢ 𝑀 = ((lInvG‘𝐺)‘𝐷) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐷 ∈ ran 𝐿) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) ⇒ ⊢ (𝜑 → (𝐵 = (𝑀‘𝐴) ↔ ((𝐴(midG‘𝐺)𝐵) ∈ 𝐷 ∧ (𝐷(⟂G‘𝐺)(𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)))) | ||
Theorem | lmicom 26502 | The line mirroring function is an involution. Theorem 10.4 of [Schwabhauser] p. 89. (Contributed by Thierry Arnoux, 11-Dec-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐺DimTarskiG≥2) & ⊢ 𝑀 = ((lInvG‘𝐺)‘𝐷) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐷 ∈ ran 𝐿) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → (𝑀‘𝐴) = 𝐵) ⇒ ⊢ (𝜑 → (𝑀‘𝐵) = 𝐴) | ||
Theorem | lmilmi 26503 | Line mirroring is an involution. Theorem 10.5 of [Schwabhauser] p. 89. (Contributed by Thierry Arnoux, 11-Dec-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐺DimTarskiG≥2) & ⊢ 𝑀 = ((lInvG‘𝐺)‘𝐷) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐷 ∈ ran 𝐿) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) ⇒ ⊢ (𝜑 → (𝑀‘(𝑀‘𝐴)) = 𝐴) | ||
Theorem | lmireu 26504* | Any point has a unique antecedent through line mirroring. Theorem 10.6 of [Schwabhauser] p. 89. (Contributed by Thierry Arnoux, 11-Dec-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐺DimTarskiG≥2) & ⊢ 𝑀 = ((lInvG‘𝐺)‘𝐷) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐷 ∈ ran 𝐿) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) ⇒ ⊢ (𝜑 → ∃!𝑏 ∈ 𝑃 (𝑀‘𝑏) = 𝐴) | ||
Theorem | lmieq 26505 | Equality deduction for line mirroring. Theorem 10.7 of [Schwabhauser] p. 89. (Contributed by Thierry Arnoux, 11-Dec-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐺DimTarskiG≥2) & ⊢ 𝑀 = ((lInvG‘𝐺)‘𝐷) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐷 ∈ ran 𝐿) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → (𝑀‘𝐴) = (𝑀‘𝐵)) ⇒ ⊢ (𝜑 → 𝐴 = 𝐵) | ||
Theorem | lmiinv 26506 | The invariants of the line mirroring lie on the mirror line. Theorem 10.8 of [Schwabhauser] p. 89. (Contributed by Thierry Arnoux, 11-Dec-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐺DimTarskiG≥2) & ⊢ 𝑀 = ((lInvG‘𝐺)‘𝐷) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐷 ∈ ran 𝐿) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) ⇒ ⊢ (𝜑 → ((𝑀‘𝐴) = 𝐴 ↔ 𝐴 ∈ 𝐷)) | ||
Theorem | lmicinv 26507 | The mirroring line is an invariant. (Contributed by Thierry Arnoux, 8-Aug-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐺DimTarskiG≥2) & ⊢ 𝑀 = ((lInvG‘𝐺)‘𝐷) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐷 ∈ ran 𝐿) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐴 ∈ 𝐷) ⇒ ⊢ (𝜑 → (𝑀‘𝐴) = 𝐴) | ||
Theorem | lmimid 26508 | If we have a right angle, then the mirror point is the point inversion. (Contributed by Thierry Arnoux, 15-Dec-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐺DimTarskiG≥2) & ⊢ 𝑀 = ((lInvG‘𝐺)‘𝐷) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐷 ∈ ran 𝐿) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ 𝑆 = ((pInvG‘𝐺)‘𝐵) & ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉 ∈ (∟G‘𝐺)) & ⊢ (𝜑 → 𝐴 ∈ 𝐷) & ⊢ (𝜑 → 𝐵 ∈ 𝐷) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) ⇒ ⊢ (𝜑 → (𝑀‘𝐶) = (𝑆‘𝐶)) | ||
Theorem | lmif1o 26509 | The line mirroring function 𝑀 is a bijection. Theorem 10.9 of [Schwabhauser] p. 89. (Contributed by Thierry Arnoux, 11-Dec-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐺DimTarskiG≥2) & ⊢ 𝑀 = ((lInvG‘𝐺)‘𝐷) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐷 ∈ ran 𝐿) ⇒ ⊢ (𝜑 → 𝑀:𝑃–1-1-onto→𝑃) | ||
Theorem | lmiisolem 26510 | Lemma for lmiiso 26511. (Contributed by Thierry Arnoux, 14-Dec-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐺DimTarskiG≥2) & ⊢ 𝑀 = ((lInvG‘𝐺)‘𝐷) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐷 ∈ ran 𝐿) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ 𝑆 = ((pInvG‘𝐺)‘𝑍) & ⊢ 𝑍 = ((𝐴(midG‘𝐺)(𝑀‘𝐴))(midG‘𝐺)(𝐵(midG‘𝐺)(𝑀‘𝐵))) ⇒ ⊢ (𝜑 → ((𝑀‘𝐴) − (𝑀‘𝐵)) = (𝐴 − 𝐵)) | ||
Theorem | lmiiso 26511 | The line mirroring function is an isometry, i.e. it is conserves congruence. Because it is also a bijection, it is also a motion. Theorem 10.10 of [Schwabhauser] p. 89. (Contributed by Thierry Arnoux, 11-Dec-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐺DimTarskiG≥2) & ⊢ 𝑀 = ((lInvG‘𝐺)‘𝐷) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐷 ∈ ran 𝐿) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) ⇒ ⊢ (𝜑 → ((𝑀‘𝐴) − (𝑀‘𝐵)) = (𝐴 − 𝐵)) | ||
Theorem | lmimot 26512 | Line mirroring is a motion of the geometric space. Theorem 10.11 of [Schwabhauser] p. 90. (Contributed by Thierry Arnoux, 15-Dec-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐺DimTarskiG≥2) & ⊢ 𝑀 = ((lInvG‘𝐺)‘𝐷) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐷 ∈ ran 𝐿) ⇒ ⊢ (𝜑 → 𝑀 ∈ (𝐺Ismt𝐺)) | ||
Theorem | hypcgrlem1 26513 | Lemma for hypcgr 26515, case where triangles share a cathetus. (Contributed by Thierry Arnoux, 15-Dec-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐺DimTarskiG≥2) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉 ∈ (∟G‘𝐺)) & ⊢ (𝜑 → 〈“𝐷𝐸𝐹”〉 ∈ (∟G‘𝐺)) & ⊢ (𝜑 → (𝐴 − 𝐵) = (𝐷 − 𝐸)) & ⊢ (𝜑 → (𝐵 − 𝐶) = (𝐸 − 𝐹)) & ⊢ (𝜑 → 𝐵 = 𝐸) & ⊢ 𝑆 = ((lInvG‘𝐺)‘((𝐴(midG‘𝐺)𝐷)(LineG‘𝐺)𝐵)) & ⊢ (𝜑 → 𝐶 = 𝐹) ⇒ ⊢ (𝜑 → (𝐴 − 𝐶) = (𝐷 − 𝐹)) | ||
Theorem | hypcgrlem2 26514 | Lemma for hypcgr 26515, case where triangles share one vertex 𝐵. (Contributed by Thierry Arnoux, 16-Dec-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐺DimTarskiG≥2) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉 ∈ (∟G‘𝐺)) & ⊢ (𝜑 → 〈“𝐷𝐸𝐹”〉 ∈ (∟G‘𝐺)) & ⊢ (𝜑 → (𝐴 − 𝐵) = (𝐷 − 𝐸)) & ⊢ (𝜑 → (𝐵 − 𝐶) = (𝐸 − 𝐹)) & ⊢ (𝜑 → 𝐵 = 𝐸) & ⊢ 𝑆 = ((lInvG‘𝐺)‘((𝐶(midG‘𝐺)𝐹)(LineG‘𝐺)𝐵)) ⇒ ⊢ (𝜑 → (𝐴 − 𝐶) = (𝐷 − 𝐹)) | ||
Theorem | hypcgr 26515 | If the catheti of two right-angled triangles are congruent, so is their hypothenuse. Theorem 10.12 of [Schwabhauser] p. 91. (Contributed by Thierry Arnoux, 16-Dec-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐺DimTarskiG≥2) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉 ∈ (∟G‘𝐺)) & ⊢ (𝜑 → 〈“𝐷𝐸𝐹”〉 ∈ (∟G‘𝐺)) & ⊢ (𝜑 → (𝐴 − 𝐵) = (𝐷 − 𝐸)) & ⊢ (𝜑 → (𝐵 − 𝐶) = (𝐸 − 𝐹)) ⇒ ⊢ (𝜑 → (𝐴 − 𝐶) = (𝐷 − 𝐹)) | ||
Theorem | lmiopp 26516* | Line mirroring produces points on the opposite side of the mirroring line. Theorem 10.14 of [Schwabhauser] p. 92. (Contributed by Thierry Arnoux, 2-Aug-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐺DimTarskiG≥2) & ⊢ (𝜑 → 𝐷 ∈ ran 𝐿) & ⊢ 𝑂 = {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑏 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑏))} & ⊢ 𝑀 = ((lInvG‘𝐺)‘𝐷) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → ¬ 𝐴 ∈ 𝐷) ⇒ ⊢ (𝜑 → 𝐴𝑂(𝑀‘𝐴)) | ||
Theorem | lnperpex 26517* | Existence of a perpendicular to a line 𝐿 at a given point 𝐴. Theorem 10.15 of [Schwabhauser] p. 92. (Contributed by Thierry Arnoux, 2-Aug-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐺DimTarskiG≥2) & ⊢ (𝜑 → 𝐷 ∈ ran 𝐿) & ⊢ 𝑂 = {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑏 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑏))} & ⊢ (𝜑 → 𝐴 ∈ 𝐷) & ⊢ (𝜑 → 𝑄 ∈ 𝑃) & ⊢ (𝜑 → ¬ 𝑄 ∈ 𝐷) ⇒ ⊢ (𝜑 → ∃𝑝 ∈ 𝑃 (𝐷(⟂G‘𝐺)(𝑝𝐿𝐴) ∧ 𝑝((hpG‘𝐺)‘𝐷)𝑄)) | ||
Theorem | trgcopy 26518* | Triangle construction: a copy of a given triangle can always be constructed in such a way that one side is lying on a half-line, and the third vertex is on a given half-plane: existence part. First part of Theorem 10.16 of [Schwabhauser] p. 92. (Contributed by Thierry Arnoux, 4-Aug-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝐾 = (hlG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ (𝜑 → ¬ (𝐴 ∈ (𝐵𝐿𝐶) ∨ 𝐵 = 𝐶)) & ⊢ (𝜑 → ¬ (𝐷 ∈ (𝐸𝐿𝐹) ∨ 𝐸 = 𝐹)) & ⊢ (𝜑 → (𝐴 − 𝐵) = (𝐷 − 𝐸)) ⇒ ⊢ (𝜑 → ∃𝑓 ∈ 𝑃 (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝐷𝐸𝑓”〉 ∧ 𝑓((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) | ||
Theorem | trgcopyeulem 26519* | Lemma for trgcopyeu 26520. (Contributed by Thierry Arnoux, 8-Aug-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝐾 = (hlG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ (𝜑 → ¬ (𝐴 ∈ (𝐵𝐿𝐶) ∨ 𝐵 = 𝐶)) & ⊢ (𝜑 → ¬ (𝐷 ∈ (𝐸𝐿𝐹) ∨ 𝐸 = 𝐹)) & ⊢ (𝜑 → (𝐴 − 𝐵) = (𝐷 − 𝐸)) & ⊢ 𝑂 = {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (𝑃 ∖ (𝐷𝐿𝐸)) ∧ 𝑏 ∈ (𝑃 ∖ (𝐷𝐿𝐸))) ∧ ∃𝑡 ∈ (𝐷𝐿𝐸)𝑡 ∈ (𝑎𝐼𝑏))} & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝐷𝐸𝑋”〉) & ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝐷𝐸𝑌”〉) & ⊢ (𝜑 → 𝑋((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹) & ⊢ (𝜑 → 𝑌((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹) ⇒ ⊢ (𝜑 → 𝑋 = 𝑌) | ||
Theorem | trgcopyeu 26520* | Triangle construction: a copy of a given triangle can always be constructed in such a way that one side is lying on a half-line, and the third vertex is on a given half-plane: uniqueness part. Second part of Theorem 10.16 of [Schwabhauser] p. 92. (Contributed by Thierry Arnoux, 8-Aug-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝐾 = (hlG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ (𝜑 → ¬ (𝐴 ∈ (𝐵𝐿𝐶) ∨ 𝐵 = 𝐶)) & ⊢ (𝜑 → ¬ (𝐷 ∈ (𝐸𝐿𝐹) ∨ 𝐸 = 𝐹)) & ⊢ (𝜑 → (𝐴 − 𝐵) = (𝐷 − 𝐸)) ⇒ ⊢ (𝜑 → ∃!𝑓 ∈ 𝑃 (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝐷𝐸𝑓”〉 ∧ 𝑓((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) | ||
Syntax | ccgra 26521 | Declare the constant for the congruence between angles relation. |
class cgrA | ||
Definition | df-cgra 26522* | Define the congruence relation between angles. As for triangles we use "words of points". See iscgra 26523 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 26523* | 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 26544 shows that those definitions are indeed equivalent. (Contributed by Thierry Arnoux, 31-Jul-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐾 = (hlG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) ⇒ ⊢ (𝜑 → (〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉 ↔ ∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑥𝐸𝑦”〉 ∧ 𝑥(𝐾‘𝐸)𝐷 ∧ 𝑦(𝐾‘𝐸)𝐹))) | ||
Theorem | iscgra1 26524* | A special version of iscgra 26523 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 26525 | Sufficient conditions for angle congruence, deduction version. (Contributed by Thierry Arnoux, 1-Aug-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐾 = (hlG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑋𝐸𝑌”〉) & ⊢ (𝜑 → 𝑋(𝐾‘𝐸)𝐷) & ⊢ (𝜑 → 𝑌(𝐾‘𝐸)𝐹) ⇒ ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) | ||
Theorem | cgrane1 26526 | Angles imply inequality. (Contributed by Thierry Arnoux, 1-Aug-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐾 = (hlG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) ⇒ ⊢ (𝜑 → 𝐴 ≠ 𝐵) | ||
Theorem | cgrane2 26527 | Angles imply inequality. (Contributed by Thierry Arnoux, 1-Aug-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐾 = (hlG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) ⇒ ⊢ (𝜑 → 𝐵 ≠ 𝐶) | ||
Theorem | cgrane3 26528 | Angles imply inequality. (Contributed by Thierry Arnoux, 1-Aug-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐾 = (hlG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) ⇒ ⊢ (𝜑 → 𝐸 ≠ 𝐷) | ||
Theorem | cgrane4 26529 | Angles imply inequality. (Contributed by Thierry Arnoux, 1-Aug-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐾 = (hlG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) ⇒ ⊢ (𝜑 → 𝐸 ≠ 𝐹) | ||
Theorem | cgrahl1 26530 | 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 26531 | 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 26532 | 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 26533 | 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 26534 | 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 26535 | 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 26536 | 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 26537 | 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 26538 | Flat angles are congruent. (Contributed by Thierry Arnoux, 13-Feb-2023.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐶)) & ⊢ (𝜑 → 𝐸 ∈ (𝐷𝐼𝐹)) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) & ⊢ (𝜑 → 𝐶 ≠ 𝐵) & ⊢ (𝜑 → 𝐷 ≠ 𝐸) & ⊢ (𝜑 → 𝐹 ≠ 𝐸) ⇒ ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) | ||
Theorem | cgraswaplr 26539 | Swap both side of angle congruence. (Contributed by Thierry Arnoux, 5-Oct-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) ⇒ ⊢ (𝜑 → 〈“𝐶𝐵𝐴”〉(cgrA‘𝐺)〈“𝐹𝐸𝐷”〉) | ||
Theorem | cgrabtwn 26540 | 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 26541 | 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 26542 | Angle congruence preserves colinearity. (Contributed by Thierry Arnoux, 9-Aug-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ⇒ ⊢ (𝜑 → (𝐹 ∈ (𝐷𝐿𝐸) ∨ 𝐷 = 𝐸)) | ||
Theorem | cgrancol 26543 | Angle congruence preserves non-colinearity. (Contributed by Thierry Arnoux, 9-Aug-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ⇒ ⊢ (𝜑 → ¬ (𝐹 ∈ (𝐷𝐿𝐸) ∨ 𝐷 = 𝐸)) | ||
Theorem | dfcgra2 26544* | 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 26522 is indeed equivalent to the textbook's definition. (Contributed by Thierry Arnoux, 2-Aug-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) ⇒ ⊢ (𝜑 → (〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉 ↔ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸) ∧ ∃𝑎 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝑎 − 𝑐) = (𝑑 − 𝑓))))) | ||
Theorem | sacgr 26545 | 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 26546 | 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 26547* | 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 26548 | 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 26549 | Extend class relation with the geometrical "point in angle" relation. |
class inA | ||
Syntax | cleag 26550 | Extend class relation with the "angle less than" relation. |
class ≤∠ | ||
Definition | df-inag 26551* | 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 26552* | 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 26553 | Sufficient conditions for in-angle relation, deduction version. (Contributed by Thierry Arnoux, 20-Oct-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐾 = (hlG‘𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐺 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) & ⊢ (𝜑 → 𝐶 ≠ 𝐵) & ⊢ (𝜑 → 𝑋 ≠ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ (𝐴𝐼𝐶)) & ⊢ (𝜑 → (𝑌 = 𝐵 ∨ 𝑌(𝐾‘𝐵)𝑋)) ⇒ ⊢ (𝜑 → 𝑋(inA‘𝐺)〈“𝐴𝐵𝐶”〉) | ||
Theorem | inagflat 26554 | Any point lies in a flat angle. (Contributed by Thierry Arnoux, 13-Feb-2023.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐾 = (hlG‘𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) & ⊢ (𝜑 → 𝐶 ≠ 𝐵) & ⊢ (𝜑 → 𝑋 ≠ 𝐵) & ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐶)) ⇒ ⊢ (𝜑 → 𝑋(inA‘𝐺)〈“𝐴𝐵𝐶”〉) | ||
Theorem | inagswap 26555 | 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 26556 | Deduce inequality from the in-angle relation. (Contributed by Thierry Arnoux, 29-Oct-2021.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐾 = (hlG‘𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝑋(inA‘𝐺)〈“𝐴𝐵𝐶”〉) ⇒ ⊢ (𝜑 → 𝐴 ≠ 𝐵) | ||
Theorem | inagne2 26557 | Deduce inequality from the in-angle relation. (Contributed by Thierry Arnoux, 29-Oct-2021.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐾 = (hlG‘𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝑋(inA‘𝐺)〈“𝐴𝐵𝐶”〉) ⇒ ⊢ (𝜑 → 𝐶 ≠ 𝐵) | ||
Theorem | inagne3 26558 | Deduce inequality from the in-angle relation. (Contributed by Thierry Arnoux, 29-Oct-2021.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐾 = (hlG‘𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝑋(inA‘𝐺)〈“𝐴𝐵𝐶”〉) ⇒ ⊢ (𝜑 → 𝑋 ≠ 𝐵) | ||
Theorem | inaghl 26559 | 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 26560* | 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 26561* | 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 26562 | Sufficient condition for "less than" angle relation, deduction version (Contributed by Thierry Arnoux, 12-Oct-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ ≤ = (≤∠‘𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑋(inA‘𝐺)〈“𝐷𝐸𝐹”〉) & ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝑋”〉) ⇒ ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉 ≤ 〈“𝐷𝐸𝐹”〉) | ||
Theorem | leagne1 26563 | Deduce inequality from the less-than angle relation. (Contributed by Thierry Arnoux, 25-Feb-2023.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉(≤∠‘𝐺)〈“𝐷𝐸𝐹”〉) ⇒ ⊢ (𝜑 → 𝐴 ≠ 𝐵) | ||
Theorem | leagne2 26564 | Deduce inequality from the less-than angle relation. (Contributed by Thierry Arnoux, 25-Feb-2023.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉(≤∠‘𝐺)〈“𝐷𝐸𝐹”〉) ⇒ ⊢ (𝜑 → 𝐶 ≠ 𝐵) | ||
Theorem | leagne3 26565 | Deduce inequality from the less-than angle relation. (Contributed by Thierry Arnoux, 25-Feb-2023.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉(≤∠‘𝐺)〈“𝐷𝐸𝐹”〉) ⇒ ⊢ (𝜑 → 𝐷 ≠ 𝐸) | ||
Theorem | leagne4 26566 | Deduce inequality from the less-than angle relation. (Contributed by Thierry Arnoux, 25-Feb-2023.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉(≤∠‘𝐺)〈“𝐷𝐸𝐹”〉) ⇒ ⊢ (𝜑 → 𝐹 ≠ 𝐸) | ||
Theorem | cgrg3col4 26567* | 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 26568 | 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 26569 | 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 26570 | 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 26571 | 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 26572 | 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 26573 | 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 26574 | 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 26575 | 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 26576 | 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 26577 | 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 26225, already covers that part: see trgcgr 26230. 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 26230 (Contributed by Thierry Arnoux, 18-Jan-2023.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) & ⊢ (𝜑 → 𝐵 ≠ 𝐶) & ⊢ (𝜑 → 𝐶 ≠ 𝐴) ⇒ ⊢ (𝜑 → (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝐷𝐸𝐹”〉 ↔ (((𝐴 − 𝐵) = (𝐷 − 𝐸) ∧ (𝐵 − 𝐶) = (𝐸 − 𝐹) ∧ (𝐶 − 𝐴) = (𝐹 − 𝐷)) ∧ (〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉 ∧ 〈“𝐶𝐴𝐵”〉(cgrA‘𝐺)〈“𝐹𝐷𝐸”〉 ∧ 〈“𝐵𝐶𝐴”〉(cgrA‘𝐺)〈“𝐸𝐹𝐷”〉)))) | ||
Theorem | isoas 26578 | 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 26579 | Declare the class of equilateral triangles. |
class eqltrG | ||
Definition | df-eqlg 26580* | 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 26581 | Property of a triangle being equilateral. (Contributed by Thierry Arnoux, 5-Oct-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) ⇒ ⊢ (𝜑 → (〈“𝐴𝐵𝐶”〉 ∈ (eqltrG‘𝐺) ↔ 〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝐵𝐶𝐴”〉)) | ||
Theorem | iseqlgd 26582 | Condition for a triangle to be equilateral. (Contributed by Thierry Arnoux, 5-Oct-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → (𝐴 − 𝐵) = (𝐵 − 𝐶)) & ⊢ (𝜑 → (𝐵 − 𝐶) = (𝐶 − 𝐴)) & ⊢ (𝜑 → (𝐶 − 𝐴) = (𝐴 − 𝐵)) ⇒ ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉 ∈ (eqltrG‘𝐺)) | ||
Theorem | f1otrgds 26583* | Convenient lemma for f1otrg 26585. (Contributed by Thierry Arnoux, 19-Mar-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐷 = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐵 = (Base‘𝐻) & ⊢ 𝐸 = (dist‘𝐻) & ⊢ 𝐽 = (Itv‘𝐻) & ⊢ (𝜑 → 𝐹:𝐵–1-1-onto→𝑃) & ⊢ ((𝜑 ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) → (𝑒𝐸𝑓) = ((𝐹‘𝑒)𝐷(𝐹‘𝑓))) & ⊢ ((𝜑 ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹‘𝑔) ∈ ((𝐹‘𝑒)𝐼(𝐹‘𝑓)))) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋𝐸𝑌) = ((𝐹‘𝑋)𝐷(𝐹‘𝑌))) | ||
Theorem | f1otrgitv 26584* | Convenient lemma for f1otrg 26585. (Contributed by Thierry Arnoux, 19-Mar-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐷 = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐵 = (Base‘𝐻) & ⊢ 𝐸 = (dist‘𝐻) & ⊢ 𝐽 = (Itv‘𝐻) & ⊢ (𝜑 → 𝐹:𝐵–1-1-onto→𝑃) & ⊢ ((𝜑 ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) → (𝑒𝐸𝑓) = ((𝐹‘𝑒)𝐷(𝐹‘𝑓))) & ⊢ ((𝜑 ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹‘𝑔) ∈ ((𝐹‘𝑒)𝐼(𝐹‘𝑓)))) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑍 ∈ (𝑋𝐽𝑌) ↔ (𝐹‘𝑍) ∈ ((𝐹‘𝑋)𝐼(𝐹‘𝑌)))) | ||
Theorem | f1otrg 26585* | 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 26586* | 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 26587 | Function to convert an algebraic structure to a Tarski geometry. |
class toTG | ||
Definition | df-ttg 26588* | 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 26589* | 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 26590 | Lemma for ttgbas 26591 and ttgvsca 26594. (Contributed by Thierry Arnoux, 15-Apr-2019.) |
⊢ 𝐺 = (toTG‘𝐻) & ⊢ 𝐸 = Slot 𝑁 & ⊢ 𝑁 ∈ ℕ & ⊢ 𝑁 < ;16 ⇒ ⊢ (𝐸‘𝐻) = (𝐸‘𝐺) | ||
Theorem | ttgbas 26591 | The base set of a subcomplex Hilbert space augmented with betweenness. (Contributed by Thierry Arnoux, 25-Mar-2019.) |
⊢ 𝐺 = (toTG‘𝐻) & ⊢ 𝐵 = (Base‘𝐻) ⇒ ⊢ 𝐵 = (Base‘𝐺) | ||
Theorem | ttgplusg 26592 | The addition operation of a subcomplex Hilbert space augmented with betweenness. (Contributed by Thierry Arnoux, 25-Mar-2019.) |
⊢ 𝐺 = (toTG‘𝐻) & ⊢ + = (+g‘𝐻) ⇒ ⊢ + = (+g‘𝐺) | ||
Theorem | ttgsub 26593 | The subtraction operation of a subcomplex Hilbert space augmented with betweenness. (Contributed by Thierry Arnoux, 25-Mar-2019.) |
⊢ 𝐺 = (toTG‘𝐻) & ⊢ − = (-g‘𝐻) ⇒ ⊢ − = (-g‘𝐺) | ||
Theorem | ttgvsca 26594 | The scalar product of a subcomplex Hilbert space augmented with betweenness. (Contributed by Thierry Arnoux, 25-Mar-2019.) |
⊢ 𝐺 = (toTG‘𝐻) & ⊢ · = ( ·𝑠 ‘𝐻) ⇒ ⊢ · = ( ·𝑠 ‘𝐺) | ||
Theorem | ttgds 26595 | The metric of a subcomplex Hilbert space augmented with betweenness. (Contributed by Thierry Arnoux, 25-Mar-2019.) |
⊢ 𝐺 = (toTG‘𝐻) & ⊢ 𝐷 = (dist‘𝐻) ⇒ ⊢ 𝐷 = (dist‘𝐺) | ||
Theorem | ttgitvval 26596* | Betweenness for a subcomplex Hilbert space augmented with betweenness. (Contributed by Thierry Arnoux, 25-Mar-2019.) |
⊢ 𝐺 = (toTG‘𝐻) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝑃 = (Base‘𝐻) & ⊢ − = (-g‘𝐻) & ⊢ · = ( ·𝑠 ‘𝐻) ⇒ ⊢ ((𝐻 ∈ 𝑉 ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃) → (𝑋𝐼𝑌) = {𝑧 ∈ 𝑃 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑋) = (𝑘 · (𝑌 − 𝑋))}) | ||
Theorem | ttgelitv 26597* | Betweenness for a subcomplex Hilbert space augmented with betweenness. (Contributed by Thierry Arnoux, 25-Mar-2019.) |
⊢ 𝐺 = (toTG‘𝐻) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝑃 = (Base‘𝐻) & ⊢ − = (-g‘𝐻) & ⊢ · = ( ·𝑠 ‘𝐻) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ (𝜑 → 𝐻 ∈ 𝑉) & ⊢ (𝜑 → 𝑍 ∈ 𝑃) ⇒ ⊢ (𝜑 → (𝑍 ∈ (𝑋𝐼𝑌) ↔ ∃𝑘 ∈ (0[,]1)(𝑍 − 𝑋) = (𝑘 · (𝑌 − 𝑋)))) | ||
Theorem | ttgbtwnid 26598 | 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 26599 | 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 26600 | Any metric space fulfills Tarski's geometry axioms of congruence. (Contributed by Thierry Arnoux, 13-Mar-2019.) |
⊢ (𝐺 ∈ ∞MetSp → 𝐺 ∈ TarskiGC) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |