Description: The operation of a quotient structure is a function. (Contributed by Mario Carneiro, 24-Feb-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | qusaddf.u | |
|
qusaddf.v | |
||
qusaddf.r | |
||
qusaddf.z | |
||
qusaddf.e | |
||
qusaddf.c | |
||
qusaddflem.f | |
||
qusaddflem.g | |
||
Assertion | qusaddflem | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | qusaddf.u | |
|
2 | qusaddf.v | |
|
3 | qusaddf.r | |
|
4 | qusaddf.z | |
|
5 | qusaddf.e | |
|
6 | qusaddf.c | |
|
7 | qusaddflem.f | |
|
8 | qusaddflem.g | |
|
9 | fvex | |
|
10 | 2 9 | eqeltrdi | |
11 | erex | |
|
12 | 3 10 11 | sylc | |
13 | 1 2 7 12 4 | quslem | |
14 | 3 10 7 6 5 | ercpbl | |
15 | 13 14 8 6 | imasaddflem | |