Metamath Proof Explorer

Theorem idmhm

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

Ref Expression
Hypothesis idmhm.b 
|- B = ( Base ` M )
Assertion idmhm 
|- ( M e. Mnd -> ( _I |` B ) e. ( M MndHom M ) )

Proof

Step Hyp Ref Expression
1 idmhm.b 
 |-  B = ( Base ` M )
2 id 
 |-  ( M e. Mnd -> M e. Mnd )
3 f1oi 
 |-  ( _I |` B ) : B -1-1-onto-> B
4 f1of 
 |-  ( ( _I |` B ) : B -1-1-onto-> B -> ( _I |` B ) : B --> B )
5 3 4 mp1i 
 |-  ( M e. Mnd -> ( _I |` B ) : B --> B )
6 eqid 
 |-  ( +g ` M ) = ( +g ` M )
7 1 6 mndcl 
 |-  ( ( M e. Mnd /\ a e. B /\ b e. B ) -> ( a ( +g ` M ) b ) e. B )
8 7 3expb 
 |-  ( ( M e. Mnd /\ ( a e. B /\ b e. B ) ) -> ( a ( +g ` M ) b ) e. B )
9 fvresi 
 |-  ( ( a ( +g ` M ) b ) e. B -> ( ( _I |` B ) ` ( a ( +g ` M ) b ) ) = ( a ( +g ` M ) b ) )
10 8 9 syl 
 |-  ( ( M e. Mnd /\ ( a e. B /\ b e. B ) ) -> ( ( _I |` B ) ` ( a ( +g ` M ) b ) ) = ( a ( +g ` M ) b ) )
11 fvresi 
 |-  ( a e. B -> ( ( _I |` B ) ` a ) = a )
12 fvresi 
 |-  ( b e. B -> ( ( _I |` B ) ` b ) = b )
13 11 12 oveqan12d 
 |-  ( ( a e. B /\ b e. B ) -> ( ( ( _I |` B ) ` a ) ( +g ` M ) ( ( _I |` B ) ` b ) ) = ( a ( +g ` M ) b ) )
14 13 adantl 
 |-  ( ( M e. Mnd /\ ( a e. B /\ b e. B ) ) -> ( ( ( _I |` B ) ` a ) ( +g ` M ) ( ( _I |` B ) ` b ) ) = ( a ( +g ` M ) b ) )
15 10 14 eqtr4d 
 |-  ( ( M e. Mnd /\ ( a e. B /\ b e. B ) ) -> ( ( _I |` B ) ` ( a ( +g ` M ) b ) ) = ( ( ( _I |` B ) ` a ) ( +g ` M ) ( ( _I |` B ) ` b ) ) )
16 15 ralrimivva 
 |-  ( M e. Mnd -> A. a e. B A. b e. B ( ( _I |` B ) ` ( a ( +g ` M ) b ) ) = ( ( ( _I |` B ) ` a ) ( +g ` M ) ( ( _I |` B ) ` b ) ) )
17 eqid 
 |-  ( 0g ` M ) = ( 0g ` M )
18 1 17 mndidcl 
 |-  ( M e. Mnd -> ( 0g ` M ) e. B )
19 fvresi 
 |-  ( ( 0g ` M ) e. B -> ( ( _I |` B ) ` ( 0g ` M ) ) = ( 0g ` M ) )
20 18 19 syl 
 |-  ( M e. Mnd -> ( ( _I |` B ) ` ( 0g ` M ) ) = ( 0g ` M ) )
21 5 16 20 3jca 
 |-  ( M e. Mnd -> ( ( _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 ) ) /\ ( ( _I |` B ) ` ( 0g ` M ) ) = ( 0g ` M ) ) )
22 1 1 6 6 17 17 ismhm 
 |-  ( ( _I |` B ) e. ( M MndHom M ) <-> ( ( M e. Mnd /\ M e. Mnd ) /\ ( ( _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 ) ) /\ ( ( _I |` B ) ` ( 0g ` M ) ) = ( 0g ` M ) ) ) )
23 2 2 21 22 syl21anbrc 
 |-  ( M e. Mnd -> ( _I |` B ) e. ( M MndHom M ) )