Description: The value of an image structure's ring multiplication. (Contributed by Mario Carneiro, 23-Feb-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 ) |
||
imasmulf.p | |- .x. = ( .r ` R ) |
||
imasmulf.a | |- .xb = ( .r ` U ) |
||
Assertion | imasmulval | |- ( ( ph /\ X e. V /\ Y e. V ) -> ( ( F ` X ) .xb ( F ` Y ) ) = ( F ` ( X .x. Y ) ) ) |
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 | imasmulf.p | |- .x. = ( .r ` R ) |
|
7 | imasmulf.a | |- .xb = ( .r ` U ) |
|
8 | 3 4 1 5 6 7 | imasmulr | |- ( ph -> .xb = U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } ) |
9 | 1 2 8 | imasaddvallem | |- ( ( ph /\ X e. V /\ Y e. V ) -> ( ( F ` X ) .xb ( F ` Y ) ) = ( F ` ( X .x. Y ) ) ) |