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 
|- B = ( Base ` G )
mulgfn.t 
|- .x. = ( .g ` G )
Assertion mulgfn 
|- .x. Fn ( ZZ X. B )

Proof

Step Hyp Ref Expression
1 mulgfn.b 
 |-  B = ( Base ` G )
2 mulgfn.t 
 |-  .x. = ( .g ` G )
3 eqid 
 |-  ( +g ` G ) = ( +g ` G )
4 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
5 eqid 
 |-  ( invg ` G ) = ( invg ` G )
6 1 3 4 5 2 mulgfval 
 |-  .x. = ( n e. ZZ , x e. B |-> if ( n = 0 , ( 0g ` G ) , if ( 0 < n , ( seq 1 ( ( +g ` G ) , ( NN X. { x } ) ) ` n ) , ( ( invg ` G ) ` ( seq 1 ( ( +g ` G ) , ( NN X. { x } ) ) ` -u n ) ) ) ) )
7 fvex 
 |-  ( 0g ` G ) e. _V
8 fvex 
 |-  ( seq 1 ( ( +g ` G ) , ( NN X. { x } ) ) ` n ) e. _V
9 fvex 
 |-  ( ( invg ` G ) ` ( seq 1 ( ( +g ` G ) , ( NN X. { x } ) ) ` -u n ) ) e. _V
10 8 9 ifex 
 |-  if ( 0 < n , ( seq 1 ( ( +g ` G ) , ( NN X. { x } ) ) ` n ) , ( ( invg ` G ) ` ( seq 1 ( ( +g ` G ) , ( NN X. { x } ) ) ` -u n ) ) ) e. _V
11 7 10 ifex 
 |-  if ( n = 0 , ( 0g ` G ) , if ( 0 < n , ( seq 1 ( ( +g ` G ) , ( NN X. { x } ) ) ` n ) , ( ( invg ` G ) ` ( seq 1 ( ( +g ` G ) , ( NN X. { x } ) ) ` -u n ) ) ) ) e. _V
12 6 11 fnmpoi 
 |-  .x. Fn ( ZZ X. B )