Metamath Proof Explorer

Theorem legov2

Description: An equivalent definition of the less-than relationship. Definition 5.5 of Schwabhauser p. 41. (Contributed by Thierry Arnoux, 21-Jun-2019)

Ref Expression
Hypotheses legval.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
legval.d ⊢ − = ( dist ‘ 𝐺 )
legval.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
legval.l ⊢ ≤ = ( ≤G ‘ 𝐺 )
legval.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
legov.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
legov.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
legov.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
legov.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
Assertion legov2 ( 𝜑 → ( ( 𝐴 − 𝐵 ) ≤ ( 𝐶 − 𝐷 ) ↔ ∃ 𝑥 ∈ 𝑃 ( 𝐵 ∈ ( 𝐴 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐶 − 𝐷 ) ) ) )

Proof

Step Hyp Ref Expression
1 legval.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 legval.d ⊢ − = ( dist ‘ 𝐺 )
3 legval.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
4 legval.l ⊢ ≤ = ( ≤G ‘ 𝐺 )
5 legval.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
6 legov.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
7 legov.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
8 legov.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
9 legov.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
10 1 2 3 4 5 6 7 8 9 legov ⊢ ( 𝜑 → ( ( 𝐴 − 𝐵 ) ≤ ( 𝐶 − 𝐷 ) ↔ ∃ 𝑦 ∈ 𝑃 ( 𝑦 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑦 ) ) ) )
11 eqid ⊢ ( LineG ‘ 𝐺 ) = ( LineG ‘ 𝐺 )
12 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑧 ) ) ) → 𝐺 ∈ TarskiG )
13 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑧 ) ) ) → 𝐶 ∈ 𝑃 )
14 simplr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑧 ) ) ) → 𝑧 ∈ 𝑃 )
15 9 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑧 ) ) ) → 𝐷 ∈ 𝑃 )
16 eqid ⊢ ( cgrG ‘ 𝐺 ) = ( cgrG ‘ 𝐺 )
17 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑧 ) ) ) → 𝐴 ∈ 𝑃 )
18 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑧 ) ) ) → 𝐵 ∈ 𝑃 )
19 simprl ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑧 ) ) ) → 𝑧 ∈ ( 𝐶 𝐼 𝐷 ) )
20 1 11 3 12 13 15 14 19 btwncolg1 ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑧 ) ) ) → ( 𝑧 ∈ ( 𝐶 ( LineG ‘ 𝐺 ) 𝐷 ) ∨ 𝐶 = 𝐷 ) )
21 simprr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑧 ) ) ) → ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑧 ) )
22 21 eqcomd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑧 ) ) ) → ( 𝐶 − 𝑧 ) = ( 𝐴 − 𝐵 ) )
23 1 11 3 12 13 14 15 16 17 18 2 20 22 lnext ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑧 ) ) ) → ∃ 𝑥 ∈ 𝑃 ⟨“ 𝐶 𝑧 𝐷 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝐵 𝑥 ”⟩ )
24 12 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑧 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ⟨“ 𝐶 𝑧 𝐷 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝐵 𝑥 ”⟩ ) → 𝐺 ∈ TarskiG )
25 13 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑧 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ⟨“ 𝐶 𝑧 𝐷 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝐵 𝑥 ”⟩ ) → 𝐶 ∈ 𝑃 )
26 14 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑧 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ⟨“ 𝐶 𝑧 𝐷 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝐵 𝑥 ”⟩ ) → 𝑧 ∈ 𝑃 )
27 15 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑧 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ⟨“ 𝐶 𝑧 𝐷 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝐵 𝑥 ”⟩ ) → 𝐷 ∈ 𝑃 )
28 17 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑧 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ⟨“ 𝐶 𝑧 𝐷 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝐵 𝑥 ”⟩ ) → 𝐴 ∈ 𝑃 )
29 18 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑧 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ⟨“ 𝐶 𝑧 𝐷 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝐵 𝑥 ”⟩ ) → 𝐵 ∈ 𝑃 )
30 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑧 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ⟨“ 𝐶 𝑧 𝐷 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝐵 𝑥 ”⟩ ) → 𝑥 ∈ 𝑃 )
31 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑧 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ⟨“ 𝐶 𝑧 𝐷 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝐵 𝑥 ”⟩ ) → ⟨“ 𝐶 𝑧 𝐷 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝐵 𝑥 ”⟩ )
32 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑧 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ⟨“ 𝐶 𝑧 𝐷 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝐵 𝑥 ”⟩ ) → ( 𝑧 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑧 ) ) )
33 32 simpld ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑧 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ⟨“ 𝐶 𝑧 𝐷 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝐵 𝑥 ”⟩ ) → 𝑧 ∈ ( 𝐶 𝐼 𝐷 ) )
34 1 2 3 16 24 25 26 27 28 29 30 31 33 tgbtwnxfr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑧 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ⟨“ 𝐶 𝑧 𝐷 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝐵 𝑥 ”⟩ ) → 𝐵 ∈ ( 𝐴 𝐼 𝑥 ) )
35 1 2 3 16 24 25 26 27 28 29 30 31 trgcgrcom ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑧 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ⟨“ 𝐶 𝑧 𝐷 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝐵 𝑥 ”⟩ ) → ⟨“ 𝐴 𝐵 𝑥 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐶 𝑧 𝐷 ”⟩ )
36 1 2 3 16 24 28 29 30 25 26 27 35 cgr3simp3 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑧 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ⟨“ 𝐶 𝑧 𝐷 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝐵 𝑥 ”⟩ ) → ( 𝑥 − 𝐴 ) = ( 𝐷 − 𝐶 ) )
37 1 2 3 24 30 28 27 25 36 tgcgrcomlr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑧 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ⟨“ 𝐶 𝑧 𝐷 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝐵 𝑥 ”⟩ ) → ( 𝐴 − 𝑥 ) = ( 𝐶 − 𝐷 ) )
38 34 37 jca ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑧 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ⟨“ 𝐶 𝑧 𝐷 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝐵 𝑥 ”⟩ ) → ( 𝐵 ∈ ( 𝐴 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐶 − 𝐷 ) ) )
39 38 ex ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑧 ) ) ) ∧ 𝑥 ∈ 𝑃 ) → ( ⟨“ 𝐶 𝑧 𝐷 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝐵 𝑥 ”⟩ → ( 𝐵 ∈ ( 𝐴 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐶 − 𝐷 ) ) ) )
40 39 reximdva ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑧 ) ) ) → ( ∃ 𝑥 ∈ 𝑃 ⟨“ 𝐶 𝑧 𝐷 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝐵 𝑥 ”⟩ → ∃ 𝑥 ∈ 𝑃 ( 𝐵 ∈ ( 𝐴 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐶 − 𝐷 ) ) ) )
41 23 40 mpd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑧 ) ) ) → ∃ 𝑥 ∈ 𝑃 ( 𝐵 ∈ ( 𝐴 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐶 − 𝐷 ) ) )
42 41 adantllr ⊢ ( ( ( ( 𝜑 ∧ ∃ 𝑦 ∈ 𝑃 ( 𝑦 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑦 ) ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑧 ) ) ) → ∃ 𝑥 ∈ 𝑃 ( 𝐵 ∈ ( 𝐴 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐶 − 𝐷 ) ) )
43 simpr ⊢ ( ( 𝜑 ∧ ∃ 𝑦 ∈ 𝑃 ( 𝑦 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑦 ) ) ) → ∃ 𝑦 ∈ 𝑃 ( 𝑦 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑦 ) ) )
44 eleq1 ⊢ ( 𝑦 = 𝑧 → ( 𝑦 ∈ ( 𝐶 𝐼 𝐷 ) ↔ 𝑧 ∈ ( 𝐶 𝐼 𝐷 ) ) )
45 oveq2 ⊢ ( 𝑦 = 𝑧 → ( 𝐶 − 𝑦 ) = ( 𝐶 − 𝑧 ) )
46 45 eqeq2d ⊢ ( 𝑦 = 𝑧 → ( ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑦 ) ↔ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑧 ) ) )
47 44 46 anbi12d ⊢ ( 𝑦 = 𝑧 → ( ( 𝑦 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑦 ) ) ↔ ( 𝑧 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑧 ) ) ) )
48 47 cbvrexvw ⊢ ( ∃ 𝑦 ∈ 𝑃 ( 𝑦 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑦 ) ) ↔ ∃ 𝑧 ∈ 𝑃 ( 𝑧 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑧 ) ) )
49 43 48 sylib ⊢ ( ( 𝜑 ∧ ∃ 𝑦 ∈ 𝑃 ( 𝑦 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑦 ) ) ) → ∃ 𝑧 ∈ 𝑃 ( 𝑧 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑧 ) ) )
50 42 49 r19.29a ⊢ ( ( 𝜑 ∧ ∃ 𝑦 ∈ 𝑃 ( 𝑦 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑦 ) ) ) → ∃ 𝑥 ∈ 𝑃 ( 𝐵 ∈ ( 𝐴 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐶 − 𝐷 ) ) )
51 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐼 𝑧 ) ∧ ( 𝐴 − 𝑧 ) = ( 𝐶 − 𝐷 ) ) ) → 𝐺 ∈ TarskiG )
52 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐼 𝑧 ) ∧ ( 𝐴 − 𝑧 ) = ( 𝐶 − 𝐷 ) ) ) → 𝐴 ∈ 𝑃 )
53 simplr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐼 𝑧 ) ∧ ( 𝐴 − 𝑧 ) = ( 𝐶 − 𝐷 ) ) ) → 𝑧 ∈ 𝑃 )
54 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐼 𝑧 ) ∧ ( 𝐴 − 𝑧 ) = ( 𝐶 − 𝐷 ) ) ) → 𝐵 ∈ 𝑃 )
55 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐼 𝑧 ) ∧ ( 𝐴 − 𝑧 ) = ( 𝐶 − 𝐷 ) ) ) → 𝐶 ∈ 𝑃 )
56 9 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐼 𝑧 ) ∧ ( 𝐴 − 𝑧 ) = ( 𝐶 − 𝐷 ) ) ) → 𝐷 ∈ 𝑃 )
57 simprl ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐼 𝑧 ) ∧ ( 𝐴 − 𝑧 ) = ( 𝐶 − 𝐷 ) ) ) → 𝐵 ∈ ( 𝐴 𝐼 𝑧 ) )
58 1 11 3 51 52 54 53 57 btwncolg3 ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐼 𝑧 ) ∧ ( 𝐴 − 𝑧 ) = ( 𝐶 − 𝐷 ) ) ) → ( 𝑧 ∈ ( 𝐴 ( LineG ‘ 𝐺 ) 𝐵 ) ∨ 𝐴 = 𝐵 ) )
59 simprr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐼 𝑧 ) ∧ ( 𝐴 − 𝑧 ) = ( 𝐶 − 𝐷 ) ) ) → ( 𝐴 − 𝑧 ) = ( 𝐶 − 𝐷 ) )
60 1 11 3 51 52 53 54 16 55 56 2 58 59 lnext ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐼 𝑧 ) ∧ ( 𝐴 − 𝑧 ) = ( 𝐶 − 𝐷 ) ) ) → ∃ 𝑦 ∈ 𝑃 ⟨“ 𝐴 𝑧 𝐵 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐶 𝐷 𝑦 ”⟩ )
61 51 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐼 𝑧 ) ∧ ( 𝐴 − 𝑧 ) = ( 𝐶 − 𝐷 ) ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝑧 𝐵 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐶 𝐷 𝑦 ”⟩ ) → 𝐺 ∈ TarskiG )
62 52 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐼 𝑧 ) ∧ ( 𝐴 − 𝑧 ) = ( 𝐶 − 𝐷 ) ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝑧 𝐵 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐶 𝐷 𝑦 ”⟩ ) → 𝐴 ∈ 𝑃 )
63 54 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐼 𝑧 ) ∧ ( 𝐴 − 𝑧 ) = ( 𝐶 − 𝐷 ) ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝑧 𝐵 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐶 𝐷 𝑦 ”⟩ ) → 𝐵 ∈ 𝑃 )
64 53 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐼 𝑧 ) ∧ ( 𝐴 − 𝑧 ) = ( 𝐶 − 𝐷 ) ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝑧 𝐵 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐶 𝐷 𝑦 ”⟩ ) → 𝑧 ∈ 𝑃 )
65 55 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐼 𝑧 ) ∧ ( 𝐴 − 𝑧 ) = ( 𝐶 − 𝐷 ) ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝑧 𝐵 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐶 𝐷 𝑦 ”⟩ ) → 𝐶 ∈ 𝑃 )
66 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐼 𝑧 ) ∧ ( 𝐴 − 𝑧 ) = ( 𝐶 − 𝐷 ) ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝑧 𝐵 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐶 𝐷 𝑦 ”⟩ ) → 𝑦 ∈ 𝑃 )
67 56 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐼 𝑧 ) ∧ ( 𝐴 − 𝑧 ) = ( 𝐶 − 𝐷 ) ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝑧 𝐵 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐶 𝐷 𝑦 ”⟩ ) → 𝐷 ∈ 𝑃 )
68 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐼 𝑧 ) ∧ ( 𝐴 − 𝑧 ) = ( 𝐶 − 𝐷 ) ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝑧 𝐵 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐶 𝐷 𝑦 ”⟩ ) → ⟨“ 𝐴 𝑧 𝐵 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐶 𝐷 𝑦 ”⟩ )
69 1 2 3 16 61 62 64 63 65 67 66 68 cgr3swap23 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐼 𝑧 ) ∧ ( 𝐴 − 𝑧 ) = ( 𝐶 − 𝐷 ) ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝑧 𝐵 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐶 𝐷 𝑦 ”⟩ ) → ⟨“ 𝐴 𝐵 𝑧 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐶 𝑦 𝐷 ”⟩ )
70 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐼 𝑧 ) ∧ ( 𝐴 − 𝑧 ) = ( 𝐶 − 𝐷 ) ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝑧 𝐵 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐶 𝐷 𝑦 ”⟩ ) → ( 𝐵 ∈ ( 𝐴 𝐼 𝑧 ) ∧ ( 𝐴 − 𝑧 ) = ( 𝐶 − 𝐷 ) ) )
71 70 simpld ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐼 𝑧 ) ∧ ( 𝐴 − 𝑧 ) = ( 𝐶 − 𝐷 ) ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝑧 𝐵 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐶 𝐷 𝑦 ”⟩ ) → 𝐵 ∈ ( 𝐴 𝐼 𝑧 ) )
72 1 2 3 16 61 62 63 64 65 66 67 69 71 tgbtwnxfr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐼 𝑧 ) ∧ ( 𝐴 − 𝑧 ) = ( 𝐶 − 𝐷 ) ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝑧 𝐵 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐶 𝐷 𝑦 ”⟩ ) → 𝑦 ∈ ( 𝐶 𝐼 𝐷 ) )
73 1 2 3 16 61 62 64 63 65 67 66 68 cgr3simp3 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐼 𝑧 ) ∧ ( 𝐴 − 𝑧 ) = ( 𝐶 − 𝐷 ) ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝑧 𝐵 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐶 𝐷 𝑦 ”⟩ ) → ( 𝐵 − 𝐴 ) = ( 𝑦 − 𝐶 ) )
74 1 2 3 61 63 62 66 65 73 tgcgrcomlr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐼 𝑧 ) ∧ ( 𝐴 − 𝑧 ) = ( 𝐶 − 𝐷 ) ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝑧 𝐵 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐶 𝐷 𝑦 ”⟩ ) → ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑦 ) )
75 72 74 jca ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐼 𝑧 ) ∧ ( 𝐴 − 𝑧 ) = ( 𝐶 − 𝐷 ) ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝑧 𝐵 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐶 𝐷 𝑦 ”⟩ ) → ( 𝑦 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑦 ) ) )
76 75 ex ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐼 𝑧 ) ∧ ( 𝐴 − 𝑧 ) = ( 𝐶 − 𝐷 ) ) ) ∧ 𝑦 ∈ 𝑃 ) → ( ⟨“ 𝐴 𝑧 𝐵 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐶 𝐷 𝑦 ”⟩ → ( 𝑦 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑦 ) ) ) )
77 76 reximdva ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐼 𝑧 ) ∧ ( 𝐴 − 𝑧 ) = ( 𝐶 − 𝐷 ) ) ) → ( ∃ 𝑦 ∈ 𝑃 ⟨“ 𝐴 𝑧 𝐵 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐶 𝐷 𝑦 ”⟩ → ∃ 𝑦 ∈ 𝑃 ( 𝑦 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑦 ) ) ) )
78 60 77 mpd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐼 𝑧 ) ∧ ( 𝐴 − 𝑧 ) = ( 𝐶 − 𝐷 ) ) ) → ∃ 𝑦 ∈ 𝑃 ( 𝑦 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑦 ) ) )
79 78 adantllr ⊢ ( ( ( ( 𝜑 ∧ ∃ 𝑥 ∈ 𝑃 ( 𝐵 ∈ ( 𝐴 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐶 − 𝐷 ) ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐼 𝑧 ) ∧ ( 𝐴 − 𝑧 ) = ( 𝐶 − 𝐷 ) ) ) → ∃ 𝑦 ∈ 𝑃 ( 𝑦 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑦 ) ) )
80 simpr ⊢ ( ( 𝜑 ∧ ∃ 𝑥 ∈ 𝑃 ( 𝐵 ∈ ( 𝐴 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐶 − 𝐷 ) ) ) → ∃ 𝑥 ∈ 𝑃 ( 𝐵 ∈ ( 𝐴 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐶 − 𝐷 ) ) )
81 oveq2 ⊢ ( 𝑥 = 𝑧 → ( 𝐴 𝐼 𝑥 ) = ( 𝐴 𝐼 𝑧 ) )
82 81 eleq2d ⊢ ( 𝑥 = 𝑧 → ( 𝐵 ∈ ( 𝐴 𝐼 𝑥 ) ↔ 𝐵 ∈ ( 𝐴 𝐼 𝑧 ) ) )
83 oveq2 ⊢ ( 𝑥 = 𝑧 → ( 𝐴 − 𝑥 ) = ( 𝐴 − 𝑧 ) )
84 83 eqeq1d ⊢ ( 𝑥 = 𝑧 → ( ( 𝐴 − 𝑥 ) = ( 𝐶 − 𝐷 ) ↔ ( 𝐴 − 𝑧 ) = ( 𝐶 − 𝐷 ) ) )
85 82 84 anbi12d ⊢ ( 𝑥 = 𝑧 → ( ( 𝐵 ∈ ( 𝐴 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐶 − 𝐷 ) ) ↔ ( 𝐵 ∈ ( 𝐴 𝐼 𝑧 ) ∧ ( 𝐴 − 𝑧 ) = ( 𝐶 − 𝐷 ) ) ) )
86 85 cbvrexvw ⊢ ( ∃ 𝑥 ∈ 𝑃 ( 𝐵 ∈ ( 𝐴 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐶 − 𝐷 ) ) ↔ ∃ 𝑧 ∈ 𝑃 ( 𝐵 ∈ ( 𝐴 𝐼 𝑧 ) ∧ ( 𝐴 − 𝑧 ) = ( 𝐶 − 𝐷 ) ) )
87 80 86 sylib ⊢ ( ( 𝜑 ∧ ∃ 𝑥 ∈ 𝑃 ( 𝐵 ∈ ( 𝐴 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐶 − 𝐷 ) ) ) → ∃ 𝑧 ∈ 𝑃 ( 𝐵 ∈ ( 𝐴 𝐼 𝑧 ) ∧ ( 𝐴 − 𝑧 ) = ( 𝐶 − 𝐷 ) ) )
88 79 87 r19.29a ⊢ ( ( 𝜑 ∧ ∃ 𝑥 ∈ 𝑃 ( 𝐵 ∈ ( 𝐴 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐶 − 𝐷 ) ) ) → ∃ 𝑦 ∈ 𝑃 ( 𝑦 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑦 ) ) )
89 50 88 impbida ⊢ ( 𝜑 → ( ∃ 𝑦 ∈ 𝑃 ( 𝑦 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑦 ) ) ↔ ∃ 𝑥 ∈ 𝑃 ( 𝐵 ∈ ( 𝐴 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐶 − 𝐷 ) ) ) )
90 10 89 bitrd ⊢ ( 𝜑 → ( ( 𝐴 − 𝐵 ) ≤ ( 𝐶 − 𝐷 ) ↔ ∃ 𝑥 ∈ 𝑃 ( 𝐵 ∈ ( 𝐴 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐶 − 𝐷 ) ) ) )