Metamath Proof Explorer


Theorem grp1inv

Description: The inverse function of the trivial group. (Contributed by FL, 21-Jun-2010) (Revised by AV, 26-Aug-2021)

Ref Expression
Hypothesis grp1.m
|- M = { <. ( Base ` ndx ) , { I } >. , <. ( +g ` ndx ) , { <. <. I , I >. , I >. } >. }
Assertion grp1inv
|- ( I e. V -> ( invg ` M ) = ( _I |` { I } ) )

Proof

Step Hyp Ref Expression
1 grp1.m
 |-  M = { <. ( Base ` ndx ) , { I } >. , <. ( +g ` ndx ) , { <. <. I , I >. , I >. } >. }
2 1 grp1
 |-  ( I e. V -> M e. Grp )
3 snex
 |-  { I } e. _V
4 1 grpbase
 |-  ( { I } e. _V -> { I } = ( Base ` M ) )
5 3 4 ax-mp
 |-  { I } = ( Base ` M )
6 eqid
 |-  ( invg ` M ) = ( invg ` M )
7 5 6 grpinvf
 |-  ( M e. Grp -> ( invg ` M ) : { I } --> { I } )
8 2 7 syl
 |-  ( I e. V -> ( invg ` M ) : { I } --> { I } )
9 fsng
 |-  ( ( I e. V /\ I e. V ) -> ( ( invg ` M ) : { I } --> { I } <-> ( invg ` M ) = { <. I , I >. } ) )
10 9 anidms
 |-  ( I e. V -> ( ( invg ` M ) : { I } --> { I } <-> ( invg ` M ) = { <. I , I >. } ) )
11 simpr
 |-  ( ( I e. V /\ ( invg ` M ) = { <. I , I >. } ) -> ( invg ` M ) = { <. I , I >. } )
12 restidsing
 |-  ( _I |` { I } ) = ( { I } X. { I } )
13 xpsng
 |-  ( ( I e. V /\ I e. V ) -> ( { I } X. { I } ) = { <. I , I >. } )
14 13 anidms
 |-  ( I e. V -> ( { I } X. { I } ) = { <. I , I >. } )
15 12 14 eqtr2id
 |-  ( I e. V -> { <. I , I >. } = ( _I |` { I } ) )
16 15 adantr
 |-  ( ( I e. V /\ ( invg ` M ) = { <. I , I >. } ) -> { <. I , I >. } = ( _I |` { I } ) )
17 11 16 eqtrd
 |-  ( ( I e. V /\ ( invg ` M ) = { <. I , I >. } ) -> ( invg ` M ) = ( _I |` { I } ) )
18 17 ex
 |-  ( I e. V -> ( ( invg ` M ) = { <. I , I >. } -> ( invg ` M ) = ( _I |` { I } ) ) )
19 10 18 sylbid
 |-  ( I e. V -> ( ( invg ` M ) : { I } --> { I } -> ( invg ` M ) = ( _I |` { I } ) ) )
20 8 19 mpd
 |-  ( I e. V -> ( invg ` M ) = ( _I |` { I } ) )