Metamath Proof Explorer

Theorem ltgov

Description: Strict "shorter than" geometric relation between segments. (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 ltgov ( 𝜑 → ( ( 𝐴 − 𝐵 ) < ( 𝐶 − 𝐷 ) ↔ ( ( 𝐴 − 𝐵 ) ≤ ( 𝐶 − 𝐷 ) ∧ ( 𝐴 − 𝐵 ) ≠ ( 𝐶 − 𝐷 ) ) ) )

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 8 breqi ⊢ ( ( 𝐴 − 𝐵 ) < ( 𝐶 − 𝐷 ) ↔ ( 𝐴 − 𝐵 ) ( ( ≤ ↾ 𝐸 ) ∖ I ) ( 𝐶 − 𝐷 ) )
13 brdif ⊢ ( ( 𝐴 − 𝐵 ) ( ( ≤ ↾ 𝐸 ) ∖ I ) ( 𝐶 − 𝐷 ) ↔ ( ( 𝐴 − 𝐵 ) ( ≤ ↾ 𝐸 ) ( 𝐶 − 𝐷 ) ∧ ¬ ( 𝐴 − 𝐵 ) I ( 𝐶 − 𝐷 ) ) )
14 12 13 bitri ⊢ ( ( 𝐴 − 𝐵 ) < ( 𝐶 − 𝐷 ) ↔ ( ( 𝐴 − 𝐵 ) ( ≤ ↾ 𝐸 ) ( 𝐶 − 𝐷 ) ∧ ¬ ( 𝐴 − 𝐵 ) I ( 𝐶 − 𝐷 ) ) )
15 ovex ⊢ ( 𝐶 − 𝐷 ) ∈ V
16 15 brresi ⊢ ( ( 𝐴 − 𝐵 ) ( ≤ ↾ 𝐸 ) ( 𝐶 − 𝐷 ) ↔ ( ( 𝐴 − 𝐵 ) ∈ 𝐸 ∧ ( 𝐴 − 𝐵 ) ≤ ( 𝐶 − 𝐷 ) ) )
17 16 anbi1i ⊢ ( ( ( 𝐴 − 𝐵 ) ( ≤ ↾ 𝐸 ) ( 𝐶 − 𝐷 ) ∧ ¬ ( 𝐴 − 𝐵 ) I ( 𝐶 − 𝐷 ) ) ↔ ( ( ( 𝐴 − 𝐵 ) ∈ 𝐸 ∧ ( 𝐴 − 𝐵 ) ≤ ( 𝐶 − 𝐷 ) ) ∧ ¬ ( 𝐴 − 𝐵 ) I ( 𝐶 − 𝐷 ) ) )
18 an21 ⊢ ( ( ( ( 𝐴 − 𝐵 ) ∈ 𝐸 ∧ ( 𝐴 − 𝐵 ) ≤ ( 𝐶 − 𝐷 ) ) ∧ ¬ ( 𝐴 − 𝐵 ) I ( 𝐶 − 𝐷 ) ) ↔ ( ( 𝐴 − 𝐵 ) ≤ ( 𝐶 − 𝐷 ) ∧ ( ( 𝐴 − 𝐵 ) ∈ 𝐸 ∧ ¬ ( 𝐴 − 𝐵 ) I ( 𝐶 − 𝐷 ) ) ) )
19 14 17 18 3bitri ⊢ ( ( 𝐴 − 𝐵 ) < ( 𝐶 − 𝐷 ) ↔ ( ( 𝐴 − 𝐵 ) ≤ ( 𝐶 − 𝐷 ) ∧ ( ( 𝐴 − 𝐵 ) ∈ 𝐸 ∧ ¬ ( 𝐴 − 𝐵 ) I ( 𝐶 − 𝐷 ) ) ) )
20 10 11 7 9 elovimad ⊢ ( 𝜑 → ( 𝐴 − 𝐵 ) ∈ ( − “ ( 𝑃 × 𝑃 ) ) )
21 20 6 eleqtrrdi ⊢ ( 𝜑 → ( 𝐴 − 𝐵 ) ∈ 𝐸 )
22 21 biantrurd ⊢ ( 𝜑 → ( ¬ ( 𝐴 − 𝐵 ) I ( 𝐶 − 𝐷 ) ↔ ( ( 𝐴 − 𝐵 ) ∈ 𝐸 ∧ ¬ ( 𝐴 − 𝐵 ) I ( 𝐶 − 𝐷 ) ) ) )
23 15 ideq ⊢ ( ( 𝐴 − 𝐵 ) I ( 𝐶 − 𝐷 ) ↔ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝐷 ) )
24 23 necon3bbii ⊢ ( ¬ ( 𝐴 − 𝐵 ) I ( 𝐶 − 𝐷 ) ↔ ( 𝐴 − 𝐵 ) ≠ ( 𝐶 − 𝐷 ) )
25 22 24 bitr3di ⊢ ( 𝜑 → ( ( ( 𝐴 − 𝐵 ) ∈ 𝐸 ∧ ¬ ( 𝐴 − 𝐵 ) I ( 𝐶 − 𝐷 ) ) ↔ ( 𝐴 − 𝐵 ) ≠ ( 𝐶 − 𝐷 ) ) )
26 25 anbi2d ⊢ ( 𝜑 → ( ( ( 𝐴 − 𝐵 ) ≤ ( 𝐶 − 𝐷 ) ∧ ( ( 𝐴 − 𝐵 ) ∈ 𝐸 ∧ ¬ ( 𝐴 − 𝐵 ) I ( 𝐶 − 𝐷 ) ) ) ↔ ( ( 𝐴 − 𝐵 ) ≤ ( 𝐶 − 𝐷 ) ∧ ( 𝐴 − 𝐵 ) ≠ ( 𝐶 − 𝐷 ) ) ) )
27 19 26 bitrid ⊢ ( 𝜑 → ( ( 𝐴 − 𝐵 ) < ( 𝐶 − 𝐷 ) ↔ ( ( 𝐴 − 𝐵 ) ≤ ( 𝐶 − 𝐷 ) ∧ ( 𝐴 − 𝐵 ) ≠ ( 𝐶 − 𝐷 ) ) ) )