Metamath Proof Explorer

Theorem idmgmhm

Description: The identity homomorphism on a magma. (Contributed by AV, 27-Feb-2020)

Ref Expression
Hypothesis idmgmhm.b 
|- B = ( Base ` M )
Assertion idmgmhm 
|- ( M e. Mgm -> ( _I |` B ) e. ( M MgmHom M ) )

Proof

Step Hyp Ref Expression
1 idmgmhm.b 
 |-  B = ( Base ` M )
2 id 
 |-  ( M e. Mgm -> M e. Mgm )
3 2 ancri 
 |-  ( M e. Mgm -> ( M e. Mgm /\ M e. Mgm ) )
4 f1oi 
 |-  ( _I |` B ) : B -1-1-onto-> B
5 f1of 
 |-  ( ( _I |` B ) : B -1-1-onto-> B -> ( _I |` B ) : B --> B )
6 4 5 mp1i 
 |-  ( M e. Mgm -> ( _I |` B ) : B --> B )
7 eqid 
 |-  ( +g ` M ) = ( +g ` M )
8 1 7 mgmcl 
 |-  ( ( M e. Mgm /\ a e. B /\ b e. B ) -> ( a ( +g ` M ) b ) e. B )
9 8 3expb 
 |-  ( ( M e. Mgm /\ ( a e. B /\ b e. B ) ) -> ( a ( +g ` M ) b ) e. B )
10 fvresi 
 |-  ( ( a ( +g ` M ) b ) e. B -> ( ( _I |` B ) ` ( a ( +g ` M ) b ) ) = ( a ( +g ` M ) b ) )
11 9 10 syl 
 |-  ( ( M e. Mgm /\ ( a e. B /\ b e. B ) ) -> ( ( _I |` B ) ` ( a ( +g ` M ) b ) ) = ( a ( +g ` M ) b ) )
12 fvresi 
 |-  ( a e. B -> ( ( _I |` B ) ` a ) = a )
13 fvresi 
 |-  ( b e. B -> ( ( _I |` B ) ` b ) = b )
14 12 13 oveqan12d 
 |-  ( ( a e. B /\ b e. B ) -> ( ( ( _I |` B ) ` a ) ( +g ` M ) ( ( _I |` B ) ` b ) ) = ( a ( +g ` M ) b ) )
15 14 adantl 
 |-  ( ( M e. Mgm /\ ( a e. B /\ b e. B ) ) -> ( ( ( _I |` B ) ` a ) ( +g ` M ) ( ( _I |` B ) ` b ) ) = ( a ( +g ` M ) b ) )
16 11 15 eqtr4d 
 |-  ( ( M e. Mgm /\ ( a e. B /\ b e. B ) ) -> ( ( _I |` B ) ` ( a ( +g ` M ) b ) ) = ( ( ( _I |` B ) ` a ) ( +g ` M ) ( ( _I |` B ) ` b ) ) )
17 16 ralrimivva 
 |-  ( M e. Mgm -> A. a e. B A. b e. B ( ( _I |` B ) ` ( a ( +g ` M ) b ) ) = ( ( ( _I |` B ) ` a ) ( +g ` M ) ( ( _I |` B ) ` b ) ) )
18 6 17 jca 
 |-  ( M e. Mgm -> ( ( _I |` B ) : B --> B /\ A. a e. B A. b e. B ( ( _I |` B ) ` ( a ( +g ` M ) b ) ) = ( ( ( _I |` B ) ` a ) ( +g ` M ) ( ( _I |` B ) ` b ) ) ) )
19 1 1 7 7 ismgmhm 
 |-  ( ( _I |` B ) e. ( M MgmHom M ) <-> ( ( M e. Mgm /\ M e. Mgm ) /\ ( ( _I |` B ) : B --> B /\ A. a e. B A. b e. B ( ( _I |` B ) ` ( a ( +g ` M ) b ) ) = ( ( ( _I |` B ) ` a ) ( +g ` M ) ( ( _I |` B ) ` b ) ) ) ) )
20 3 18 19 sylanbrc 
 |-  ( M e. Mgm -> ( _I |` B ) e. ( M MgmHom M ) )