Description: Lemma for tgbtwnconn1 . (Contributed by Thierry Arnoux, 30-Apr-2019)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | tgbtwnconn1.p | ⊢ 𝑃 = ( Base ‘ 𝐺 ) | |
| tgbtwnconn1.i | ⊢ 𝐼 = ( Itv ‘ 𝐺 ) | ||
| tgbtwnconn1.g | ⊢ ( 𝜑 → 𝐺 ∈ TarskiG ) | ||
| tgbtwnconn1.a | ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 ) | ||
| tgbtwnconn1.b | ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 ) | ||
| tgbtwnconn1.c | ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 ) | ||
| tgbtwnconn1.d | ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 ) | ||
| tgbtwnconn1.1 | ⊢ ( 𝜑 → 𝐴 ≠ 𝐵 ) | ||
| tgbtwnconn1.2 | ⊢ ( 𝜑 → 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) | ||
| tgbtwnconn1.3 | ⊢ ( 𝜑 → 𝐵 ∈ ( 𝐴 𝐼 𝐷 ) ) | ||
| tgbtwnconn1.m | ⊢ − = ( dist ‘ 𝐺 ) | ||
| tgbtwnconn1.e | ⊢ ( 𝜑 → 𝐸 ∈ 𝑃 ) | ||
| tgbtwnconn1.f | ⊢ ( 𝜑 → 𝐹 ∈ 𝑃 ) | ||
| tgbtwnconn1.h | ⊢ ( 𝜑 → 𝐻 ∈ 𝑃 ) | ||
| tgbtwnconn1.j | ⊢ ( 𝜑 → 𝐽 ∈ 𝑃 ) | ||
| tgbtwnconn1.4 | ⊢ ( 𝜑 → 𝐷 ∈ ( 𝐴 𝐼 𝐸 ) ) | ||
| tgbtwnconn1.5 | ⊢ ( 𝜑 → 𝐶 ∈ ( 𝐴 𝐼 𝐹 ) ) | ||
| tgbtwnconn1.6 | ⊢ ( 𝜑 → 𝐸 ∈ ( 𝐴 𝐼 𝐻 ) ) | ||
| tgbtwnconn1.7 | ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐴 𝐼 𝐽 ) ) | ||
| tgbtwnconn1.8 | ⊢ ( 𝜑 → ( 𝐸 − 𝐷 ) = ( 𝐶 − 𝐷 ) ) | ||
| tgbtwnconn1.9 | ⊢ ( 𝜑 → ( 𝐶 − 𝐹 ) = ( 𝐶 − 𝐷 ) ) | ||
| tgbtwnconn1.10 | ⊢ ( 𝜑 → ( 𝐸 − 𝐻 ) = ( 𝐵 − 𝐶 ) ) | ||
| tgbtwnconn1.11 | ⊢ ( 𝜑 → ( 𝐹 − 𝐽 ) = ( 𝐵 − 𝐷 ) ) | ||
| Assertion | tgbtwnconn1lem1 | ⊢ ( 𝜑 → 𝐻 = 𝐽 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | tgbtwnconn1.p | ⊢ 𝑃 = ( Base ‘ 𝐺 ) | |
| 2 | tgbtwnconn1.i | ⊢ 𝐼 = ( Itv ‘ 𝐺 ) | |
| 3 | tgbtwnconn1.g | ⊢ ( 𝜑 → 𝐺 ∈ TarskiG ) | |
| 4 | tgbtwnconn1.a | ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 ) | |
| 5 | tgbtwnconn1.b | ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 ) | |
| 6 | tgbtwnconn1.c | ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 ) | |
| 7 | tgbtwnconn1.d | ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 ) | |
| 8 | tgbtwnconn1.1 | ⊢ ( 𝜑 → 𝐴 ≠ 𝐵 ) | |
| 9 | tgbtwnconn1.2 | ⊢ ( 𝜑 → 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) | |
| 10 | tgbtwnconn1.3 | ⊢ ( 𝜑 → 𝐵 ∈ ( 𝐴 𝐼 𝐷 ) ) | |
| 11 | tgbtwnconn1.m | ⊢ − = ( dist ‘ 𝐺 ) | |
| 12 | tgbtwnconn1.e | ⊢ ( 𝜑 → 𝐸 ∈ 𝑃 ) | |
| 13 | tgbtwnconn1.f | ⊢ ( 𝜑 → 𝐹 ∈ 𝑃 ) | |
| 14 | tgbtwnconn1.h | ⊢ ( 𝜑 → 𝐻 ∈ 𝑃 ) | |
| 15 | tgbtwnconn1.j | ⊢ ( 𝜑 → 𝐽 ∈ 𝑃 ) | |
| 16 | tgbtwnconn1.4 | ⊢ ( 𝜑 → 𝐷 ∈ ( 𝐴 𝐼 𝐸 ) ) | |
| 17 | tgbtwnconn1.5 | ⊢ ( 𝜑 → 𝐶 ∈ ( 𝐴 𝐼 𝐹 ) ) | |
| 18 | tgbtwnconn1.6 | ⊢ ( 𝜑 → 𝐸 ∈ ( 𝐴 𝐼 𝐻 ) ) | |
| 19 | tgbtwnconn1.7 | ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐴 𝐼 𝐽 ) ) | |
| 20 | tgbtwnconn1.8 | ⊢ ( 𝜑 → ( 𝐸 − 𝐷 ) = ( 𝐶 − 𝐷 ) ) | |
| 21 | tgbtwnconn1.9 | ⊢ ( 𝜑 → ( 𝐶 − 𝐹 ) = ( 𝐶 − 𝐷 ) ) | |
| 22 | tgbtwnconn1.10 | ⊢ ( 𝜑 → ( 𝐸 − 𝐻 ) = ( 𝐵 − 𝐶 ) ) | |
| 23 | tgbtwnconn1.11 | ⊢ ( 𝜑 → ( 𝐹 − 𝐽 ) = ( 𝐵 − 𝐷 ) ) | |
| 24 | 1 11 2 3 4 5 7 12 10 16 | tgbtwnexch | ⊢ ( 𝜑 → 𝐵 ∈ ( 𝐴 𝐼 𝐸 ) ) |
| 25 | 1 11 2 3 4 5 12 14 24 18 | tgbtwnexch | ⊢ ( 𝜑 → 𝐵 ∈ ( 𝐴 𝐼 𝐻 ) ) |
| 26 | 1 11 2 3 4 5 6 13 9 17 | tgbtwnexch | ⊢ ( 𝜑 → 𝐵 ∈ ( 𝐴 𝐼 𝐹 ) ) |
| 27 | 1 11 2 3 4 5 13 15 26 19 | tgbtwnexch | ⊢ ( 𝜑 → 𝐵 ∈ ( 𝐴 𝐼 𝐽 ) ) |
| 28 | 1 11 2 3 4 5 12 14 24 18 | tgbtwnexch3 | ⊢ ( 𝜑 → 𝐸 ∈ ( 𝐵 𝐼 𝐻 ) ) |
| 29 | 1 11 2 3 4 6 13 15 17 19 | tgbtwnexch | ⊢ ( 𝜑 → 𝐶 ∈ ( 𝐴 𝐼 𝐽 ) ) |
| 30 | 1 11 2 3 4 5 6 15 9 29 | tgbtwnexch3 | ⊢ ( 𝜑 → 𝐶 ∈ ( 𝐵 𝐼 𝐽 ) ) |
| 31 | 1 11 2 3 5 6 15 30 | tgbtwncom | ⊢ ( 𝜑 → 𝐶 ∈ ( 𝐽 𝐼 𝐵 ) ) |
| 32 | 1 11 2 3 4 5 7 12 10 16 | tgbtwnexch3 | ⊢ ( 𝜑 → 𝐷 ∈ ( 𝐵 𝐼 𝐸 ) ) |
| 33 | 1 11 2 3 4 6 13 15 17 19 | tgbtwnexch3 | ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 𝐼 𝐽 ) ) |
| 34 | 1 11 2 3 6 13 15 33 | tgbtwncom | ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐽 𝐼 𝐶 ) ) |
| 35 | 1 11 2 3 15 13 | axtgcgrrflx | ⊢ ( 𝜑 → ( 𝐽 − 𝐹 ) = ( 𝐹 − 𝐽 ) ) |
| 36 | 35 23 | eqtr2d | ⊢ ( 𝜑 → ( 𝐵 − 𝐷 ) = ( 𝐽 − 𝐹 ) ) |
| 37 | 20 21 | eqtr4d | ⊢ ( 𝜑 → ( 𝐸 − 𝐷 ) = ( 𝐶 − 𝐹 ) ) |
| 38 | 1 11 2 3 12 7 6 13 37 | tgcgrcomlr | ⊢ ( 𝜑 → ( 𝐷 − 𝐸 ) = ( 𝐹 − 𝐶 ) ) |
| 39 | 1 11 2 3 5 7 12 15 13 6 32 34 36 38 | tgcgrextend | ⊢ ( 𝜑 → ( 𝐵 − 𝐸 ) = ( 𝐽 − 𝐶 ) ) |
| 40 | 1 11 2 3 12 14 5 6 22 | tgcgrcomr | ⊢ ( 𝜑 → ( 𝐸 − 𝐻 ) = ( 𝐶 − 𝐵 ) ) |
| 41 | 1 11 2 3 5 12 14 15 6 5 28 31 39 40 | tgcgrextend | ⊢ ( 𝜑 → ( 𝐵 − 𝐻 ) = ( 𝐽 − 𝐵 ) ) |
| 42 | 1 11 2 3 5 15 | axtgcgrrflx | ⊢ ( 𝜑 → ( 𝐵 − 𝐽 ) = ( 𝐽 − 𝐵 ) ) |
| 43 | 1 11 2 3 5 15 5 4 14 15 8 25 27 41 42 | tgsegconeq | ⊢ ( 𝜑 → 𝐻 = 𝐽 ) |