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