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 âŠĒ ( 𝜑 → ( ðī − ðĩ ) = ( ðķ − 𝐷 ) )