Theorem gxval 25074

Description: The result of the group power operator. (Contributed by Paul Chapman, 17-Apr-2009.) (Revised by Mario Carneiro, 15-Dec-2013.) (New usage is discouraged.)

Hypotheses

Ref	Expression
gxfval.1	|- X = ran G
gxfval.2	|- U = (GId ` G )
gxfval.3	|- N = ( inv ` G )
gxfval.4	|- P = ( ^g ` G )

Assertion

Ref	Expression
gxval	|- ( ( G e. GrpOp /\ A e. X /\ K e. ZZ ) -> ( A P K ) = if ( K = 0 , U , if ( 0 < K , ( seq 1 ( G , ( NN X. { A } ) ) ` K ) , ( N ` ( seq 1 ( G , ( NN X. { A } ) ) ` -u K ) ) ) ) )

Proof of Theorem gxval

Dummy variables x y are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		gxfval.1	. . . . 5 |- X = ran G
2		gxfval.2	. . . . 5 |- U = (GId ` G )
3		gxfval.3	. . . . 5 |- N = ( inv ` G )
4		gxfval.4	. . . . 5 |- P = ( ^g ` G )
5	1, 2, 3, 4	gxfval 25073	. . . 4 |- ( G e. GrpOp -> P = ( x e. X , y e. ZZ |-> if ( y = 0 , U , if ( 0 < y , ( seq 1 ( G , ( NN X. { x } ) ) ` y ) , ( N ` ( seq 1 ( G , ( NN X. { x } ) ) ` -u y ) ) ) ) ) )
6	5	oveqd 6312	. . 3 |- ( G e. GrpOp -> ( A P K ) = ( A ( x e. X , y e. ZZ |-> if ( y = 0 , U , if ( 0 < y , ( seq 1 ( G , ( NN X. { x } ) ) ` y ) , ( N ` ( seq 1 ( G , ( NN X. { x } ) ) ` -u y ) ) ) ) ) K ) )
7		sneq 4043	. . . . . . . . 9 |- ( x = A -> { x } = { A } )
8	7	xpeq2d 5029	. . . . . . . 8 |- ( x = A -> ( NN X. { x } ) = ( NN X. { A } ) )
9	8	seqeq3d 12095	. . . . . . 7 |- ( x = A -> seq 1 ( G , ( NN X. { x } ) ) = seq 1 ( G , ( NN X. { A } ) ) )
10	9	fveq1d 5874	. . . . . 6 |- ( x = A -> ( seq 1 ( G , ( NN X. { x } ) ) ` y ) = ( seq 1 ( G , ( NN X. { A } ) ) ` y ) )
11	9	fveq1d 5874	. . . . . . 7 |- ( x = A -> ( seq 1 ( G , ( NN X. { x } ) ) ` -u y ) = ( seq 1 ( G , ( NN X. { A } ) ) ` -u y ) )
12	11	fveq2d 5876	. . . . . 6 |- ( x = A -> ( N ` ( seq 1 ( G , ( NN X. { x } ) ) ` -u y ) ) = ( N ` ( seq 1 ( G , ( NN X. { A } ) ) ` -u y ) ) )
13	10, 12	ifeq12d 3965	. . . . 5 |- ( x = A -> if ( 0 < y , ( seq 1 ( G , ( NN X. { x } ) ) ` y ) , ( N ` ( seq 1 ( G , ( NN X. { x } ) ) ` -u y ) ) ) = if ( 0 < y , ( seq 1 ( G , ( NN X. { A } ) ) ` y ) , ( N ` ( seq 1 ( G , ( NN X. { A } ) ) ` -u y ) ) ) )
14	13	ifeq2d 3964	. . . 4 |- ( x = A -> if ( y = 0 , U , if ( 0 < y , ( seq 1 ( G , ( NN X. { x } ) ) ` y ) , ( N ` ( seq 1 ( G , ( NN X. { x } ) ) ` -u y ) ) ) ) = if ( y = 0 , U , if ( 0 < y , ( seq 1 ( G , ( NN X. { A } ) ) ` y ) , ( N ` ( seq 1 ( G , ( NN X. { A } ) ) ` -u y ) ) ) ) )
15		eqeq1 2471	. . . . 5 |- ( y = K -> ( y = 0 <-> K = 0 ) )
16		breq2 4457	. . . . . 6 |- ( y = K -> ( 0 < y <-> 0 < K ) )
17		fveq2 5872	. . . . . 6 |- ( y = K -> ( seq 1 ( G , ( NN X. { A } ) ) ` y ) = ( seq 1 ( G , ( NN X. { A } ) ) ` K ) )
18		negeq 9824	. . . . . . . 8 |- ( y = K -> -u y = -u K )
19	18	fveq2d 5876	. . . . . . 7 |- ( y = K -> ( seq 1 ( G , ( NN X. { A } ) ) ` -u y ) = ( seq 1 ( G , ( NN X. { A } ) ) ` -u K ) )
20	19	fveq2d 5876	. . . . . 6 |- ( y = K -> ( N ` ( seq 1 ( G , ( NN X. { A } ) ) ` -u y ) ) = ( N ` ( seq 1 ( G , ( NN X. { A } ) ) ` -u K ) ) )
21	16, 17, 20	ifbieq12d 3972	. . . . 5 |- ( y = K -> if ( 0 < y , ( seq 1 ( G , ( NN X. { A } ) ) ` y ) , ( N ` ( seq 1 ( G , ( NN X. { A } ) ) ` -u y ) ) ) = if ( 0 < K , ( seq 1 ( G , ( NN X. { A } ) ) ` K ) , ( N ` ( seq 1 ( G , ( NN X. { A } ) ) ` -u K ) ) ) )
22	15, 21	ifbieq2d 3970	. . . 4 |- ( y = K -> if ( y = 0 , U , if ( 0 < y , ( seq 1 ( G , ( NN X. { A } ) ) ` y ) , ( N ` ( seq 1 ( G , ( NN X. { A } ) ) ` -u y ) ) ) ) = if ( K = 0 , U , if ( 0 < K , ( seq 1 ( G , ( NN X. { A } ) ) ` K ) , ( N ` ( seq 1 ( G , ( NN X. { A } ) ) ` -u K ) ) ) ) )
23		eqid 2467	. . . 4 |- ( x e. X , y e. ZZ |-> if ( y = 0 , U , if ( 0 < y , ( seq 1 ( G , ( NN X. { x } ) ) ` y ) , ( N ` ( seq 1 ( G , ( NN X. { x } ) ) ` -u y ) ) ) ) ) = ( x e. X , y e. ZZ |-> if ( y = 0 , U , if ( 0 < y , ( seq 1 ( G , ( NN X. { x } ) ) ` y ) , ( N ` ( seq 1 ( G , ( NN X. { x } ) ) ` -u y ) ) ) ) )
24		fvex 5882	. . . . . 6 |- (GId ` G ) e. _V
25	2, 24	eqeltri 2551	. . . . 5 |- U e. _V
26		fvex 5882	. . . . . 6 |- ( seq 1 ( G , ( NN X. { A } ) ) ` K ) e. _V
27		fvex 5882	. . . . . 6 |- ( N ` ( seq 1 ( G , ( NN X. { A } ) ) ` -u K ) ) e. _V
28	26, 27	ifex 4014	. . . . 5 |- if ( 0 < K , ( seq 1 ( G , ( NN X. { A } ) ) ` K ) , ( N ` ( seq 1 ( G , ( NN X. { A } ) ) ` -u K ) ) ) e. _V
29	25, 28	ifex 4014	. . . 4 |- if ( K = 0 , U , if ( 0 < K , ( seq 1 ( G , ( NN X. { A } ) ) ` K ) , ( N ` ( seq 1 ( G , ( NN X. { A } ) ) ` -u K ) ) ) ) e. _V
30	14, 22, 23, 29	ovmpt2 6433	. . 3 |- ( ( A e. X /\ K e. ZZ ) -> ( A ( x e. X , y e. ZZ |-> if ( y = 0 , U , if ( 0 < y , ( seq 1 ( G , ( NN X. { x } ) ) ` y ) , ( N ` ( seq 1 ( G , ( NN X. { x } ) ) ` -u y ) ) ) ) ) K ) = if ( K = 0 , U , if ( 0 < K , ( seq 1 ( G , ( NN X. { A } ) ) ` K ) , ( N ` ( seq 1 ( G , ( NN X. { A } ) ) ` -u K ) ) ) ) )
31	6, 30	sylan9eq 2528	. 2 |- ( ( G e. GrpOp /\ ( A e. X /\ K e. ZZ ) ) -> ( A P K ) = if ( K = 0 , U , if ( 0 < K , ( seq 1 ( G , ( NN X. { A } ) ) ` K ) , ( N ` ( seq 1 ( G , ( NN X. { A } ) ) ` -u K ) ) ) ) )
32	31	3impb 1192	1 |- ( ( G e. GrpOp /\ A e. X /\ K e. ZZ ) -> ( A P K ) = if ( K = 0 , U , if ( 0 < K , ( seq 1 ( G , ( NN X. { A } ) ) ` K ) , ( N ` ( seq 1 ( G , ( NN X. { A } ) ) ` -u K ) ) ) ) )

Syntax hints:   -> wi 4   /\ wa 369   /\ w3a 973   = wceq 1379   e. wcel 1767   _Vcvv 3118   ifcif 3945   {csn 4033   class class class wbr 4453   X. cxp 5003   ran crn 5006   ` cfv 5594  (class class class)co 6295   |-> cmpt2 6297   0cc0 9504   1c1 9505   < clt 9640   -ucneg 9818   NNcn 10548   ZZcz 10876   seqcseq 12087   GrpOpcgr 25002  GIdcgi 25003   invcgn 25004   ^gcgx 25006

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-rep 4564  ax-sep 4574  ax-nul 4582  ax-pow 4631  ax-pr 4692  ax-un 6587  ax-cnex 9560  ax-resscn 9561

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2822  df-rex 2823  df-reu 2824  df-rab 2826  df-v 3120  df-sbc 3337  df-csb 3441  df-dif 3484  df-un 3486  df-in 3488  df-ss 3495  df-nul 3791  df-if 3946  df-pw 4018  df-sn 4034  df-pr 4036  df-op 4040  df-uni 4252  df-iun 4333  df-br 4454  df-opab 4512  df-mpt 4513  df-id 4801  df-xp 5011  df-rel 5012  df-cnv 5013  df-co 5014  df-dm 5015  df-rn 5016  df-res 5017  df-ima 5018  df-iota 5557  df-fun 5596  df-fn 5597  df-f 5598  df-f1 5599  df-fo 5600  df-f1o 5601  df-fv 5602  df-ov 6298  df-oprab 6299  df-mpt2 6300  df-1st 6795  df-2nd 6796  df-recs 7054  df-rdg 7088  df-neg 9820  df-z 10877  df-seq 12088  df-gx 25011

This theorem is referenced by:  gxpval  25075  gxnval  25076  gx0  25077