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

Metamath Proof Explorer

Theorem mulgfn

Description: Functionality of the group multiple operation. (Contributed by Mario Carneiro, 21-Mar-2015) (Revised by Mario Carneiro, 2-Oct-2015)

Ref Expression
Hypotheses mulgfn.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
mulgfn.t ⊢ · = ( .g ‘ 𝐺 )
Assertion mulgfn · Fn ( ℤ × 𝐵 )

Proof

Step Hyp Ref Expression
1 mulgfn.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 mulgfn.t ⊢ · = ( .g ‘ 𝐺 )
3 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
4 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
5 eqid ⊢ ( invg ‘ 𝐺 ) = ( invg ‘ 𝐺 )
6 1 3 4 5 2 mulgfval ⊢ · = ( 𝑛 ∈ ℤ , 𝑥 ∈ 𝐵 ↦ if ( 𝑛 = 0 , ( 0g ‘ 𝐺 ) , if ( 0 < 𝑛 , ( seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑥 } ) ) ‘ 𝑛 ) , ( ( invg ‘ 𝐺 ) ‘ ( seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑥 } ) ) ‘ - 𝑛 ) ) ) ) )
7 fvex ⊢ ( 0g ‘ 𝐺 ) ∈ V
8 fvex ⊢ ( seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑥 } ) ) ‘ 𝑛 ) ∈ V
9 fvex ⊢ ( ( invg ‘ 𝐺 ) ‘ ( seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑥 } ) ) ‘ - 𝑛 ) ) ∈ V
10 8 9 ifex ⊢ if ( 0 < 𝑛 , ( seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑥 } ) ) ‘ 𝑛 ) , ( ( invg ‘ 𝐺 ) ‘ ( seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑥 } ) ) ‘ - 𝑛 ) ) ) ∈ V
11 7 10 ifex ⊢ if ( 𝑛 = 0 , ( 0g ‘ 𝐺 ) , if ( 0 < 𝑛 , ( seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑥 } ) ) ‘ 𝑛 ) , ( ( invg ‘ 𝐺 ) ‘ ( seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑥 } ) ) ‘ - 𝑛 ) ) ) ) ∈ V
12 6 11 fnmpoi ⊢ · Fn ( ℤ × 𝐵 )