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	⊢ ( 𝜑 → ( ( 𝐴 − 𝐵 ) ≤ ( 𝐶 − 𝐷 ) ↔ ∃ 𝑧 ∈ 𝑃 ( 𝑧 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑧 ) ) ) )