This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝑁 = ( invg ‘ 𝐺 )
Assertion grpinvfvi 𝑁 = ( invg ‘ ( I ‘ 𝐺 ) )

Proof

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