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 ‘ 𝐺 ) )