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 ( ℤ × 𝐵 )