Metamath Proof Explorer


Theorem imasaddf

Description: The image structure's group operation is closed in the base set. (Contributed by Mario Carneiro, 23-Feb-2015)

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

Proof

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