Metamath Proof Explorer

Theorem grpinvfvi

Description: The group inverse function is compatible with identity-function protection. (Contributed by Stefan O'Rear, 21-Mar-2015)

Ref Expression
Hypothesis grpinvfvi.t ⊢ N = inv g ⁡ G
Assertion grpinvfvi ⊢ N = inv g ⁡ I ⁡ G

Proof

Step Hyp Ref Expression
1 grpinvfvi.t ⊢ N = inv g ⁡ G
2 fvi ⊢ G ∈ V → I ⁡ G = G
3 2 fveq2d ⊢ G ∈ V → inv g ⁡ I ⁡ G = inv g ⁡ G
4 base0 ⊢ ∅ = Base ∅
5 eqid ⊢ inv g ⁡ ∅ = inv g ⁡ ∅
6 4 5 grpinvfn ⊢ inv g ⁡ ∅ Fn ∅
7 fn0 ⊢ inv g ⁡ ∅ Fn ∅ ↔ inv g ⁡ ∅ = ∅
8 6 7 mpbi ⊢ inv g ⁡ ∅ = ∅
9 fvprc ⊢ ¬ G ∈ V → I ⁡ G = ∅
10 9 fveq2d ⊢ ¬ G ∈ V → inv g ⁡ I ⁡ G = inv g ⁡ ∅
11 fvprc ⊢ ¬ G ∈ V → inv g ⁡ G = ∅
12 8 10 11 3eqtr4a ⊢ ¬ G ∈ V → inv g ⁡ I ⁡ G = inv g ⁡ G
13 3 12 pm2.61i ⊢ inv g ⁡ I ⁡ G = inv g ⁡ G
14 1 13 eqtr4i ⊢ N = inv g ⁡ I ⁡ G