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

Metamath Proof Explorer

Theorem ogrpaddlt

Description: In an ordered group, strict ordering is compatible with group addition. (Contributed by Thierry Arnoux, 20-Jan-2018)

Ref Expression
Hypotheses ogrpaddlt.0 ⊢ 𝐵 = ( Base ‘ 𝐺 )
ogrpaddlt.1 ⊢ < = ( lt ‘ 𝐺 )
ogrpaddlt.2 ⊢ + = ( +g ‘ 𝐺 )
Assertion ogrpaddlt ( ( 𝐺 ∈ oGrp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑋 < 𝑌 ) → ( 𝑋 + 𝑍 ) < ( 𝑌 + 𝑍 ) )

Proof

Step Hyp Ref Expression
1 ogrpaddlt.0 ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 ogrpaddlt.1 ⊢ < = ( lt ‘ 𝐺 )
3 ogrpaddlt.2 ⊢ + = ( +g ‘ 𝐺 )
4 isogrp ⊢ ( 𝐺 ∈ oGrp ↔ ( 𝐺 ∈ Grp ∧ 𝐺 ∈ oMnd ) )
5 4 simprbi ⊢ ( 𝐺 ∈ oGrp → 𝐺 ∈ oMnd )
6 5 3ad2ant1 ⊢ ( ( 𝐺 ∈ oGrp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑋 < 𝑌 ) → 𝐺 ∈ oMnd )
7 simp2 ⊢ ( ( 𝐺 ∈ oGrp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑋 < 𝑌 ) → ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) )
8 simp1 ⊢ ( ( 𝐺 ∈ oGrp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑋 < 𝑌 ) → 𝐺 ∈ oGrp )
9 simp21 ⊢ ( ( 𝐺 ∈ oGrp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑋 < 𝑌 ) → 𝑋 ∈ 𝐵 )
10 simp22 ⊢ ( ( 𝐺 ∈ oGrp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑋 < 𝑌 ) → 𝑌 ∈ 𝐵 )
11 simp3 ⊢ ( ( 𝐺 ∈ oGrp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑋 < 𝑌 ) → 𝑋 < 𝑌 )
12 eqid ⊢ ( le ‘ 𝐺 ) = ( le ‘ 𝐺 )
13 12 2 pltle ⊢ ( ( 𝐺 ∈ oGrp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 < 𝑌 → 𝑋 ( le ‘ 𝐺 ) 𝑌 ) )
14 13 imp ⊢ ( ( ( 𝐺 ∈ oGrp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 < 𝑌 ) → 𝑋 ( le ‘ 𝐺 ) 𝑌 )
15 8 9 10 11 14 syl31anc ⊢ ( ( 𝐺 ∈ oGrp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑋 < 𝑌 ) → 𝑋 ( le ‘ 𝐺 ) 𝑌 )
16 1 12 3 omndadd ⊢ ( ( 𝐺 ∈ oMnd ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑋 ( le ‘ 𝐺 ) 𝑌 ) → ( 𝑋 + 𝑍 ) ( le ‘ 𝐺 ) ( 𝑌 + 𝑍 ) )
17 6 7 15 16 syl3anc ⊢ ( ( 𝐺 ∈ oGrp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑋 < 𝑌 ) → ( 𝑋 + 𝑍 ) ( le ‘ 𝐺 ) ( 𝑌 + 𝑍 ) )
18 2 pltne ⊢ ( ( 𝐺 ∈ oGrp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 < 𝑌 → 𝑋 ≠ 𝑌 ) )
19 18 imp ⊢ ( ( ( 𝐺 ∈ oGrp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 < 𝑌 ) → 𝑋 ≠ 𝑌 )
20 8 9 10 11 19 syl31anc ⊢ ( ( 𝐺 ∈ oGrp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑋 < 𝑌 ) → 𝑋 ≠ 𝑌 )
21 ogrpgrp ⊢ ( 𝐺 ∈ oGrp → 𝐺 ∈ Grp )
22 1 3 grprcan ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( 𝑋 + 𝑍 ) = ( 𝑌 + 𝑍 ) ↔ 𝑋 = 𝑌 ) )
23 22 biimpd ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( 𝑋 + 𝑍 ) = ( 𝑌 + 𝑍 ) → 𝑋 = 𝑌 ) )
24 21 23 sylan ⊢ ( ( 𝐺 ∈ oGrp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( 𝑋 + 𝑍 ) = ( 𝑌 + 𝑍 ) → 𝑋 = 𝑌 ) )
25 24 necon3d ⊢ ( ( 𝐺 ∈ oGrp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑋 ≠ 𝑌 → ( 𝑋 + 𝑍 ) ≠ ( 𝑌 + 𝑍 ) ) )
26 25 3impia ⊢ ( ( 𝐺 ∈ oGrp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑋 ≠ 𝑌 ) → ( 𝑋 + 𝑍 ) ≠ ( 𝑌 + 𝑍 ) )
27 8 7 20 26 syl3anc ⊢ ( ( 𝐺 ∈ oGrp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑋 < 𝑌 ) → ( 𝑋 + 𝑍 ) ≠ ( 𝑌 + 𝑍 ) )
28 ovex ⊢ ( 𝑋 + 𝑍 ) ∈ V
29 ovex ⊢ ( 𝑌 + 𝑍 ) ∈ V
30 12 2 pltval ⊢ ( ( 𝐺 ∈ oGrp ∧ ( 𝑋 + 𝑍 ) ∈ V ∧ ( 𝑌 + 𝑍 ) ∈ V ) → ( ( 𝑋 + 𝑍 ) < ( 𝑌 + 𝑍 ) ↔ ( ( 𝑋 + 𝑍 ) ( le ‘ 𝐺 ) ( 𝑌 + 𝑍 ) ∧ ( 𝑋 + 𝑍 ) ≠ ( 𝑌 + 𝑍 ) ) ) )
31 28 29 30 mp3an23 ⊢ ( 𝐺 ∈ oGrp → ( ( 𝑋 + 𝑍 ) < ( 𝑌 + 𝑍 ) ↔ ( ( 𝑋 + 𝑍 ) ( le ‘ 𝐺 ) ( 𝑌 + 𝑍 ) ∧ ( 𝑋 + 𝑍 ) ≠ ( 𝑌 + 𝑍 ) ) ) )
32 31 3ad2ant1 ⊢ ( ( 𝐺 ∈ oGrp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑋 < 𝑌 ) → ( ( 𝑋 + 𝑍 ) < ( 𝑌 + 𝑍 ) ↔ ( ( 𝑋 + 𝑍 ) ( le ‘ 𝐺 ) ( 𝑌 + 𝑍 ) ∧ ( 𝑋 + 𝑍 ) ≠ ( 𝑌 + 𝑍 ) ) ) )
33 17 27 32 mpbir2and ⊢ ( ( 𝐺 ∈ oGrp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑋 < 𝑌 ) → ( 𝑋 + 𝑍 ) < ( 𝑌 + 𝑍 ) )