Description: Ring addition operation. (Contributed by NM, 10-Jun-2013)
Ref | Expression | ||
---|---|---|---|
Hypotheses | erngset.h | |
|
erngset.t | |
||
erngset.e | |
||
erngset.d | |
||
erng.p | |
||
Assertion | erngplus | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | erngset.h | |
|
2 | erngset.t | |
|
3 | erngset.e | |
|
4 | erngset.d | |
|
5 | erng.p | |
|
6 | 1 2 3 4 5 | erngfplus | |
7 | 6 | oveqd | |
8 | eqid | |
|
9 | 8 2 | tendopl | |
10 | 7 9 | sylan9eq | |