Description: Ring addition operation. (Contributed by NM, 10-Jun-2013)
Ref | Expression | ||
---|---|---|---|
Hypotheses | erngset.h | |
|
erngset.t | |
||
erngset.e | |
||
erngset.d | |
||
erng.p | |
||
Assertion | erngplus2 | |
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 | erngplus | |
7 | 6 | 3adantr3 | |
8 | fveq2 | |
|
9 | fveq2 | |
|
10 | 8 9 | coeq12d | |
11 | 10 | adantl | |
12 | simpr3 | |
|
13 | fvex | |
|
14 | fvex | |
|
15 | 13 14 | coex | |
16 | 15 | a1i | |
17 | 7 11 12 16 | fvmptd | |