Metamath Proof Explorer

Theorem tgbtwnxfr

Description: A condition for extending betweenness to a new set of points based on congruence with another set of points. Theorem 4.6 of Schwabhauser p. 36. (Contributed by Thierry Arnoux, 27-Apr-2019)

Ref Expression
Hypotheses tgcgrxfr.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
tgcgrxfr.m ⊢ − = ( dist ‘ 𝐺 )
tgcgrxfr.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
tgcgrxfr.r ⊢ ∼ = ( cgrG ‘ 𝐺 )
tgcgrxfr.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
tgbtwnxfr.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
tgbtwnxfr.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
tgbtwnxfr.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
tgbtwnxfr.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
tgbtwnxfr.e ⊢ ( 𝜑 → 𝐸 ∈ 𝑃 )
tgbtwnxfr.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑃 )
tgbtwnxfr.2 ⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∼ ⟨“ 𝐷 𝐸 𝐹 ”⟩ )
tgbtwnxfr.1 ⊢ ( 𝜑 → 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) )
Assertion tgbtwnxfr ( 𝜑 → 𝐸 ∈ ( 𝐷 𝐼 𝐹 ) )

Proof

Step Hyp Ref Expression
1 tgcgrxfr.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 tgcgrxfr.m ⊢ − = ( dist ‘ 𝐺 )
3 tgcgrxfr.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
4 tgcgrxfr.r ⊢ ∼ = ( cgrG ‘ 𝐺 )
5 tgcgrxfr.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
6 tgbtwnxfr.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
7 tgbtwnxfr.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
8 tgbtwnxfr.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
9 tgbtwnxfr.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
10 tgbtwnxfr.e ⊢ ( 𝜑 → 𝐸 ∈ 𝑃 )
11 tgbtwnxfr.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑃 )
12 tgbtwnxfr.2 ⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∼ ⟨“ 𝐷 𝐸 𝐹 ”⟩ )
13 tgbtwnxfr.1 ⊢ ( 𝜑 → 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) )
14 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∼ ⟨“ 𝐷 𝑒 𝐹 ”⟩ ) ) → 𝐺 ∈ TarskiG )
15 simplr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∼ ⟨“ 𝐷 𝑒 𝐹 ”⟩ ) ) → 𝑒 ∈ 𝑃 )
16 10 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∼ ⟨“ 𝐷 𝑒 𝐹 ”⟩ ) ) → 𝐸 ∈ 𝑃 )
17 9 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∼ ⟨“ 𝐷 𝑒 𝐹 ”⟩ ) ) → 𝐷 ∈ 𝑃 )
18 11 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∼ ⟨“ 𝐷 𝑒 𝐹 ”⟩ ) ) → 𝐹 ∈ 𝑃 )
19 simprl ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∼ ⟨“ 𝐷 𝑒 𝐹 ”⟩ ) ) → 𝑒 ∈ ( 𝐷 𝐼 𝐹 ) )
20 eqidd ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∼ ⟨“ 𝐷 𝑒 𝐹 ”⟩ ) ) → ( 𝐷 − 𝐹 ) = ( 𝐷 − 𝐹 ) )
21 eqidd ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∼ ⟨“ 𝐷 𝑒 𝐹 ”⟩ ) ) → ( 𝑒 − 𝐹 ) = ( 𝑒 − 𝐹 ) )
22 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∼ ⟨“ 𝐷 𝑒 𝐹 ”⟩ ) ) → 𝐴 ∈ 𝑃 )
23 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∼ ⟨“ 𝐷 𝑒 𝐹 ”⟩ ) ) → 𝐵 ∈ 𝑃 )
24 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∼ ⟨“ 𝐷 𝑒 𝐹 ”⟩ ) ) → 𝐶 ∈ 𝑃 )
25 simprr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∼ ⟨“ 𝐷 𝑒 𝐹 ”⟩ ) ) → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∼ ⟨“ 𝐷 𝑒 𝐹 ”⟩ )
26 1 2 3 4 14 22 23 24 17 15 18 25 trgcgrcom ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∼ ⟨“ 𝐷 𝑒 𝐹 ”⟩ ) ) → ⟨“ 𝐷 𝑒 𝐹 ”⟩ ∼ ⟨“ 𝐴 𝐵 𝐶 ”⟩ )
27 12 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∼ ⟨“ 𝐷 𝑒 𝐹 ”⟩ ) ) → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∼ ⟨“ 𝐷 𝐸 𝐹 ”⟩ )
28 1 2 3 4 14 17 15 18 22 23 24 26 17 16 18 27 cgr3tr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∼ ⟨“ 𝐷 𝑒 𝐹 ”⟩ ) ) → ⟨“ 𝐷 𝑒 𝐹 ”⟩ ∼ ⟨“ 𝐷 𝐸 𝐹 ”⟩ )
29 1 2 3 4 14 17 15 18 17 16 18 28 trgcgrcom ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∼ ⟨“ 𝐷 𝑒 𝐹 ”⟩ ) ) → ⟨“ 𝐷 𝐸 𝐹 ”⟩ ∼ ⟨“ 𝐷 𝑒 𝐹 ”⟩ )
30 1 2 3 4 14 17 16 18 17 15 18 29 cgr3simp1 ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∼ ⟨“ 𝐷 𝑒 𝐹 ”⟩ ) ) → ( 𝐷 − 𝐸 ) = ( 𝐷 − 𝑒 ) )
31 1 2 3 4 14 17 16 18 17 15 18 29 cgr3simp2 ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∼ ⟨“ 𝐷 𝑒 𝐹 ”⟩ ) ) → ( 𝐸 − 𝐹 ) = ( 𝑒 − 𝐹 ) )
32 1 2 3 14 16 18 15 18 31 tgcgrcomlr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∼ ⟨“ 𝐷 𝑒 𝐹 ”⟩ ) ) → ( 𝐹 − 𝐸 ) = ( 𝐹 − 𝑒 ) )
33 1 2 3 14 17 15 18 16 17 15 18 15 19 19 20 21 30 32 tgifscgr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∼ ⟨“ 𝐷 𝑒 𝐹 ”⟩ ) ) → ( 𝑒 − 𝐸 ) = ( 𝑒 − 𝑒 ) )
34 1 2 3 14 15 16 15 33 axtgcgrid ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∼ ⟨“ 𝐷 𝑒 𝐹 ”⟩ ) ) → 𝑒 = 𝐸 )
35 34 19 eqeltrrd ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∼ ⟨“ 𝐷 𝑒 𝐹 ”⟩ ) ) → 𝐸 ∈ ( 𝐷 𝐼 𝐹 ) )
36 1 2 3 4 5 6 7 8 9 10 11 12 cgr3simp3 ⊢ ( 𝜑 → ( 𝐶 − 𝐴 ) = ( 𝐹 − 𝐷 ) )
37 1 2 3 5 8 6 11 9 36 tgcgrcomlr ⊢ ( 𝜑 → ( 𝐴 − 𝐶 ) = ( 𝐷 − 𝐹 ) )
38 1 2 3 4 5 6 7 8 9 11 13 37 tgcgrxfr ⊢ ( 𝜑 → ∃ 𝑒 ∈ 𝑃 ( 𝑒 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∼ ⟨“ 𝐷 𝑒 𝐹 ”⟩ ) )
39 35 38 r19.29a ⊢ ( 𝜑 → 𝐸 ∈ ( 𝐷 𝐼 𝐹 ) )