Description: The image structure's group operation is a function. (Contributed by Mario Carneiro, 23-Feb-2015) (Revised by Mario Carneiro, 10-Jul-2015)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | imasaddf.f | |- ( ph -> F : V -onto-> B ) |
|
| imasaddf.e | |- ( ( ph /\ ( a e. V /\ b e. V ) /\ ( p e. V /\ q e. V ) ) -> ( ( ( F ` a ) = ( F ` p ) /\ ( F ` b ) = ( F ` q ) ) -> ( F ` ( a .x. b ) ) = ( F ` ( p .x. q ) ) ) ) |
||
| imasaddf.u | |- ( ph -> U = ( F "s R ) ) |
||
| imasaddf.v | |- ( ph -> V = ( Base ` R ) ) |
||
| imasaddf.r | |- ( ph -> R e. Z ) |
||
| imasaddf.p | |- .x. = ( +g ` R ) |
||
| imasaddf.a | |- .xb = ( +g ` U ) |
||
| Assertion | imasaddfn | |- ( ph -> .xb Fn ( B X. B ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | imasaddf.f | |- ( ph -> F : V -onto-> B ) |
|
| 2 | imasaddf.e | |- ( ( ph /\ ( a e. V /\ b e. V ) /\ ( p e. V /\ q e. V ) ) -> ( ( ( F ` a ) = ( F ` p ) /\ ( F ` b ) = ( F ` q ) ) -> ( F ` ( a .x. b ) ) = ( F ` ( p .x. q ) ) ) ) |
|
| 3 | imasaddf.u | |- ( ph -> U = ( F "s R ) ) |
|
| 4 | imasaddf.v | |- ( ph -> V = ( Base ` R ) ) |
|
| 5 | imasaddf.r | |- ( ph -> R e. Z ) |
|
| 6 | imasaddf.p | |- .x. = ( +g ` R ) |
|
| 7 | imasaddf.a | |- .xb = ( +g ` U ) |
|
| 8 | 3 4 1 5 6 7 | imasplusg | |- ( ph -> .xb = U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } ) |
| 9 | 1 2 8 | imasaddfnlem | |- ( ph -> .xb Fn ( B X. B ) ) |