Metamath Proof Explorer

Theorem mgmidpfod

Description: The operation of a magma with identity as a function is an onto function. (Contributed by FL, 2-Nov-2009) (Revised by Mario Carneiro, 22-Dec-2013) (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 mgmidpfod 
|- ( ph -> .+^ : ( B X. B ) -onto-> 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 5 mgmplusf 
 |-  ( G e. Mgm -> .+^ : ( B X. B ) --> B )
7 3 6 syl 
 |-  ( ph -> .+^ : ( B X. B ) --> B )
8 1 2 5 plusfval 
 |-  ( ( e e. B /\ x e. B ) -> ( e .+^ x ) = ( e .+ x ) )
9 8 adantll 
 |-  ( ( ( ph /\ e e. B ) /\ x e. B ) -> ( e .+^ x ) = ( e .+ x ) )
10 9 eqeq1d 
 |-  ( ( ( ph /\ e e. B ) /\ x e. B ) -> ( ( e .+^ x ) = x <-> ( e .+ x ) = x ) )
11 10 anbi1d 
 |-  ( ( ( ph /\ e e. B ) /\ x e. B ) -> ( ( ( e .+^ x ) = x /\ ( x .+ e ) = x ) <-> ( ( e .+ x ) = x /\ ( x .+ e ) = x ) ) )
12 11 ralbidva 
 |-  ( ( ph /\ e e. B ) -> ( A. x e. B ( ( e .+^ x ) = x /\ ( x .+ e ) = x ) <-> A. x e. B ( ( e .+ x ) = x /\ ( x .+ e ) = x ) ) )
13 12 rexbidva 
 |-  ( ph -> ( E. e e. B A. x e. B ( ( e .+^ x ) = x /\ ( x .+ e ) = x ) <-> E. e e. B A. x e. B ( ( e .+ x ) = x /\ ( x .+ e ) = x ) ) )
14 4 13 mpbird 
 |-  ( ph -> E. e e. B A. x e. B ( ( e .+^ x ) = x /\ ( x .+ e ) = x ) )
15 simpl 
 |-  ( ( ( e .+^ x ) = x /\ ( x .+ e ) = x ) -> ( e .+^ x ) = x )
16 15 ralimi 
 |-  ( A. x e. B ( ( e .+^ x ) = x /\ ( x .+ e ) = x ) -> A. x e. B ( e .+^ x ) = x )
17 oveq2 
 |-  ( x = y -> ( e .+^ x ) = ( e .+^ y ) )
18 id 
 |-  ( x = y -> x = y )
19 17 18 eqeq12d 
 |-  ( x = y -> ( ( e .+^ x ) = x <-> ( e .+^ y ) = y ) )
20 19 rspcv 
 |-  ( y e. B -> ( A. x e. B ( e .+^ x ) = x -> ( e .+^ y ) = y ) )
21 eqcom 
 |-  ( y = ( e .+^ x ) <-> ( e .+^ x ) = y )
22 17 eqeq1d 
 |-  ( x = y -> ( ( e .+^ x ) = y <-> ( e .+^ y ) = y ) )
23 21 22 bitrid 
 |-  ( x = y -> ( y = ( e .+^ x ) <-> ( e .+^ y ) = y ) )
24 23 rspcev 
 |-  ( ( y e. B /\ ( e .+^ y ) = y ) -> E. x e. B y = ( e .+^ x ) )
25 24 ex 
 |-  ( y e. B -> ( ( e .+^ y ) = y -> E. x e. B y = ( e .+^ x ) ) )
26 20 25 syld 
 |-  ( y e. B -> ( A. x e. B ( e .+^ x ) = x -> E. x e. B y = ( e .+^ x ) ) )
27 16 26 syl5 
 |-  ( y e. B -> ( A. x e. B ( ( e .+^ x ) = x /\ ( x .+ e ) = x ) -> E. x e. B y = ( e .+^ x ) ) )
28 27 reximdv 
 |-  ( y e. B -> ( E. e e. B A. x e. B ( ( e .+^ x ) = x /\ ( x .+ e ) = x ) -> E. e e. B E. x e. B y = ( e .+^ x ) ) )
29 28 impcom 
 |-  ( ( E. e e. B A. x e. B ( ( e .+^ x ) = x /\ ( x .+ e ) = x ) /\ y e. B ) -> E. e e. B E. x e. B y = ( e .+^ x ) )
30 29 ralrimiva 
 |-  ( E. e e. B A. x e. B ( ( e .+^ x ) = x /\ ( x .+ e ) = x ) -> A. y e. B E. e e. B E. x e. B y = ( e .+^ x ) )
31 14 30 syl 
 |-  ( ph -> A. y e. B E. e e. B E. x e. B y = ( e .+^ x ) )
32 foov 
 |-  ( .+^ : ( B X. B ) -onto-> B <-> ( .+^ : ( B X. B ) --> B /\ A. y e. B E. e e. B E. x e. B y = ( e .+^ x ) ) )
33 7 31 32 sylanbrc 
 |-  ( ph -> .+^ : ( B X. B ) -onto-> B )