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