This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem archiabllem2c

Description: Lemma for archiabl . (Contributed by Thierry Arnoux, 1-May-2018)

Ref Expression
Hypotheses archiabllem.b ⊢ 𝐵 = ( Base ‘ 𝑊 )
archiabllem.0 ⊢ 0 = ( 0g ‘ 𝑊 )
archiabllem.e ⊢ ≤ = ( le ‘ 𝑊 )
archiabllem.t ⊢ < = ( lt ‘ 𝑊 )
archiabllem.m ⊢ · = ( .g ‘ 𝑊 )
archiabllem.g ⊢ ( 𝜑 → 𝑊 ∈ oGrp )
archiabllem.a ⊢ ( 𝜑 → 𝑊 ∈ Archi )
archiabllem2.1 ⊢ + = ( +g ‘ 𝑊 )
archiabllem2.2 ⊢ ( 𝜑 → ( oppg ‘ 𝑊 ) ∈ oGrp )
archiabllem2.3 ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ∧ 0 < 𝑎 ) → ∃ 𝑏 ∈ 𝐵 ( 0 < 𝑏 ∧ 𝑏 < 𝑎 ) )
archiabllem2b.4 ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
archiabllem2b.5 ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
Assertion archiabllem2c ( 𝜑 → ¬ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) )

Proof

Step Hyp Ref Expression
1 archiabllem.b ⊢ 𝐵 = ( Base ‘ 𝑊 )
2 archiabllem.0 ⊢ 0 = ( 0g ‘ 𝑊 )
3 archiabllem.e ⊢ ≤ = ( le ‘ 𝑊 )
4 archiabllem.t ⊢ < = ( lt ‘ 𝑊 )
5 archiabllem.m ⊢ · = ( .g ‘ 𝑊 )
6 archiabllem.g ⊢ ( 𝜑 → 𝑊 ∈ oGrp )
7 archiabllem.a ⊢ ( 𝜑 → 𝑊 ∈ Archi )
8 archiabllem2.1 ⊢ + = ( +g ‘ 𝑊 )
9 archiabllem2.2 ⊢ ( 𝜑 → ( oppg ‘ 𝑊 ) ∈ oGrp )
10 archiabllem2.3 ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ∧ 0 < 𝑎 ) → ∃ 𝑏 ∈ 𝐵 ( 0 < 𝑏 ∧ 𝑏 < 𝑎 ) )
11 archiabllem2b.4 ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
12 archiabllem2b.5 ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
13 simprr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) ∧ 𝑡 ∈ 𝐵 ) ∧ ( 0 < 𝑡 ∧ ( 𝑡 + 𝑡 ) ≤ ( ( 𝑌 + 𝑋 ) ( -g ‘ 𝑊 ) ( 𝑋 + 𝑌 ) ) ) ) → ( 𝑡 + 𝑡 ) ≤ ( ( 𝑌 + 𝑋 ) ( -g ‘ 𝑊 ) ( 𝑋 + 𝑌 ) ) )
14 simpl1l ⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) ∧ 𝑡 ∈ 𝐵 ∧ 0 < 𝑡 ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ ( ( ( 𝑛 · 𝑡 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑛 + 1 ) · 𝑡 ) ) ∧ ( ( 𝑚 · 𝑡 ) < 𝑌 ∧ 𝑌 ≤ ( ( 𝑚 + 1 ) · 𝑡 ) ) ) ) ) → 𝜑 )
15 14 6 syl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) ∧ 𝑡 ∈ 𝐵 ∧ 0 < 𝑡 ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ ( ( ( 𝑛 · 𝑡 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑛 + 1 ) · 𝑡 ) ) ∧ ( ( 𝑚 · 𝑡 ) < 𝑌 ∧ 𝑌 ≤ ( ( 𝑚 + 1 ) · 𝑡 ) ) ) ) ) → 𝑊 ∈ oGrp )
16 simpl1r ⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) ∧ 𝑡 ∈ 𝐵 ∧ 0 < 𝑡 ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ ( ( ( 𝑛 · 𝑡 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑛 + 1 ) · 𝑡 ) ) ∧ ( ( 𝑚 · 𝑡 ) < 𝑌 ∧ 𝑌 ≤ ( ( 𝑚 + 1 ) · 𝑡 ) ) ) ) ) → ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) )
17 6 adantr ⊢ ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) → 𝑊 ∈ oGrp )
18 ogrpgrp ⊢ ( 𝑊 ∈ oGrp → 𝑊 ∈ Grp )
19 17 18 syl ⊢ ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) → 𝑊 ∈ Grp )
20 12 adantr ⊢ ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) → 𝑌 ∈ 𝐵 )
21 11 adantr ⊢ ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) → 𝑋 ∈ 𝐵 )
22 1 8 grpcl ⊢ ( ( 𝑊 ∈ Grp ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑌 + 𝑋 ) ∈ 𝐵 )
23 19 20 21 22 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) → ( 𝑌 + 𝑋 ) ∈ 𝐵 )
24 14 16 23 syl2anc ⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) ∧ 𝑡 ∈ 𝐵 ∧ 0 < 𝑡 ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ ( ( ( 𝑛 · 𝑡 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑛 + 1 ) · 𝑡 ) ) ∧ ( ( 𝑚 · 𝑡 ) < 𝑌 ∧ 𝑌 ≤ ( ( 𝑚 + 1 ) · 𝑡 ) ) ) ) ) → ( 𝑌 + 𝑋 ) ∈ 𝐵 )
25 14 6 18 3syl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) ∧ 𝑡 ∈ 𝐵 ∧ 0 < 𝑡 ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ ( ( ( 𝑛 · 𝑡 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑛 + 1 ) · 𝑡 ) ) ∧ ( ( 𝑚 · 𝑡 ) < 𝑌 ∧ 𝑌 ≤ ( ( 𝑚 + 1 ) · 𝑡 ) ) ) ) ) → 𝑊 ∈ Grp )
26 simpr2 ⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) ∧ 𝑡 ∈ 𝐵 ∧ 0 < 𝑡 ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ ( ( ( 𝑛 · 𝑡 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑛 + 1 ) · 𝑡 ) ) ∧ ( ( 𝑚 · 𝑡 ) < 𝑌 ∧ 𝑌 ≤ ( ( 𝑚 + 1 ) · 𝑡 ) ) ) ) ) → 𝑚 ∈ ℤ )
27 26 peano2zd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) ∧ 𝑡 ∈ 𝐵 ∧ 0 < 𝑡 ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ ( ( ( 𝑛 · 𝑡 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑛 + 1 ) · 𝑡 ) ) ∧ ( ( 𝑚 · 𝑡 ) < 𝑌 ∧ 𝑌 ≤ ( ( 𝑚 + 1 ) · 𝑡 ) ) ) ) ) → ( 𝑚 + 1 ) ∈ ℤ )
28 simp2 ⊢ ( ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) ∧ 𝑡 ∈ 𝐵 ∧ 0 < 𝑡 ) → 𝑡 ∈ 𝐵 )
29 28 adantr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) ∧ 𝑡 ∈ 𝐵 ∧ 0 < 𝑡 ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ ( ( ( 𝑛 · 𝑡 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑛 + 1 ) · 𝑡 ) ) ∧ ( ( 𝑚 · 𝑡 ) < 𝑌 ∧ 𝑌 ≤ ( ( 𝑚 + 1 ) · 𝑡 ) ) ) ) ) → 𝑡 ∈ 𝐵 )
30 1 5 mulgcl ⊢ ( ( 𝑊 ∈ Grp ∧ ( 𝑚 + 1 ) ∈ ℤ ∧ 𝑡 ∈ 𝐵 ) → ( ( 𝑚 + 1 ) · 𝑡 ) ∈ 𝐵 )
31 25 27 29 30 syl3anc ⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) ∧ 𝑡 ∈ 𝐵 ∧ 0 < 𝑡 ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ ( ( ( 𝑛 · 𝑡 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑛 + 1 ) · 𝑡 ) ) ∧ ( ( 𝑚 · 𝑡 ) < 𝑌 ∧ 𝑌 ≤ ( ( 𝑚 + 1 ) · 𝑡 ) ) ) ) ) → ( ( 𝑚 + 1 ) · 𝑡 ) ∈ 𝐵 )
32 simpr1 ⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) ∧ 𝑡 ∈ 𝐵 ∧ 0 < 𝑡 ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ ( ( ( 𝑛 · 𝑡 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑛 + 1 ) · 𝑡 ) ) ∧ ( ( 𝑚 · 𝑡 ) < 𝑌 ∧ 𝑌 ≤ ( ( 𝑚 + 1 ) · 𝑡 ) ) ) ) ) → 𝑛 ∈ ℤ )
33 32 peano2zd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) ∧ 𝑡 ∈ 𝐵 ∧ 0 < 𝑡 ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ ( ( ( 𝑛 · 𝑡 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑛 + 1 ) · 𝑡 ) ) ∧ ( ( 𝑚 · 𝑡 ) < 𝑌 ∧ 𝑌 ≤ ( ( 𝑚 + 1 ) · 𝑡 ) ) ) ) ) → ( 𝑛 + 1 ) ∈ ℤ )
34 1 5 mulgcl ⊢ ( ( 𝑊 ∈ Grp ∧ ( 𝑛 + 1 ) ∈ ℤ ∧ 𝑡 ∈ 𝐵 ) → ( ( 𝑛 + 1 ) · 𝑡 ) ∈ 𝐵 )
35 25 33 29 34 syl3anc ⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) ∧ 𝑡 ∈ 𝐵 ∧ 0 < 𝑡 ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ ( ( ( 𝑛 · 𝑡 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑛 + 1 ) · 𝑡 ) ) ∧ ( ( 𝑚 · 𝑡 ) < 𝑌 ∧ 𝑌 ≤ ( ( 𝑚 + 1 ) · 𝑡 ) ) ) ) ) → ( ( 𝑛 + 1 ) · 𝑡 ) ∈ 𝐵 )
36 1 8 grpcl ⊢ ( ( 𝑊 ∈ Grp ∧ ( ( 𝑚 + 1 ) · 𝑡 ) ∈ 𝐵 ∧ ( ( 𝑛 + 1 ) · 𝑡 ) ∈ 𝐵 ) → ( ( ( 𝑚 + 1 ) · 𝑡 ) + ( ( 𝑛 + 1 ) · 𝑡 ) ) ∈ 𝐵 )
37 25 31 35 36 syl3anc ⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) ∧ 𝑡 ∈ 𝐵 ∧ 0 < 𝑡 ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ ( ( ( 𝑛 · 𝑡 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑛 + 1 ) · 𝑡 ) ) ∧ ( ( 𝑚 · 𝑡 ) < 𝑌 ∧ 𝑌 ≤ ( ( 𝑚 + 1 ) · 𝑡 ) ) ) ) ) → ( ( ( 𝑚 + 1 ) · 𝑡 ) + ( ( 𝑛 + 1 ) · 𝑡 ) ) ∈ 𝐵 )
38 21 3ad2ant1 ⊢ ( ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) ∧ 𝑡 ∈ 𝐵 ∧ 0 < 𝑡 ) → 𝑋 ∈ 𝐵 )
39 38 adantr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) ∧ 𝑡 ∈ 𝐵 ∧ 0 < 𝑡 ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ ( ( ( 𝑛 · 𝑡 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑛 + 1 ) · 𝑡 ) ) ∧ ( ( 𝑚 · 𝑡 ) < 𝑌 ∧ 𝑌 ≤ ( ( 𝑚 + 1 ) · 𝑡 ) ) ) ) ) → 𝑋 ∈ 𝐵 )
40 20 3ad2ant1 ⊢ ( ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) ∧ 𝑡 ∈ 𝐵 ∧ 0 < 𝑡 ) → 𝑌 ∈ 𝐵 )
41 40 adantr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) ∧ 𝑡 ∈ 𝐵 ∧ 0 < 𝑡 ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ ( ( ( 𝑛 · 𝑡 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑛 + 1 ) · 𝑡 ) ) ∧ ( ( 𝑚 · 𝑡 ) < 𝑌 ∧ 𝑌 ≤ ( ( 𝑚 + 1 ) · 𝑡 ) ) ) ) ) → 𝑌 ∈ 𝐵 )
42 1 8 grpcl ⊢ ( ( 𝑊 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 + 𝑌 ) ∈ 𝐵 )
43 25 39 41 42 syl3anc ⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) ∧ 𝑡 ∈ 𝐵 ∧ 0 < 𝑡 ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ ( ( ( 𝑛 · 𝑡 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑛 + 1 ) · 𝑡 ) ) ∧ ( ( 𝑚 · 𝑡 ) < 𝑌 ∧ 𝑌 ≤ ( ( 𝑚 + 1 ) · 𝑡 ) ) ) ) ) → ( 𝑋 + 𝑌 ) ∈ 𝐵 )
44 isogrp ⊢ ( 𝑊 ∈ oGrp ↔ ( 𝑊 ∈ Grp ∧ 𝑊 ∈ oMnd ) )
45 44 simprbi ⊢ ( 𝑊 ∈ oGrp → 𝑊 ∈ oMnd )
46 14 6 45 3syl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) ∧ 𝑡 ∈ 𝐵 ∧ 0 < 𝑡 ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ ( ( ( 𝑛 · 𝑡 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑛 + 1 ) · 𝑡 ) ) ∧ ( ( 𝑚 · 𝑡 ) < 𝑌 ∧ 𝑌 ≤ ( ( 𝑚 + 1 ) · 𝑡 ) ) ) ) ) → 𝑊 ∈ oMnd )
47 simpr3 ⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) ∧ 𝑡 ∈ 𝐵 ∧ 0 < 𝑡 ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ ( ( ( 𝑛 · 𝑡 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑛 + 1 ) · 𝑡 ) ) ∧ ( ( 𝑚 · 𝑡 ) < 𝑌 ∧ 𝑌 ≤ ( ( 𝑚 + 1 ) · 𝑡 ) ) ) ) ) → ( ( ( 𝑛 · 𝑡 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑛 + 1 ) · 𝑡 ) ) ∧ ( ( 𝑚 · 𝑡 ) < 𝑌 ∧ 𝑌 ≤ ( ( 𝑚 + 1 ) · 𝑡 ) ) ) )
48 47 simprd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) ∧ 𝑡 ∈ 𝐵 ∧ 0 < 𝑡 ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ ( ( ( 𝑛 · 𝑡 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑛 + 1 ) · 𝑡 ) ) ∧ ( ( 𝑚 · 𝑡 ) < 𝑌 ∧ 𝑌 ≤ ( ( 𝑚 + 1 ) · 𝑡 ) ) ) ) ) → ( ( 𝑚 · 𝑡 ) < 𝑌 ∧ 𝑌 ≤ ( ( 𝑚 + 1 ) · 𝑡 ) ) )
49 48 simprd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) ∧ 𝑡 ∈ 𝐵 ∧ 0 < 𝑡 ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ ( ( ( 𝑛 · 𝑡 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑛 + 1 ) · 𝑡 ) ) ∧ ( ( 𝑚 · 𝑡 ) < 𝑌 ∧ 𝑌 ≤ ( ( 𝑚 + 1 ) · 𝑡 ) ) ) ) ) → 𝑌 ≤ ( ( 𝑚 + 1 ) · 𝑡 ) )
50 47 simpld ⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) ∧ 𝑡 ∈ 𝐵 ∧ 0 < 𝑡 ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ ( ( ( 𝑛 · 𝑡 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑛 + 1 ) · 𝑡 ) ) ∧ ( ( 𝑚 · 𝑡 ) < 𝑌 ∧ 𝑌 ≤ ( ( 𝑚 + 1 ) · 𝑡 ) ) ) ) ) → ( ( 𝑛 · 𝑡 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑛 + 1 ) · 𝑡 ) ) )
51 50 simprd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) ∧ 𝑡 ∈ 𝐵 ∧ 0 < 𝑡 ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ ( ( ( 𝑛 · 𝑡 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑛 + 1 ) · 𝑡 ) ) ∧ ( ( 𝑚 · 𝑡 ) < 𝑌 ∧ 𝑌 ≤ ( ( 𝑚 + 1 ) · 𝑡 ) ) ) ) ) → 𝑋 ≤ ( ( 𝑛 + 1 ) · 𝑡 ) )
52 isogrp ⊢ ( ( oppg ‘ 𝑊 ) ∈ oGrp ↔ ( ( oppg ‘ 𝑊 ) ∈ Grp ∧ ( oppg ‘ 𝑊 ) ∈ oMnd ) )
53 52 simprbi ⊢ ( ( oppg ‘ 𝑊 ) ∈ oGrp → ( oppg ‘ 𝑊 ) ∈ oMnd )
54 14 9 53 3syl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) ∧ 𝑡 ∈ 𝐵 ∧ 0 < 𝑡 ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ ( ( ( 𝑛 · 𝑡 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑛 + 1 ) · 𝑡 ) ) ∧ ( ( 𝑚 · 𝑡 ) < 𝑌 ∧ 𝑌 ≤ ( ( 𝑚 + 1 ) · 𝑡 ) ) ) ) ) → ( oppg ‘ 𝑊 ) ∈ oMnd )
55 1 3 8 46 35 41 39 31 49 51 54 omndadd2rd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) ∧ 𝑡 ∈ 𝐵 ∧ 0 < 𝑡 ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ ( ( ( 𝑛 · 𝑡 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑛 + 1 ) · 𝑡 ) ) ∧ ( ( 𝑚 · 𝑡 ) < 𝑌 ∧ 𝑌 ≤ ( ( 𝑚 + 1 ) · 𝑡 ) ) ) ) ) → ( 𝑌 + 𝑋 ) ≤ ( ( ( 𝑚 + 1 ) · 𝑡 ) + ( ( 𝑛 + 1 ) · 𝑡 ) ) )
56 eqid ⊢ ( -g ‘ 𝑊 ) = ( -g ‘ 𝑊 )
57 1 3 56 ogrpsub ⊢ ( ( 𝑊 ∈ oGrp ∧ ( ( 𝑌 + 𝑋 ) ∈ 𝐵 ∧ ( ( ( 𝑚 + 1 ) · 𝑡 ) + ( ( 𝑛 + 1 ) · 𝑡 ) ) ∈ 𝐵 ∧ ( 𝑋 + 𝑌 ) ∈ 𝐵 ) ∧ ( 𝑌 + 𝑋 ) ≤ ( ( ( 𝑚 + 1 ) · 𝑡 ) + ( ( 𝑛 + 1 ) · 𝑡 ) ) ) → ( ( 𝑌 + 𝑋 ) ( -g ‘ 𝑊 ) ( 𝑋 + 𝑌 ) ) ≤ ( ( ( ( 𝑚 + 1 ) · 𝑡 ) + ( ( 𝑛 + 1 ) · 𝑡 ) ) ( -g ‘ 𝑊 ) ( 𝑋 + 𝑌 ) ) )
58 15 24 37 43 55 57 syl131anc ⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) ∧ 𝑡 ∈ 𝐵 ∧ 0 < 𝑡 ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ ( ( ( 𝑛 · 𝑡 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑛 + 1 ) · 𝑡 ) ) ∧ ( ( 𝑚 · 𝑡 ) < 𝑌 ∧ 𝑌 ≤ ( ( 𝑚 + 1 ) · 𝑡 ) ) ) ) ) → ( ( 𝑌 + 𝑋 ) ( -g ‘ 𝑊 ) ( 𝑋 + 𝑌 ) ) ≤ ( ( ( ( 𝑚 + 1 ) · 𝑡 ) + ( ( 𝑛 + 1 ) · 𝑡 ) ) ( -g ‘ 𝑊 ) ( 𝑋 + 𝑌 ) ) )
59 26 zcnd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) ∧ 𝑡 ∈ 𝐵 ∧ 0 < 𝑡 ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ ( ( ( 𝑛 · 𝑡 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑛 + 1 ) · 𝑡 ) ) ∧ ( ( 𝑚 · 𝑡 ) < 𝑌 ∧ 𝑌 ≤ ( ( 𝑚 + 1 ) · 𝑡 ) ) ) ) ) → 𝑚 ∈ ℂ )
60 32 zcnd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) ∧ 𝑡 ∈ 𝐵 ∧ 0 < 𝑡 ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ ( ( ( 𝑛 · 𝑡 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑛 + 1 ) · 𝑡 ) ) ∧ ( ( 𝑚 · 𝑡 ) < 𝑌 ∧ 𝑌 ≤ ( ( 𝑚 + 1 ) · 𝑡 ) ) ) ) ) → 𝑛 ∈ ℂ )
61 1cnd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) ∧ 𝑡 ∈ 𝐵 ∧ 0 < 𝑡 ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ ( ( ( 𝑛 · 𝑡 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑛 + 1 ) · 𝑡 ) ) ∧ ( ( 𝑚 · 𝑡 ) < 𝑌 ∧ 𝑌 ≤ ( ( 𝑚 + 1 ) · 𝑡 ) ) ) ) ) → 1 ∈ ℂ )
62 59 60 61 61 add4d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) ∧ 𝑡 ∈ 𝐵 ∧ 0 < 𝑡 ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ ( ( ( 𝑛 · 𝑡 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑛 + 1 ) · 𝑡 ) ) ∧ ( ( 𝑚 · 𝑡 ) < 𝑌 ∧ 𝑌 ≤ ( ( 𝑚 + 1 ) · 𝑡 ) ) ) ) ) → ( ( 𝑚 + 𝑛 ) + ( 1 + 1 ) ) = ( ( 𝑚 + 1 ) + ( 𝑛 + 1 ) ) )
63 1p1e2 ⊢ ( 1 + 1 ) = 2
64 63 oveq2i ⊢ ( ( 𝑚 + 𝑛 ) + ( 1 + 1 ) ) = ( ( 𝑚 + 𝑛 ) + 2 )
65 addcom ⊢ ( ( 𝑚 ∈ ℂ ∧ 𝑛 ∈ ℂ ) → ( 𝑚 + 𝑛 ) = ( 𝑛 + 𝑚 ) )
66 65 oveq1d ⊢ ( ( 𝑚 ∈ ℂ ∧ 𝑛 ∈ ℂ ) → ( ( 𝑚 + 𝑛 ) + 2 ) = ( ( 𝑛 + 𝑚 ) + 2 ) )
67 64 66 eqtrid ⊢ ( ( 𝑚 ∈ ℂ ∧ 𝑛 ∈ ℂ ) → ( ( 𝑚 + 𝑛 ) + ( 1 + 1 ) ) = ( ( 𝑛 + 𝑚 ) + 2 ) )
68 2cnd ⊢ ( ( 𝑚 ∈ ℂ ∧ 𝑛 ∈ ℂ ) → 2 ∈ ℂ )
69 simpr ⊢ ( ( 𝑚 ∈ ℂ ∧ 𝑛 ∈ ℂ ) → 𝑛 ∈ ℂ )
70 simpl ⊢ ( ( 𝑚 ∈ ℂ ∧ 𝑛 ∈ ℂ ) → 𝑚 ∈ ℂ )
71 69 70 addcld ⊢ ( ( 𝑚 ∈ ℂ ∧ 𝑛 ∈ ℂ ) → ( 𝑛 + 𝑚 ) ∈ ℂ )
72 68 71 addcomd ⊢ ( ( 𝑚 ∈ ℂ ∧ 𝑛 ∈ ℂ ) → ( 2 + ( 𝑛 + 𝑚 ) ) = ( ( 𝑛 + 𝑚 ) + 2 ) )
73 67 72 eqtr4d ⊢ ( ( 𝑚 ∈ ℂ ∧ 𝑛 ∈ ℂ ) → ( ( 𝑚 + 𝑛 ) + ( 1 + 1 ) ) = ( 2 + ( 𝑛 + 𝑚 ) ) )
74 59 60 73 syl2anc ⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) ∧ 𝑡 ∈ 𝐵 ∧ 0 < 𝑡 ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ ( ( ( 𝑛 · 𝑡 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑛 + 1 ) · 𝑡 ) ) ∧ ( ( 𝑚 · 𝑡 ) < 𝑌 ∧ 𝑌 ≤ ( ( 𝑚 + 1 ) · 𝑡 ) ) ) ) ) → ( ( 𝑚 + 𝑛 ) + ( 1 + 1 ) ) = ( 2 + ( 𝑛 + 𝑚 ) ) )
75 62 74 eqtr3d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) ∧ 𝑡 ∈ 𝐵 ∧ 0 < 𝑡 ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ ( ( ( 𝑛 · 𝑡 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑛 + 1 ) · 𝑡 ) ) ∧ ( ( 𝑚 · 𝑡 ) < 𝑌 ∧ 𝑌 ≤ ( ( 𝑚 + 1 ) · 𝑡 ) ) ) ) ) → ( ( 𝑚 + 1 ) + ( 𝑛 + 1 ) ) = ( 2 + ( 𝑛 + 𝑚 ) ) )
76 75 oveq1d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) ∧ 𝑡 ∈ 𝐵 ∧ 0 < 𝑡 ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ ( ( ( 𝑛 · 𝑡 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑛 + 1 ) · 𝑡 ) ) ∧ ( ( 𝑚 · 𝑡 ) < 𝑌 ∧ 𝑌 ≤ ( ( 𝑚 + 1 ) · 𝑡 ) ) ) ) ) → ( ( ( 𝑚 + 1 ) + ( 𝑛 + 1 ) ) · 𝑡 ) = ( ( 2 + ( 𝑛 + 𝑚 ) ) · 𝑡 ) )
77 2z ⊢ 2 ∈ ℤ
78 77 a1i ⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) ∧ 𝑡 ∈ 𝐵 ∧ 0 < 𝑡 ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ ( ( ( 𝑛 · 𝑡 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑛 + 1 ) · 𝑡 ) ) ∧ ( ( 𝑚 · 𝑡 ) < 𝑌 ∧ 𝑌 ≤ ( ( 𝑚 + 1 ) · 𝑡 ) ) ) ) ) → 2 ∈ ℤ )
79 32 26 zaddcld ⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) ∧ 𝑡 ∈ 𝐵 ∧ 0 < 𝑡 ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ ( ( ( 𝑛 · 𝑡 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑛 + 1 ) · 𝑡 ) ) ∧ ( ( 𝑚 · 𝑡 ) < 𝑌 ∧ 𝑌 ≤ ( ( 𝑚 + 1 ) · 𝑡 ) ) ) ) ) → ( 𝑛 + 𝑚 ) ∈ ℤ )
80 1 5 8 mulgdir ⊢ ( ( 𝑊 ∈ Grp ∧ ( 2 ∈ ℤ ∧ ( 𝑛 + 𝑚 ) ∈ ℤ ∧ 𝑡 ∈ 𝐵 ) ) → ( ( 2 + ( 𝑛 + 𝑚 ) ) · 𝑡 ) = ( ( 2 · 𝑡 ) + ( ( 𝑛 + 𝑚 ) · 𝑡 ) ) )
81 25 78 79 29 80 syl13anc ⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) ∧ 𝑡 ∈ 𝐵 ∧ 0 < 𝑡 ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ ( ( ( 𝑛 · 𝑡 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑛 + 1 ) · 𝑡 ) ) ∧ ( ( 𝑚 · 𝑡 ) < 𝑌 ∧ 𝑌 ≤ ( ( 𝑚 + 1 ) · 𝑡 ) ) ) ) ) → ( ( 2 + ( 𝑛 + 𝑚 ) ) · 𝑡 ) = ( ( 2 · 𝑡 ) + ( ( 𝑛 + 𝑚 ) · 𝑡 ) ) )
82 76 81 eqtrd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) ∧ 𝑡 ∈ 𝐵 ∧ 0 < 𝑡 ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ ( ( ( 𝑛 · 𝑡 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑛 + 1 ) · 𝑡 ) ) ∧ ( ( 𝑚 · 𝑡 ) < 𝑌 ∧ 𝑌 ≤ ( ( 𝑚 + 1 ) · 𝑡 ) ) ) ) ) → ( ( ( 𝑚 + 1 ) + ( 𝑛 + 1 ) ) · 𝑡 ) = ( ( 2 · 𝑡 ) + ( ( 𝑛 + 𝑚 ) · 𝑡 ) ) )
83 1 5 8 mulgdir ⊢ ( ( 𝑊 ∈ Grp ∧ ( ( 𝑚 + 1 ) ∈ ℤ ∧ ( 𝑛 + 1 ) ∈ ℤ ∧ 𝑡 ∈ 𝐵 ) ) → ( ( ( 𝑚 + 1 ) + ( 𝑛 + 1 ) ) · 𝑡 ) = ( ( ( 𝑚 + 1 ) · 𝑡 ) + ( ( 𝑛 + 1 ) · 𝑡 ) ) )
84 25 27 33 29 83 syl13anc ⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) ∧ 𝑡 ∈ 𝐵 ∧ 0 < 𝑡 ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ ( ( ( 𝑛 · 𝑡 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑛 + 1 ) · 𝑡 ) ) ∧ ( ( 𝑚 · 𝑡 ) < 𝑌 ∧ 𝑌 ≤ ( ( 𝑚 + 1 ) · 𝑡 ) ) ) ) ) → ( ( ( 𝑚 + 1 ) + ( 𝑛 + 1 ) ) · 𝑡 ) = ( ( ( 𝑚 + 1 ) · 𝑡 ) + ( ( 𝑛 + 1 ) · 𝑡 ) ) )
85 1 5 8 mulg2 ⊢ ( 𝑡 ∈ 𝐵 → ( 2 · 𝑡 ) = ( 𝑡 + 𝑡 ) )
86 29 85 syl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) ∧ 𝑡 ∈ 𝐵 ∧ 0 < 𝑡 ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ ( ( ( 𝑛 · 𝑡 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑛 + 1 ) · 𝑡 ) ) ∧ ( ( 𝑚 · 𝑡 ) < 𝑌 ∧ 𝑌 ≤ ( ( 𝑚 + 1 ) · 𝑡 ) ) ) ) ) → ( 2 · 𝑡 ) = ( 𝑡 + 𝑡 ) )
87 86 oveq1d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) ∧ 𝑡 ∈ 𝐵 ∧ 0 < 𝑡 ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ ( ( ( 𝑛 · 𝑡 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑛 + 1 ) · 𝑡 ) ) ∧ ( ( 𝑚 · 𝑡 ) < 𝑌 ∧ 𝑌 ≤ ( ( 𝑚 + 1 ) · 𝑡 ) ) ) ) ) → ( ( 2 · 𝑡 ) + ( ( 𝑛 + 𝑚 ) · 𝑡 ) ) = ( ( 𝑡 + 𝑡 ) + ( ( 𝑛 + 𝑚 ) · 𝑡 ) ) )
88 82 84 87 3eqtr3d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) ∧ 𝑡 ∈ 𝐵 ∧ 0 < 𝑡 ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ ( ( ( 𝑛 · 𝑡 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑛 + 1 ) · 𝑡 ) ) ∧ ( ( 𝑚 · 𝑡 ) < 𝑌 ∧ 𝑌 ≤ ( ( 𝑚 + 1 ) · 𝑡 ) ) ) ) ) → ( ( ( 𝑚 + 1 ) · 𝑡 ) + ( ( 𝑛 + 1 ) · 𝑡 ) ) = ( ( 𝑡 + 𝑡 ) + ( ( 𝑛 + 𝑚 ) · 𝑡 ) ) )
89 88 oveq1d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) ∧ 𝑡 ∈ 𝐵 ∧ 0 < 𝑡 ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ ( ( ( 𝑛 · 𝑡 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑛 + 1 ) · 𝑡 ) ) ∧ ( ( 𝑚 · 𝑡 ) < 𝑌 ∧ 𝑌 ≤ ( ( 𝑚 + 1 ) · 𝑡 ) ) ) ) ) → ( ( ( ( 𝑚 + 1 ) · 𝑡 ) + ( ( 𝑛 + 1 ) · 𝑡 ) ) ( -g ‘ 𝑊 ) ( 𝑋 + 𝑌 ) ) = ( ( ( 𝑡 + 𝑡 ) + ( ( 𝑛 + 𝑚 ) · 𝑡 ) ) ( -g ‘ 𝑊 ) ( 𝑋 + 𝑌 ) ) )
90 58 89 breqtrd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) ∧ 𝑡 ∈ 𝐵 ∧ 0 < 𝑡 ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ ( ( ( 𝑛 · 𝑡 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑛 + 1 ) · 𝑡 ) ) ∧ ( ( 𝑚 · 𝑡 ) < 𝑌 ∧ 𝑌 ≤ ( ( 𝑚 + 1 ) · 𝑡 ) ) ) ) ) → ( ( 𝑌 + 𝑋 ) ( -g ‘ 𝑊 ) ( 𝑋 + 𝑌 ) ) ≤ ( ( ( 𝑡 + 𝑡 ) + ( ( 𝑛 + 𝑚 ) · 𝑡 ) ) ( -g ‘ 𝑊 ) ( 𝑋 + 𝑌 ) ) )
91 88 37 eqeltrrd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) ∧ 𝑡 ∈ 𝐵 ∧ 0 < 𝑡 ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ ( ( ( 𝑛 · 𝑡 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑛 + 1 ) · 𝑡 ) ) ∧ ( ( 𝑚 · 𝑡 ) < 𝑌 ∧ 𝑌 ≤ ( ( 𝑚 + 1 ) · 𝑡 ) ) ) ) ) → ( ( 𝑡 + 𝑡 ) + ( ( 𝑛 + 𝑚 ) · 𝑡 ) ) ∈ 𝐵 )
92 eqid ⊢ ( invg ‘ 𝑊 ) = ( invg ‘ 𝑊 )
93 1 8 92 56 grpsubval ⊢ ( ( ( ( 𝑡 + 𝑡 ) + ( ( 𝑛 + 𝑚 ) · 𝑡 ) ) ∈ 𝐵 ∧ ( 𝑋 + 𝑌 ) ∈ 𝐵 ) → ( ( ( 𝑡 + 𝑡 ) + ( ( 𝑛 + 𝑚 ) · 𝑡 ) ) ( -g ‘ 𝑊 ) ( 𝑋 + 𝑌 ) ) = ( ( ( 𝑡 + 𝑡 ) + ( ( 𝑛 + 𝑚 ) · 𝑡 ) ) + ( ( invg ‘ 𝑊 ) ‘ ( 𝑋 + 𝑌 ) ) ) )
94 91 43 93 syl2anc ⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) ∧ 𝑡 ∈ 𝐵 ∧ 0 < 𝑡 ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ ( ( ( 𝑛 · 𝑡 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑛 + 1 ) · 𝑡 ) ) ∧ ( ( 𝑚 · 𝑡 ) < 𝑌 ∧ 𝑌 ≤ ( ( 𝑚 + 1 ) · 𝑡 ) ) ) ) ) → ( ( ( 𝑡 + 𝑡 ) + ( ( 𝑛 + 𝑚 ) · 𝑡 ) ) ( -g ‘ 𝑊 ) ( 𝑋 + 𝑌 ) ) = ( ( ( 𝑡 + 𝑡 ) + ( ( 𝑛 + 𝑚 ) · 𝑡 ) ) + ( ( invg ‘ 𝑊 ) ‘ ( 𝑋 + 𝑌 ) ) ) )
95 90 94 breqtrd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) ∧ 𝑡 ∈ 𝐵 ∧ 0 < 𝑡 ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ ( ( ( 𝑛 · 𝑡 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑛 + 1 ) · 𝑡 ) ) ∧ ( ( 𝑚 · 𝑡 ) < 𝑌 ∧ 𝑌 ≤ ( ( 𝑚 + 1 ) · 𝑡 ) ) ) ) ) → ( ( 𝑌 + 𝑋 ) ( -g ‘ 𝑊 ) ( 𝑋 + 𝑌 ) ) ≤ ( ( ( 𝑡 + 𝑡 ) + ( ( 𝑛 + 𝑚 ) · 𝑡 ) ) + ( ( invg ‘ 𝑊 ) ‘ ( 𝑋 + 𝑌 ) ) ) )
96 14 9 syl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) ∧ 𝑡 ∈ 𝐵 ∧ 0 < 𝑡 ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ ( ( ( 𝑛 · 𝑡 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑛 + 1 ) · 𝑡 ) ) ∧ ( ( 𝑚 · 𝑡 ) < 𝑌 ∧ 𝑌 ≤ ( ( 𝑚 + 1 ) · 𝑡 ) ) ) ) ) → ( oppg ‘ 𝑊 ) ∈ oGrp )
97 1 92 grpinvcl ⊢ ( ( 𝑊 ∈ Grp ∧ ( 𝑋 + 𝑌 ) ∈ 𝐵 ) → ( ( invg ‘ 𝑊 ) ‘ ( 𝑋 + 𝑌 ) ) ∈ 𝐵 )
98 25 43 97 syl2anc ⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) ∧ 𝑡 ∈ 𝐵 ∧ 0 < 𝑡 ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ ( ( ( 𝑛 · 𝑡 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑛 + 1 ) · 𝑡 ) ) ∧ ( ( 𝑚 · 𝑡 ) < 𝑌 ∧ 𝑌 ≤ ( ( 𝑚 + 1 ) · 𝑡 ) ) ) ) ) → ( ( invg ‘ 𝑊 ) ‘ ( 𝑋 + 𝑌 ) ) ∈ 𝐵 )
99 79 znegcld ⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) ∧ 𝑡 ∈ 𝐵 ∧ 0 < 𝑡 ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ ( ( ( 𝑛 · 𝑡 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑛 + 1 ) · 𝑡 ) ) ∧ ( ( 𝑚 · 𝑡 ) < 𝑌 ∧ 𝑌 ≤ ( ( 𝑚 + 1 ) · 𝑡 ) ) ) ) ) → - ( 𝑛 + 𝑚 ) ∈ ℤ )
100 1 5 mulgcl ⊢ ( ( 𝑊 ∈ Grp ∧ - ( 𝑛 + 𝑚 ) ∈ ℤ ∧ 𝑡 ∈ 𝐵 ) → ( - ( 𝑛 + 𝑚 ) · 𝑡 ) ∈ 𝐵 )
101 25 99 29 100 syl3anc ⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) ∧ 𝑡 ∈ 𝐵 ∧ 0 < 𝑡 ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ ( ( ( 𝑛 · 𝑡 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑛 + 1 ) · 𝑡 ) ) ∧ ( ( 𝑚 · 𝑡 ) < 𝑌 ∧ 𝑌 ≤ ( ( 𝑚 + 1 ) · 𝑡 ) ) ) ) ) → ( - ( 𝑛 + 𝑚 ) · 𝑡 ) ∈ 𝐵 )
102 1 5 8 mulgdir ⊢ ( ( 𝑊 ∈ Grp ∧ ( 𝑛 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ 𝑡 ∈ 𝐵 ) ) → ( ( 𝑛 + 𝑚 ) · 𝑡 ) = ( ( 𝑛 · 𝑡 ) + ( 𝑚 · 𝑡 ) ) )
103 25 32 26 29 102 syl13anc ⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) ∧ 𝑡 ∈ 𝐵 ∧ 0 < 𝑡 ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ ( ( ( 𝑛 · 𝑡 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑛 + 1 ) · 𝑡 ) ) ∧ ( ( 𝑚 · 𝑡 ) < 𝑌 ∧ 𝑌 ≤ ( ( 𝑚 + 1 ) · 𝑡 ) ) ) ) ) → ( ( 𝑛 + 𝑚 ) · 𝑡 ) = ( ( 𝑛 · 𝑡 ) + ( 𝑚 · 𝑡 ) ) )
104 1 5 mulgcl ⊢ ( ( 𝑊 ∈ Grp ∧ 𝑛 ∈ ℤ ∧ 𝑡 ∈ 𝐵 ) → ( 𝑛 · 𝑡 ) ∈ 𝐵 )
105 25 32 29 104 syl3anc ⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) ∧ 𝑡 ∈ 𝐵 ∧ 0 < 𝑡 ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ ( ( ( 𝑛 · 𝑡 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑛 + 1 ) · 𝑡 ) ) ∧ ( ( 𝑚 · 𝑡 ) < 𝑌 ∧ 𝑌 ≤ ( ( 𝑚 + 1 ) · 𝑡 ) ) ) ) ) → ( 𝑛 · 𝑡 ) ∈ 𝐵 )
106 1 5 mulgcl ⊢ ( ( 𝑊 ∈ Grp ∧ 𝑚 ∈ ℤ ∧ 𝑡 ∈ 𝐵 ) → ( 𝑚 · 𝑡 ) ∈ 𝐵 )
107 25 26 29 106 syl3anc ⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) ∧ 𝑡 ∈ 𝐵 ∧ 0 < 𝑡 ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ ( ( ( 𝑛 · 𝑡 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑛 + 1 ) · 𝑡 ) ) ∧ ( ( 𝑚 · 𝑡 ) < 𝑌 ∧ 𝑌 ≤ ( ( 𝑚 + 1 ) · 𝑡 ) ) ) ) ) → ( 𝑚 · 𝑡 ) ∈ 𝐵 )
108 50 simpld ⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) ∧ 𝑡 ∈ 𝐵 ∧ 0 < 𝑡 ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ ( ( ( 𝑛 · 𝑡 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑛 + 1 ) · 𝑡 ) ) ∧ ( ( 𝑚 · 𝑡 ) < 𝑌 ∧ 𝑌 ≤ ( ( 𝑚 + 1 ) · 𝑡 ) ) ) ) ) → ( 𝑛 · 𝑡 ) < 𝑋 )
109 1 4 8 ogrpaddlt ⊢ ( ( 𝑊 ∈ oGrp ∧ ( ( 𝑛 · 𝑡 ) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑚 · 𝑡 ) ∈ 𝐵 ) ∧ ( 𝑛 · 𝑡 ) < 𝑋 ) → ( ( 𝑛 · 𝑡 ) + ( 𝑚 · 𝑡 ) ) < ( 𝑋 + ( 𝑚 · 𝑡 ) ) )
110 15 105 39 107 108 109 syl131anc ⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) ∧ 𝑡 ∈ 𝐵 ∧ 0 < 𝑡 ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ ( ( ( 𝑛 · 𝑡 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑛 + 1 ) · 𝑡 ) ) ∧ ( ( 𝑚 · 𝑡 ) < 𝑌 ∧ 𝑌 ≤ ( ( 𝑚 + 1 ) · 𝑡 ) ) ) ) ) → ( ( 𝑛 · 𝑡 ) + ( 𝑚 · 𝑡 ) ) < ( 𝑋 + ( 𝑚 · 𝑡 ) ) )
111 48 simpld ⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) ∧ 𝑡 ∈ 𝐵 ∧ 0 < 𝑡 ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ ( ( ( 𝑛 · 𝑡 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑛 + 1 ) · 𝑡 ) ) ∧ ( ( 𝑚 · 𝑡 ) < 𝑌 ∧ 𝑌 ≤ ( ( 𝑚 + 1 ) · 𝑡 ) ) ) ) ) → ( 𝑚 · 𝑡 ) < 𝑌 )
112 1 4 8 15 96 107 41 39 111 ogrpaddltrd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) ∧ 𝑡 ∈ 𝐵 ∧ 0 < 𝑡 ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ ( ( ( 𝑛 · 𝑡 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑛 + 1 ) · 𝑡 ) ) ∧ ( ( 𝑚 · 𝑡 ) < 𝑌 ∧ 𝑌 ≤ ( ( 𝑚 + 1 ) · 𝑡 ) ) ) ) ) → ( 𝑋 + ( 𝑚 · 𝑡 ) ) < ( 𝑋 + 𝑌 ) )
113 omndtos ⊢ ( 𝑊 ∈ oMnd → 𝑊 ∈ Toset )
114 tospos ⊢ ( 𝑊 ∈ Toset → 𝑊 ∈ Poset )
115 46 113 114 3syl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) ∧ 𝑡 ∈ 𝐵 ∧ 0 < 𝑡 ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ ( ( ( 𝑛 · 𝑡 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑛 + 1 ) · 𝑡 ) ) ∧ ( ( 𝑚 · 𝑡 ) < 𝑌 ∧ 𝑌 ≤ ( ( 𝑚 + 1 ) · 𝑡 ) ) ) ) ) → 𝑊 ∈ Poset )
116 1 8 grpcl ⊢ ( ( 𝑊 ∈ Grp ∧ ( 𝑛 · 𝑡 ) ∈ 𝐵 ∧ ( 𝑚 · 𝑡 ) ∈ 𝐵 ) → ( ( 𝑛 · 𝑡 ) + ( 𝑚 · 𝑡 ) ) ∈ 𝐵 )
117 25 105 107 116 syl3anc ⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) ∧ 𝑡 ∈ 𝐵 ∧ 0 < 𝑡 ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ ( ( ( 𝑛 · 𝑡 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑛 + 1 ) · 𝑡 ) ) ∧ ( ( 𝑚 · 𝑡 ) < 𝑌 ∧ 𝑌 ≤ ( ( 𝑚 + 1 ) · 𝑡 ) ) ) ) ) → ( ( 𝑛 · 𝑡 ) + ( 𝑚 · 𝑡 ) ) ∈ 𝐵 )
118 1 8 grpcl ⊢ ( ( 𝑊 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑚 · 𝑡 ) ∈ 𝐵 ) → ( 𝑋 + ( 𝑚 · 𝑡 ) ) ∈ 𝐵 )
119 25 39 107 118 syl3anc ⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) ∧ 𝑡 ∈ 𝐵 ∧ 0 < 𝑡 ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ ( ( ( 𝑛 · 𝑡 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑛 + 1 ) · 𝑡 ) ) ∧ ( ( 𝑚 · 𝑡 ) < 𝑌 ∧ 𝑌 ≤ ( ( 𝑚 + 1 ) · 𝑡 ) ) ) ) ) → ( 𝑋 + ( 𝑚 · 𝑡 ) ) ∈ 𝐵 )
120 1 4 plttr ⊢ ( ( 𝑊 ∈ Poset ∧ ( ( ( 𝑛 · 𝑡 ) + ( 𝑚 · 𝑡 ) ) ∈ 𝐵 ∧ ( 𝑋 + ( 𝑚 · 𝑡 ) ) ∈ 𝐵 ∧ ( 𝑋 + 𝑌 ) ∈ 𝐵 ) ) → ( ( ( ( 𝑛 · 𝑡 ) + ( 𝑚 · 𝑡 ) ) < ( 𝑋 + ( 𝑚 · 𝑡 ) ) ∧ ( 𝑋 + ( 𝑚 · 𝑡 ) ) < ( 𝑋 + 𝑌 ) ) → ( ( 𝑛 · 𝑡 ) + ( 𝑚 · 𝑡 ) ) < ( 𝑋 + 𝑌 ) ) )
121 115 117 119 43 120 syl13anc ⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) ∧ 𝑡 ∈ 𝐵 ∧ 0 < 𝑡 ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ ( ( ( 𝑛 · 𝑡 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑛 + 1 ) · 𝑡 ) ) ∧ ( ( 𝑚 · 𝑡 ) < 𝑌 ∧ 𝑌 ≤ ( ( 𝑚 + 1 ) · 𝑡 ) ) ) ) ) → ( ( ( ( 𝑛 · 𝑡 ) + ( 𝑚 · 𝑡 ) ) < ( 𝑋 + ( 𝑚 · 𝑡 ) ) ∧ ( 𝑋 + ( 𝑚 · 𝑡 ) ) < ( 𝑋 + 𝑌 ) ) → ( ( 𝑛 · 𝑡 ) + ( 𝑚 · 𝑡 ) ) < ( 𝑋 + 𝑌 ) ) )
122 110 112 121 mp2and ⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) ∧ 𝑡 ∈ 𝐵 ∧ 0 < 𝑡 ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ ( ( ( 𝑛 · 𝑡 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑛 + 1 ) · 𝑡 ) ) ∧ ( ( 𝑚 · 𝑡 ) < 𝑌 ∧ 𝑌 ≤ ( ( 𝑚 + 1 ) · 𝑡 ) ) ) ) ) → ( ( 𝑛 · 𝑡 ) + ( 𝑚 · 𝑡 ) ) < ( 𝑋 + 𝑌 ) )
123 103 122 eqbrtrd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) ∧ 𝑡 ∈ 𝐵 ∧ 0 < 𝑡 ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ ( ( ( 𝑛 · 𝑡 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑛 + 1 ) · 𝑡 ) ) ∧ ( ( 𝑚 · 𝑡 ) < 𝑌 ∧ 𝑌 ≤ ( ( 𝑚 + 1 ) · 𝑡 ) ) ) ) ) → ( ( 𝑛 + 𝑚 ) · 𝑡 ) < ( 𝑋 + 𝑌 ) )
124 103 117 eqeltrd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) ∧ 𝑡 ∈ 𝐵 ∧ 0 < 𝑡 ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ ( ( ( 𝑛 · 𝑡 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑛 + 1 ) · 𝑡 ) ) ∧ ( ( 𝑚 · 𝑡 ) < 𝑌 ∧ 𝑌 ≤ ( ( 𝑚 + 1 ) · 𝑡 ) ) ) ) ) → ( ( 𝑛 + 𝑚 ) · 𝑡 ) ∈ 𝐵 )
125 1 4 92 ogrpinvlt ⊢ ( ( ( 𝑊 ∈ oGrp ∧ ( oppg ‘ 𝑊 ) ∈ oGrp ) ∧ ( ( 𝑛 + 𝑚 ) · 𝑡 ) ∈ 𝐵 ∧ ( 𝑋 + 𝑌 ) ∈ 𝐵 ) → ( ( ( 𝑛 + 𝑚 ) · 𝑡 ) < ( 𝑋 + 𝑌 ) ↔ ( ( invg ‘ 𝑊 ) ‘ ( 𝑋 + 𝑌 ) ) < ( ( invg ‘ 𝑊 ) ‘ ( ( 𝑛 + 𝑚 ) · 𝑡 ) ) ) )
126 15 96 124 43 125 syl211anc ⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) ∧ 𝑡 ∈ 𝐵 ∧ 0 < 𝑡 ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ ( ( ( 𝑛 · 𝑡 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑛 + 1 ) · 𝑡 ) ) ∧ ( ( 𝑚 · 𝑡 ) < 𝑌 ∧ 𝑌 ≤ ( ( 𝑚 + 1 ) · 𝑡 ) ) ) ) ) → ( ( ( 𝑛 + 𝑚 ) · 𝑡 ) < ( 𝑋 + 𝑌 ) ↔ ( ( invg ‘ 𝑊 ) ‘ ( 𝑋 + 𝑌 ) ) < ( ( invg ‘ 𝑊 ) ‘ ( ( 𝑛 + 𝑚 ) · 𝑡 ) ) ) )
127 123 126 mpbid ⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) ∧ 𝑡 ∈ 𝐵 ∧ 0 < 𝑡 ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ ( ( ( 𝑛 · 𝑡 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑛 + 1 ) · 𝑡 ) ) ∧ ( ( 𝑚 · 𝑡 ) < 𝑌 ∧ 𝑌 ≤ ( ( 𝑚 + 1 ) · 𝑡 ) ) ) ) ) → ( ( invg ‘ 𝑊 ) ‘ ( 𝑋 + 𝑌 ) ) < ( ( invg ‘ 𝑊 ) ‘ ( ( 𝑛 + 𝑚 ) · 𝑡 ) ) )
128 1 5 92 mulgneg ⊢ ( ( 𝑊 ∈ Grp ∧ ( 𝑛 + 𝑚 ) ∈ ℤ ∧ 𝑡 ∈ 𝐵 ) → ( - ( 𝑛 + 𝑚 ) · 𝑡 ) = ( ( invg ‘ 𝑊 ) ‘ ( ( 𝑛 + 𝑚 ) · 𝑡 ) ) )
129 25 79 29 128 syl3anc ⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) ∧ 𝑡 ∈ 𝐵 ∧ 0 < 𝑡 ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ ( ( ( 𝑛 · 𝑡 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑛 + 1 ) · 𝑡 ) ) ∧ ( ( 𝑚 · 𝑡 ) < 𝑌 ∧ 𝑌 ≤ ( ( 𝑚 + 1 ) · 𝑡 ) ) ) ) ) → ( - ( 𝑛 + 𝑚 ) · 𝑡 ) = ( ( invg ‘ 𝑊 ) ‘ ( ( 𝑛 + 𝑚 ) · 𝑡 ) ) )
130 127 129 breqtrrd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) ∧ 𝑡 ∈ 𝐵 ∧ 0 < 𝑡 ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ ( ( ( 𝑛 · 𝑡 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑛 + 1 ) · 𝑡 ) ) ∧ ( ( 𝑚 · 𝑡 ) < 𝑌 ∧ 𝑌 ≤ ( ( 𝑚 + 1 ) · 𝑡 ) ) ) ) ) → ( ( invg ‘ 𝑊 ) ‘ ( 𝑋 + 𝑌 ) ) < ( - ( 𝑛 + 𝑚 ) · 𝑡 ) )
131 1 4 8 15 96 98 101 91 130 ogrpaddltrd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) ∧ 𝑡 ∈ 𝐵 ∧ 0 < 𝑡 ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ ( ( ( 𝑛 · 𝑡 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑛 + 1 ) · 𝑡 ) ) ∧ ( ( 𝑚 · 𝑡 ) < 𝑌 ∧ 𝑌 ≤ ( ( 𝑚 + 1 ) · 𝑡 ) ) ) ) ) → ( ( ( 𝑡 + 𝑡 ) + ( ( 𝑛 + 𝑚 ) · 𝑡 ) ) + ( ( invg ‘ 𝑊 ) ‘ ( 𝑋 + 𝑌 ) ) ) < ( ( ( 𝑡 + 𝑡 ) + ( ( 𝑛 + 𝑚 ) · 𝑡 ) ) + ( - ( 𝑛 + 𝑚 ) · 𝑡 ) ) )
132 1 56 grpsubcl ⊢ ( ( 𝑊 ∈ Grp ∧ ( 𝑌 + 𝑋 ) ∈ 𝐵 ∧ ( 𝑋 + 𝑌 ) ∈ 𝐵 ) → ( ( 𝑌 + 𝑋 ) ( -g ‘ 𝑊 ) ( 𝑋 + 𝑌 ) ) ∈ 𝐵 )
133 25 24 43 132 syl3anc ⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) ∧ 𝑡 ∈ 𝐵 ∧ 0 < 𝑡 ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ ( ( ( 𝑛 · 𝑡 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑛 + 1 ) · 𝑡 ) ) ∧ ( ( 𝑚 · 𝑡 ) < 𝑌 ∧ 𝑌 ≤ ( ( 𝑚 + 1 ) · 𝑡 ) ) ) ) ) → ( ( 𝑌 + 𝑋 ) ( -g ‘ 𝑊 ) ( 𝑋 + 𝑌 ) ) ∈ 𝐵 )
134 1 8 grpcl ⊢ ( ( 𝑊 ∈ Grp ∧ ( ( 𝑡 + 𝑡 ) + ( ( 𝑛 + 𝑚 ) · 𝑡 ) ) ∈ 𝐵 ∧ ( ( invg ‘ 𝑊 ) ‘ ( 𝑋 + 𝑌 ) ) ∈ 𝐵 ) → ( ( ( 𝑡 + 𝑡 ) + ( ( 𝑛 + 𝑚 ) · 𝑡 ) ) + ( ( invg ‘ 𝑊 ) ‘ ( 𝑋 + 𝑌 ) ) ) ∈ 𝐵 )
135 25 91 98 134 syl3anc ⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) ∧ 𝑡 ∈ 𝐵 ∧ 0 < 𝑡 ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ ( ( ( 𝑛 · 𝑡 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑛 + 1 ) · 𝑡 ) ) ∧ ( ( 𝑚 · 𝑡 ) < 𝑌 ∧ 𝑌 ≤ ( ( 𝑚 + 1 ) · 𝑡 ) ) ) ) ) → ( ( ( 𝑡 + 𝑡 ) + ( ( 𝑛 + 𝑚 ) · 𝑡 ) ) + ( ( invg ‘ 𝑊 ) ‘ ( 𝑋 + 𝑌 ) ) ) ∈ 𝐵 )
136 1 8 grpcl ⊢ ( ( 𝑊 ∈ Grp ∧ ( ( 𝑡 + 𝑡 ) + ( ( 𝑛 + 𝑚 ) · 𝑡 ) ) ∈ 𝐵 ∧ ( - ( 𝑛 + 𝑚 ) · 𝑡 ) ∈ 𝐵 ) → ( ( ( 𝑡 + 𝑡 ) + ( ( 𝑛 + 𝑚 ) · 𝑡 ) ) + ( - ( 𝑛 + 𝑚 ) · 𝑡 ) ) ∈ 𝐵 )
137 25 91 101 136 syl3anc ⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) ∧ 𝑡 ∈ 𝐵 ∧ 0 < 𝑡 ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ ( ( ( 𝑛 · 𝑡 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑛 + 1 ) · 𝑡 ) ) ∧ ( ( 𝑚 · 𝑡 ) < 𝑌 ∧ 𝑌 ≤ ( ( 𝑚 + 1 ) · 𝑡 ) ) ) ) ) → ( ( ( 𝑡 + 𝑡 ) + ( ( 𝑛 + 𝑚 ) · 𝑡 ) ) + ( - ( 𝑛 + 𝑚 ) · 𝑡 ) ) ∈ 𝐵 )
138 1 3 4 plelttr ⊢ ( ( 𝑊 ∈ Poset ∧ ( ( ( 𝑌 + 𝑋 ) ( -g ‘ 𝑊 ) ( 𝑋 + 𝑌 ) ) ∈ 𝐵 ∧ ( ( ( 𝑡 + 𝑡 ) + ( ( 𝑛 + 𝑚 ) · 𝑡 ) ) + ( ( invg ‘ 𝑊 ) ‘ ( 𝑋 + 𝑌 ) ) ) ∈ 𝐵 ∧ ( ( ( 𝑡 + 𝑡 ) + ( ( 𝑛 + 𝑚 ) · 𝑡 ) ) + ( - ( 𝑛 + 𝑚 ) · 𝑡 ) ) ∈ 𝐵 ) ) → ( ( ( ( 𝑌 + 𝑋 ) ( -g ‘ 𝑊 ) ( 𝑋 + 𝑌 ) ) ≤ ( ( ( 𝑡 + 𝑡 ) + ( ( 𝑛 + 𝑚 ) · 𝑡 ) ) + ( ( invg ‘ 𝑊 ) ‘ ( 𝑋 + 𝑌 ) ) ) ∧ ( ( ( 𝑡 + 𝑡 ) + ( ( 𝑛 + 𝑚 ) · 𝑡 ) ) + ( ( invg ‘ 𝑊 ) ‘ ( 𝑋 + 𝑌 ) ) ) < ( ( ( 𝑡 + 𝑡 ) + ( ( 𝑛 + 𝑚 ) · 𝑡 ) ) + ( - ( 𝑛 + 𝑚 ) · 𝑡 ) ) ) → ( ( 𝑌 + 𝑋 ) ( -g ‘ 𝑊 ) ( 𝑋 + 𝑌 ) ) < ( ( ( 𝑡 + 𝑡 ) + ( ( 𝑛 + 𝑚 ) · 𝑡 ) ) + ( - ( 𝑛 + 𝑚 ) · 𝑡 ) ) ) )
139 115 133 135 137 138 syl13anc ⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) ∧ 𝑡 ∈ 𝐵 ∧ 0 < 𝑡 ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ ( ( ( 𝑛 · 𝑡 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑛 + 1 ) · 𝑡 ) ) ∧ ( ( 𝑚 · 𝑡 ) < 𝑌 ∧ 𝑌 ≤ ( ( 𝑚 + 1 ) · 𝑡 ) ) ) ) ) → ( ( ( ( 𝑌 + 𝑋 ) ( -g ‘ 𝑊 ) ( 𝑋 + 𝑌 ) ) ≤ ( ( ( 𝑡 + 𝑡 ) + ( ( 𝑛 + 𝑚 ) · 𝑡 ) ) + ( ( invg ‘ 𝑊 ) ‘ ( 𝑋 + 𝑌 ) ) ) ∧ ( ( ( 𝑡 + 𝑡 ) + ( ( 𝑛 + 𝑚 ) · 𝑡 ) ) + ( ( invg ‘ 𝑊 ) ‘ ( 𝑋 + 𝑌 ) ) ) < ( ( ( 𝑡 + 𝑡 ) + ( ( 𝑛 + 𝑚 ) · 𝑡 ) ) + ( - ( 𝑛 + 𝑚 ) · 𝑡 ) ) ) → ( ( 𝑌 + 𝑋 ) ( -g ‘ 𝑊 ) ( 𝑋 + 𝑌 ) ) < ( ( ( 𝑡 + 𝑡 ) + ( ( 𝑛 + 𝑚 ) · 𝑡 ) ) + ( - ( 𝑛 + 𝑚 ) · 𝑡 ) ) ) )
140 95 131 139 mp2and ⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) ∧ 𝑡 ∈ 𝐵 ∧ 0 < 𝑡 ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ ( ( ( 𝑛 · 𝑡 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑛 + 1 ) · 𝑡 ) ) ∧ ( ( 𝑚 · 𝑡 ) < 𝑌 ∧ 𝑌 ≤ ( ( 𝑚 + 1 ) · 𝑡 ) ) ) ) ) → ( ( 𝑌 + 𝑋 ) ( -g ‘ 𝑊 ) ( 𝑋 + 𝑌 ) ) < ( ( ( 𝑡 + 𝑡 ) + ( ( 𝑛 + 𝑚 ) · 𝑡 ) ) + ( - ( 𝑛 + 𝑚 ) · 𝑡 ) ) )
141 1 8 grpcl ⊢ ( ( 𝑊 ∈ Grp ∧ 𝑡 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵 ) → ( 𝑡 + 𝑡 ) ∈ 𝐵 )
142 25 29 29 141 syl3anc ⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) ∧ 𝑡 ∈ 𝐵 ∧ 0 < 𝑡 ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ ( ( ( 𝑛 · 𝑡 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑛 + 1 ) · 𝑡 ) ) ∧ ( ( 𝑚 · 𝑡 ) < 𝑌 ∧ 𝑌 ≤ ( ( 𝑚 + 1 ) · 𝑡 ) ) ) ) ) → ( 𝑡 + 𝑡 ) ∈ 𝐵 )
143 1 8 grpass ⊢ ( ( 𝑊 ∈ Grp ∧ ( ( 𝑡 + 𝑡 ) ∈ 𝐵 ∧ ( ( 𝑛 + 𝑚 ) · 𝑡 ) ∈ 𝐵 ∧ ( - ( 𝑛 + 𝑚 ) · 𝑡 ) ∈ 𝐵 ) ) → ( ( ( 𝑡 + 𝑡 ) + ( ( 𝑛 + 𝑚 ) · 𝑡 ) ) + ( - ( 𝑛 + 𝑚 ) · 𝑡 ) ) = ( ( 𝑡 + 𝑡 ) + ( ( ( 𝑛 + 𝑚 ) · 𝑡 ) + ( - ( 𝑛 + 𝑚 ) · 𝑡 ) ) ) )
144 25 142 124 101 143 syl13anc ⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) ∧ 𝑡 ∈ 𝐵 ∧ 0 < 𝑡 ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ ( ( ( 𝑛 · 𝑡 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑛 + 1 ) · 𝑡 ) ) ∧ ( ( 𝑚 · 𝑡 ) < 𝑌 ∧ 𝑌 ≤ ( ( 𝑚 + 1 ) · 𝑡 ) ) ) ) ) → ( ( ( 𝑡 + 𝑡 ) + ( ( 𝑛 + 𝑚 ) · 𝑡 ) ) + ( - ( 𝑛 + 𝑚 ) · 𝑡 ) ) = ( ( 𝑡 + 𝑡 ) + ( ( ( 𝑛 + 𝑚 ) · 𝑡 ) + ( - ( 𝑛 + 𝑚 ) · 𝑡 ) ) ) )
145 60 59 addcld ⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) ∧ 𝑡 ∈ 𝐵 ∧ 0 < 𝑡 ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ ( ( ( 𝑛 · 𝑡 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑛 + 1 ) · 𝑡 ) ) ∧ ( ( 𝑚 · 𝑡 ) < 𝑌 ∧ 𝑌 ≤ ( ( 𝑚 + 1 ) · 𝑡 ) ) ) ) ) → ( 𝑛 + 𝑚 ) ∈ ℂ )
146 145 negidd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) ∧ 𝑡 ∈ 𝐵 ∧ 0 < 𝑡 ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ ( ( ( 𝑛 · 𝑡 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑛 + 1 ) · 𝑡 ) ) ∧ ( ( 𝑚 · 𝑡 ) < 𝑌 ∧ 𝑌 ≤ ( ( 𝑚 + 1 ) · 𝑡 ) ) ) ) ) → ( ( 𝑛 + 𝑚 ) + - ( 𝑛 + 𝑚 ) ) = 0 )
147 146 oveq1d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) ∧ 𝑡 ∈ 𝐵 ∧ 0 < 𝑡 ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ ( ( ( 𝑛 · 𝑡 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑛 + 1 ) · 𝑡 ) ) ∧ ( ( 𝑚 · 𝑡 ) < 𝑌 ∧ 𝑌 ≤ ( ( 𝑚 + 1 ) · 𝑡 ) ) ) ) ) → ( ( ( 𝑛 + 𝑚 ) + - ( 𝑛 + 𝑚 ) ) · 𝑡 ) = ( 0 · 𝑡 ) )
148 1 5 8 mulgdir ⊢ ( ( 𝑊 ∈ Grp ∧ ( ( 𝑛 + 𝑚 ) ∈ ℤ ∧ - ( 𝑛 + 𝑚 ) ∈ ℤ ∧ 𝑡 ∈ 𝐵 ) ) → ( ( ( 𝑛 + 𝑚 ) + - ( 𝑛 + 𝑚 ) ) · 𝑡 ) = ( ( ( 𝑛 + 𝑚 ) · 𝑡 ) + ( - ( 𝑛 + 𝑚 ) · 𝑡 ) ) )
149 25 79 99 29 148 syl13anc ⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) ∧ 𝑡 ∈ 𝐵 ∧ 0 < 𝑡 ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ ( ( ( 𝑛 · 𝑡 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑛 + 1 ) · 𝑡 ) ) ∧ ( ( 𝑚 · 𝑡 ) < 𝑌 ∧ 𝑌 ≤ ( ( 𝑚 + 1 ) · 𝑡 ) ) ) ) ) → ( ( ( 𝑛 + 𝑚 ) + - ( 𝑛 + 𝑚 ) ) · 𝑡 ) = ( ( ( 𝑛 + 𝑚 ) · 𝑡 ) + ( - ( 𝑛 + 𝑚 ) · 𝑡 ) ) )
150 1 2 5 mulg0 ⊢ ( 𝑡 ∈ 𝐵 → ( 0 · 𝑡 ) = 0 )
151 29 150 syl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) ∧ 𝑡 ∈ 𝐵 ∧ 0 < 𝑡 ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ ( ( ( 𝑛 · 𝑡 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑛 + 1 ) · 𝑡 ) ) ∧ ( ( 𝑚 · 𝑡 ) < 𝑌 ∧ 𝑌 ≤ ( ( 𝑚 + 1 ) · 𝑡 ) ) ) ) ) → ( 0 · 𝑡 ) = 0 )
152 147 149 151 3eqtr3d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) ∧ 𝑡 ∈ 𝐵 ∧ 0 < 𝑡 ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ ( ( ( 𝑛 · 𝑡 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑛 + 1 ) · 𝑡 ) ) ∧ ( ( 𝑚 · 𝑡 ) < 𝑌 ∧ 𝑌 ≤ ( ( 𝑚 + 1 ) · 𝑡 ) ) ) ) ) → ( ( ( 𝑛 + 𝑚 ) · 𝑡 ) + ( - ( 𝑛 + 𝑚 ) · 𝑡 ) ) = 0 )
153 152 oveq2d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) ∧ 𝑡 ∈ 𝐵 ∧ 0 < 𝑡 ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ ( ( ( 𝑛 · 𝑡 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑛 + 1 ) · 𝑡 ) ) ∧ ( ( 𝑚 · 𝑡 ) < 𝑌 ∧ 𝑌 ≤ ( ( 𝑚 + 1 ) · 𝑡 ) ) ) ) ) → ( ( 𝑡 + 𝑡 ) + ( ( ( 𝑛 + 𝑚 ) · 𝑡 ) + ( - ( 𝑛 + 𝑚 ) · 𝑡 ) ) ) = ( ( 𝑡 + 𝑡 ) + 0 ) )
154 1 8 2 grprid ⊢ ( ( 𝑊 ∈ Grp ∧ ( 𝑡 + 𝑡 ) ∈ 𝐵 ) → ( ( 𝑡 + 𝑡 ) + 0 ) = ( 𝑡 + 𝑡 ) )
155 25 142 154 syl2anc ⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) ∧ 𝑡 ∈ 𝐵 ∧ 0 < 𝑡 ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ ( ( ( 𝑛 · 𝑡 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑛 + 1 ) · 𝑡 ) ) ∧ ( ( 𝑚 · 𝑡 ) < 𝑌 ∧ 𝑌 ≤ ( ( 𝑚 + 1 ) · 𝑡 ) ) ) ) ) → ( ( 𝑡 + 𝑡 ) + 0 ) = ( 𝑡 + 𝑡 ) )
156 144 153 155 3eqtrd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) ∧ 𝑡 ∈ 𝐵 ∧ 0 < 𝑡 ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ ( ( ( 𝑛 · 𝑡 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑛 + 1 ) · 𝑡 ) ) ∧ ( ( 𝑚 · 𝑡 ) < 𝑌 ∧ 𝑌 ≤ ( ( 𝑚 + 1 ) · 𝑡 ) ) ) ) ) → ( ( ( 𝑡 + 𝑡 ) + ( ( 𝑛 + 𝑚 ) · 𝑡 ) ) + ( - ( 𝑛 + 𝑚 ) · 𝑡 ) ) = ( 𝑡 + 𝑡 ) )
157 140 156 breqtrd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) ∧ 𝑡 ∈ 𝐵 ∧ 0 < 𝑡 ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ ( ( ( 𝑛 · 𝑡 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑛 + 1 ) · 𝑡 ) ) ∧ ( ( 𝑚 · 𝑡 ) < 𝑌 ∧ 𝑌 ≤ ( ( 𝑚 + 1 ) · 𝑡 ) ) ) ) ) → ( ( 𝑌 + 𝑋 ) ( -g ‘ 𝑊 ) ( 𝑋 + 𝑌 ) ) < ( 𝑡 + 𝑡 ) )
158 157 3anassrs ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) ∧ 𝑡 ∈ 𝐵 ∧ 0 < 𝑡 ) ∧ 𝑛 ∈ ℤ ) ∧ 𝑚 ∈ ℤ ) ∧ ( ( ( 𝑛 · 𝑡 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑛 + 1 ) · 𝑡 ) ) ∧ ( ( 𝑚 · 𝑡 ) < 𝑌 ∧ 𝑌 ≤ ( ( 𝑚 + 1 ) · 𝑡 ) ) ) ) → ( ( 𝑌 + 𝑋 ) ( -g ‘ 𝑊 ) ( 𝑋 + 𝑌 ) ) < ( 𝑡 + 𝑡 ) )
159 17 3ad2ant1 ⊢ ( ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) ∧ 𝑡 ∈ 𝐵 ∧ 0 < 𝑡 ) → 𝑊 ∈ oGrp )
160 7 adantr ⊢ ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) → 𝑊 ∈ Archi )
161 160 3ad2ant1 ⊢ ( ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) ∧ 𝑡 ∈ 𝐵 ∧ 0 < 𝑡 ) → 𝑊 ∈ Archi )
162 simp3 ⊢ ( ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) ∧ 𝑡 ∈ 𝐵 ∧ 0 < 𝑡 ) → 0 < 𝑡 )
163 9 adantr ⊢ ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) → ( oppg ‘ 𝑊 ) ∈ oGrp )
164 163 3ad2ant1 ⊢ ( ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) ∧ 𝑡 ∈ 𝐵 ∧ 0 < 𝑡 ) → ( oppg ‘ 𝑊 ) ∈ oGrp )
165 1 2 4 3 5 159 161 28 38 162 164 archirngz ⊢ ( ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) ∧ 𝑡 ∈ 𝐵 ∧ 0 < 𝑡 ) → ∃ 𝑛 ∈ ℤ ( ( 𝑛 · 𝑡 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑛 + 1 ) · 𝑡 ) ) )
166 1 2 4 3 5 159 161 28 40 162 164 archirngz ⊢ ( ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) ∧ 𝑡 ∈ 𝐵 ∧ 0 < 𝑡 ) → ∃ 𝑚 ∈ ℤ ( ( 𝑚 · 𝑡 ) < 𝑌 ∧ 𝑌 ≤ ( ( 𝑚 + 1 ) · 𝑡 ) ) )
167 reeanv ⊢ ( ∃ 𝑛 ∈ ℤ ∃ 𝑚 ∈ ℤ ( ( ( 𝑛 · 𝑡 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑛 + 1 ) · 𝑡 ) ) ∧ ( ( 𝑚 · 𝑡 ) < 𝑌 ∧ 𝑌 ≤ ( ( 𝑚 + 1 ) · 𝑡 ) ) ) ↔ ( ∃ 𝑛 ∈ ℤ ( ( 𝑛 · 𝑡 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑛 + 1 ) · 𝑡 ) ) ∧ ∃ 𝑚 ∈ ℤ ( ( 𝑚 · 𝑡 ) < 𝑌 ∧ 𝑌 ≤ ( ( 𝑚 + 1 ) · 𝑡 ) ) ) )
168 165 166 167 sylanbrc ⊢ ( ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) ∧ 𝑡 ∈ 𝐵 ∧ 0 < 𝑡 ) → ∃ 𝑛 ∈ ℤ ∃ 𝑚 ∈ ℤ ( ( ( 𝑛 · 𝑡 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑛 + 1 ) · 𝑡 ) ) ∧ ( ( 𝑚 · 𝑡 ) < 𝑌 ∧ 𝑌 ≤ ( ( 𝑚 + 1 ) · 𝑡 ) ) ) )
169 158 168 r19.29vva ⊢ ( ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) ∧ 𝑡 ∈ 𝐵 ∧ 0 < 𝑡 ) → ( ( 𝑌 + 𝑋 ) ( -g ‘ 𝑊 ) ( 𝑋 + 𝑌 ) ) < ( 𝑡 + 𝑡 ) )
170 159 45 113 3syl ⊢ ( ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) ∧ 𝑡 ∈ 𝐵 ∧ 0 < 𝑡 ) → 𝑊 ∈ Toset )
171 19 21 20 42 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) → ( 𝑋 + 𝑌 ) ∈ 𝐵 )
172 19 23 171 132 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) → ( ( 𝑌 + 𝑋 ) ( -g ‘ 𝑊 ) ( 𝑋 + 𝑌 ) ) ∈ 𝐵 )
173 172 3ad2ant1 ⊢ ( ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) ∧ 𝑡 ∈ 𝐵 ∧ 0 < 𝑡 ) → ( ( 𝑌 + 𝑋 ) ( -g ‘ 𝑊 ) ( 𝑋 + 𝑌 ) ) ∈ 𝐵 )
174 159 18 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) ∧ 𝑡 ∈ 𝐵 ∧ 0 < 𝑡 ) → 𝑊 ∈ Grp )
175 174 28 28 141 syl3anc ⊢ ( ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) ∧ 𝑡 ∈ 𝐵 ∧ 0 < 𝑡 ) → ( 𝑡 + 𝑡 ) ∈ 𝐵 )
176 1 3 4 tltnle ⊢ ( ( 𝑊 ∈ Toset ∧ ( ( 𝑌 + 𝑋 ) ( -g ‘ 𝑊 ) ( 𝑋 + 𝑌 ) ) ∈ 𝐵 ∧ ( 𝑡 + 𝑡 ) ∈ 𝐵 ) → ( ( ( 𝑌 + 𝑋 ) ( -g ‘ 𝑊 ) ( 𝑋 + 𝑌 ) ) < ( 𝑡 + 𝑡 ) ↔ ¬ ( 𝑡 + 𝑡 ) ≤ ( ( 𝑌 + 𝑋 ) ( -g ‘ 𝑊 ) ( 𝑋 + 𝑌 ) ) ) )
177 170 173 175 176 syl3anc ⊢ ( ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) ∧ 𝑡 ∈ 𝐵 ∧ 0 < 𝑡 ) → ( ( ( 𝑌 + 𝑋 ) ( -g ‘ 𝑊 ) ( 𝑋 + 𝑌 ) ) < ( 𝑡 + 𝑡 ) ↔ ¬ ( 𝑡 + 𝑡 ) ≤ ( ( 𝑌 + 𝑋 ) ( -g ‘ 𝑊 ) ( 𝑋 + 𝑌 ) ) ) )
178 169 177 mpbid ⊢ ( ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) ∧ 𝑡 ∈ 𝐵 ∧ 0 < 𝑡 ) → ¬ ( 𝑡 + 𝑡 ) ≤ ( ( 𝑌 + 𝑋 ) ( -g ‘ 𝑊 ) ( 𝑋 + 𝑌 ) ) )
179 178 3expa ⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) ∧ 𝑡 ∈ 𝐵 ) ∧ 0 < 𝑡 ) → ¬ ( 𝑡 + 𝑡 ) ≤ ( ( 𝑌 + 𝑋 ) ( -g ‘ 𝑊 ) ( 𝑋 + 𝑌 ) ) )
180 179 adantrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) ∧ 𝑡 ∈ 𝐵 ) ∧ ( 0 < 𝑡 ∧ ( 𝑡 + 𝑡 ) ≤ ( ( 𝑌 + 𝑋 ) ( -g ‘ 𝑊 ) ( 𝑋 + 𝑌 ) ) ) ) → ¬ ( 𝑡 + 𝑡 ) ≤ ( ( 𝑌 + 𝑋 ) ( -g ‘ 𝑊 ) ( 𝑋 + 𝑌 ) ) )
181 13 180 pm2.21fal ⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) ∧ 𝑡 ∈ 𝐵 ) ∧ ( 0 < 𝑡 ∧ ( 𝑡 + 𝑡 ) ≤ ( ( 𝑌 + 𝑋 ) ( -g ‘ 𝑊 ) ( 𝑋 + 𝑌 ) ) ) ) → ⊥ )
182 10 3adant1r ⊢ ( ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) ∧ 𝑎 ∈ 𝐵 ∧ 0 < 𝑎 ) → ∃ 𝑏 ∈ 𝐵 ( 0 < 𝑏 ∧ 𝑏 < 𝑎 ) )
183 1 2 56 grpsubid ⊢ ( ( 𝑊 ∈ Grp ∧ ( 𝑋 + 𝑌 ) ∈ 𝐵 ) → ( ( 𝑋 + 𝑌 ) ( -g ‘ 𝑊 ) ( 𝑋 + 𝑌 ) ) = 0 )
184 19 171 183 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) → ( ( 𝑋 + 𝑌 ) ( -g ‘ 𝑊 ) ( 𝑋 + 𝑌 ) ) = 0 )
185 simpr ⊢ ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) → ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) )
186 1 4 56 ogrpsublt ⊢ ( ( 𝑊 ∈ oGrp ∧ ( ( 𝑋 + 𝑌 ) ∈ 𝐵 ∧ ( 𝑌 + 𝑋 ) ∈ 𝐵 ∧ ( 𝑋 + 𝑌 ) ∈ 𝐵 ) ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) → ( ( 𝑋 + 𝑌 ) ( -g ‘ 𝑊 ) ( 𝑋 + 𝑌 ) ) < ( ( 𝑌 + 𝑋 ) ( -g ‘ 𝑊 ) ( 𝑋 + 𝑌 ) ) )
187 17 171 23 171 185 186 syl131anc ⊢ ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) → ( ( 𝑋 + 𝑌 ) ( -g ‘ 𝑊 ) ( 𝑋 + 𝑌 ) ) < ( ( 𝑌 + 𝑋 ) ( -g ‘ 𝑊 ) ( 𝑋 + 𝑌 ) ) )
188 184 187 eqbrtrrd ⊢ ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) → 0 < ( ( 𝑌 + 𝑋 ) ( -g ‘ 𝑊 ) ( 𝑋 + 𝑌 ) ) )
189 1 2 3 4 5 17 160 8 163 182 172 188 archiabllem2a ⊢ ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) → ∃ 𝑡 ∈ 𝐵 ( 0 < 𝑡 ∧ ( 𝑡 + 𝑡 ) ≤ ( ( 𝑌 + 𝑋 ) ( -g ‘ 𝑊 ) ( 𝑋 + 𝑌 ) ) ) )
190 181 189 r19.29a ⊢ ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ) → ⊥ )
191 190 inegd ⊢ ( 𝜑 → ¬ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) )