Description: Point inversion of one point of a triangle around another point preserves triangle congruence. (Contributed by Thierry Arnoux, 4-Oct-2020)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | mirval.p | ⊢ 𝑃 = ( Base ‘ 𝐺 ) | |
| mirval.d | ⊢ − = ( dist ‘ 𝐺 ) | ||
| mirval.i | ⊢ 𝐼 = ( Itv ‘ 𝐺 ) | ||
| mirval.l | ⊢ 𝐿 = ( LineG ‘ 𝐺 ) | ||
| mirval.s | ⊢ 𝑆 = ( pInvG ‘ 𝐺 ) | ||
| mirval.g | ⊢ ( 𝜑 → 𝐺 ∈ TarskiG ) | ||
| mirtrcgr.e | ⊢ ∼ = ( cgrG ‘ 𝐺 ) | ||
| mirtrcgr.m | ⊢ 𝑀 = ( 𝑆 ‘ 𝐵 ) | ||
| mirtrcgr.n | ⊢ 𝑁 = ( 𝑆 ‘ 𝑌 ) | ||
| mirtrcgr.a | ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 ) | ||
| mirtrcgr.b | ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 ) | ||
| mirtrcgr.x | ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 ) | ||
| mirtrcgr.y | ⊢ ( 𝜑 → 𝑌 ∈ 𝑃 ) | ||
| mirtrcgr.c | ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 ) | ||
| mirtrcgr.z | ⊢ ( 𝜑 → 𝑍 ∈ 𝑃 ) | ||
| mirtrcgr.1 | ⊢ ( 𝜑 → 𝐴 ≠ 𝐵 ) | ||
| mirtrcgr.2 | ⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∼ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) | ||
| Assertion | mirtrcgr | ⊢ ( 𝜑 → ⟨“ ( 𝑀 ‘ 𝐴 ) 𝐵 𝐶 ”⟩ ∼ ⟨“ ( 𝑁 ‘ 𝑋 ) 𝑌 𝑍 ”⟩ ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | mirval.p | ⊢ 𝑃 = ( Base ‘ 𝐺 ) | |
| 2 | mirval.d | ⊢ − = ( dist ‘ 𝐺 ) | |
| 3 | mirval.i | ⊢ 𝐼 = ( Itv ‘ 𝐺 ) | |
| 4 | mirval.l | ⊢ 𝐿 = ( LineG ‘ 𝐺 ) | |
| 5 | mirval.s | ⊢ 𝑆 = ( pInvG ‘ 𝐺 ) | |
| 6 | mirval.g | ⊢ ( 𝜑 → 𝐺 ∈ TarskiG ) | |
| 7 | mirtrcgr.e | ⊢ ∼ = ( cgrG ‘ 𝐺 ) | |
| 8 | mirtrcgr.m | ⊢ 𝑀 = ( 𝑆 ‘ 𝐵 ) | |
| 9 | mirtrcgr.n | ⊢ 𝑁 = ( 𝑆 ‘ 𝑌 ) | |
| 10 | mirtrcgr.a | ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 ) | |
| 11 | mirtrcgr.b | ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 ) | |
| 12 | mirtrcgr.x | ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 ) | |
| 13 | mirtrcgr.y | ⊢ ( 𝜑 → 𝑌 ∈ 𝑃 ) | |
| 14 | mirtrcgr.c | ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 ) | |
| 15 | mirtrcgr.z | ⊢ ( 𝜑 → 𝑍 ∈ 𝑃 ) | |
| 16 | mirtrcgr.1 | ⊢ ( 𝜑 → 𝐴 ≠ 𝐵 ) | |
| 17 | mirtrcgr.2 | ⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∼ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) | |
| 18 | 1 2 3 4 5 6 11 8 10 | mircl | ⊢ ( 𝜑 → ( 𝑀 ‘ 𝐴 ) ∈ 𝑃 ) |
| 19 | 1 2 3 4 5 6 13 9 12 | mircl | ⊢ ( 𝜑 → ( 𝑁 ‘ 𝑋 ) ∈ 𝑃 ) |
| 20 | 1 2 3 7 6 10 11 14 12 13 15 17 | cgr3simp1 | ⊢ ( 𝜑 → ( 𝐴 − 𝐵 ) = ( 𝑋 − 𝑌 ) ) |
| 21 | 1 2 3 6 10 11 12 13 20 | tgcgrcomlr | ⊢ ( 𝜑 → ( 𝐵 − 𝐴 ) = ( 𝑌 − 𝑋 ) ) |
| 22 | 1 2 3 4 5 6 11 8 10 | mircgr | ⊢ ( 𝜑 → ( 𝐵 − ( 𝑀 ‘ 𝐴 ) ) = ( 𝐵 − 𝐴 ) ) |
| 23 | 1 2 3 4 5 6 13 9 12 | mircgr | ⊢ ( 𝜑 → ( 𝑌 − ( 𝑁 ‘ 𝑋 ) ) = ( 𝑌 − 𝑋 ) ) |
| 24 | 21 22 23 | 3eqtr4d | ⊢ ( 𝜑 → ( 𝐵 − ( 𝑀 ‘ 𝐴 ) ) = ( 𝑌 − ( 𝑁 ‘ 𝑋 ) ) ) |
| 25 | 1 2 3 6 11 18 13 19 24 | tgcgrcomlr | ⊢ ( 𝜑 → ( ( 𝑀 ‘ 𝐴 ) − 𝐵 ) = ( ( 𝑁 ‘ 𝑋 ) − 𝑌 ) ) |
| 26 | 1 2 3 7 6 10 11 14 12 13 15 17 | cgr3simp2 | ⊢ ( 𝜑 → ( 𝐵 − 𝐶 ) = ( 𝑌 − 𝑍 ) ) |
| 27 | 1 2 3 4 5 6 11 8 10 | mirbtwn | ⊢ ( 𝜑 → 𝐵 ∈ ( ( 𝑀 ‘ 𝐴 ) 𝐼 𝐴 ) ) |
| 28 | 1 4 3 6 18 10 11 27 | btwncolg1 | ⊢ ( 𝜑 → ( 𝐵 ∈ ( ( 𝑀 ‘ 𝐴 ) 𝐿 𝐴 ) ∨ ( 𝑀 ‘ 𝐴 ) = 𝐴 ) ) |
| 29 | 1 4 3 6 18 10 11 28 | colcom | ⊢ ( 𝜑 → ( 𝐵 ∈ ( 𝐴 𝐿 ( 𝑀 ‘ 𝐴 ) ) ∨ 𝐴 = ( 𝑀 ‘ 𝐴 ) ) ) |
| 30 | 1 2 3 4 5 6 7 8 9 10 11 12 13 20 | mircgrextend | ⊢ ( 𝜑 → ( 𝐴 − ( 𝑀 ‘ 𝐴 ) ) = ( 𝑋 − ( 𝑁 ‘ 𝑋 ) ) ) |
| 31 | 1 2 3 6 10 18 12 19 30 | tgcgrcomlr | ⊢ ( 𝜑 → ( ( 𝑀 ‘ 𝐴 ) − 𝐴 ) = ( ( 𝑁 ‘ 𝑋 ) − 𝑋 ) ) |
| 32 | 1 2 7 6 10 11 18 12 13 19 20 24 31 | trgcgr | ⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 ( 𝑀 ‘ 𝐴 ) ”⟩ ∼ ⟨“ 𝑋 𝑌 ( 𝑁 ‘ 𝑋 ) ”⟩ ) |
| 33 | 1 2 3 7 6 10 11 14 12 13 15 17 | cgr3simp3 | ⊢ ( 𝜑 → ( 𝐶 − 𝐴 ) = ( 𝑍 − 𝑋 ) ) |
| 34 | 1 2 3 6 14 10 15 12 33 | tgcgrcomlr | ⊢ ( 𝜑 → ( 𝐴 − 𝐶 ) = ( 𝑋 − 𝑍 ) ) |
| 35 | 1 4 3 6 10 11 18 7 12 13 2 14 19 15 29 32 34 26 16 | tgfscgr | ⊢ ( 𝜑 → ( ( 𝑀 ‘ 𝐴 ) − 𝐶 ) = ( ( 𝑁 ‘ 𝑋 ) − 𝑍 ) ) |
| 36 | 1 2 3 6 18 14 19 15 35 | tgcgrcomlr | ⊢ ( 𝜑 → ( 𝐶 − ( 𝑀 ‘ 𝐴 ) ) = ( 𝑍 − ( 𝑁 ‘ 𝑋 ) ) ) |
| 37 | 1 2 7 6 18 11 14 19 13 15 25 26 36 | trgcgr | ⊢ ( 𝜑 → ⟨“ ( 𝑀 ‘ 𝐴 ) 𝐵 𝐶 ”⟩ ∼ ⟨“ ( 𝑁 ‘ 𝑋 ) 𝑌 𝑍 ”⟩ ) |