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	⊢ ( 𝜑 → ¬ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) )