Metamath Proof Explorer

Theorem legtrd

Description: Transitivity of the less-than relationship. Proposition 5.8 of Schwabhauser p. 42. (Contributed by Thierry Arnoux, 27-Jun-2019)

Ref Expression
Hypotheses legval.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
legval.d ⊢ − = ( dist ‘ 𝐺 )
legval.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
legval.l ⊢ ≤ = ( ≤G ‘ 𝐺 )
legval.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
legid.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
legid.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
legtrd.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
legtrd.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
legtrd.e ⊢ ( 𝜑 → 𝐸 ∈ 𝑃 )
legtrd.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑃 )
legtrd.1 ⊢ ( 𝜑 → ( 𝐴 − 𝐵 ) ≤ ( 𝐶 − 𝐷 ) )
legtrd.2 ⊢ ( 𝜑 → ( 𝐶 − 𝐷 ) ≤ ( 𝐸 − 𝐹 ) )
Assertion legtrd ( 𝜑 → ( 𝐴 − 𝐵 ) ≤ ( 𝐸 − 𝐹 ) )

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 legid.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
7 legid.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
8 legtrd.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
9 legtrd.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
10 legtrd.e ⊢ ( 𝜑 → 𝐸 ∈ 𝑃 )
11 legtrd.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑃 )
12 legtrd.1 ⊢ ( 𝜑 → ( 𝐴 − 𝐵 ) ≤ ( 𝐶 − 𝐷 ) )
13 legtrd.2 ⊢ ( 𝜑 → ( 𝐶 − 𝐷 ) ≤ ( 𝐸 − 𝐹 ) )
14 eqid ⊢ ( LineG ‘ 𝐺 ) = ( LineG ‘ 𝐺 )
15 5 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑥 ) ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝐸 𝐼 𝐹 ) ∧ ( 𝐶 − 𝐷 ) = ( 𝐸 − 𝑦 ) ) ) → 𝐺 ∈ TarskiG )
16 8 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑥 ) ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝐸 𝐼 𝐹 ) ∧ ( 𝐶 − 𝐷 ) = ( 𝐸 − 𝑦 ) ) ) → 𝐶 ∈ 𝑃 )
17 9 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑥 ) ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝐸 𝐼 𝐹 ) ∧ ( 𝐶 − 𝐷 ) = ( 𝐸 − 𝑦 ) ) ) → 𝐷 ∈ 𝑃 )
18 simp-4r ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑥 ) ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝐸 𝐼 𝐹 ) ∧ ( 𝐶 − 𝐷 ) = ( 𝐸 − 𝑦 ) ) ) → 𝑥 ∈ 𝑃 )
19 eqid ⊢ ( cgrG ‘ 𝐺 ) = ( cgrG ‘ 𝐺 )
20 10 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑥 ) ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝐸 𝐼 𝐹 ) ∧ ( 𝐶 − 𝐷 ) = ( 𝐸 − 𝑦 ) ) ) → 𝐸 ∈ 𝑃 )
21 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑥 ) ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝐸 𝐼 𝐹 ) ∧ ( 𝐶 − 𝐷 ) = ( 𝐸 − 𝑦 ) ) ) → 𝑦 ∈ 𝑃 )
22 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑥 ) ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝐸 𝐼 𝐹 ) ∧ ( 𝐶 − 𝐷 ) = ( 𝐸 − 𝑦 ) ) ) → ( 𝑥 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑥 ) ) )
23 22 simpld ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑥 ) ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝐸 𝐼 𝐹 ) ∧ ( 𝐶 − 𝐷 ) = ( 𝐸 − 𝑦 ) ) ) → 𝑥 ∈ ( 𝐶 𝐼 𝐷 ) )
24 1 14 3 15 16 18 17 23 btwncolg3 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑥 ) ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝐸 𝐼 𝐹 ) ∧ ( 𝐶 − 𝐷 ) = ( 𝐸 − 𝑦 ) ) ) → ( 𝐷 ∈ ( 𝐶 ( LineG ‘ 𝐺 ) 𝑥 ) ∨ 𝐶 = 𝑥 ) )
25 simprr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑥 ) ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝐸 𝐼 𝐹 ) ∧ ( 𝐶 − 𝐷 ) = ( 𝐸 − 𝑦 ) ) ) → ( 𝐶 − 𝐷 ) = ( 𝐸 − 𝑦 ) )
26 1 14 3 15 16 17 18 19 20 21 2 24 25 lnext ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑥 ) ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝐸 𝐼 𝐹 ) ∧ ( 𝐶 − 𝐷 ) = ( 𝐸 − 𝑦 ) ) ) → ∃ 𝑧 ∈ 𝑃 ⟨“ 𝐶 𝐷 𝑥 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐸 𝑦 𝑧 ”⟩ )
27 15 ad2antrr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑥 ) ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝐸 𝐼 𝐹 ) ∧ ( 𝐶 − 𝐷 ) = ( 𝐸 − 𝑦 ) ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ⟨“ 𝐶 𝐷 𝑥 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐸 𝑦 𝑧 ”⟩ ) → 𝐺 ∈ TarskiG )
28 20 ad2antrr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑥 ) ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝐸 𝐼 𝐹 ) ∧ ( 𝐶 − 𝐷 ) = ( 𝐸 − 𝑦 ) ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ⟨“ 𝐶 𝐷 𝑥 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐸 𝑦 𝑧 ”⟩ ) → 𝐸 ∈ 𝑃 )
29 simplr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑥 ) ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝐸 𝐼 𝐹 ) ∧ ( 𝐶 − 𝐷 ) = ( 𝐸 − 𝑦 ) ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ⟨“ 𝐶 𝐷 𝑥 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐸 𝑦 𝑧 ”⟩ ) → 𝑧 ∈ 𝑃 )
30 simp-4r ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑥 ) ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝐸 𝐼 𝐹 ) ∧ ( 𝐶 − 𝐷 ) = ( 𝐸 − 𝑦 ) ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ⟨“ 𝐶 𝐷 𝑥 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐸 𝑦 𝑧 ”⟩ ) → 𝑦 ∈ 𝑃 )
31 11 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑥 ) ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝐸 𝐼 𝐹 ) ∧ ( 𝐶 − 𝐷 ) = ( 𝐸 − 𝑦 ) ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ⟨“ 𝐶 𝐷 𝑥 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐸 𝑦 𝑧 ”⟩ ) → 𝐹 ∈ 𝑃 )
32 16 ad2antrr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑥 ) ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝐸 𝐼 𝐹 ) ∧ ( 𝐶 − 𝐷 ) = ( 𝐸 − 𝑦 ) ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ⟨“ 𝐶 𝐷 𝑥 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐸 𝑦 𝑧 ”⟩ ) → 𝐶 ∈ 𝑃 )
33 18 ad2antrr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑥 ) ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝐸 𝐼 𝐹 ) ∧ ( 𝐶 − 𝐷 ) = ( 𝐸 − 𝑦 ) ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ⟨“ 𝐶 𝐷 𝑥 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐸 𝑦 𝑧 ”⟩ ) → 𝑥 ∈ 𝑃 )
34 17 ad2antrr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑥 ) ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝐸 𝐼 𝐹 ) ∧ ( 𝐶 − 𝐷 ) = ( 𝐸 − 𝑦 ) ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ⟨“ 𝐶 𝐷 𝑥 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐸 𝑦 𝑧 ”⟩ ) → 𝐷 ∈ 𝑃 )
35 simpr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑥 ) ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝐸 𝐼 𝐹 ) ∧ ( 𝐶 − 𝐷 ) = ( 𝐸 − 𝑦 ) ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ⟨“ 𝐶 𝐷 𝑥 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐸 𝑦 𝑧 ”⟩ ) → ⟨“ 𝐶 𝐷 𝑥 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐸 𝑦 𝑧 ”⟩ )
36 1 2 3 19 27 32 34 33 28 30 29 35 cgr3swap23 ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑥 ) ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝐸 𝐼 𝐹 ) ∧ ( 𝐶 − 𝐷 ) = ( 𝐸 − 𝑦 ) ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ⟨“ 𝐶 𝐷 𝑥 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐸 𝑦 𝑧 ”⟩ ) → ⟨“ 𝐶 𝑥 𝐷 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐸 𝑧 𝑦 ”⟩ )
37 23 ad2antrr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑥 ) ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝐸 𝐼 𝐹 ) ∧ ( 𝐶 − 𝐷 ) = ( 𝐸 − 𝑦 ) ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ⟨“ 𝐶 𝐷 𝑥 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐸 𝑦 𝑧 ”⟩ ) → 𝑥 ∈ ( 𝐶 𝐼 𝐷 ) )
38 1 2 3 19 27 32 33 34 28 29 30 36 37 tgbtwnxfr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑥 ) ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝐸 𝐼 𝐹 ) ∧ ( 𝐶 − 𝐷 ) = ( 𝐸 − 𝑦 ) ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ⟨“ 𝐶 𝐷 𝑥 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐸 𝑦 𝑧 ”⟩ ) → 𝑧 ∈ ( 𝐸 𝐼 𝑦 ) )
39 simpllr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑥 ) ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝐸 𝐼 𝐹 ) ∧ ( 𝐶 − 𝐷 ) = ( 𝐸 − 𝑦 ) ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ⟨“ 𝐶 𝐷 𝑥 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐸 𝑦 𝑧 ”⟩ ) → ( 𝑦 ∈ ( 𝐸 𝐼 𝐹 ) ∧ ( 𝐶 − 𝐷 ) = ( 𝐸 − 𝑦 ) ) )
40 39 simpld ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑥 ) ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝐸 𝐼 𝐹 ) ∧ ( 𝐶 − 𝐷 ) = ( 𝐸 − 𝑦 ) ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ⟨“ 𝐶 𝐷 𝑥 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐸 𝑦 𝑧 ”⟩ ) → 𝑦 ∈ ( 𝐸 𝐼 𝐹 ) )
41 1 2 3 27 28 29 30 31 38 40 tgbtwnexch ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑥 ) ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝐸 𝐼 𝐹 ) ∧ ( 𝐶 − 𝐷 ) = ( 𝐸 − 𝑦 ) ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ⟨“ 𝐶 𝐷 𝑥 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐸 𝑦 𝑧 ”⟩ ) → 𝑧 ∈ ( 𝐸 𝐼 𝐹 ) )
42 simp-5r ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑥 ) ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝐸 𝐼 𝐹 ) ∧ ( 𝐶 − 𝐷 ) = ( 𝐸 − 𝑦 ) ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ⟨“ 𝐶 𝐷 𝑥 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐸 𝑦 𝑧 ”⟩ ) → ( 𝑥 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑥 ) ) )
43 42 simprd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑥 ) ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝐸 𝐼 𝐹 ) ∧ ( 𝐶 − 𝐷 ) = ( 𝐸 − 𝑦 ) ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ⟨“ 𝐶 𝐷 𝑥 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐸 𝑦 𝑧 ”⟩ ) → ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑥 ) )
44 1 2 3 19 27 32 33 34 28 29 30 36 cgr3simp1 ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑥 ) ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝐸 𝐼 𝐹 ) ∧ ( 𝐶 − 𝐷 ) = ( 𝐸 − 𝑦 ) ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ⟨“ 𝐶 𝐷 𝑥 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐸 𝑦 𝑧 ”⟩ ) → ( 𝐶 − 𝑥 ) = ( 𝐸 − 𝑧 ) )
45 43 44 eqtrd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑥 ) ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝐸 𝐼 𝐹 ) ∧ ( 𝐶 − 𝐷 ) = ( 𝐸 − 𝑦 ) ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ⟨“ 𝐶 𝐷 𝑥 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐸 𝑦 𝑧 ”⟩ ) → ( 𝐴 − 𝐵 ) = ( 𝐸 − 𝑧 ) )
46 41 45 jca ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑥 ) ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝐸 𝐼 𝐹 ) ∧ ( 𝐶 − 𝐷 ) = ( 𝐸 − 𝑦 ) ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ⟨“ 𝐶 𝐷 𝑥 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐸 𝑦 𝑧 ”⟩ ) → ( 𝑧 ∈ ( 𝐸 𝐼 𝐹 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐸 − 𝑧 ) ) )
47 46 ex ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑥 ) ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝐸 𝐼 𝐹 ) ∧ ( 𝐶 − 𝐷 ) = ( 𝐸 − 𝑦 ) ) ) ∧ 𝑧 ∈ 𝑃 ) → ( ⟨“ 𝐶 𝐷 𝑥 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐸 𝑦 𝑧 ”⟩ → ( 𝑧 ∈ ( 𝐸 𝐼 𝐹 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐸 − 𝑧 ) ) ) )
48 47 reximdva ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑥 ) ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝐸 𝐼 𝐹 ) ∧ ( 𝐶 − 𝐷 ) = ( 𝐸 − 𝑦 ) ) ) → ( ∃ 𝑧 ∈ 𝑃 ⟨“ 𝐶 𝐷 𝑥 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐸 𝑦 𝑧 ”⟩ → ∃ 𝑧 ∈ 𝑃 ( 𝑧 ∈ ( 𝐸 𝐼 𝐹 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐸 − 𝑧 ) ) ) )
49 26 48 mpd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑥 ) ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝐸 𝐼 𝐹 ) ∧ ( 𝐶 − 𝐷 ) = ( 𝐸 − 𝑦 ) ) ) → ∃ 𝑧 ∈ 𝑃 ( 𝑧 ∈ ( 𝐸 𝐼 𝐹 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐸 − 𝑧 ) ) )
50 1 2 3 4 5 8 9 10 11 legov ⊢ ( 𝜑 → ( ( 𝐶 − 𝐷 ) ≤ ( 𝐸 − 𝐹 ) ↔ ∃ 𝑦 ∈ 𝑃 ( 𝑦 ∈ ( 𝐸 𝐼 𝐹 ) ∧ ( 𝐶 − 𝐷 ) = ( 𝐸 − 𝑦 ) ) ) )
51 13 50 mpbid ⊢ ( 𝜑 → ∃ 𝑦 ∈ 𝑃 ( 𝑦 ∈ ( 𝐸 𝐼 𝐹 ) ∧ ( 𝐶 − 𝐷 ) = ( 𝐸 − 𝑦 ) ) )
52 51 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑥 ) ) ) → ∃ 𝑦 ∈ 𝑃 ( 𝑦 ∈ ( 𝐸 𝐼 𝐹 ) ∧ ( 𝐶 − 𝐷 ) = ( 𝐸 − 𝑦 ) ) )
53 49 52 r19.29a ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑥 ) ) ) → ∃ 𝑧 ∈ 𝑃 ( 𝑧 ∈ ( 𝐸 𝐼 𝐹 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐸 − 𝑧 ) ) )
54 1 2 3 4 5 6 7 8 9 legov ⊢ ( 𝜑 → ( ( 𝐴 − 𝐵 ) ≤ ( 𝐶 − 𝐷 ) ↔ ∃ 𝑥 ∈ 𝑃 ( 𝑥 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑥 ) ) ) )
55 12 54 mpbid ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝑃 ( 𝑥 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑥 ) ) )
56 53 55 r19.29a ⊢ ( 𝜑 → ∃ 𝑧 ∈ 𝑃 ( 𝑧 ∈ ( 𝐸 𝐼 𝐹 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐸 − 𝑧 ) ) )
57 1 2 3 4 5 6 7 10 11 legov ⊢ ( 𝜑 → ( ( 𝐴 − 𝐵 ) ≤ ( 𝐸 − 𝐹 ) ↔ ∃ 𝑧 ∈ 𝑃 ( 𝑧 ∈ ( 𝐸 𝐼 𝐹 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐸 − 𝑧 ) ) ) )
58 56 57 mpbird ⊢ ( 𝜑 → ( 𝐴 − 𝐵 ) ≤ ( 𝐸 − 𝐹 ) )