ltgov - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > ltgov		Structured version Visualization version GIF version

Theorem ltgov 29060

Description: Strict "shorter than" geometric relation between segments. (Contributed by Thierry Arnoux, 15-Dec-2019.)

**Hypotheses**
Ref	Expression
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**
Ref	Expression
ltgov	⊢ (𝜑 → ((𝐴 − 𝐵) < (𝐶 − 𝐷) ↔ ((𝐴 − 𝐵) ≤ (𝐶 − 𝐷) ∧ (𝐴 − 𝐵) ≠ (𝐶 − 𝐷))))

**Proof of Theorem ltgov**
Step	Hyp	Ref	Expression
1		legso.l	. . . . 5 ⊢ < = (( ≤ ↾ 𝐸) ∖ I )
2	1	breqi 5108	. . . 4 ⊢ ((𝐴 − 𝐵) < (𝐶 − 𝐷) ↔ (𝐴 − 𝐵)(( ≤ ↾ 𝐸) ∖ I )(𝐶 − 𝐷))
3		brdif 5157	. . . 4 ⊢ ((𝐴 − 𝐵)(( ≤ ↾ 𝐸) ∖ I )(𝐶 − 𝐷) ↔ ((𝐴 − 𝐵)( ≤ ↾ 𝐸)(𝐶 − 𝐷) ∧ ¬ (𝐴 − 𝐵) I (𝐶 − 𝐷)))
4	2, 3	bitri 278	. . 3 ⊢ ((𝐴 − 𝐵) < (𝐶 − 𝐷) ↔ ((𝐴 − 𝐵)( ≤ ↾ 𝐸)(𝐶 − 𝐷) ∧ ¬ (𝐴 − 𝐵) I (𝐶 − 𝐷)))
5		ovex 7453	. . . . 5 ⊢ (𝐶 − 𝐷) ∈ V
6	5	brresi 5978	. . . 4 ⊢ ((𝐴 − 𝐵)( ≤ ↾ 𝐸)(𝐶 − 𝐷) ↔ ((𝐴 − 𝐵) ∈ 𝐸 ∧ (𝐴 − 𝐵) ≤ (𝐶 − 𝐷)))
7	6	anbi1i 636	. . 3 ⊢ (((𝐴 − 𝐵)( ≤ ↾ 𝐸)(𝐶 − 𝐷) ∧ ¬ (𝐴 − 𝐵) I (𝐶 − 𝐷)) ↔ (((𝐴 − 𝐵) ∈ 𝐸 ∧ (𝐴 − 𝐵) ≤ (𝐶 − 𝐷)) ∧ ¬ (𝐴 − 𝐵) I (𝐶 − 𝐷)))
8		an21 657	. . 3 ⊢ ((((𝐴 − 𝐵) ∈ 𝐸 ∧ (𝐴 − 𝐵) ≤ (𝐶 − 𝐷)) ∧ ¬ (𝐴 − 𝐵) I (𝐶 − 𝐷)) ↔ ((𝐴 − 𝐵) ≤ (𝐶 − 𝐷) ∧ ((𝐴 − 𝐵) ∈ 𝐸 ∧ ¬ (𝐴 − 𝐵) I (𝐶 − 𝐷))))
9	4, 7, 8	3bitri 300	. 2 ⊢ ((𝐴 − 𝐵) < (𝐶 − 𝐷) ↔ ((𝐴 − 𝐵) ≤ (𝐶 − 𝐷) ∧ ((𝐴 − 𝐵) ∈ 𝐸 ∧ ¬ (𝐴 − 𝐵) I (𝐶 − 𝐷))))
10		ltgov.a	. . . . . . 7 ⊢ (𝜑 → 𝐴 ∈ 𝑃)
11		ltgov.b	. . . . . . 7 ⊢ (𝜑 → 𝐵 ∈ 𝑃)
12		legso.f	. . . . . . 7 ⊢ (𝜑 → Fun − )
13		legso.d	. . . . . . 7 ⊢ (𝜑 → (𝑃 × 𝑃) ⊆ dom − )
14	10, 11, 12, 13	elovimad 7470	. . . . . 6 ⊢ (𝜑 → (𝐴 − 𝐵) ∈ ( − “ (𝑃 × 𝑃)))
15		legso.a	. . . . . 6 ⊢ 𝐸 = ( − “ (𝑃 × 𝑃))
16	14, 15	eleqtrrdi 2871	. . . . 5 ⊢ (𝜑 → (𝐴 − 𝐵) ∈ 𝐸)
17	16	biantrurd 542	. . . 4 ⊢ (𝜑 → (¬ (𝐴 − 𝐵) I (𝐶 − 𝐷) ↔ ((𝐴 − 𝐵) ∈ 𝐸 ∧ ¬ (𝐴 − 𝐵) I (𝐶 − 𝐷))))
18	5	ideq 5829	. . . . 5 ⊢ ((𝐴 − 𝐵) I (𝐶 − 𝐷) ↔ (𝐴 − 𝐵) = (𝐶 − 𝐷))
19	18	necon3bbii 3002	. . . 4 ⊢ (¬ (𝐴 − 𝐵) I (𝐶 − 𝐷) ↔ (𝐴 − 𝐵) ≠ (𝐶 − 𝐷))
20	17, 19	bitr3di 289	. . 3 ⊢ (𝜑 → (((𝐴 − 𝐵) ∈ 𝐸 ∧ ¬ (𝐴 − 𝐵) I (𝐶 − 𝐷)) ↔ (𝐴 − 𝐵) ≠ (𝐶 − 𝐷)))
21	20	anbi2d 642	. 2 ⊢ (𝜑 → (((𝐴 − 𝐵) ≤ (𝐶 − 𝐷) ∧ ((𝐴 − 𝐵) ∈ 𝐸 ∧ ¬ (𝐴 − 𝐵) I (𝐶 − 𝐷))) ↔ ((𝐴 − 𝐵) ≤ (𝐶 − 𝐷) ∧ (𝐴 − 𝐵) ≠ (𝐶 − 𝐷))))
22	9, 21	bitrid 286	1 ⊢ (𝜑 → ((𝐴 − 𝐵) < (𝐶 − 𝐷) ↔ ((𝐴 − 𝐵) ≤ (𝐶 − 𝐷) ∧ (𝐴 − 𝐵) ≠ (𝐶 − 𝐷))))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 = wceq 1569 ∈ wcel 2144 ≠ wne 2955 ⊆ wss 3895 ∖ cdif 4045 class class class wbr 5102 I cid 5544 × cxp 5648 dom cdm 5650 ↾ cres 5652 “ cima 5653 Fun wfun 6532 ‘cfv 6538 (class class class)co 7420 Basecbs 17387 distcds 17437 TarskiGcstrkg 28889 Itvcitv 28895 ≤Gcleg 29045

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-10 2177 ax-12 2212 ax-ext 2732 ax-sep 5248 ax-nul 5259 ax-pr 5390

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2099 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-ne 2956 df-ral 3077 df-rex 3087 df-rab 3413 df-v 3452 df-ss 3896 df-dif 4047 df-in 4091 df-un 4151 df-nul 4279 df-if 4482 df-sn 4584 df-pr 4586 df-op 4590 df-uni 4867 df-br 5103 df-opab 5167 df-id 5545 df-xp 5656 df-rel 5657 df-cnv 5658 df-co 5659 df-dm 5660 df-rn 5661 df-res 5662 df-ima 5663 df-iota 6494 df-fun 6540 df-fn 6541 df-fv 6546 df-ov 7423

This theorem is used by: legov3 29061 legso 29062

W3C validator