Metamath Proof Explorer

Theorem legov

Description: Value of the less-than relationship. Definition 5.4 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 legov ( 𝜑 → ( ( 𝐴 − 𝐵 ) ≤ ( 𝐶 − 𝐷 ) ↔ ∃ 𝑧 ∈ 𝑃 ( 𝑧 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑧 ) ) ) )

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 legval ⊢ ( 𝜑 → ≤ = { ⟨ 𝑒 , 𝑓 ⟩ ∣ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( 𝑓 = ( 𝑥 − 𝑦 ) ∧ ∃ 𝑧 ∈ 𝑃 ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∧ 𝑒 = ( 𝑥 − 𝑧 ) ) ) } )
11 10 breqd ⊢ ( 𝜑 → ( ( 𝐴 − 𝐵 ) ≤ ( 𝐶 − 𝐷 ) ↔ ( 𝐴 − 𝐵 ) { ⟨ 𝑒 , 𝑓 ⟩ ∣ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( 𝑓 = ( 𝑥 − 𝑦 ) ∧ ∃ 𝑧 ∈ 𝑃 ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∧ 𝑒 = ( 𝑥 − 𝑧 ) ) ) } ( 𝐶 − 𝐷 ) ) )
12 ovex ⊢ ( 𝐴 − 𝐵 ) ∈ V
13 ovex ⊢ ( 𝐶 − 𝐷 ) ∈ V
14 simpr ⊢ ( ( 𝑒 = ( 𝐴 − 𝐵 ) ∧ 𝑓 = ( 𝐶 − 𝐷 ) ) → 𝑓 = ( 𝐶 − 𝐷 ) )
15 14 eqeq1d ⊢ ( ( 𝑒 = ( 𝐴 − 𝐵 ) ∧ 𝑓 = ( 𝐶 − 𝐷 ) ) → ( 𝑓 = ( 𝑥 − 𝑦 ) ↔ ( 𝐶 − 𝐷 ) = ( 𝑥 − 𝑦 ) ) )
16 simpl ⊢ ( ( 𝑒 = ( 𝐴 − 𝐵 ) ∧ 𝑓 = ( 𝐶 − 𝐷 ) ) → 𝑒 = ( 𝐴 − 𝐵 ) )
17 16 eqeq1d ⊢ ( ( 𝑒 = ( 𝐴 − 𝐵 ) ∧ 𝑓 = ( 𝐶 − 𝐷 ) ) → ( 𝑒 = ( 𝑥 − 𝑧 ) ↔ ( 𝐴 − 𝐵 ) = ( 𝑥 − 𝑧 ) ) )
18 17 anbi2d ⊢ ( ( 𝑒 = ( 𝐴 − 𝐵 ) ∧ 𝑓 = ( 𝐶 − 𝐷 ) ) → ( ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∧ 𝑒 = ( 𝑥 − 𝑧 ) ) ↔ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝑥 − 𝑧 ) ) ) )
19 18 rexbidv ⊢ ( ( 𝑒 = ( 𝐴 − 𝐵 ) ∧ 𝑓 = ( 𝐶 − 𝐷 ) ) → ( ∃ 𝑧 ∈ 𝑃 ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∧ 𝑒 = ( 𝑥 − 𝑧 ) ) ↔ ∃ 𝑧 ∈ 𝑃 ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝑥 − 𝑧 ) ) ) )
20 15 19 anbi12d ⊢ ( ( 𝑒 = ( 𝐴 − 𝐵 ) ∧ 𝑓 = ( 𝐶 − 𝐷 ) ) → ( ( 𝑓 = ( 𝑥 − 𝑦 ) ∧ ∃ 𝑧 ∈ 𝑃 ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∧ 𝑒 = ( 𝑥 − 𝑧 ) ) ) ↔ ( ( 𝐶 − 𝐷 ) = ( 𝑥 − 𝑦 ) ∧ ∃ 𝑧 ∈ 𝑃 ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝑥 − 𝑧 ) ) ) ) )
21 20 2rexbidv ⊢ ( ( 𝑒 = ( 𝐴 − 𝐵 ) ∧ 𝑓 = ( 𝐶 − 𝐷 ) ) → ( ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( 𝑓 = ( 𝑥 − 𝑦 ) ∧ ∃ 𝑧 ∈ 𝑃 ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∧ 𝑒 = ( 𝑥 − 𝑧 ) ) ) ↔ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( ( 𝐶 − 𝐷 ) = ( 𝑥 − 𝑦 ) ∧ ∃ 𝑧 ∈ 𝑃 ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝑥 − 𝑧 ) ) ) ) )
22 eqid ⊢ { ⟨ 𝑒 , 𝑓 ⟩ ∣ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( 𝑓 = ( 𝑥 − 𝑦 ) ∧ ∃ 𝑧 ∈ 𝑃 ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∧ 𝑒 = ( 𝑥 − 𝑧 ) ) ) } = { ⟨ 𝑒 , 𝑓 ⟩ ∣ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( 𝑓 = ( 𝑥 − 𝑦 ) ∧ ∃ 𝑧 ∈ 𝑃 ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∧ 𝑒 = ( 𝑥 − 𝑧 ) ) ) }
23 12 13 21 22 braba ⊢ ( ( 𝐴 − 𝐵 ) { ⟨ 𝑒 , 𝑓 ⟩ ∣ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( 𝑓 = ( 𝑥 − 𝑦 ) ∧ ∃ 𝑧 ∈ 𝑃 ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∧ 𝑒 = ( 𝑥 − 𝑧 ) ) ) } ( 𝐶 − 𝐷 ) ↔ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( ( 𝐶 − 𝐷 ) = ( 𝑥 − 𝑦 ) ∧ ∃ 𝑧 ∈ 𝑃 ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝑥 − 𝑧 ) ) ) )
24 11 23 bitrdi ⊢ ( 𝜑 → ( ( 𝐴 − 𝐵 ) ≤ ( 𝐶 − 𝐷 ) ↔ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( ( 𝐶 − 𝐷 ) = ( 𝑥 − 𝑦 ) ∧ ∃ 𝑧 ∈ 𝑃 ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝑥 − 𝑧 ) ) ) ) )
25 anass ⊢ ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐶 − 𝐷 ) = ( 𝑐 − 𝑑 ) ) ∧ ∃ 𝑧 ∈ 𝑃 ( 𝑧 ∈ ( 𝑐 𝐼 𝑑 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝑐 − 𝑧 ) ) ) ↔ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( ( 𝐶 − 𝐷 ) = ( 𝑐 − 𝑑 ) ∧ ∃ 𝑧 ∈ 𝑃 ( 𝑧 ∈ ( 𝑐 𝐼 𝑑 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝑐 − 𝑧 ) ) ) ) )
26 25 anbi1i ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐶 − 𝐷 ) = ( 𝑐 − 𝑑 ) ) ∧ ∃ 𝑧 ∈ 𝑃 ( 𝑧 ∈ ( 𝑐 𝐼 𝑑 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝑐 − 𝑧 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ↔ ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( ( 𝐶 − 𝐷 ) = ( 𝑐 − 𝑑 ) ∧ ∃ 𝑧 ∈ 𝑃 ( 𝑧 ∈ ( 𝑐 𝐼 𝑑 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝑐 − 𝑧 ) ) ) ) ∧ 𝑥 ∈ 𝑃 ) )
27 eqid ⊢ ( cgrG ‘ 𝐺 ) = ( cgrG ‘ 𝐺 )
28 5 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐶 − 𝐷 ) = ( 𝑐 − 𝑑 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝑐 𝐼 𝑑 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝑐 − 𝑥 ) ) ) → 𝐺 ∈ TarskiG )
29 28 adantr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐶 − 𝐷 ) = ( 𝑐 − 𝑑 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝑐 𝐼 𝑑 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝑐 − 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝑃 ∧ ⟨“ 𝑐 𝑑 𝑥 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐶 𝐷 𝑧 ”⟩ ) ) → 𝐺 ∈ TarskiG )
30 simp-5r ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐶 − 𝐷 ) = ( 𝑐 − 𝑑 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝑐 𝐼 𝑑 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝑐 − 𝑥 ) ) ) → 𝑐 ∈ 𝑃 )
31 30 adantr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐶 − 𝐷 ) = ( 𝑐 − 𝑑 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝑐 𝐼 𝑑 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝑐 − 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝑃 ∧ ⟨“ 𝑐 𝑑 𝑥 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐶 𝐷 𝑧 ”⟩ ) ) → 𝑐 ∈ 𝑃 )
32 simpllr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐶 − 𝐷 ) = ( 𝑐 − 𝑑 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝑐 𝐼 𝑑 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝑐 − 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝑃 ∧ ⟨“ 𝑐 𝑑 𝑥 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐶 𝐷 𝑧 ”⟩ ) ) → 𝑥 ∈ 𝑃 )
33 simp-4r ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐶 − 𝐷 ) = ( 𝑐 − 𝑑 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝑐 𝐼 𝑑 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝑐 − 𝑥 ) ) ) → 𝑑 ∈ 𝑃 )
34 33 adantr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐶 − 𝐷 ) = ( 𝑐 − 𝑑 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝑐 𝐼 𝑑 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝑐 − 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝑃 ∧ ⟨“ 𝑐 𝑑 𝑥 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐶 𝐷 𝑧 ”⟩ ) ) → 𝑑 ∈ 𝑃 )
35 8 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐶 − 𝐷 ) = ( 𝑐 − 𝑑 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝑐 𝐼 𝑑 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝑐 − 𝑥 ) ) ) → 𝐶 ∈ 𝑃 )
36 35 adantr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐶 − 𝐷 ) = ( 𝑐 − 𝑑 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝑐 𝐼 𝑑 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝑐 − 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝑃 ∧ ⟨“ 𝑐 𝑑 𝑥 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐶 𝐷 𝑧 ”⟩ ) ) → 𝐶 ∈ 𝑃 )
37 simprl ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐶 − 𝐷 ) = ( 𝑐 − 𝑑 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝑐 𝐼 𝑑 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝑐 − 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝑃 ∧ ⟨“ 𝑐 𝑑 𝑥 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐶 𝐷 𝑧 ”⟩ ) ) → 𝑧 ∈ 𝑃 )
38 9 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐶 − 𝐷 ) = ( 𝑐 − 𝑑 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝑐 𝐼 𝑑 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝑐 − 𝑥 ) ) ) → 𝐷 ∈ 𝑃 )
39 38 adantr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐶 − 𝐷 ) = ( 𝑐 − 𝑑 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝑐 𝐼 𝑑 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝑐 − 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝑃 ∧ ⟨“ 𝑐 𝑑 𝑥 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐶 𝐷 𝑧 ”⟩ ) ) → 𝐷 ∈ 𝑃 )
40 simprr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐶 − 𝐷 ) = ( 𝑐 − 𝑑 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝑐 𝐼 𝑑 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝑐 − 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝑃 ∧ ⟨“ 𝑐 𝑑 𝑥 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐶 𝐷 𝑧 ”⟩ ) ) → ⟨“ 𝑐 𝑑 𝑥 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐶 𝐷 𝑧 ”⟩ )
41 1 2 3 27 29 31 34 32 36 39 37 40 cgr3swap23 ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐶 − 𝐷 ) = ( 𝑐 − 𝑑 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝑐 𝐼 𝑑 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝑐 − 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝑃 ∧ ⟨“ 𝑐 𝑑 𝑥 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐶 𝐷 𝑧 ”⟩ ) ) → ⟨“ 𝑐 𝑥 𝑑 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐶 𝑧 𝐷 ”⟩ )
42 simprl ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐶 − 𝐷 ) = ( 𝑐 − 𝑑 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝑐 𝐼 𝑑 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝑐 − 𝑥 ) ) ) → 𝑥 ∈ ( 𝑐 𝐼 𝑑 ) )
43 42 adantr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐶 − 𝐷 ) = ( 𝑐 − 𝑑 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝑐 𝐼 𝑑 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝑐 − 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝑃 ∧ ⟨“ 𝑐 𝑑 𝑥 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐶 𝐷 𝑧 ”⟩ ) ) → 𝑥 ∈ ( 𝑐 𝐼 𝑑 ) )
44 1 2 3 27 29 31 32 34 36 37 39 41 43 tgbtwnxfr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐶 − 𝐷 ) = ( 𝑐 − 𝑑 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝑐 𝐼 𝑑 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝑐 − 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝑃 ∧ ⟨“ 𝑐 𝑑 𝑥 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐶 𝐷 𝑧 ”⟩ ) ) → 𝑧 ∈ ( 𝐶 𝐼 𝐷 ) )
45 simplrr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐶 − 𝐷 ) = ( 𝑐 − 𝑑 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝑐 𝐼 𝑑 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝑐 − 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝑃 ∧ ⟨“ 𝑐 𝑑 𝑥 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐶 𝐷 𝑧 ”⟩ ) ) → ( 𝐴 − 𝐵 ) = ( 𝑐 − 𝑥 ) )
46 1 2 3 27 29 31 32 34 36 37 39 41 cgr3simp1 ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐶 − 𝐷 ) = ( 𝑐 − 𝑑 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝑐 𝐼 𝑑 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝑐 − 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝑃 ∧ ⟨“ 𝑐 𝑑 𝑥 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐶 𝐷 𝑧 ”⟩ ) ) → ( 𝑐 − 𝑥 ) = ( 𝐶 − 𝑧 ) )
47 45 46 eqtrd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐶 − 𝐷 ) = ( 𝑐 − 𝑑 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝑐 𝐼 𝑑 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝑐 − 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝑃 ∧ ⟨“ 𝑐 𝑑 𝑥 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐶 𝐷 𝑧 ”⟩ ) ) → ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑧 ) )
48 44 47 jca ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐶 − 𝐷 ) = ( 𝑐 − 𝑑 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝑐 𝐼 𝑑 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝑐 − 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝑃 ∧ ⟨“ 𝑐 𝑑 𝑥 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐶 𝐷 𝑧 ”⟩ ) ) → ( 𝑧 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑧 ) ) )
49 eqid ⊢ ( LineG ‘ 𝐺 ) = ( LineG ‘ 𝐺 )
50 simplr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐶 − 𝐷 ) = ( 𝑐 − 𝑑 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝑐 𝐼 𝑑 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝑐 − 𝑥 ) ) ) → 𝑥 ∈ 𝑃 )
51 1 49 3 28 30 50 33 42 btwncolg3 ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐶 − 𝐷 ) = ( 𝑐 − 𝑑 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝑐 𝐼 𝑑 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝑐 − 𝑥 ) ) ) → ( 𝑑 ∈ ( 𝑐 ( LineG ‘ 𝐺 ) 𝑥 ) ∨ 𝑐 = 𝑥 ) )
52 simpllr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐶 − 𝐷 ) = ( 𝑐 − 𝑑 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝑐 𝐼 𝑑 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝑐 − 𝑥 ) ) ) → ( 𝐶 − 𝐷 ) = ( 𝑐 − 𝑑 ) )
53 52 eqcomd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐶 − 𝐷 ) = ( 𝑐 − 𝑑 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝑐 𝐼 𝑑 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝑐 − 𝑥 ) ) ) → ( 𝑐 − 𝑑 ) = ( 𝐶 − 𝐷 ) )
54 1 49 3 28 30 33 50 27 35 38 2 51 53 lnext ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐶 − 𝐷 ) = ( 𝑐 − 𝑑 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝑐 𝐼 𝑑 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝑐 − 𝑥 ) ) ) → ∃ 𝑧 ∈ 𝑃 ⟨“ 𝑐 𝑑 𝑥 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐶 𝐷 𝑧 ”⟩ )
55 48 54 reximddv ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐶 − 𝐷 ) = ( 𝑐 − 𝑑 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝑐 𝐼 𝑑 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝑐 − 𝑥 ) ) ) → ∃ 𝑧 ∈ 𝑃 ( 𝑧 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑧 ) ) )
56 55 adantllr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐶 − 𝐷 ) = ( 𝑐 − 𝑑 ) ) ∧ ∃ 𝑧 ∈ 𝑃 ( 𝑧 ∈ ( 𝑐 𝐼 𝑑 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝑐 − 𝑧 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝑐 𝐼 𝑑 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝑐 − 𝑥 ) ) ) → ∃ 𝑧 ∈ 𝑃 ( 𝑧 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑧 ) ) )
57 26 56 sylanbr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( ( 𝐶 − 𝐷 ) = ( 𝑐 − 𝑑 ) ∧ ∃ 𝑧 ∈ 𝑃 ( 𝑧 ∈ ( 𝑐 𝐼 𝑑 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝑐 − 𝑧 ) ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝑐 𝐼 𝑑 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝑐 − 𝑥 ) ) ) → ∃ 𝑧 ∈ 𝑃 ( 𝑧 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑧 ) ) )
58 simprr ⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( ( 𝐶 − 𝐷 ) = ( 𝑐 − 𝑑 ) ∧ ∃ 𝑧 ∈ 𝑃 ( 𝑧 ∈ ( 𝑐 𝐼 𝑑 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝑐 − 𝑧 ) ) ) ) → ∃ 𝑧 ∈ 𝑃 ( 𝑧 ∈ ( 𝑐 𝐼 𝑑 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝑐 − 𝑧 ) ) )
59 eleq1w ⊢ ( 𝑥 = 𝑧 → ( 𝑥 ∈ ( 𝑐 𝐼 𝑑 ) ↔ 𝑧 ∈ ( 𝑐 𝐼 𝑑 ) ) )
60 oveq2 ⊢ ( 𝑥 = 𝑧 → ( 𝑐 − 𝑥 ) = ( 𝑐 − 𝑧 ) )
61 60 eqeq2d ⊢ ( 𝑥 = 𝑧 → ( ( 𝐴 − 𝐵 ) = ( 𝑐 − 𝑥 ) ↔ ( 𝐴 − 𝐵 ) = ( 𝑐 − 𝑧 ) ) )
62 59 61 anbi12d ⊢ ( 𝑥 = 𝑧 → ( ( 𝑥 ∈ ( 𝑐 𝐼 𝑑 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝑐 − 𝑥 ) ) ↔ ( 𝑧 ∈ ( 𝑐 𝐼 𝑑 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝑐 − 𝑧 ) ) ) )
63 62 cbvrexvw ⊢ ( ∃ 𝑥 ∈ 𝑃 ( 𝑥 ∈ ( 𝑐 𝐼 𝑑 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝑐 − 𝑥 ) ) ↔ ∃ 𝑧 ∈ 𝑃 ( 𝑧 ∈ ( 𝑐 𝐼 𝑑 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝑐 − 𝑧 ) ) )
64 58 63 sylibr ⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( ( 𝐶 − 𝐷 ) = ( 𝑐 − 𝑑 ) ∧ ∃ 𝑧 ∈ 𝑃 ( 𝑧 ∈ ( 𝑐 𝐼 𝑑 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝑐 − 𝑧 ) ) ) ) → ∃ 𝑥 ∈ 𝑃 ( 𝑥 ∈ ( 𝑐 𝐼 𝑑 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝑐 − 𝑥 ) ) )
65 57 64 r19.29a ⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( ( 𝐶 − 𝐷 ) = ( 𝑐 − 𝑑 ) ∧ ∃ 𝑧 ∈ 𝑃 ( 𝑧 ∈ ( 𝑐 𝐼 𝑑 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝑐 − 𝑧 ) ) ) ) → ∃ 𝑧 ∈ 𝑃 ( 𝑧 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑧 ) ) )
66 65 adantl3r ⊢ ( ( ( ( ( 𝜑 ∧ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( ( 𝐶 − 𝐷 ) = ( 𝑥 − 𝑦 ) ∧ ∃ 𝑧 ∈ 𝑃 ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝑥 − 𝑧 ) ) ) ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( ( 𝐶 − 𝐷 ) = ( 𝑐 − 𝑑 ) ∧ ∃ 𝑧 ∈ 𝑃 ( 𝑧 ∈ ( 𝑐 𝐼 𝑑 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝑐 − 𝑧 ) ) ) ) → ∃ 𝑧 ∈ 𝑃 ( 𝑧 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑧 ) ) )
67 simpr ⊢ ( ( 𝜑 ∧ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( ( 𝐶 − 𝐷 ) = ( 𝑥 − 𝑦 ) ∧ ∃ 𝑧 ∈ 𝑃 ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝑥 − 𝑧 ) ) ) ) → ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( ( 𝐶 − 𝐷 ) = ( 𝑥 − 𝑦 ) ∧ ∃ 𝑧 ∈ 𝑃 ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝑥 − 𝑧 ) ) ) )
68 oveq1 ⊢ ( 𝑐 = 𝑥 → ( 𝑐 − 𝑑 ) = ( 𝑥 − 𝑑 ) )
69 68 eqeq2d ⊢ ( 𝑐 = 𝑥 → ( ( 𝐶 − 𝐷 ) = ( 𝑐 − 𝑑 ) ↔ ( 𝐶 − 𝐷 ) = ( 𝑥 − 𝑑 ) ) )
70 oveq1 ⊢ ( 𝑐 = 𝑥 → ( 𝑐 𝐼 𝑑 ) = ( 𝑥 𝐼 𝑑 ) )
71 70 eleq2d ⊢ ( 𝑐 = 𝑥 → ( 𝑧 ∈ ( 𝑐 𝐼 𝑑 ) ↔ 𝑧 ∈ ( 𝑥 𝐼 𝑑 ) ) )
72 oveq1 ⊢ ( 𝑐 = 𝑥 → ( 𝑐 − 𝑧 ) = ( 𝑥 − 𝑧 ) )
73 72 eqeq2d ⊢ ( 𝑐 = 𝑥 → ( ( 𝐴 − 𝐵 ) = ( 𝑐 − 𝑧 ) ↔ ( 𝐴 − 𝐵 ) = ( 𝑥 − 𝑧 ) ) )
74 71 73 anbi12d ⊢ ( 𝑐 = 𝑥 → ( ( 𝑧 ∈ ( 𝑐 𝐼 𝑑 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝑐 − 𝑧 ) ) ↔ ( 𝑧 ∈ ( 𝑥 𝐼 𝑑 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝑥 − 𝑧 ) ) ) )
75 74 rexbidv ⊢ ( 𝑐 = 𝑥 → ( ∃ 𝑧 ∈ 𝑃 ( 𝑧 ∈ ( 𝑐 𝐼 𝑑 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝑐 − 𝑧 ) ) ↔ ∃ 𝑧 ∈ 𝑃 ( 𝑧 ∈ ( 𝑥 𝐼 𝑑 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝑥 − 𝑧 ) ) ) )
76 69 75 anbi12d ⊢ ( 𝑐 = 𝑥 → ( ( ( 𝐶 − 𝐷 ) = ( 𝑐 − 𝑑 ) ∧ ∃ 𝑧 ∈ 𝑃 ( 𝑧 ∈ ( 𝑐 𝐼 𝑑 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝑐 − 𝑧 ) ) ) ↔ ( ( 𝐶 − 𝐷 ) = ( 𝑥 − 𝑑 ) ∧ ∃ 𝑧 ∈ 𝑃 ( 𝑧 ∈ ( 𝑥 𝐼 𝑑 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝑥 − 𝑧 ) ) ) ) )
77 oveq2 ⊢ ( 𝑑 = 𝑦 → ( 𝑥 − 𝑑 ) = ( 𝑥 − 𝑦 ) )
78 77 eqeq2d ⊢ ( 𝑑 = 𝑦 → ( ( 𝐶 − 𝐷 ) = ( 𝑥 − 𝑑 ) ↔ ( 𝐶 − 𝐷 ) = ( 𝑥 − 𝑦 ) ) )
79 oveq2 ⊢ ( 𝑑 = 𝑦 → ( 𝑥 𝐼 𝑑 ) = ( 𝑥 𝐼 𝑦 ) )
80 79 eleq2d ⊢ ( 𝑑 = 𝑦 → ( 𝑧 ∈ ( 𝑥 𝐼 𝑑 ) ↔ 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ) )
81 80 anbi1d ⊢ ( 𝑑 = 𝑦 → ( ( 𝑧 ∈ ( 𝑥 𝐼 𝑑 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝑥 − 𝑧 ) ) ↔ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝑥 − 𝑧 ) ) ) )
82 81 rexbidv ⊢ ( 𝑑 = 𝑦 → ( ∃ 𝑧 ∈ 𝑃 ( 𝑧 ∈ ( 𝑥 𝐼 𝑑 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝑥 − 𝑧 ) ) ↔ ∃ 𝑧 ∈ 𝑃 ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝑥 − 𝑧 ) ) ) )
83 78 82 anbi12d ⊢ ( 𝑑 = 𝑦 → ( ( ( 𝐶 − 𝐷 ) = ( 𝑥 − 𝑑 ) ∧ ∃ 𝑧 ∈ 𝑃 ( 𝑧 ∈ ( 𝑥 𝐼 𝑑 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝑥 − 𝑧 ) ) ) ↔ ( ( 𝐶 − 𝐷 ) = ( 𝑥 − 𝑦 ) ∧ ∃ 𝑧 ∈ 𝑃 ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝑥 − 𝑧 ) ) ) ) )
84 76 83 cbvrex2vw ⊢ ( ∃ 𝑐 ∈ 𝑃 ∃ 𝑑 ∈ 𝑃 ( ( 𝐶 − 𝐷 ) = ( 𝑐 − 𝑑 ) ∧ ∃ 𝑧 ∈ 𝑃 ( 𝑧 ∈ ( 𝑐 𝐼 𝑑 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝑐 − 𝑧 ) ) ) ↔ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( ( 𝐶 − 𝐷 ) = ( 𝑥 − 𝑦 ) ∧ ∃ 𝑧 ∈ 𝑃 ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝑥 − 𝑧 ) ) ) )
85 67 84 sylibr ⊢ ( ( 𝜑 ∧ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( ( 𝐶 − 𝐷 ) = ( 𝑥 − 𝑦 ) ∧ ∃ 𝑧 ∈ 𝑃 ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝑥 − 𝑧 ) ) ) ) → ∃ 𝑐 ∈ 𝑃 ∃ 𝑑 ∈ 𝑃 ( ( 𝐶 − 𝐷 ) = ( 𝑐 − 𝑑 ) ∧ ∃ 𝑧 ∈ 𝑃 ( 𝑧 ∈ ( 𝑐 𝐼 𝑑 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝑐 − 𝑧 ) ) ) )
86 66 85 r19.29vva ⊢ ( ( 𝜑 ∧ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( ( 𝐶 − 𝐷 ) = ( 𝑥 − 𝑦 ) ∧ ∃ 𝑧 ∈ 𝑃 ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝑥 − 𝑧 ) ) ) ) → ∃ 𝑧 ∈ 𝑃 ( 𝑧 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑧 ) ) )
87 8 adantr ⊢ ( ( 𝜑 ∧ ∃ 𝑧 ∈ 𝑃 ( 𝑧 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑧 ) ) ) → 𝐶 ∈ 𝑃 )
88 9 adantr ⊢ ( ( 𝜑 ∧ ∃ 𝑧 ∈ 𝑃 ( 𝑧 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑧 ) ) ) → 𝐷 ∈ 𝑃 )
89 eqidd ⊢ ( ( 𝜑 ∧ ∃ 𝑧 ∈ 𝑃 ( 𝑧 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑧 ) ) ) → ( 𝐶 − 𝐷 ) = ( 𝐶 − 𝐷 ) )
90 simpr ⊢ ( ( 𝜑 ∧ ∃ 𝑧 ∈ 𝑃 ( 𝑧 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑧 ) ) ) → ∃ 𝑧 ∈ 𝑃 ( 𝑧 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑧 ) ) )
91 oveq1 ⊢ ( 𝑥 = 𝐶 → ( 𝑥 − 𝑦 ) = ( 𝐶 − 𝑦 ) )
92 91 eqeq2d ⊢ ( 𝑥 = 𝐶 → ( ( 𝐶 − 𝐷 ) = ( 𝑥 − 𝑦 ) ↔ ( 𝐶 − 𝐷 ) = ( 𝐶 − 𝑦 ) ) )
93 oveq1 ⊢ ( 𝑥 = 𝐶 → ( 𝑥 𝐼 𝑦 ) = ( 𝐶 𝐼 𝑦 ) )
94 93 eleq2d ⊢ ( 𝑥 = 𝐶 → ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ↔ 𝑧 ∈ ( 𝐶 𝐼 𝑦 ) ) )
95 oveq1 ⊢ ( 𝑥 = 𝐶 → ( 𝑥 − 𝑧 ) = ( 𝐶 − 𝑧 ) )
96 95 eqeq2d ⊢ ( 𝑥 = 𝐶 → ( ( 𝐴 − 𝐵 ) = ( 𝑥 − 𝑧 ) ↔ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑧 ) ) )
97 94 96 anbi12d ⊢ ( 𝑥 = 𝐶 → ( ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝑥 − 𝑧 ) ) ↔ ( 𝑧 ∈ ( 𝐶 𝐼 𝑦 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑧 ) ) ) )
98 97 rexbidv ⊢ ( 𝑥 = 𝐶 → ( ∃ 𝑧 ∈ 𝑃 ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝑥 − 𝑧 ) ) ↔ ∃ 𝑧 ∈ 𝑃 ( 𝑧 ∈ ( 𝐶 𝐼 𝑦 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑧 ) ) ) )
99 92 98 anbi12d ⊢ ( 𝑥 = 𝐶 → ( ( ( 𝐶 − 𝐷 ) = ( 𝑥 − 𝑦 ) ∧ ∃ 𝑧 ∈ 𝑃 ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝑥 − 𝑧 ) ) ) ↔ ( ( 𝐶 − 𝐷 ) = ( 𝐶 − 𝑦 ) ∧ ∃ 𝑧 ∈ 𝑃 ( 𝑧 ∈ ( 𝐶 𝐼 𝑦 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑧 ) ) ) ) )
100 oveq2 ⊢ ( 𝑦 = 𝐷 → ( 𝐶 − 𝑦 ) = ( 𝐶 − 𝐷 ) )
101 100 eqeq2d ⊢ ( 𝑦 = 𝐷 → ( ( 𝐶 − 𝐷 ) = ( 𝐶 − 𝑦 ) ↔ ( 𝐶 − 𝐷 ) = ( 𝐶 − 𝐷 ) ) )
102 oveq2 ⊢ ( 𝑦 = 𝐷 → ( 𝐶 𝐼 𝑦 ) = ( 𝐶 𝐼 𝐷 ) )
103 102 eleq2d ⊢ ( 𝑦 = 𝐷 → ( 𝑧 ∈ ( 𝐶 𝐼 𝑦 ) ↔ 𝑧 ∈ ( 𝐶 𝐼 𝐷 ) ) )
104 103 anbi1d ⊢ ( 𝑦 = 𝐷 → ( ( 𝑧 ∈ ( 𝐶 𝐼 𝑦 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑧 ) ) ↔ ( 𝑧 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑧 ) ) ) )
105 104 rexbidv ⊢ ( 𝑦 = 𝐷 → ( ∃ 𝑧 ∈ 𝑃 ( 𝑧 ∈ ( 𝐶 𝐼 𝑦 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑧 ) ) ↔ ∃ 𝑧 ∈ 𝑃 ( 𝑧 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑧 ) ) ) )
106 101 105 anbi12d ⊢ ( 𝑦 = 𝐷 → ( ( ( 𝐶 − 𝐷 ) = ( 𝐶 − 𝑦 ) ∧ ∃ 𝑧 ∈ 𝑃 ( 𝑧 ∈ ( 𝐶 𝐼 𝑦 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑧 ) ) ) ↔ ( ( 𝐶 − 𝐷 ) = ( 𝐶 − 𝐷 ) ∧ ∃ 𝑧 ∈ 𝑃 ( 𝑧 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑧 ) ) ) ) )
107 99 106 rspc2ev ⊢ ( ( 𝐶 ∈ 𝑃 ∧ 𝐷 ∈ 𝑃 ∧ ( ( 𝐶 − 𝐷 ) = ( 𝐶 − 𝐷 ) ∧ ∃ 𝑧 ∈ 𝑃 ( 𝑧 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑧 ) ) ) ) → ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( ( 𝐶 − 𝐷 ) = ( 𝑥 − 𝑦 ) ∧ ∃ 𝑧 ∈ 𝑃 ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝑥 − 𝑧 ) ) ) )
108 87 88 89 90 107 syl112anc ⊢ ( ( 𝜑 ∧ ∃ 𝑧 ∈ 𝑃 ( 𝑧 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑧 ) ) ) → ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( ( 𝐶 − 𝐷 ) = ( 𝑥 − 𝑦 ) ∧ ∃ 𝑧 ∈ 𝑃 ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝑥 − 𝑧 ) ) ) )
109 86 108 impbida ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( ( 𝐶 − 𝐷 ) = ( 𝑥 − 𝑦 ) ∧ ∃ 𝑧 ∈ 𝑃 ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝑥 − 𝑧 ) ) ) ↔ ∃ 𝑧 ∈ 𝑃 ( 𝑧 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑧 ) ) ) )
110 24 109 bitrd ⊢ ( 𝜑 → ( ( 𝐴 − 𝐵 ) ≤ ( 𝐶 − 𝐷 ) ↔ ∃ 𝑧 ∈ 𝑃 ( 𝑧 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑧 ) ) ) )