Metamath Proof Explorer


Theorem grpinvfn

Description: Functionality of the group inverse function. (Contributed by Stefan O'Rear, 21-Mar-2015)

Ref Expression
Hypotheses grpinvfn.b 𝐵 = ( Base ‘ 𝐺 )
grpinvfn.n 𝑁 = ( invg𝐺 )
Assertion grpinvfn 𝑁 Fn 𝐵

Proof

Step Hyp Ref Expression
1 grpinvfn.b 𝐵 = ( Base ‘ 𝐺 )
2 grpinvfn.n 𝑁 = ( invg𝐺 )
3 riotaex ( 𝑦𝐵 ( 𝑦 ( +g𝐺 ) 𝑥 ) = ( 0g𝐺 ) ) ∈ V
4 eqid ( +g𝐺 ) = ( +g𝐺 )
5 eqid ( 0g𝐺 ) = ( 0g𝐺 )
6 1 4 5 2 grpinvfval 𝑁 = ( 𝑥𝐵 ↦ ( 𝑦𝐵 ( 𝑦 ( +g𝐺 ) 𝑥 ) = ( 0g𝐺 ) ) )
7 3 6 fnmpti 𝑁 Fn 𝐵