Metamath Proof Explorer


Theorem imasmulf

Description: The image structure's ring multiplication is closed in the base set. (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 )
imasmulf.c
|- ( ( ph /\ ( p e. V /\ q e. V ) ) -> ( p .x. q ) e. V )
Assertion imasmulf
|- ( ph -> .xb : ( B X. B ) --> B )

Proof

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 imasmulf.c
 |-  ( ( ph /\ ( p e. V /\ q e. V ) ) -> ( p .x. q ) e. V )
9 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 ) ) >. } )
10 1 2 9 8 imasaddflem
 |-  ( ph -> .xb : ( B X. B ) --> B )