Description: Cancellation law for group subtraction. ( nncan analog.) (Contributed by NM, 7-Apr-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | ablnncan.b | |
|
ablnncan.m | |
||
ablnncan.g | |
||
ablnncan.x | |
||
ablnncan.y | |
||
Assertion | ablnncan | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ablnncan.b | |
|
2 | ablnncan.m | |
|
3 | ablnncan.g | |
|
4 | ablnncan.x | |
|
5 | ablnncan.y | |
|
6 | eqid | |
|
7 | 1 6 2 3 4 4 5 | ablsubsub | |
8 | ablgrp | |
|
9 | 3 8 | syl | |
10 | eqid | |
|
11 | 1 10 2 | grpsubid | |
12 | 9 4 11 | syl2anc | |
13 | 12 | oveq1d | |
14 | 1 6 10 | grplid | |
15 | 9 5 14 | syl2anc | |
16 | 7 13 15 | 3eqtrd | |