Theorem mgmidprnd

Description: Range of an operation with a left and right identity element. (Contributed by FL, 2-Nov-2009) (Revised by AV, 16-Aug-2026)

	Ref	Expression
Hypotheses	mgmidpfod.b	|- B = ( Base ` G )
	mgmidpfod.p	|- .+ = ( +g ` G )
	mgmidpfod.g	|- ( ph -> G e. Mgm )
	mgmidpfod.e	|- ( ph -> E. e e. B A. x e. B ( ( e .+ x ) = x /\ ( x .+ e ) = x ) )
	mgmidpfod.f	|- .+^ = ( +f ` G )
Assertion	mgmidprnd	|- ( ph -> ran .+^ = B )

Proof

Step	Hyp	Ref	Expression
1		mgmidpfod.b	|- B = ( Base ` G )
2		mgmidpfod.p	|- .+ = ( +g ` G )
3		mgmidpfod.g	|- ( ph -> G e. Mgm )
4		mgmidpfod.e	|- ( ph -> E. e e. B A. x e. B ( ( e .+ x ) = x /\ ( x .+ e ) = x ) )
5		mgmidpfod.f	|- .+^ = ( +f ` G )
6	1 2 3 4 5	mgmidpfod	|- ( ph -> .+^ : ( B X. B ) -onto-> B )
7		forn	|- ( .+^ : ( B X. B ) -onto-> B -> ran .+^ = B )
8	6 7	syl	|- ( ph -> ran .+^ = B )