Metamath Proof Explorer

Theorem tgbtwnouttr2

Description: Outer transitivity law for betweenness. Left-hand side of Theorem 3.7 of Schwabhauser p. 30. (Contributed by Thierry Arnoux, 18-Mar-2019)

Ref Expression
Hypotheses tkgeom.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
tkgeom.d ⊢ − = ( dist ‘ 𝐺 )
tkgeom.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
tkgeom.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
tgbtwnintr.1 ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
tgbtwnintr.2 ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
tgbtwnintr.3 ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
tgbtwnintr.4 ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
tgbtwnouttr2.1 ⊢ ( 𝜑 → 𝐵 ≠ 𝐶 )
tgbtwnouttr2.2 ⊢ ( 𝜑 → 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) )
tgbtwnouttr2.3 ⊢ ( 𝜑 → 𝐶 ∈ ( 𝐵 𝐼 𝐷 ) )
Assertion tgbtwnouttr2 ( 𝜑 → 𝐶 ∈ ( 𝐴 𝐼 𝐷 ) )

Proof

Step Hyp Ref Expression
1 tkgeom.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 tkgeom.d ⊢ − = ( dist ‘ 𝐺 )
3 tkgeom.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
4 tkgeom.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
5 tgbtwnintr.1 ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
6 tgbtwnintr.2 ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
7 tgbtwnintr.3 ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
8 tgbtwnintr.4 ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
9 tgbtwnouttr2.1 ⊢ ( 𝜑 → 𝐵 ≠ 𝐶 )
10 tgbtwnouttr2.2 ⊢ ( 𝜑 → 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) )
11 tgbtwnouttr2.3 ⊢ ( 𝜑 → 𝐶 ∈ ( 𝐵 𝐼 𝐷 ) )
12 simprl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑥 ) ∧ ( 𝐶 − 𝑥 ) = ( 𝐶 − 𝐷 ) ) ) → 𝐶 ∈ ( 𝐴 𝐼 𝑥 ) )
13 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑥 ) ∧ ( 𝐶 − 𝑥 ) = ( 𝐶 − 𝐷 ) ) ) → 𝐺 ∈ TarskiG )
14 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑥 ) ∧ ( 𝐶 − 𝑥 ) = ( 𝐶 − 𝐷 ) ) ) → 𝐶 ∈ 𝑃 )
15 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑥 ) ∧ ( 𝐶 − 𝑥 ) = ( 𝐶 − 𝐷 ) ) ) → 𝐷 ∈ 𝑃 )
16 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑥 ) ∧ ( 𝐶 − 𝑥 ) = ( 𝐶 − 𝐷 ) ) ) → 𝐵 ∈ 𝑃 )
17 simplr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑥 ) ∧ ( 𝐶 − 𝑥 ) = ( 𝐶 − 𝐷 ) ) ) → 𝑥 ∈ 𝑃 )
18 9 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑥 ) ∧ ( 𝐶 − 𝑥 ) = ( 𝐶 − 𝐷 ) ) ) → 𝐵 ≠ 𝐶 )
19 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑥 ) ∧ ( 𝐶 − 𝑥 ) = ( 𝐶 − 𝐷 ) ) ) → 𝐴 ∈ 𝑃 )
20 10 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑥 ) ∧ ( 𝐶 − 𝑥 ) = ( 𝐶 − 𝐷 ) ) ) → 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) )
21 1 2 3 13 19 16 14 17 20 12 tgbtwnexch3 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑥 ) ∧ ( 𝐶 − 𝑥 ) = ( 𝐶 − 𝐷 ) ) ) → 𝐶 ∈ ( 𝐵 𝐼 𝑥 ) )
22 11 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑥 ) ∧ ( 𝐶 − 𝑥 ) = ( 𝐶 − 𝐷 ) ) ) → 𝐶 ∈ ( 𝐵 𝐼 𝐷 ) )
23 simprr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑥 ) ∧ ( 𝐶 − 𝑥 ) = ( 𝐶 − 𝐷 ) ) ) → ( 𝐶 − 𝑥 ) = ( 𝐶 − 𝐷 ) )
24 eqidd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑥 ) ∧ ( 𝐶 − 𝑥 ) = ( 𝐶 − 𝐷 ) ) ) → ( 𝐶 − 𝐷 ) = ( 𝐶 − 𝐷 ) )
25 1 2 3 13 14 14 15 16 17 15 18 21 22 23 24 tgsegconeq ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑥 ) ∧ ( 𝐶 − 𝑥 ) = ( 𝐶 − 𝐷 ) ) ) → 𝑥 = 𝐷 )
26 25 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑥 ) ∧ ( 𝐶 − 𝑥 ) = ( 𝐶 − 𝐷 ) ) ) → ( 𝐴 𝐼 𝑥 ) = ( 𝐴 𝐼 𝐷 ) )
27 12 26 eleqtrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑥 ) ∧ ( 𝐶 − 𝑥 ) = ( 𝐶 − 𝐷 ) ) ) → 𝐶 ∈ ( 𝐴 𝐼 𝐷 ) )
28 1 2 3 4 5 7 7 8 axtgsegcon ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝑃 ( 𝐶 ∈ ( 𝐴 𝐼 𝑥 ) ∧ ( 𝐶 − 𝑥 ) = ( 𝐶 − 𝐷 ) ) )
29 27 28 r19.29a ⊢ ( 𝜑 → 𝐶 ∈ ( 𝐴 𝐼 𝐷 ) )