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 syl5bb ( 𝜑 → ( ( 𝐴 𝐵 ) < ( 𝐶 𝐷 ) ↔ ( ( 𝐴 𝐵 ) ( 𝐶 𝐷 ) ∧ ( 𝐴 𝐵 ) ≠ ( 𝐶 𝐷 ) ) ) )