Metamath Proof Explorer


Theorem imasmulfn

Description: The image structure's ring multiplication is a function. (Contributed by Mario Carneiro, 23-Feb-2015)

Ref Expression
Hypotheses imasaddf.f โŠข ( ๐œ‘ โ†’ ๐น : ๐‘‰ โ€“ontoโ†’ ๐ต )
imasaddf.e โŠข ( ( ๐œ‘ โˆง ( ๐‘Ž โˆˆ ๐‘‰ โˆง ๐‘ โˆˆ ๐‘‰ ) โˆง ( ๐‘ โˆˆ ๐‘‰ โˆง ๐‘ž โˆˆ ๐‘‰ ) ) โ†’ ( ( ( ๐น โ€˜ ๐‘Ž ) = ( ๐น โ€˜ ๐‘ ) โˆง ( ๐น โ€˜ ๐‘ ) = ( ๐น โ€˜ ๐‘ž ) ) โ†’ ( ๐น โ€˜ ( ๐‘Ž ยท ๐‘ ) ) = ( ๐น โ€˜ ( ๐‘ ยท ๐‘ž ) ) ) )
imasaddf.u โŠข ( ๐œ‘ โ†’ ๐‘ˆ = ( ๐น โ€œs ๐‘… ) )
imasaddf.v โŠข ( ๐œ‘ โ†’ ๐‘‰ = ( Base โ€˜ ๐‘… ) )
imasaddf.r โŠข ( ๐œ‘ โ†’ ๐‘… โˆˆ ๐‘ )
imasmulf.p โŠข ยท = ( .r โ€˜ ๐‘… )
imasmulf.a โŠข โˆ™ = ( .r โ€˜ ๐‘ˆ )
Assertion imasmulfn ( ๐œ‘ โ†’ โˆ™ Fn ( ๐ต ร— ๐ต ) )

Proof

Step Hyp Ref Expression
1 imasaddf.f โŠข ( ๐œ‘ โ†’ ๐น : ๐‘‰ โ€“ontoโ†’ ๐ต )
2 imasaddf.e โŠข ( ( ๐œ‘ โˆง ( ๐‘Ž โˆˆ ๐‘‰ โˆง ๐‘ โˆˆ ๐‘‰ ) โˆง ( ๐‘ โˆˆ ๐‘‰ โˆง ๐‘ž โˆˆ ๐‘‰ ) ) โ†’ ( ( ( ๐น โ€˜ ๐‘Ž ) = ( ๐น โ€˜ ๐‘ ) โˆง ( ๐น โ€˜ ๐‘ ) = ( ๐น โ€˜ ๐‘ž ) ) โ†’ ( ๐น โ€˜ ( ๐‘Ž ยท ๐‘ ) ) = ( ๐น โ€˜ ( ๐‘ ยท ๐‘ž ) ) ) )
3 imasaddf.u โŠข ( ๐œ‘ โ†’ ๐‘ˆ = ( ๐น โ€œs ๐‘… ) )
4 imasaddf.v โŠข ( ๐œ‘ โ†’ ๐‘‰ = ( Base โ€˜ ๐‘… ) )
5 imasaddf.r โŠข ( ๐œ‘ โ†’ ๐‘… โˆˆ ๐‘ )
6 imasmulf.p โŠข ยท = ( .r โ€˜ ๐‘… )
7 imasmulf.a โŠข โˆ™ = ( .r โ€˜ ๐‘ˆ )
8 3 4 1 5 6 7 imasmulr โŠข ( ๐œ‘ โ†’ โˆ™ = โˆช ๐‘ โˆˆ ๐‘‰ โˆช ๐‘ž โˆˆ ๐‘‰ { โŸจ โŸจ ( ๐น โ€˜ ๐‘ ) , ( ๐น โ€˜ ๐‘ž ) โŸฉ , ( ๐น โ€˜ ( ๐‘ ยท ๐‘ž ) ) โŸฉ } )
9 1 2 8 imasaddfnlem โŠข ( ๐œ‘ โ†’ โˆ™ Fn ( ๐ต ร— ๐ต ) )