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

Metamath Proof Explorer

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