Metamath Proof Explorer

Theorem legov3

Description: An equivalent definition of the less-than relationship, from the strict relation. (Contributed by Thierry Arnoux, 15-Dec-2019)

Ref Expression
Hypotheses legval.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
legval.d ⊢ − = ( dist ‘ 𝐺 )
legval.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
legval.l ⊢ ≤ = ( ≤G ‘ 𝐺 )
legval.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
legso.a ⊢ 𝐸 = ( − “ ( 𝑃 × 𝑃 ) )
legso.f ⊢ ( 𝜑 → Fun − )
legso.l ⊢ < = ( ( ≤ ↾ 𝐸 ) ∖ I )
legso.d ⊢ ( 𝜑 → ( 𝑃 × 𝑃 ) ⊆ dom − )
ltgov.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
ltgov.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
Assertion legov3 ( 𝜑 → ( ( 𝐴 − 𝐵 ) ≤ ( 𝐶 − 𝐷 ) ↔ ( ( 𝐴 − 𝐵 ) < ( 𝐶 − 𝐷 ) ∨ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝐷 ) ) ) )

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 legso.a ⊢ 𝐸 = ( − “ ( 𝑃 × 𝑃 ) )
7 legso.f ⊢ ( 𝜑 → Fun − )
8 legso.l ⊢ < = ( ( ≤ ↾ 𝐸 ) ∖ I )
9 legso.d ⊢ ( 𝜑 → ( 𝑃 × 𝑃 ) ⊆ dom − )
10 ltgov.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
11 ltgov.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
12 1 2 3 4 5 6 7 8 9 10 11 ltgov ⊢ ( 𝜑 → ( ( 𝐴 − 𝐵 ) < ( 𝐶 − 𝐷 ) ↔ ( ( 𝐴 − 𝐵 ) ≤ ( 𝐶 − 𝐷 ) ∧ ( 𝐴 − 𝐵 ) ≠ ( 𝐶 − 𝐷 ) ) ) )
13 12 orbi1d ⊢ ( 𝜑 → ( ( ( 𝐴 − 𝐵 ) < ( 𝐶 − 𝐷 ) ∨ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝐷 ) ) ↔ ( ( ( 𝐴 − 𝐵 ) ≤ ( 𝐶 − 𝐷 ) ∧ ( 𝐴 − 𝐵 ) ≠ ( 𝐶 − 𝐷 ) ) ∨ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝐷 ) ) ) )
14 simprl ⊢ ( ( ( 𝜑 ∧ ( ( ( 𝐴 − 𝐵 ) ≤ ( 𝐶 − 𝐷 ) ∧ ( 𝐴 − 𝐵 ) ≠ ( 𝐶 − 𝐷 ) ) ∨ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝐷 ) ) ) ∧ ( ( 𝐴 − 𝐵 ) ≤ ( 𝐶 − 𝐷 ) ∧ ( 𝐴 − 𝐵 ) ≠ ( 𝐶 − 𝐷 ) ) ) → ( 𝐴 − 𝐵 ) ≤ ( 𝐶 − 𝐷 ) )
15 1 2 3 4 5 10 11 legid ⊢ ( 𝜑 → ( 𝐴 − 𝐵 ) ≤ ( 𝐴 − 𝐵 ) )
16 15 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝐷 ) ) → ( 𝐴 − 𝐵 ) ≤ ( 𝐴 − 𝐵 ) )
17 simpr ⊢ ( ( 𝜑 ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝐷 ) ) → ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝐷 ) )
18 16 17 breqtrd ⊢ ( ( 𝜑 ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝐷 ) ) → ( 𝐴 − 𝐵 ) ≤ ( 𝐶 − 𝐷 ) )
19 18 adantlr ⊢ ( ( ( 𝜑 ∧ ( ( ( 𝐴 − 𝐵 ) ≤ ( 𝐶 − 𝐷 ) ∧ ( 𝐴 − 𝐵 ) ≠ ( 𝐶 − 𝐷 ) ) ∨ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝐷 ) ) ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝐷 ) ) → ( 𝐴 − 𝐵 ) ≤ ( 𝐶 − 𝐷 ) )
20 simpr ⊢ ( ( 𝜑 ∧ ( ( ( 𝐴 − 𝐵 ) ≤ ( 𝐶 − 𝐷 ) ∧ ( 𝐴 − 𝐵 ) ≠ ( 𝐶 − 𝐷 ) ) ∨ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝐷 ) ) ) → ( ( ( 𝐴 − 𝐵 ) ≤ ( 𝐶 − 𝐷 ) ∧ ( 𝐴 − 𝐵 ) ≠ ( 𝐶 − 𝐷 ) ) ∨ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝐷 ) ) )
21 14 19 20 mpjaodan ⊢ ( ( 𝜑 ∧ ( ( ( 𝐴 − 𝐵 ) ≤ ( 𝐶 − 𝐷 ) ∧ ( 𝐴 − 𝐵 ) ≠ ( 𝐶 − 𝐷 ) ) ∨ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝐷 ) ) ) → ( 𝐴 − 𝐵 ) ≤ ( 𝐶 − 𝐷 ) )
22 simplr ⊢ ( ( ( 𝜑 ∧ ( 𝐴 − 𝐵 ) ≤ ( 𝐶 − 𝐷 ) ) ∧ ¬ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝐷 ) ) → ( 𝐴 − 𝐵 ) ≤ ( 𝐶 − 𝐷 ) )
23 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝐴 − 𝐵 ) ≤ ( 𝐶 − 𝐷 ) ) ∧ ¬ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝐷 ) ) → ¬ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝐷 ) )
24 23 neqned ⊢ ( ( ( 𝜑 ∧ ( 𝐴 − 𝐵 ) ≤ ( 𝐶 − 𝐷 ) ) ∧ ¬ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝐷 ) ) → ( 𝐴 − 𝐵 ) ≠ ( 𝐶 − 𝐷 ) )
25 22 24 jca ⊢ ( ( ( 𝜑 ∧ ( 𝐴 − 𝐵 ) ≤ ( 𝐶 − 𝐷 ) ) ∧ ¬ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝐷 ) ) → ( ( 𝐴 − 𝐵 ) ≤ ( 𝐶 − 𝐷 ) ∧ ( 𝐴 − 𝐵 ) ≠ ( 𝐶 − 𝐷 ) ) )
26 25 ex ⊢ ( ( 𝜑 ∧ ( 𝐴 − 𝐵 ) ≤ ( 𝐶 − 𝐷 ) ) → ( ¬ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝐷 ) → ( ( 𝐴 − 𝐵 ) ≤ ( 𝐶 − 𝐷 ) ∧ ( 𝐴 − 𝐵 ) ≠ ( 𝐶 − 𝐷 ) ) ) )
27 26 orrd ⊢ ( ( 𝜑 ∧ ( 𝐴 − 𝐵 ) ≤ ( 𝐶 − 𝐷 ) ) → ( ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝐷 ) ∨ ( ( 𝐴 − 𝐵 ) ≤ ( 𝐶 − 𝐷 ) ∧ ( 𝐴 − 𝐵 ) ≠ ( 𝐶 − 𝐷 ) ) ) )
28 27 orcomd ⊢ ( ( 𝜑 ∧ ( 𝐴 − 𝐵 ) ≤ ( 𝐶 − 𝐷 ) ) → ( ( ( 𝐴 − 𝐵 ) ≤ ( 𝐶 − 𝐷 ) ∧ ( 𝐴 − 𝐵 ) ≠ ( 𝐶 − 𝐷 ) ) ∨ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝐷 ) ) )
29 21 28 impbida ⊢ ( 𝜑 → ( ( ( ( 𝐴 − 𝐵 ) ≤ ( 𝐶 − 𝐷 ) ∧ ( 𝐴 − 𝐵 ) ≠ ( 𝐶 − 𝐷 ) ) ∨ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝐷 ) ) ↔ ( 𝐴 − 𝐵 ) ≤ ( 𝐶 − 𝐷 ) ) )
30 13 29 bitr2d ⊢ ( 𝜑 → ( ( 𝐴 − 𝐵 ) ≤ ( 𝐶 − 𝐷 ) ↔ ( ( 𝐴 − 𝐵 ) < ( 𝐶 − 𝐷 ) ∨ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝐷 ) ) ) )