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