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

Metamath Proof Explorer

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