Theorem mulgfvi

Description: The group multiple operation is compatible with identity-function protection. (Contributed by Mario Carneiro, 21-Mar-2015)

	Ref	Expression
Hypothesis	mulgfvi.t	⊢ · = ( .g ‘ 𝐺 )
Assertion	mulgfvi	⊢ · = ( .g ‘ ( I ‘ 𝐺 ) )

Proof

Step	Hyp	Ref	Expression
1		mulgfvi.t	⊢ · = ( .g ‘ 𝐺 )
2		fvi	⊢ ( 𝐺 ∈ V → ( I ‘ 𝐺 ) = 𝐺 )
3	2	eqcomd	⊢ ( 𝐺 ∈ V → 𝐺 = ( I ‘ 𝐺 ) )
4	3	fveq2d	⊢ ( 𝐺 ∈ V → ( .g ‘ 𝐺 ) = ( .g ‘ ( I ‘ 𝐺 ) ) )
5		fvprc	⊢ ( ¬ 𝐺 ∈ V → ( .g ‘ 𝐺 ) = ∅ )
6		fvprc	⊢ ( ¬ 𝐺 ∈ V → ( I ‘ 𝐺 ) = ∅ )
7	6	fveq2d	⊢ ( ¬ 𝐺 ∈ V → ( .g ‘ ( I ‘ 𝐺 ) ) = ( .g ‘ ∅ ) )
8		base0	⊢ ∅ = ( Base ‘ ∅ )
9		eqid	⊢ ( .g ‘ ∅ ) = ( .g ‘ ∅ )
10	8 9	mulgfn	⊢ ( .g ‘ ∅ ) Fn ( ℤ × ∅ )
11		xp0	⊢ ( ℤ × ∅ ) = ∅
12	11	fneq2i	⊢ ( ( .g ‘ ∅ ) Fn ( ℤ × ∅ ) ↔ ( .g ‘ ∅ ) Fn ∅ )
13	10 12	mpbi	⊢ ( .g ‘ ∅ ) Fn ∅
14		fn0	⊢ ( ( .g ‘ ∅ ) Fn ∅ ↔ ( .g ‘ ∅ ) = ∅ )
15	13 14	mpbi	⊢ ( .g ‘ ∅ ) = ∅
16	7 15	eqtrdi	⊢ ( ¬ 𝐺 ∈ V → ( .g ‘ ( I ‘ 𝐺 ) ) = ∅ )
17	5 16	eqtr4d	⊢ ( ¬ 𝐺 ∈ V → ( .g ‘ 𝐺 ) = ( .g ‘ ( I ‘ 𝐺 ) ) )
18	4 17	pm2.61i	⊢ ( .g ‘ 𝐺 ) = ( .g ‘ ( I ‘ 𝐺 ) )
19	1 18	eqtri	⊢ · = ( .g ‘ ( I ‘ 𝐺 ) )