Metamath Proof Explorer


Theorem legtrid

Description: Trichotomy law for the less-than relationship. Proposition 5.10 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 ( 𝜑𝐷𝑃 )
Assertion legtrid ( 𝜑 → ( ( 𝐴 𝐵 ) ( 𝐶 𝐷 ) ∨ ( 𝐶 𝐷 ) ( 𝐴 𝐵 ) ) )

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 5 adantr ( ( 𝜑 ∧ ( ♯ ‘ 𝑃 ) = 1 ) → 𝐺 ∈ TarskiG )
11 6 adantr ( ( 𝜑 ∧ ( ♯ ‘ 𝑃 ) = 1 ) → 𝐴𝑃 )
12 7 adantr ( ( 𝜑 ∧ ( ♯ ‘ 𝑃 ) = 1 ) → 𝐵𝑃 )
13 1 2 3 4 10 11 12 legid ( ( 𝜑 ∧ ( ♯ ‘ 𝑃 ) = 1 ) → ( 𝐴 𝐵 ) ( 𝐴 𝐵 ) )
14 8 adantr ( ( 𝜑 ∧ ( ♯ ‘ 𝑃 ) = 1 ) → 𝐶𝑃 )
15 simpr ( ( 𝜑 ∧ ( ♯ ‘ 𝑃 ) = 1 ) → ( ♯ ‘ 𝑃 ) = 1 )
16 9 adantr ( ( 𝜑 ∧ ( ♯ ‘ 𝑃 ) = 1 ) → 𝐷𝑃 )
17 1 2 3 10 11 12 14 15 16 tgldim0cgr ( ( 𝜑 ∧ ( ♯ ‘ 𝑃 ) = 1 ) → ( 𝐴 𝐵 ) = ( 𝐶 𝐷 ) )
18 13 17 breqtrd ( ( 𝜑 ∧ ( ♯ ‘ 𝑃 ) = 1 ) → ( 𝐴 𝐵 ) ( 𝐶 𝐷 ) )
19 18 orcd ( ( 𝜑 ∧ ( ♯ ‘ 𝑃 ) = 1 ) → ( ( 𝐴 𝐵 ) ( 𝐶 𝐷 ) ∨ ( 𝐶 𝐷 ) ( 𝐴 𝐵 ) ) )
20 5 ad3antrrr ( ( ( ( 𝜑𝑥𝑃 ) ∧ ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ 𝐴𝑥 ) ) ∧ ( 𝑦𝑃 ∧ ( 𝐴 ∈ ( 𝑥 𝐼 𝑦 ) ∧ ( 𝐴 𝑦 ) = ( 𝐶 𝐷 ) ) ) ) → 𝐺 ∈ TarskiG )
21 simplr ( ( ( 𝜑𝑥𝑃 ) ∧ ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ 𝐴𝑥 ) ) → 𝑥𝑃 )
22 21 adantr ( ( ( ( 𝜑𝑥𝑃 ) ∧ ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ 𝐴𝑥 ) ) ∧ ( 𝑦𝑃 ∧ ( 𝐴 ∈ ( 𝑥 𝐼 𝑦 ) ∧ ( 𝐴 𝑦 ) = ( 𝐶 𝐷 ) ) ) ) → 𝑥𝑃 )
23 6 ad3antrrr ( ( ( ( 𝜑𝑥𝑃 ) ∧ ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ 𝐴𝑥 ) ) ∧ ( 𝑦𝑃 ∧ ( 𝐴 ∈ ( 𝑥 𝐼 𝑦 ) ∧ ( 𝐴 𝑦 ) = ( 𝐶 𝐷 ) ) ) ) → 𝐴𝑃 )
24 7 ad3antrrr ( ( ( ( 𝜑𝑥𝑃 ) ∧ ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ 𝐴𝑥 ) ) ∧ ( 𝑦𝑃 ∧ ( 𝐴 ∈ ( 𝑥 𝐼 𝑦 ) ∧ ( 𝐴 𝑦 ) = ( 𝐶 𝐷 ) ) ) ) → 𝐵𝑃 )
25 simprl ( ( ( ( 𝜑𝑥𝑃 ) ∧ ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ 𝐴𝑥 ) ) ∧ ( 𝑦𝑃 ∧ ( 𝐴 ∈ ( 𝑥 𝐼 𝑦 ) ∧ ( 𝐴 𝑦 ) = ( 𝐶 𝐷 ) ) ) ) → 𝑦𝑃 )
26 simplrr ( ( ( ( 𝜑𝑥𝑃 ) ∧ ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ 𝐴𝑥 ) ) ∧ ( 𝑦𝑃 ∧ ( 𝐴 ∈ ( 𝑥 𝐼 𝑦 ) ∧ ( 𝐴 𝑦 ) = ( 𝐶 𝐷 ) ) ) ) → 𝐴𝑥 )
27 26 necomd ( ( ( ( 𝜑𝑥𝑃 ) ∧ ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ 𝐴𝑥 ) ) ∧ ( 𝑦𝑃 ∧ ( 𝐴 ∈ ( 𝑥 𝐼 𝑦 ) ∧ ( 𝐴 𝑦 ) = ( 𝐶 𝐷 ) ) ) ) → 𝑥𝐴 )
28 simplrl ( ( ( ( 𝜑𝑥𝑃 ) ∧ ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ 𝐴𝑥 ) ) ∧ ( 𝑦𝑃 ∧ ( 𝐴 ∈ ( 𝑥 𝐼 𝑦 ) ∧ ( 𝐴 𝑦 ) = ( 𝐶 𝐷 ) ) ) ) → 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) )
29 1 2 3 20 24 23 22 28 tgbtwncom ( ( ( ( 𝜑𝑥𝑃 ) ∧ ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ 𝐴𝑥 ) ) ∧ ( 𝑦𝑃 ∧ ( 𝐴 ∈ ( 𝑥 𝐼 𝑦 ) ∧ ( 𝐴 𝑦 ) = ( 𝐶 𝐷 ) ) ) ) → 𝐴 ∈ ( 𝑥 𝐼 𝐵 ) )
30 simprrl ( ( ( ( 𝜑𝑥𝑃 ) ∧ ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ 𝐴𝑥 ) ) ∧ ( 𝑦𝑃 ∧ ( 𝐴 ∈ ( 𝑥 𝐼 𝑦 ) ∧ ( 𝐴 𝑦 ) = ( 𝐶 𝐷 ) ) ) ) → 𝐴 ∈ ( 𝑥 𝐼 𝑦 ) )
31 1 3 20 22 23 24 25 27 29 30 tgbtwnconn2 ( ( ( ( 𝜑𝑥𝑃 ) ∧ ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ 𝐴𝑥 ) ) ∧ ( 𝑦𝑃 ∧ ( 𝐴 ∈ ( 𝑥 𝐼 𝑦 ) ∧ ( 𝐴 𝑦 ) = ( 𝐶 𝐷 ) ) ) ) → ( 𝐵 ∈ ( 𝐴 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝐴 𝐼 𝐵 ) ) )
32 simprrr ( ( ( ( 𝜑𝑥𝑃 ) ∧ ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ 𝐴𝑥 ) ) ∧ ( 𝑦𝑃 ∧ ( 𝐴 ∈ ( 𝑥 𝐼 𝑦 ) ∧ ( 𝐴 𝑦 ) = ( 𝐶 𝐷 ) ) ) ) → ( 𝐴 𝑦 ) = ( 𝐶 𝐷 ) )
33 31 32 jca ( ( ( ( 𝜑𝑥𝑃 ) ∧ ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ 𝐴𝑥 ) ) ∧ ( 𝑦𝑃 ∧ ( 𝐴 ∈ ( 𝑥 𝐼 𝑦 ) ∧ ( 𝐴 𝑦 ) = ( 𝐶 𝐷 ) ) ) ) → ( ( 𝐵 ∈ ( 𝐴 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝐴 𝐼 𝐵 ) ) ∧ ( 𝐴 𝑦 ) = ( 𝐶 𝐷 ) ) )
34 5 ad2antrr ( ( ( 𝜑𝑥𝑃 ) ∧ ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ 𝐴𝑥 ) ) → 𝐺 ∈ TarskiG )
35 6 ad2antrr ( ( ( 𝜑𝑥𝑃 ) ∧ ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ 𝐴𝑥 ) ) → 𝐴𝑃 )
36 8 ad2antrr ( ( ( 𝜑𝑥𝑃 ) ∧ ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ 𝐴𝑥 ) ) → 𝐶𝑃 )
37 9 ad2antrr ( ( ( 𝜑𝑥𝑃 ) ∧ ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ 𝐴𝑥 ) ) → 𝐷𝑃 )
38 1 2 3 34 21 35 36 37 axtgsegcon ( ( ( 𝜑𝑥𝑃 ) ∧ ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ 𝐴𝑥 ) ) → ∃ 𝑦𝑃 ( 𝐴 ∈ ( 𝑥 𝐼 𝑦 ) ∧ ( 𝐴 𝑦 ) = ( 𝐶 𝐷 ) ) )
39 33 38 reximddv ( ( ( 𝜑𝑥𝑃 ) ∧ ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ 𝐴𝑥 ) ) → ∃ 𝑦𝑃 ( ( 𝐵 ∈ ( 𝐴 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝐴 𝐼 𝐵 ) ) ∧ ( 𝐴 𝑦 ) = ( 𝐶 𝐷 ) ) )
40 39 adantllr ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑥𝑃 ) ∧ ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ 𝐴𝑥 ) ) → ∃ 𝑦𝑃 ( ( 𝐵 ∈ ( 𝐴 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝐴 𝐼 𝐵 ) ) ∧ ( 𝐴 𝑦 ) = ( 𝐶 𝐷 ) ) )
41 5 adantr ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → 𝐺 ∈ TarskiG )
42 7 adantr ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → 𝐵𝑃 )
43 6 adantr ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → 𝐴𝑃 )
44 simpr ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → 2 ≤ ( ♯ ‘ 𝑃 ) )
45 1 2 3 41 42 43 44 tgbtwndiff ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ∃ 𝑥𝑃 ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ 𝐴𝑥 ) )
46 40 45 r19.29a ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ∃ 𝑦𝑃 ( ( 𝐵 ∈ ( 𝐴 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝐴 𝐼 𝐵 ) ) ∧ ( 𝐴 𝑦 ) = ( 𝐶 𝐷 ) ) )
47 andir ( ( ( 𝐵 ∈ ( 𝐴 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝐴 𝐼 𝐵 ) ) ∧ ( 𝐴 𝑦 ) = ( 𝐶 𝐷 ) ) ↔ ( ( 𝐵 ∈ ( 𝐴 𝐼 𝑦 ) ∧ ( 𝐴 𝑦 ) = ( 𝐶 𝐷 ) ) ∨ ( 𝑦 ∈ ( 𝐴 𝐼 𝐵 ) ∧ ( 𝐴 𝑦 ) = ( 𝐶 𝐷 ) ) ) )
48 eqcom ( ( 𝐴 𝑦 ) = ( 𝐶 𝐷 ) ↔ ( 𝐶 𝐷 ) = ( 𝐴 𝑦 ) )
49 48 anbi2i ( ( 𝑦 ∈ ( 𝐴 𝐼 𝐵 ) ∧ ( 𝐴 𝑦 ) = ( 𝐶 𝐷 ) ) ↔ ( 𝑦 ∈ ( 𝐴 𝐼 𝐵 ) ∧ ( 𝐶 𝐷 ) = ( 𝐴 𝑦 ) ) )
50 49 orbi2i ( ( ( 𝐵 ∈ ( 𝐴 𝐼 𝑦 ) ∧ ( 𝐴 𝑦 ) = ( 𝐶 𝐷 ) ) ∨ ( 𝑦 ∈ ( 𝐴 𝐼 𝐵 ) ∧ ( 𝐴 𝑦 ) = ( 𝐶 𝐷 ) ) ) ↔ ( ( 𝐵 ∈ ( 𝐴 𝐼 𝑦 ) ∧ ( 𝐴 𝑦 ) = ( 𝐶 𝐷 ) ) ∨ ( 𝑦 ∈ ( 𝐴 𝐼 𝐵 ) ∧ ( 𝐶 𝐷 ) = ( 𝐴 𝑦 ) ) ) )
51 47 50 bitri ( ( ( 𝐵 ∈ ( 𝐴 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝐴 𝐼 𝐵 ) ) ∧ ( 𝐴 𝑦 ) = ( 𝐶 𝐷 ) ) ↔ ( ( 𝐵 ∈ ( 𝐴 𝐼 𝑦 ) ∧ ( 𝐴 𝑦 ) = ( 𝐶 𝐷 ) ) ∨ ( 𝑦 ∈ ( 𝐴 𝐼 𝐵 ) ∧ ( 𝐶 𝐷 ) = ( 𝐴 𝑦 ) ) ) )
52 51 rexbii ( ∃ 𝑦𝑃 ( ( 𝐵 ∈ ( 𝐴 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝐴 𝐼 𝐵 ) ) ∧ ( 𝐴 𝑦 ) = ( 𝐶 𝐷 ) ) ↔ ∃ 𝑦𝑃 ( ( 𝐵 ∈ ( 𝐴 𝐼 𝑦 ) ∧ ( 𝐴 𝑦 ) = ( 𝐶 𝐷 ) ) ∨ ( 𝑦 ∈ ( 𝐴 𝐼 𝐵 ) ∧ ( 𝐶 𝐷 ) = ( 𝐴 𝑦 ) ) ) )
53 r19.43 ( ∃ 𝑦𝑃 ( ( 𝐵 ∈ ( 𝐴 𝐼 𝑦 ) ∧ ( 𝐴 𝑦 ) = ( 𝐶 𝐷 ) ) ∨ ( 𝑦 ∈ ( 𝐴 𝐼 𝐵 ) ∧ ( 𝐶 𝐷 ) = ( 𝐴 𝑦 ) ) ) ↔ ( ∃ 𝑦𝑃 ( 𝐵 ∈ ( 𝐴 𝐼 𝑦 ) ∧ ( 𝐴 𝑦 ) = ( 𝐶 𝐷 ) ) ∨ ∃ 𝑦𝑃 ( 𝑦 ∈ ( 𝐴 𝐼 𝐵 ) ∧ ( 𝐶 𝐷 ) = ( 𝐴 𝑦 ) ) ) )
54 52 53 bitri ( ∃ 𝑦𝑃 ( ( 𝐵 ∈ ( 𝐴 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝐴 𝐼 𝐵 ) ) ∧ ( 𝐴 𝑦 ) = ( 𝐶 𝐷 ) ) ↔ ( ∃ 𝑦𝑃 ( 𝐵 ∈ ( 𝐴 𝐼 𝑦 ) ∧ ( 𝐴 𝑦 ) = ( 𝐶 𝐷 ) ) ∨ ∃ 𝑦𝑃 ( 𝑦 ∈ ( 𝐴 𝐼 𝐵 ) ∧ ( 𝐶 𝐷 ) = ( 𝐴 𝑦 ) ) ) )
55 46 54 sylib ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( ∃ 𝑦𝑃 ( 𝐵 ∈ ( 𝐴 𝐼 𝑦 ) ∧ ( 𝐴 𝑦 ) = ( 𝐶 𝐷 ) ) ∨ ∃ 𝑦𝑃 ( 𝑦 ∈ ( 𝐴 𝐼 𝐵 ) ∧ ( 𝐶 𝐷 ) = ( 𝐴 𝑦 ) ) ) )
56 1 2 3 4 5 6 7 8 9 legov2 ( 𝜑 → ( ( 𝐴 𝐵 ) ( 𝐶 𝐷 ) ↔ ∃ 𝑦𝑃 ( 𝐵 ∈ ( 𝐴 𝐼 𝑦 ) ∧ ( 𝐴 𝑦 ) = ( 𝐶 𝐷 ) ) ) )
57 1 2 3 4 5 8 9 6 7 legov ( 𝜑 → ( ( 𝐶 𝐷 ) ( 𝐴 𝐵 ) ↔ ∃ 𝑦𝑃 ( 𝑦 ∈ ( 𝐴 𝐼 𝐵 ) ∧ ( 𝐶 𝐷 ) = ( 𝐴 𝑦 ) ) ) )
58 56 57 orbi12d ( 𝜑 → ( ( ( 𝐴 𝐵 ) ( 𝐶 𝐷 ) ∨ ( 𝐶 𝐷 ) ( 𝐴 𝐵 ) ) ↔ ( ∃ 𝑦𝑃 ( 𝐵 ∈ ( 𝐴 𝐼 𝑦 ) ∧ ( 𝐴 𝑦 ) = ( 𝐶 𝐷 ) ) ∨ ∃ 𝑦𝑃 ( 𝑦 ∈ ( 𝐴 𝐼 𝐵 ) ∧ ( 𝐶 𝐷 ) = ( 𝐴 𝑦 ) ) ) ) )
59 58 adantr ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( ( ( 𝐴 𝐵 ) ( 𝐶 𝐷 ) ∨ ( 𝐶 𝐷 ) ( 𝐴 𝐵 ) ) ↔ ( ∃ 𝑦𝑃 ( 𝐵 ∈ ( 𝐴 𝐼 𝑦 ) ∧ ( 𝐴 𝑦 ) = ( 𝐶 𝐷 ) ) ∨ ∃ 𝑦𝑃 ( 𝑦 ∈ ( 𝐴 𝐼 𝐵 ) ∧ ( 𝐶 𝐷 ) = ( 𝐴 𝑦 ) ) ) ) )
60 55 59 mpbird ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( ( 𝐴 𝐵 ) ( 𝐶 𝐷 ) ∨ ( 𝐶 𝐷 ) ( 𝐴 𝐵 ) ) )
61 1 6 tgldimor ( 𝜑 → ( ( ♯ ‘ 𝑃 ) = 1 ∨ 2 ≤ ( ♯ ‘ 𝑃 ) ) )
62 19 60 61 mpjaodan ( 𝜑 → ( ( 𝐴 𝐵 ) ( 𝐶 𝐷 ) ∨ ( 𝐶 𝐷 ) ( 𝐴 𝐵 ) ) )