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	|- ( 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 )
	imasaddf.c	|- ( ( ph /\ ( p e. V /\ q e. V ) ) -> ( p .x. q ) e. V )
Assertion	imasaddf	|- ( 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		imasaddf.p	|- .x. = ( +g ` R )
7		imasaddf.a	|- .xb = ( +g ` U )
8		imasaddf.c	|- ( ( ph /\ ( p e. V /\ q e. V ) ) -> ( p .x. q ) e. V )
9	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 ) ) >. } )
10	1 2 9 8	imasaddflem	|- ( ph -> .xb : ( B X. B ) --> B )