Metamath Proof Explorer


Theorem grpoinvfval

Description: The inverse function of a group. (Contributed by NM, 26-Oct-2006) (Revised by Mario Carneiro, 15-Dec-2013) (New usage is discouraged.)

Ref Expression
Hypotheses grpinvfval.1 X=ranG
grpinvfval.2 U=GIdG
grpinvfval.3 N=invG
Assertion grpoinvfval GGrpOpN=xXιyX|yGx=U

Proof

Step Hyp Ref Expression
1 grpinvfval.1 X=ranG
2 grpinvfval.2 U=GIdG
3 grpinvfval.3 N=invG
4 rnexg GGrpOpranGV
5 1 4 eqeltrid GGrpOpXV
6 mptexg XVxXιyX|yGx=UV
7 5 6 syl GGrpOpxXιyX|yGx=UV
8 rneq g=Grang=ranG
9 8 1 eqtr4di g=Grang=X
10 oveq g=Gygx=yGx
11 fveq2 g=GGIdg=GIdG
12 11 2 eqtr4di g=GGIdg=U
13 10 12 eqeq12d g=Gygx=GIdgyGx=U
14 9 13 riotaeqbidv g=Gιyrang|ygx=GIdg=ιyX|yGx=U
15 9 14 mpteq12dv g=Gxrangιyrang|ygx=GIdg=xXιyX|yGx=U
16 df-ginv inv=gGrpOpxrangιyrang|ygx=GIdg
17 15 16 fvmptg GGrpOpxXιyX|yGx=UVinvG=xXιyX|yGx=U
18 7 17 mpdan GGrpOpinvG=xXιyX|yGx=U
19 3 18 eqtrid GGrpOpN=xXιyX|yGx=U