Theorem grpinvfvi

Description: The group inverse function is compatible with identity-function protection. (Contributed by Stefan O'Rear, 21-Mar-2015)

	Ref	Expression
Hypothesis	grpinvfvi.t	|- N = ( invg ` G )
Assertion	grpinvfvi	|- N = ( invg ` ( _I ` G ) )

Proof

Step	Hyp	Ref	Expression
1		grpinvfvi.t	|- N = ( invg ` G )
2		fvi	|- ( G e. _V -> ( _I ` G ) = G )
3	2	fveq2d	|- ( G e. _V -> ( invg ` ( _I ` G ) ) = ( invg ` G ) )
4		base0	|- (/) = ( Base ` (/) )
5		eqid	|- ( invg ` (/) ) = ( invg ` (/) )
6	4 5	grpinvfn	|- ( invg ` (/) ) Fn (/)
7		fn0	|- ( ( invg ` (/) ) Fn (/) <-> ( invg ` (/) ) = (/) )
8	6 7	mpbi	|- ( invg ` (/) ) = (/)
9		fvprc	|- ( -. G e. _V -> ( _I ` G ) = (/) )
10	9	fveq2d	|- ( -. G e. _V -> ( invg ` ( _I ` G ) ) = ( invg ` (/) ) )
11		fvprc	|- ( -. G e. _V -> ( invg ` G ) = (/) )
12	8 10 11	3eqtr4a	|- ( -. G e. _V -> ( invg ` ( _I ` G ) ) = ( invg ` G ) )
13	3 12	pm2.61i	|- ( invg ` ( _I ` G ) ) = ( invg ` G )
14	1 13	eqtr4i	|- N = ( invg ` ( _I ` G ) )