Theorem mndpfo

Description: The addition operation of a monoid as a function is an onto function. (Contributed by FL, 2-Nov-2009) (Revised by Mario Carneiro, 11-Oct-2013) (Revised by AV, 23-Jan-2020)

	Ref	Expression
Hypotheses	mndpf.b	|- B = ( Base ` G )
	mndpf.p	|- .+^ = ( +f ` G )
Assertion	mndpfo	|- ( G e. Mnd -> .+^ : ( B X. B ) -onto-> B )

Proof

Step	Hyp	Ref	Expression
1		mndpf.b	|- B = ( Base ` G )
2		mndpf.p	|- .+^ = ( +f ` G )
3	1 2	mndplusf	|- ( G e. Mnd -> .+^ : ( B X. B ) --> B )
4		simpr	|- ( ( G e. Mnd /\ x e. B ) -> x e. B )
5		eqid	|- ( 0g ` G ) = ( 0g ` G )
6	1 5	mndidcl	|- ( G e. Mnd -> ( 0g ` G ) e. B )
7	6	adantr	|- ( ( G e. Mnd /\ x e. B ) -> ( 0g ` G ) e. B )
8		eqid	|- ( +g ` G ) = ( +g ` G )
9	1 8 5	mndrid	|- ( ( G e. Mnd /\ x e. B ) -> ( x ( +g ` G ) ( 0g ` G ) ) = x )
10	9	eqcomd	|- ( ( G e. Mnd /\ x e. B ) -> x = ( x ( +g ` G ) ( 0g ` G ) ) )
11		rspceov	|- ( ( x e. B /\ ( 0g ` G ) e. B /\ x = ( x ( +g ` G ) ( 0g ` G ) ) ) -> E. y e. B E. z e. B x = ( y ( +g ` G ) z ) )
12	4 7 10 11	syl3anc	|- ( ( G e. Mnd /\ x e. B ) -> E. y e. B E. z e. B x = ( y ( +g ` G ) z ) )
13	1 8 2	plusfval	|- ( ( y e. B /\ z e. B ) -> ( y .+^ z ) = ( y ( +g ` G ) z ) )
14	13	eqeq2d	|- ( ( y e. B /\ z e. B ) -> ( x = ( y .+^ z ) <-> x = ( y ( +g ` G ) z ) ) )
15	14	2rexbiia	|- ( E. y e. B E. z e. B x = ( y .+^ z ) <-> E. y e. B E. z e. B x = ( y ( +g ` G ) z ) )
16	12 15	sylibr	|- ( ( G e. Mnd /\ x e. B ) -> E. y e. B E. z e. B x = ( y .+^ z ) )
17	16	ralrimiva	|- ( G e. Mnd -> A. x e. B E. y e. B E. z e. B x = ( y .+^ z ) )
18		foov	|- ( .+^ : ( B X. B ) -onto-> B <-> ( .+^ : ( B X. B ) --> B /\ A. x e. B E. y e. B E. z e. B x = ( y .+^ z ) ) )
19	3 17 18	sylanbrc	|- ( G e. Mnd -> .+^ : ( B X. B ) -onto-> B )