Home | Metamath
Proof Explorer Theorem List (p. 258 of 426) | < 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-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | iscgra 25701* | 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 25721 shows that those definitions are indeed equivalent. (Contributed by Thierry Arnoux, 31-Jul-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐾 = (hlG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) ⇒ ⊢ (𝜑 → (〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉 ↔ ∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑥𝐸𝑦”〉 ∧ 𝑥(𝐾‘𝐸)𝐷 ∧ 𝑦(𝐾‘𝐸)𝐹))) | ||
Theorem | iscgra1 25702* | A special version of iscgra 25701 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 25703 | Sufficient conditions for angle congruence, deduction version. (Contributed by Thierry Arnoux, 1-Aug-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐾 = (hlG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑋𝐸𝑌”〉) & ⊢ (𝜑 → 𝑋(𝐾‘𝐸)𝐷) & ⊢ (𝜑 → 𝑌(𝐾‘𝐸)𝐹) ⇒ ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) | ||
Theorem | cgrane1 25704 | Angles imply inequality. (Contributed by Thierry Arnoux, 1-Aug-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐾 = (hlG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) ⇒ ⊢ (𝜑 → 𝐴 ≠ 𝐵) | ||
Theorem | cgrane2 25705 | Angles imply inequality. (Contributed by Thierry Arnoux, 1-Aug-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐾 = (hlG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) ⇒ ⊢ (𝜑 → 𝐵 ≠ 𝐶) | ||
Theorem | cgrane3 25706 | Angles imply inequality. (Contributed by Thierry Arnoux, 1-Aug-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐾 = (hlG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) ⇒ ⊢ (𝜑 → 𝐸 ≠ 𝐷) | ||
Theorem | cgrane4 25707 | Angles imply inequality. (Contributed by Thierry Arnoux, 1-Aug-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐾 = (hlG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) ⇒ ⊢ (𝜑 → 𝐸 ≠ 𝐹) | ||
Theorem | cgrahl1 25708 | 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 25709 | 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 25710 | 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 25711 | 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 25712 | 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 25713 | Triangle congruence implies angle congruence. (Contributed by Thierry Arnoux, 2-Aug-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ 𝐾 = (hlG‘𝐺) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) & ⊢ (𝜑 → 𝐵 ≠ 𝐶) & ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝐷𝐸𝐹”〉) ⇒ ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) | ||
Theorem | cgracom 25714 | 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 25715 | 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 | cgraswaplr 25716 | Swap both side of angle congruence. (Contributed by Thierry Arnoux, 5-Oct-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) ⇒ ⊢ (𝜑 → 〈“𝐶𝐵𝐴”〉(cgrA‘𝐺)〈“𝐹𝐸𝐷”〉) | ||
Theorem | cgrabtwn 25717 | 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 25718 | 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 25719 | Angle congruence preserves colinearity. (Contributed by Thierry Arnoux, 9-Aug-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ⇒ ⊢ (𝜑 → (𝐹 ∈ (𝐷𝐿𝐸) ∨ 𝐷 = 𝐸)) | ||
Theorem | cgrancol 25720 | Angle congruence preserves non-colinearity. (Contributed by Thierry Arnoux, 9-Aug-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ⇒ ⊢ (𝜑 → ¬ (𝐹 ∈ (𝐷𝐿𝐸) ∨ 𝐷 = 𝐸)) | ||
Theorem | dfcgra2 25721* | 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 25700 is indeed equivalent with the textbook's definition. (Contributed by Thierry Arnoux, 2-Aug-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) ⇒ ⊢ (𝜑 → (〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉 ↔ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸) ∧ ∃𝑎 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝑎 − 𝑐) = (𝑑 − 𝑓))))) | ||
Theorem | sacgr 25722 | Supplementary angles of congruent angles are themselves congruent. Theorem 11.13 of [Schwabhauser] p. 98. (Contributed by Thierry Arnoux, 30-Sep-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) & ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝑋)) & ⊢ (𝜑 → 𝐸 ∈ (𝐷𝐼𝑌)) & ⊢ (𝜑 → 𝐵 ≠ 𝑋) & ⊢ (𝜑 → 𝐸 ≠ 𝑌) ⇒ ⊢ (𝜑 → 〈“𝑋𝐵𝐶”〉(cgrA‘𝐺)〈“𝑌𝐸𝐹”〉) | ||
Theorem | oacgr 25723 | 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 25724* | 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 25725 | 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 25726 | Extend class relation with the geometrical "point in angle" relation. |
class inA | ||
Syntax | cleag 25727 | Extend class relation with the "angle less than" relation. |
class ≤∠ | ||
Definition | df-inag 25728* | Definition of the geometrical "in angle" relation. (Contributed by Thierry Arnoux, 15-Aug-2020.) |
⊢ inA = (𝑔 ∈ V ↦ {〈𝑝, 𝑡〉 ∣ ((𝑝 ∈ (Base‘𝑔) ∧ 𝑡 ∈ ((Base‘𝑔) ↑𝑚 (0..^3))) ∧ (((𝑡‘0) ≠ (𝑡‘1) ∧ (𝑡‘2) ≠ (𝑡‘1) ∧ 𝑝 ≠ (𝑡‘1)) ∧ ∃𝑥 ∈ (Base‘𝑔)(𝑥 ∈ ((𝑡‘0)(Itv‘𝑔)(𝑡‘2)) ∧ (𝑥 = (𝑡‘1) ∨ 𝑥((hlG‘𝑔)‘(𝑡‘1))𝑝))))}) | ||
Theorem | isinag 25729* | Property for point 𝑋 to lie in the angle 〈“𝐴𝐵𝐶”〉 Defnition 11.23 of [Schwabhauser] p. 101. (Contributed by Thierry Arnoux, 15-Aug-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐾 = (hlG‘𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐺 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝑋(inA‘𝐺)〈“𝐴𝐵𝐶”〉 ↔ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ∧ 𝑋 ≠ 𝐵) ∧ ∃𝑥 ∈ 𝑃 (𝑥 ∈ (𝐴𝐼𝐶) ∧ (𝑥 = 𝐵 ∨ 𝑥(𝐾‘𝐵)𝑋))))) | ||
Theorem | inagswap 25730 | 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 | inaghl 25731 | 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 25732* | Definition of the geometrical "angle less than" relation. Definition 11.27 of [Schwabhauser] p. 102. (Contributed by Thierry Arnoux, 7-Oct-2020.) |
⊢ ≤∠ = (𝑔 ∈ V ↦ {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ ((Base‘𝑔) ↑𝑚 (0..^3)) ∧ 𝑏 ∈ ((Base‘𝑔) ↑𝑚 (0..^3))) ∧ ∃𝑥 ∈ (Base‘𝑔)(𝑥(inA‘𝑔)〈“(𝑏‘0)(𝑏‘1)(𝑏‘2)”〉 ∧ 〈“(𝑎‘0)(𝑎‘1)(𝑎‘2)”〉(cgrA‘𝑔)〈“(𝑏‘0)(𝑏‘1)𝑥”〉))}) | ||
Theorem | isleag 25733* | 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 | cgrg3col4 25734* | 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 25735 | 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 25736 | 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 25737 | 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 25738 | 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 25739 | 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 25740 | 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 25741 | 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 25742 | 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 25743 | Third congruence theorem: SSS. Theorem 11.51 of [Schwabhauser] p. 109. (Contributed by Thierry Arnoux, 1-Aug-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ (𝜑 → (𝐴 − 𝐵) = (𝐷 − 𝐸)) & ⊢ (𝜑 → (𝐵 − 𝐶) = (𝐸 − 𝐹)) & ⊢ (𝜑 → (𝐶 − 𝐴) = (𝐹 − 𝐷)) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) & ⊢ (𝜑 → 𝐵 ≠ 𝐶) & ⊢ (𝜑 → 𝐶 ≠ 𝐴) ⇒ ⊢ (𝜑 → 〈“𝐵𝐶𝐴”〉(cgrA‘𝐺)〈“𝐸𝐹𝐷”〉) | ||
Theorem | isoas 25744 | 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 25745 | Declare the class of equilateral triangles. |
class eqltrG | ||
Definition | df-eqlg 25746* | Define the class of equilateral triangles. (Contributed by Thierry Arnoux, 27-Nov-2019.) |
⊢ eqltrG = (𝑔 ∈ V ↦ {𝑥 ∈ ((Base‘𝑔) ↑𝑚 (0..^3)) ∣ 𝑥(cgrG‘𝑔)〈“(𝑥‘1)(𝑥‘2)(𝑥‘0)”〉}) | ||
Theorem | iseqlg 25747 | Property of a triangle being equilateral. (Contributed by Thierry Arnoux, 5-Oct-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) ⇒ ⊢ (𝜑 → (〈“𝐴𝐵𝐶”〉 ∈ (eqltrG‘𝐺) ↔ 〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝐵𝐶𝐴”〉)) | ||
Theorem | iseqlgd 25748 | Condition for a triangle to be equilateral. (Contributed by Thierry Arnoux, 5-Oct-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → (𝐴 − 𝐵) = (𝐵 − 𝐶)) & ⊢ (𝜑 → (𝐵 − 𝐶) = (𝐶 − 𝐴)) & ⊢ (𝜑 → (𝐶 − 𝐴) = (𝐴 − 𝐵)) ⇒ ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉 ∈ (eqltrG‘𝐺)) | ||
Theorem | f1otrgds 25749* | Convenient lemma for f1otrg 25751. (Contributed by Thierry Arnoux, 19-Mar-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐷 = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐵 = (Base‘𝐻) & ⊢ 𝐸 = (dist‘𝐻) & ⊢ 𝐽 = (Itv‘𝐻) & ⊢ (𝜑 → 𝐹:𝐵–1-1-onto→𝑃) & ⊢ ((𝜑 ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) → (𝑒𝐸𝑓) = ((𝐹‘𝑒)𝐷(𝐹‘𝑓))) & ⊢ ((𝜑 ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹‘𝑔) ∈ ((𝐹‘𝑒)𝐼(𝐹‘𝑓)))) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋𝐸𝑌) = ((𝐹‘𝑋)𝐷(𝐹‘𝑌))) | ||
Theorem | f1otrgitv 25750* | Convenient lemma for f1otrg 25751. (Contributed by Thierry Arnoux, 19-Mar-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐷 = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐵 = (Base‘𝐻) & ⊢ 𝐸 = (dist‘𝐻) & ⊢ 𝐽 = (Itv‘𝐻) & ⊢ (𝜑 → 𝐹:𝐵–1-1-onto→𝑃) & ⊢ ((𝜑 ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) → (𝑒𝐸𝑓) = ((𝐹‘𝑒)𝐷(𝐹‘𝑓))) & ⊢ ((𝜑 ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹‘𝑔) ∈ ((𝐹‘𝑒)𝐼(𝐹‘𝑓)))) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑍 ∈ (𝑋𝐽𝑌) ↔ (𝐹‘𝑍) ∈ ((𝐹‘𝑋)𝐼(𝐹‘𝑌)))) | ||
Theorem | f1otrg 25751* | 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 25752* | 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 25753 | Function to convert an algebraic structure to a Tarski geometry. |
class toTG | ||
Definition | df-ttg 25754* | 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 25755* | 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 25756 | Lemma for ttgbas 25757 and ttgvsca 25760. (Contributed by Thierry Arnoux, 15-Apr-2019.) |
⊢ 𝐺 = (toTG‘𝐻) & ⊢ 𝐸 = Slot 𝑁 & ⊢ 𝑁 ∈ ℕ & ⊢ 𝑁 < ;16 ⇒ ⊢ (𝐸‘𝐻) = (𝐸‘𝐺) | ||
Theorem | ttgbas 25757 | The base set of a subcomplex Hilbert space augmented with betweenness. (Contributed by Thierry Arnoux, 25-Mar-2019.) |
⊢ 𝐺 = (toTG‘𝐻) & ⊢ 𝐵 = (Base‘𝐻) ⇒ ⊢ 𝐵 = (Base‘𝐺) | ||
Theorem | ttgplusg 25758 | The addition operation of a subcomplex Hilbert space augmented with betweenness. (Contributed by Thierry Arnoux, 25-Mar-2019.) |
⊢ 𝐺 = (toTG‘𝐻) & ⊢ + = (+g‘𝐻) ⇒ ⊢ + = (+g‘𝐺) | ||
Theorem | ttgsub 25759 | The subtraction operation of a subcomplex Hilbert space augmented with betweenness. (Contributed by Thierry Arnoux, 25-Mar-2019.) |
⊢ 𝐺 = (toTG‘𝐻) & ⊢ − = (-g‘𝐻) ⇒ ⊢ − = (-g‘𝐺) | ||
Theorem | ttgvsca 25760 | The scalar product of a subcomplex Hilbert space augmented with betweenness. (Contributed by Thierry Arnoux, 25-Mar-2019.) |
⊢ 𝐺 = (toTG‘𝐻) & ⊢ · = ( ·𝑠 ‘𝐻) ⇒ ⊢ · = ( ·𝑠 ‘𝐺) | ||
Theorem | ttgds 25761 | The metric of a subcomplex Hilbert space augmented with betweenness. (Contributed by Thierry Arnoux, 25-Mar-2019.) |
⊢ 𝐺 = (toTG‘𝐻) & ⊢ 𝐷 = (dist‘𝐻) ⇒ ⊢ 𝐷 = (dist‘𝐺) | ||
Theorem | ttgitvval 25762* | Betweenness for a subcomplex Hilbert space augmented with betweenness. (Contributed by Thierry Arnoux, 25-Mar-2019.) |
⊢ 𝐺 = (toTG‘𝐻) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝑃 = (Base‘𝐻) & ⊢ − = (-g‘𝐻) & ⊢ · = ( ·𝑠 ‘𝐻) ⇒ ⊢ ((𝐻 ∈ 𝑉 ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃) → (𝑋𝐼𝑌) = {𝑧 ∈ 𝑃 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑋) = (𝑘 · (𝑌 − 𝑋))}) | ||
Theorem | ttgelitv 25763* | Betweenness for a subcomplex Hilbert space augmented with betweenness. (Contributed by Thierry Arnoux, 25-Mar-2019.) |
⊢ 𝐺 = (toTG‘𝐻) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝑃 = (Base‘𝐻) & ⊢ − = (-g‘𝐻) & ⊢ · = ( ·𝑠 ‘𝐻) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ (𝜑 → 𝐻 ∈ 𝑉) & ⊢ (𝜑 → 𝑍 ∈ 𝑃) ⇒ ⊢ (𝜑 → (𝑍 ∈ (𝑋𝐼𝑌) ↔ ∃𝑘 ∈ (0[,]1)(𝑍 − 𝑋) = (𝑘 · (𝑌 − 𝑋)))) | ||
Theorem | ttgbtwnid 25764 | 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 25765 | 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 25766 | Any metric space fulfills Tarski's geometry axioms of congruence. (Contributed by Thierry Arnoux, 13-Mar-2019.) |
⊢ (𝐺 ∈ ∞MetSp → 𝐺 ∈ TarskiGC) | ||
Theorem | cchhllem 25767* | Lemma for chlbas and chlvsca . (Contributed by Thierry Arnoux, 15-Apr-2019.) |
⊢ 𝐶 = (((subringAlg ‘ℂfld)‘ℝ) sSet 〈(·𝑖‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · (∗‘𝑦)))〉) & ⊢ 𝐸 = Slot 𝑁 & ⊢ 𝑁 ∈ ℕ & ⊢ (𝑁 < 5 ∨ 8 < 𝑁) ⇒ ⊢ (𝐸‘ℂfld) = (𝐸‘𝐶) | ||
Syntax | cee 25768 | Declare the syntax for the Euclidean space generator. |
class 𝔼 | ||
Syntax | cbtwn 25769 | Declare the syntax for the Euclidean betweenness predicate. |
class Btwn | ||
Syntax | ccgr 25770 | Declare the syntax for the Euclidean congruence predicate. |
class Cgr | ||
Definition | df-ee 25771 | Define the Euclidean space generator. For details, see elee 25774. (Contributed by Scott Fenton, 3-Jun-2013.) |
⊢ 𝔼 = (𝑛 ∈ ℕ ↦ (ℝ ↑𝑚 (1...𝑛))) | ||
Definition | df-btwn 25772* | Define the Euclidean betweenness predicate. For details, see brbtwn 25779. (Contributed by Scott Fenton, 3-Jun-2013.) |
⊢ Btwn = ◡{〈〈𝑥, 𝑧〉, 𝑦〉 ∣ ∃𝑛 ∈ ℕ ((𝑥 ∈ (𝔼‘𝑛) ∧ 𝑧 ∈ (𝔼‘𝑛) ∧ 𝑦 ∈ (𝔼‘𝑛)) ∧ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑛)(𝑦‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑧‘𝑖))))} | ||
Definition | df-cgr 25773* | Define the Euclidean congruence predicate. For details, see brcgr 25780. (Contributed by Scott Fenton, 3-Jun-2013.) |
⊢ Cgr = {〈𝑥, 𝑦〉 ∣ ∃𝑛 ∈ ℕ ((𝑥 ∈ ((𝔼‘𝑛) × (𝔼‘𝑛)) ∧ 𝑦 ∈ ((𝔼‘𝑛) × (𝔼‘𝑛))) ∧ Σ𝑖 ∈ (1...𝑛)((((1st ‘𝑥)‘𝑖) − ((2nd ‘𝑥)‘𝑖))↑2) = Σ𝑖 ∈ (1...𝑛)((((1st ‘𝑦)‘𝑖) − ((2nd ‘𝑦)‘𝑖))↑2))} | ||
Theorem | elee 25774 | 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 25775* | A condition for a mapping to be an element of a Euclidean space. (Contributed by Scott Fenton, 7-Jun-2013.) |
⊢ (𝑁 ∈ ℕ → ((𝑘 ∈ (1...𝑁) ↦ (𝐴𝐹𝐵)) ∈ (𝔼‘𝑁) ↔ ∀𝑘 ∈ (1...𝑁)(𝐴𝐹𝐵) ∈ ℝ)) | ||
Theorem | eleenn 25776 | If 𝐴 is in (𝔼‘𝑁), then 𝑁 is a natural. (Contributed by Scott Fenton, 1-Jul-2013.) |
⊢ (𝐴 ∈ (𝔼‘𝑁) → 𝑁 ∈ ℕ) | ||
Theorem | eleei 25777 | The forward direction of elee 25774. (Contributed by Scott Fenton, 1-Jul-2013.) |
⊢ (𝐴 ∈ (𝔼‘𝑁) → 𝐴:(1...𝑁)⟶ℝ) | ||
Theorem | eedimeq 25778 | A point belongs to at most one Euclidean space. (Contributed by Scott Fenton, 1-Jul-2013.) |
⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑀)) → 𝑁 = 𝑀) | ||
Theorem | brbtwn 25779* | 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 25780* | 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 25781 | The function value of a point is a real. (Contributed by Scott Fenton, 10-Jun-2013.) |
⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐼 ∈ (1...𝑁)) → (𝐴‘𝐼) ∈ ℝ) | ||
Theorem | fveecn 25782 | The function value of a point is a complex. (Contributed by Scott Fenton, 10-Jun-2013.) |
⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐼 ∈ (1...𝑁)) → (𝐴‘𝐼) ∈ ℂ) | ||
Theorem | eqeefv 25783* | Two points are equal iff they agree in all dimensions. (Contributed by Scott Fenton, 10-Jun-2013.) |
⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) → (𝐴 = 𝐵 ↔ ∀𝑖 ∈ (1...𝑁)(𝐴‘𝑖) = (𝐵‘𝑖))) | ||
Theorem | eqeelen 25784* | 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 25785* | Alternate characterization of betweenness, with no existential quantifiers. (Contributed by Scott Fenton, 24-Jun-2013.) |
⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → (𝐴 Btwn 〈𝐵, 𝐶〉 ↔ (∀𝑖 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑖) − (𝐴‘𝑖))) ≤ 0 ∧ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑗) − (𝐴‘𝑗))) = (((𝐵‘𝑗) − (𝐴‘𝑗)) · ((𝐶‘𝑖) − (𝐴‘𝑖)))))) | ||
Theorem | colinearalglem1 25786 | Lemma for colinearalg 25790. Expand out a multiplication. (Contributed by Scott Fenton, 24-Jun-2013.) |
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ)) → (((𝐵 − 𝐴) · (𝐹 − 𝐷)) = ((𝐸 − 𝐷) · (𝐶 − 𝐴)) ↔ ((𝐵 · 𝐹) − ((𝐴 · 𝐹) + (𝐵 · 𝐷))) = ((𝐶 · 𝐸) − ((𝐴 · 𝐸) + (𝐶 · 𝐷))))) | ||
Theorem | colinearalglem2 25787* | Lemma for colinearalg 25790. Translate between two forms of the colinearity condition. (Contributed by Scott Fenton, 24-Jun-2013.) |
⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → (∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑗) − (𝐴‘𝑗))) = (((𝐵‘𝑗) − (𝐴‘𝑗)) · ((𝐶‘𝑖) − (𝐴‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐶‘𝑖) − (𝐵‘𝑖)) · ((𝐴‘𝑗) − (𝐵‘𝑗))) = (((𝐶‘𝑗) − (𝐵‘𝑗)) · ((𝐴‘𝑖) − (𝐵‘𝑖))))) | ||
Theorem | colinearalglem3 25788* | Lemma for colinearalg 25790. Translate between two forms of the colinearity condition. (Contributed by Scott Fenton, 24-Jun-2013.) |
⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → (∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑗) − (𝐴‘𝑗))) = (((𝐵‘𝑗) − (𝐴‘𝑗)) · ((𝐶‘𝑖) − (𝐴‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐴‘𝑖) − (𝐶‘𝑖)) · ((𝐵‘𝑗) − (𝐶‘𝑗))) = (((𝐴‘𝑗) − (𝐶‘𝑗)) · ((𝐵‘𝑖) − (𝐶‘𝑖))))) | ||
Theorem | colinearalglem4 25789* | Lemma for colinearalg 25790. Prove a disjunction that will be needed in the final proof. (Contributed by Scott Fenton, 27-Jun-2013.) |
⊢ (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ 𝐾 ∈ ℝ) → (∀𝑖 ∈ (1...𝑁)((((𝐾 · ((𝐶‘𝑖) − (𝐴‘𝑖))) + (𝐴‘𝑖)) − (𝐴‘𝑖)) · ((𝐶‘𝑖) − (𝐴‘𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐶‘𝑖) − ((𝐾 · ((𝐶‘𝑖) − (𝐴‘𝑖))) + (𝐴‘𝑖))) · ((𝐴‘𝑖) − ((𝐾 · ((𝐶‘𝑖) − (𝐴‘𝑖))) + (𝐴‘𝑖)))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐴‘𝑖) − (𝐶‘𝑖)) · (((𝐾 · ((𝐶‘𝑖) − (𝐴‘𝑖))) + (𝐴‘𝑖)) − (𝐶‘𝑖))) ≤ 0)) | ||
Theorem | colinearalg 25790* | An algebraic characterization of colinearity. Note the similarity to brbtwn2 25785. (Contributed by Scott Fenton, 24-Jun-2013.) |
⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → ((𝐴 Btwn 〈𝐵, 𝐶〉 ∨ 𝐵 Btwn 〈𝐶, 𝐴〉 ∨ 𝐶 Btwn 〈𝐴, 𝐵〉) ↔ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑗) − (𝐴‘𝑗))) = (((𝐵‘𝑗) − (𝐴‘𝑗)) · ((𝐶‘𝑖) − (𝐴‘𝑖))))) | ||
Theorem | eleesub 25791* | Membership of a subtraction mapping in a Euclidean space. (Contributed by Scott Fenton, 17-Jul-2013.) |
⊢ 𝐶 = (𝑖 ∈ (1...𝑁) ↦ ((𝐴‘𝑖) − (𝐵‘𝑖))) ⇒ ⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) → 𝐶 ∈ (𝔼‘𝑁)) | ||
Theorem | eleesubd 25792* | Membership of a subtraction mapping in a Euclidean space. Deduction form of eleesub 25791. (Contributed by Scott Fenton, 17-Jul-2013.) |
⊢ (𝜑 → 𝐶 = (𝑖 ∈ (1...𝑁) ↦ ((𝐴‘𝑖) − (𝐵‘𝑖)))) ⇒ ⊢ ((𝜑 ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) → 𝐶 ∈ (𝔼‘𝑁)) | ||
Theorem | axdimuniq 25793 | The unique dimension axiom. If a point is in 𝑁 dimensional space and in 𝑀 dimensional space, then 𝑁 = 𝑀. This axiom is not traditionally presented with Tarski's axioms, but we require it here as we are considering spaces in arbitrary dimensions. (Contributed by Scott Fenton, 24-Sep-2013.) |
⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁)) ∧ (𝑀 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑀))) → 𝑁 = 𝑀) | ||
Theorem | axcgrrflx 25794 | 𝐴 is as far from 𝐵 as 𝐵 is from 𝐴. Axiom A1 of [Schwabhauser] p. 10. (Contributed by Scott Fenton, 3-Jun-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) → 〈𝐴, 𝐵〉Cgr〈𝐵, 𝐴〉) | ||
Theorem | axcgrtr 25795 | Congruence is transitive. Axiom A2 of [Schwabhauser] p. 10. (Contributed by Scott Fenton, 3-Jun-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) → ((〈𝐴, 𝐵〉Cgr〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐸, 𝐹〉) → 〈𝐶, 𝐷〉Cgr〈𝐸, 𝐹〉)) | ||
Theorem | axcgrid 25796 | If there is no distance between 𝐴 and 𝐵, then 𝐴 = 𝐵. Axiom A3 of [Schwabhauser] p. 10. (Contributed by Scott Fenton, 3-Jun-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → (〈𝐴, 𝐵〉Cgr〈𝐶, 𝐶〉 → 𝐴 = 𝐵)) | ||
Theorem | axsegconlem1 25797* | Lemma for axsegcon 25807. Handle the degenerate case. (Contributed by Scott Fenton, 7-Jun-2013.) |
⊢ ((𝐴 = 𝐵 ∧ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)))) → ∃𝑥 ∈ (𝔼‘𝑁)∃𝑡 ∈ (0[,]1)(∀𝑖 ∈ (1...𝑁)(𝐵‘𝑖) = (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝑥‘𝑖))) ∧ Σ𝑖 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝑥‘𝑖))↑2) = Σ𝑖 ∈ (1...𝑁)(((𝐶‘𝑖) − (𝐷‘𝑖))↑2))) | ||
Theorem | axsegconlem2 25798* | Lemma for axsegcon 25807. Show that the square of the distance between two points is a real number. (Contributed by Scott Fenton, 17-Sep-2013.) |
⊢ 𝑆 = Σ𝑝 ∈ (1...𝑁)(((𝐴‘𝑝) − (𝐵‘𝑝))↑2) ⇒ ⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) → 𝑆 ∈ ℝ) | ||
Theorem | axsegconlem3 25799* | Lemma for axsegcon 25807. Show that the square of the distance between two points is nonnegative. (Contributed by Scott Fenton, 17-Sep-2013.) |
⊢ 𝑆 = Σ𝑝 ∈ (1...𝑁)(((𝐴‘𝑝) − (𝐵‘𝑝))↑2) ⇒ ⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) → 0 ≤ 𝑆) | ||
Theorem | axsegconlem4 25800* | Lemma for axsegcon 25807. Show that the distance between two points is a real number. (Contributed by Scott Fenton, 17-Sep-2013.) |
⊢ 𝑆 = Σ𝑝 ∈ (1...𝑁)(((𝐴‘𝑝) − (𝐵‘𝑝))↑2) ⇒ ⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) → (√‘𝑆) ∈ ℝ) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |