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

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 } ) )