Metamath Proof Explorer

Theorem grpoinvval

Description: The inverse of a group element. (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 grpoinvval ⊢ G ∈ GrpOp ∧ A ∈ X → N ⁡ A = ι y ∈ X | y G A = 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 1 2 3 grpoinvfval ⊢ G ∈ GrpOp → N = x ∈ X ⟼ ι y ∈ X | y G x = U
5 4 fveq1d ⊢ G ∈ GrpOp → N ⁡ A = x ∈ X ⟼ ι y ∈ X | y G x = U ⁡ A
6 oveq2 ⊢ x = A → y G x = y G A
7 6 eqeq1d ⊢ x = A → y G x = U ↔ y G A = U
8 7 riotabidv ⊢ x = A → ι y ∈ X | y G x = U = ι y ∈ X | y G A = U
9 eqid ⊢ x ∈ X ⟼ ι y ∈ X | y G x = U = x ∈ X ⟼ ι y ∈ X | y G x = U
10 riotaex ⊢ ι y ∈ X | y G A = U ∈ V
11 8 9 10 fvmpt ⊢ A ∈ X → x ∈ X ⟼ ι y ∈ X | y G x = U ⁡ A = ι y ∈ X | y G A = U
12 5 11 sylan9eq ⊢ G ∈ GrpOp ∧ A ∈ X → N ⁡ A = ι y ∈ X | y G A = U