| 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 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑋 < 𝑌 ) → ( 𝑋 + 𝑍 ) < ( 𝑌 + 𝑍 ) ) |