Metamath Proof Explorer

Theorem legtri3

Description: Equality from the less-than relationship. Proposition 5.9 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 ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
legtri3.1 ⊢ ( 𝜑 → ( 𝐴 − 𝐵 ) ≤ ( 𝐶 − 𝐷 ) )
legtri3.2 ⊢ ( 𝜑 → ( 𝐶 − 𝐷 ) ≤ ( 𝐴 − 𝐵 ) )
Assertion legtri3 ( 𝜑 → ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝐷 ) )

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 legtri3.1 ⊢ ( 𝜑 → ( 𝐴 − 𝐵 ) ≤ ( 𝐶 − 𝐷 ) )
11 legtri3.2 ⊢ ( 𝜑 → ( 𝐶 − 𝐷 ) ≤ ( 𝐴 − 𝐵 ) )
12 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑥 ) ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐶 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐴 − 𝐵 ) ) ) → ( 𝑥 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑥 ) ) )
13 12 simprd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑥 ) ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐶 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐴 − 𝐵 ) ) ) → ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑥 ) )
14 5 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑥 ) ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐶 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐴 − 𝐵 ) ) ) → 𝐺 ∈ TarskiG )
15 simp-4r ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑥 ) ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐶 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐴 − 𝐵 ) ) ) → 𝑥 ∈ 𝑃 )
16 9 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑥 ) ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐶 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐴 − 𝐵 ) ) ) → 𝐷 ∈ 𝑃 )
17 8 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑥 ) ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐶 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐴 − 𝐵 ) ) ) → 𝐶 ∈ 𝑃 )
18 12 simpld ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑥 ) ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐶 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐴 − 𝐵 ) ) ) → 𝑥 ∈ ( 𝐶 𝐼 𝐷 ) )
19 1 2 3 14 17 15 16 18 tgbtwncom ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑥 ) ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐶 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐴 − 𝐵 ) ) ) → 𝑥 ∈ ( 𝐷 𝐼 𝐶 ) )
20 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑥 ) ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐶 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐴 − 𝐵 ) ) ) → ( 𝐷 ∈ ( 𝐶 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐴 − 𝐵 ) ) )
21 20 simpld ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑥 ) ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐶 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐴 − 𝐵 ) ) ) → 𝐷 ∈ ( 𝐶 𝐼 𝑦 ) )
22 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑥 ) ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐶 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐴 − 𝐵 ) ) ) → 𝑦 ∈ 𝑃 )
23 7 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑥 ) ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐶 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐴 − 𝐵 ) ) ) → 𝐵 ∈ 𝑃 )
24 6 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑥 ) ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐶 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐴 − 𝐵 ) ) ) → 𝐴 ∈ 𝑃 )
25 1 2 3 14 17 16 22 21 tgbtwncom ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑥 ) ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐶 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐴 − 𝐵 ) ) ) → 𝐷 ∈ ( 𝑦 𝐼 𝐶 ) )
26 1 2 3 14 22 16 15 17 25 19 tgbtwnexch2 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑥 ) ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐶 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐴 − 𝐵 ) ) ) → 𝑥 ∈ ( 𝑦 𝐼 𝐶 ) )
27 1 2 3 14 23 24 tgbtwntriv1 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑥 ) ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐶 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐴 − 𝐵 ) ) ) → 𝐵 ∈ ( 𝐵 𝐼 𝐴 ) )
28 20 simprd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑥 ) ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐶 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐴 − 𝐵 ) ) ) → ( 𝐶 − 𝑦 ) = ( 𝐴 − 𝐵 ) )
29 1 2 3 14 17 22 24 23 28 tgcgrcomlr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑥 ) ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐶 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐴 − 𝐵 ) ) ) → ( 𝑦 − 𝐶 ) = ( 𝐵 − 𝐴 ) )
30 13 eqcomd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑥 ) ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐶 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐴 − 𝐵 ) ) ) → ( 𝐶 − 𝑥 ) = ( 𝐴 − 𝐵 ) )
31 1 2 3 14 17 15 24 23 30 tgcgrcomlr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑥 ) ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐶 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐴 − 𝐵 ) ) ) → ( 𝑥 − 𝐶 ) = ( 𝐵 − 𝐴 ) )
32 1 2 3 14 22 15 17 23 23 24 26 27 29 31 tgcgrsub ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑥 ) ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐶 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐴 − 𝐵 ) ) ) → ( 𝑦 − 𝑥 ) = ( 𝐵 − 𝐵 ) )
33 1 2 3 14 22 15 23 32 axtgcgrid ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑥 ) ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐶 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐴 − 𝐵 ) ) ) → 𝑦 = 𝑥 )
34 33 oveq2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑥 ) ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐶 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐴 − 𝐵 ) ) ) → ( 𝐶 𝐼 𝑦 ) = ( 𝐶 𝐼 𝑥 ) )
35 21 34 eleqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑥 ) ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐶 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐴 − 𝐵 ) ) ) → 𝐷 ∈ ( 𝐶 𝐼 𝑥 ) )
36 1 2 3 14 17 16 15 35 tgbtwncom ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑥 ) ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐶 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐴 − 𝐵 ) ) ) → 𝐷 ∈ ( 𝑥 𝐼 𝐶 ) )
37 1 2 3 14 15 16 17 19 36 tgbtwnswapid ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑥 ) ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐶 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐴 − 𝐵 ) ) ) → 𝑥 = 𝐷 )
38 37 oveq2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑥 ) ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐶 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐴 − 𝐵 ) ) ) → ( 𝐶 − 𝑥 ) = ( 𝐶 − 𝐷 ) )
39 13 38 eqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑥 ) ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐶 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐴 − 𝐵 ) ) ) → ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝐷 ) )
40 1 2 3 4 5 8 9 6 7 legov2 ⊢ ( 𝜑 → ( ( 𝐶 − 𝐷 ) ≤ ( 𝐴 − 𝐵 ) ↔ ∃ 𝑦 ∈ 𝑃 ( 𝐷 ∈ ( 𝐶 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐴 − 𝐵 ) ) ) )
41 11 40 mpbid ⊢ ( 𝜑 → ∃ 𝑦 ∈ 𝑃 ( 𝐷 ∈ ( 𝐶 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐴 − 𝐵 ) ) )
42 41 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑥 ) ) ) → ∃ 𝑦 ∈ 𝑃 ( 𝐷 ∈ ( 𝐶 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐴 − 𝐵 ) ) )
43 39 42 r19.29a ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑥 ) ) ) → ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝐷 ) )
44 1 2 3 4 5 6 7 8 9 legov ⊢ ( 𝜑 → ( ( 𝐴 − 𝐵 ) ≤ ( 𝐶 − 𝐷 ) ↔ ∃ 𝑥 ∈ 𝑃 ( 𝑥 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑥 ) ) ) )
45 10 44 mpbid ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝑃 ( 𝑥 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝑥 ) ) )
46 43 45 r19.29a ⊢ ( 𝜑 → ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝐷 ) )