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 eleq1 ⊢ ( 𝑦 = 𝑧 → ( 𝑦 ∈ ( 𝐶 𝐼 𝐷 ) ↔ 𝑧 ∈ ( 𝐶 𝐼 𝐷 ) ) )
44 oveq2 ⊢ ( 𝑦 = 𝑧 → ( 𝐶 − 𝑦 ) = ( 𝐶 − 𝑧 ) )
45 44 eqeq2d ⊢ ( 𝑦 = 𝑧 → ( ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑦 ) ↔ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑧 ) ) )
46 43 45 anbi12d ⊢ ( 𝑦 = 𝑧 → ( ( 𝑦 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑦 ) ) ↔ ( 𝑧 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑧 ) ) ) )
47 46 cbvrexvw ⊢ ( ∃ 𝑦 ∈ 𝑃 ( 𝑦 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑦 ) ) ↔ ∃ 𝑧 ∈ 𝑃 ( 𝑧 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑧 ) ) )
48 47 bilani ⊢ ( ( 𝜑 ∧ ∃ 𝑦 ∈ 𝑃 ( 𝑦 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑦 ) ) ) → ∃ 𝑧 ∈ 𝑃 ( 𝑧 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑧 ) ) )
49 42 48 r19.29a ⊢ ( ( 𝜑 ∧ ∃ 𝑦 ∈ 𝑃 ( 𝑦 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑦 ) ) ) → ∃ 𝑥 ∈ 𝑃 ( 𝐵 ∈ ( 𝐴 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐶 − 𝐷 ) ) )
50 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐼 𝑧 ) ∧ ( 𝐴 − 𝑧 ) = ( 𝐶 − 𝐷 ) ) ) → 𝐺 ∈ TarskiG )
51 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐼 𝑧 ) ∧ ( 𝐴 − 𝑧 ) = ( 𝐶 − 𝐷 ) ) ) → 𝐴 ∈ 𝑃 )
52 simplr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐼 𝑧 ) ∧ ( 𝐴 − 𝑧 ) = ( 𝐶 − 𝐷 ) ) ) → 𝑧 ∈ 𝑃 )
53 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐼 𝑧 ) ∧ ( 𝐴 − 𝑧 ) = ( 𝐶 − 𝐷 ) ) ) → 𝐵 ∈ 𝑃 )
54 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐼 𝑧 ) ∧ ( 𝐴 − 𝑧 ) = ( 𝐶 − 𝐷 ) ) ) → 𝐶 ∈ 𝑃 )
55 9 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐼 𝑧 ) ∧ ( 𝐴 − 𝑧 ) = ( 𝐶 − 𝐷 ) ) ) → 𝐷 ∈ 𝑃 )
56 simprl ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐼 𝑧 ) ∧ ( 𝐴 − 𝑧 ) = ( 𝐶 − 𝐷 ) ) ) → 𝐵 ∈ ( 𝐴 𝐼 𝑧 ) )
57 1 11 3 50 51 53 52 56 btwncolg3 ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐼 𝑧 ) ∧ ( 𝐴 − 𝑧 ) = ( 𝐶 − 𝐷 ) ) ) → ( 𝑧 ∈ ( 𝐴 ( LineG ‘ 𝐺 ) 𝐵 ) ∨ 𝐴 = 𝐵 ) )
58 simprr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐼 𝑧 ) ∧ ( 𝐴 − 𝑧 ) = ( 𝐶 − 𝐷 ) ) ) → ( 𝐴 − 𝑧 ) = ( 𝐶 − 𝐷 ) )
59 1 11 3 50 51 52 53 16 54 55 2 57 58 lnext ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐼 𝑧 ) ∧ ( 𝐴 − 𝑧 ) = ( 𝐶 − 𝐷 ) ) ) → ∃ 𝑦 ∈ 𝑃 ⟨“ 𝐴 𝑧 𝐵 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐶 𝐷 𝑦 ”⟩ )
60 50 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐼 𝑧 ) ∧ ( 𝐴 − 𝑧 ) = ( 𝐶 − 𝐷 ) ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝑧 𝐵 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐶 𝐷 𝑦 ”⟩ ) → 𝐺 ∈ TarskiG )
61 51 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐼 𝑧 ) ∧ ( 𝐴 − 𝑧 ) = ( 𝐶 − 𝐷 ) ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝑧 𝐵 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐶 𝐷 𝑦 ”⟩ ) → 𝐴 ∈ 𝑃 )
62 53 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐼 𝑧 ) ∧ ( 𝐴 − 𝑧 ) = ( 𝐶 − 𝐷 ) ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝑧 𝐵 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐶 𝐷 𝑦 ”⟩ ) → 𝐵 ∈ 𝑃 )
63 52 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐼 𝑧 ) ∧ ( 𝐴 − 𝑧 ) = ( 𝐶 − 𝐷 ) ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝑧 𝐵 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐶 𝐷 𝑦 ”⟩ ) → 𝑧 ∈ 𝑃 )
64 54 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐼 𝑧 ) ∧ ( 𝐴 − 𝑧 ) = ( 𝐶 − 𝐷 ) ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝑧 𝐵 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐶 𝐷 𝑦 ”⟩ ) → 𝐶 ∈ 𝑃 )
65 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐼 𝑧 ) ∧ ( 𝐴 − 𝑧 ) = ( 𝐶 − 𝐷 ) ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝑧 𝐵 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐶 𝐷 𝑦 ”⟩ ) → 𝑦 ∈ 𝑃 )
66 55 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐼 𝑧 ) ∧ ( 𝐴 − 𝑧 ) = ( 𝐶 − 𝐷 ) ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝑧 𝐵 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐶 𝐷 𝑦 ”⟩ ) → 𝐷 ∈ 𝑃 )
67 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐼 𝑧 ) ∧ ( 𝐴 − 𝑧 ) = ( 𝐶 − 𝐷 ) ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝑧 𝐵 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐶 𝐷 𝑦 ”⟩ ) → ⟨“ 𝐴 𝑧 𝐵 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐶 𝐷 𝑦 ”⟩ )
68 1 2 3 16 60 61 63 62 64 66 65 67 cgr3swap23 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐼 𝑧 ) ∧ ( 𝐴 − 𝑧 ) = ( 𝐶 − 𝐷 ) ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝑧 𝐵 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐶 𝐷 𝑦 ”⟩ ) → ⟨“ 𝐴 𝐵 𝑧 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐶 𝑦 𝐷 ”⟩ )
69 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐼 𝑧 ) ∧ ( 𝐴 − 𝑧 ) = ( 𝐶 − 𝐷 ) ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝑧 𝐵 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐶 𝐷 𝑦 ”⟩ ) → ( 𝐵 ∈ ( 𝐴 𝐼 𝑧 ) ∧ ( 𝐴 − 𝑧 ) = ( 𝐶 − 𝐷 ) ) )
70 69 simpld ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐼 𝑧 ) ∧ ( 𝐴 − 𝑧 ) = ( 𝐶 − 𝐷 ) ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝑧 𝐵 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐶 𝐷 𝑦 ”⟩ ) → 𝐵 ∈ ( 𝐴 𝐼 𝑧 ) )
71 1 2 3 16 60 61 62 63 64 65 66 68 70 tgbtwnxfr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐼 𝑧 ) ∧ ( 𝐴 − 𝑧 ) = ( 𝐶 − 𝐷 ) ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝑧 𝐵 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐶 𝐷 𝑦 ”⟩ ) → 𝑦 ∈ ( 𝐶 𝐼 𝐷 ) )
72 1 2 3 16 60 61 63 62 64 66 65 67 cgr3simp3 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐼 𝑧 ) ∧ ( 𝐴 − 𝑧 ) = ( 𝐶 − 𝐷 ) ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝑧 𝐵 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐶 𝐷 𝑦 ”⟩ ) → ( 𝐵 − 𝐴 ) = ( 𝑦 − 𝐶 ) )
73 1 2 3 60 62 61 65 64 72 tgcgrcomlr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐼 𝑧 ) ∧ ( 𝐴 − 𝑧 ) = ( 𝐶 − 𝐷 ) ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝑧 𝐵 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐶 𝐷 𝑦 ”⟩ ) → ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑦 ) )
74 71 73 jca ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐼 𝑧 ) ∧ ( 𝐴 − 𝑧 ) = ( 𝐶 − 𝐷 ) ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝑧 𝐵 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐶 𝐷 𝑦 ”⟩ ) → ( 𝑦 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑦 ) ) )
75 74 ex ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐼 𝑧 ) ∧ ( 𝐴 − 𝑧 ) = ( 𝐶 − 𝐷 ) ) ) ∧ 𝑦 ∈ 𝑃 ) → ( ⟨“ 𝐴 𝑧 𝐵 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐶 𝐷 𝑦 ”⟩ → ( 𝑦 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑦 ) ) ) )
76 75 reximdva ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐼 𝑧 ) ∧ ( 𝐴 − 𝑧 ) = ( 𝐶 − 𝐷 ) ) ) → ( ∃ 𝑦 ∈ 𝑃 ⟨“ 𝐴 𝑧 𝐵 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐶 𝐷 𝑦 ”⟩ → ∃ 𝑦 ∈ 𝑃 ( 𝑦 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑦 ) ) ) )
77 59 76 mpd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐼 𝑧 ) ∧ ( 𝐴 − 𝑧 ) = ( 𝐶 − 𝐷 ) ) ) → ∃ 𝑦 ∈ 𝑃 ( 𝑦 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑦 ) ) )
78 77 adantllr ⊢ ( ( ( ( 𝜑 ∧ ∃ 𝑥 ∈ 𝑃 ( 𝐵 ∈ ( 𝐴 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐶 − 𝐷 ) ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐼 𝑧 ) ∧ ( 𝐴 − 𝑧 ) = ( 𝐶 − 𝐷 ) ) ) → ∃ 𝑦 ∈ 𝑃 ( 𝑦 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑦 ) ) )
79 oveq2 ⊢ ( 𝑥 = 𝑧 → ( 𝐴 𝐼 𝑥 ) = ( 𝐴 𝐼 𝑧 ) )
80 79 eleq2d ⊢ ( 𝑥 = 𝑧 → ( 𝐵 ∈ ( 𝐴 𝐼 𝑥 ) ↔ 𝐵 ∈ ( 𝐴 𝐼 𝑧 ) ) )
81 oveq2 ⊢ ( 𝑥 = 𝑧 → ( 𝐴 − 𝑥 ) = ( 𝐴 − 𝑧 ) )
82 81 eqeq1d ⊢ ( 𝑥 = 𝑧 → ( ( 𝐴 − 𝑥 ) = ( 𝐶 − 𝐷 ) ↔ ( 𝐴 − 𝑧 ) = ( 𝐶 − 𝐷 ) ) )
83 80 82 anbi12d ⊢ ( 𝑥 = 𝑧 → ( ( 𝐵 ∈ ( 𝐴 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐶 − 𝐷 ) ) ↔ ( 𝐵 ∈ ( 𝐴 𝐼 𝑧 ) ∧ ( 𝐴 − 𝑧 ) = ( 𝐶 − 𝐷 ) ) ) )
84 83 cbvrexvw ⊢ ( ∃ 𝑥 ∈ 𝑃 ( 𝐵 ∈ ( 𝐴 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐶 − 𝐷 ) ) ↔ ∃ 𝑧 ∈ 𝑃 ( 𝐵 ∈ ( 𝐴 𝐼 𝑧 ) ∧ ( 𝐴 − 𝑧 ) = ( 𝐶 − 𝐷 ) ) )
85 84 bilani ⊢ ( ( 𝜑 ∧ ∃ 𝑥 ∈ 𝑃 ( 𝐵 ∈ ( 𝐴 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐶 − 𝐷 ) ) ) → ∃ 𝑧 ∈ 𝑃 ( 𝐵 ∈ ( 𝐴 𝐼 𝑧 ) ∧ ( 𝐴 − 𝑧 ) = ( 𝐶 − 𝐷 ) ) )
86 78 85 r19.29a ⊢ ( ( 𝜑 ∧ ∃ 𝑥 ∈ 𝑃 ( 𝐵 ∈ ( 𝐴 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐶 − 𝐷 ) ) ) → ∃ 𝑦 ∈ 𝑃 ( 𝑦 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑦 ) ) )
87 49 86 impbida ⊢ ( 𝜑 → ( ∃ 𝑦 ∈ 𝑃 ( 𝑦 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑦 ) ) ↔ ∃ 𝑥 ∈ 𝑃 ( 𝐵 ∈ ( 𝐴 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐶 − 𝐷 ) ) ) )
88 10 87 bitrd ⊢ ( 𝜑 → ( ( 𝐴 − 𝐵 ) ≤ ( 𝐶 − 𝐷 ) ↔ ∃ 𝑥 ∈ 𝑃 ( 𝐵 ∈ ( 𝐴 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐶 − 𝐷 ) ) ) )