This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )