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 = ran ⁡ G
grpinvfval.2 ⊢ U = GId ⁡ G
grpinvfval.3 ⊢ N = inv ⁡ G
Assertion grpoinvfval ⊢ G ∈ GrpOp → N = x ∈ X ⟼ ι y ∈ X | y G x = U

Proof

Step Hyp Ref Expression
1 grpinvfval.1 ⊢ X = ran ⁡ G
2 grpinvfval.2 ⊢ U = GId ⁡ G
3 grpinvfval.3 ⊢ N = inv ⁡ G
4 rnexg ⊢ G ∈ GrpOp → ran ⁡ G ∈ V
5 1 4 eqeltrid ⊢ G ∈ GrpOp → X ∈ V
6 mptexg ⊢ X ∈ V → x ∈ X ⟼ ι y ∈ X | y G x = U ∈ V
7 5 6 syl ⊢ G ∈ GrpOp → x ∈ X ⟼ ι y ∈ X | y G x = U ∈ V
8 rneq ⊢ g = G → ran ⁡ g = ran ⁡ G
9 8 1 eqtr4di ⊢ g = G → ran ⁡ g = X
10 oveq ⊢ g = G → y g x = y G x
11 fveq2 ⊢ g = G → GId ⁡ g = GId ⁡ G
12 11 2 eqtr4di ⊢ g = G → GId ⁡ g = U
13 10 12 eqeq12d ⊢ g = G → y g x = GId ⁡ g ↔ y G x = U
14 9 13 riotaeqbidv ⊢ g = G → ι y ∈ ran ⁡ g | y g x = GId ⁡ g = ι y ∈ X | y G x = U
15 9 14 mpteq12dv ⊢ g = G → x ∈ ran ⁡ g ⟼ ι y ∈ ran ⁡ g | y g x = GId ⁡ g = x ∈ X ⟼ ι y ∈ X | y G x = U
16 df-ginv ⊢ inv = g ∈ GrpOp ⟼ x ∈ ran ⁡ g ⟼ ι y ∈ ran ⁡ g | y g x = GId ⁡ g
17 15 16 fvmptg ⊢ G ∈ GrpOp ∧ x ∈ X ⟼ ι y ∈ X | y G x = U ∈ V → inv ⁡ G = x ∈ X ⟼ ι y ∈ X | y G x = U
18 7 17 mpdan ⊢ G ∈ GrpOp → inv ⁡ G = x ∈ X ⟼ ι y ∈ X | y G x = U
19 3 18 syl5eq ⊢ G ∈ GrpOp → N = x ∈ X ⟼ ι y ∈ X | y G x = U