Metamath Proof Explorer

Theorem mulgfvalALT

Description: Shorter proof of mulgfval using ax-rep . (Contributed by Mario Carneiro, 11-Dec-2014) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses mulgval.b 
|- B = ( Base ` G )
mulgval.p 
|- .+ = ( +g ` G )
mulgval.o 
|- .0. = ( 0g ` G )
mulgval.i 
|- I = ( invg ` G )
mulgval.t 
|- .x. = ( .g ` G )
Assertion mulgfvalALT 
|- .x. = ( n e. ZZ , x e. B |-> if ( n = 0 , .0. , if ( 0 < n , ( seq 1 ( .+ , ( NN X. { x } ) ) ` n ) , ( I ` ( seq 1 ( .+ , ( NN X. { x } ) ) ` -u n ) ) ) ) )

Proof

Step Hyp Ref Expression
1 mulgval.b 
 |-  B = ( Base ` G )
2 mulgval.p 
 |-  .+ = ( +g ` G )
3 mulgval.o 
 |-  .0. = ( 0g ` G )
4 mulgval.i 
 |-  I = ( invg ` G )
5 mulgval.t 
 |-  .x. = ( .g ` G )
6 eqidd 
 |-  ( w = G -> ZZ = ZZ )
7 fveq2 
 |-  ( w = G -> ( Base ` w ) = ( Base ` G ) )
8 7 1 eqtr4di 
 |-  ( w = G -> ( Base ` w ) = B )
9 fveq2 
 |-  ( w = G -> ( 0g ` w ) = ( 0g ` G ) )
10 9 3 eqtr4di 
 |-  ( w = G -> ( 0g ` w ) = .0. )
11 seqex 
 |-  seq 1 ( ( +g ` w ) , ( NN X. { x } ) ) e. _V
12 11 a1i 
 |-  ( w = G -> seq 1 ( ( +g ` w ) , ( NN X. { x } ) ) e. _V )
13 id 
 |-  ( s = seq 1 ( ( +g ` w ) , ( NN X. { x } ) ) -> s = seq 1 ( ( +g ` w ) , ( NN X. { x } ) ) )
14 fveq2 
 |-  ( w = G -> ( +g ` w ) = ( +g ` G ) )
15 14 2 eqtr4di 
 |-  ( w = G -> ( +g ` w ) = .+ )
16 15 seqeq2d 
 |-  ( w = G -> seq 1 ( ( +g ` w ) , ( NN X. { x } ) ) = seq 1 ( .+ , ( NN X. { x } ) ) )
17 13 16 sylan9eqr 
 |-  ( ( w = G /\ s = seq 1 ( ( +g ` w ) , ( NN X. { x } ) ) ) -> s = seq 1 ( .+ , ( NN X. { x } ) ) )
18 17 fveq1d 
 |-  ( ( w = G /\ s = seq 1 ( ( +g ` w ) , ( NN X. { x } ) ) ) -> ( s ` n ) = ( seq 1 ( .+ , ( NN X. { x } ) ) ` n ) )
19 simpl 
 |-  ( ( w = G /\ s = seq 1 ( ( +g ` w ) , ( NN X. { x } ) ) ) -> w = G )
20 19 fveq2d 
 |-  ( ( w = G /\ s = seq 1 ( ( +g ` w ) , ( NN X. { x } ) ) ) -> ( invg ` w ) = ( invg ` G ) )
21 20 4 eqtr4di 
 |-  ( ( w = G /\ s = seq 1 ( ( +g ` w ) , ( NN X. { x } ) ) ) -> ( invg ` w ) = I )
22 17 fveq1d 
 |-  ( ( w = G /\ s = seq 1 ( ( +g ` w ) , ( NN X. { x } ) ) ) -> ( s ` -u n ) = ( seq 1 ( .+ , ( NN X. { x } ) ) ` -u n ) )
23 21 22 fveq12d 
 |-  ( ( w = G /\ s = seq 1 ( ( +g ` w ) , ( NN X. { x } ) ) ) -> ( ( invg ` w ) ` ( s ` -u n ) ) = ( I ` ( seq 1 ( .+ , ( NN X. { x } ) ) ` -u n ) ) )
24 18 23 ifeq12d 
 |-  ( ( w = G /\ s = seq 1 ( ( +g ` w ) , ( NN X. { x } ) ) ) -> if ( 0 < n , ( s ` n ) , ( ( invg ` w ) ` ( s ` -u n ) ) ) = if ( 0 < n , ( seq 1 ( .+ , ( NN X. { x } ) ) ` n ) , ( I ` ( seq 1 ( .+ , ( NN X. { x } ) ) ` -u n ) ) ) )
25 12 24 csbied 
 |-  ( w = G -> [_ seq 1 ( ( +g ` w ) , ( NN X. { x } ) ) / s ]_ if ( 0 < n , ( s ` n ) , ( ( invg ` w ) ` ( s ` -u n ) ) ) = if ( 0 < n , ( seq 1 ( .+ , ( NN X. { x } ) ) ` n ) , ( I ` ( seq 1 ( .+ , ( NN X. { x } ) ) ` -u n ) ) ) )
26 10 25 ifeq12d 
 |-  ( w = G -> if ( n = 0 , ( 0g ` w ) , [_ seq 1 ( ( +g ` w ) , ( NN X. { x } ) ) / s ]_ if ( 0 < n , ( s ` n ) , ( ( invg ` w ) ` ( s ` -u n ) ) ) ) = if ( n = 0 , .0. , if ( 0 < n , ( seq 1 ( .+ , ( NN X. { x } ) ) ` n ) , ( I ` ( seq 1 ( .+ , ( NN X. { x } ) ) ` -u n ) ) ) ) )
27 6 8 26 mpoeq123dv 
 |-  ( w = G -> ( n e. ZZ , x e. ( Base ` w ) |-> if ( n = 0 , ( 0g ` w ) , [_ seq 1 ( ( +g ` w ) , ( NN X. { x } ) ) / s ]_ if ( 0 < n , ( s ` n ) , ( ( invg ` w ) ` ( s ` -u n ) ) ) ) ) = ( n e. ZZ , x e. B |-> if ( n = 0 , .0. , if ( 0 < n , ( seq 1 ( .+ , ( NN X. { x } ) ) ` n ) , ( I ` ( seq 1 ( .+ , ( NN X. { x } ) ) ` -u n ) ) ) ) ) )
28 df-mulg 
 |-  .g = ( w e. _V |-> ( n e. ZZ , x e. ( Base ` w ) |-> if ( n = 0 , ( 0g ` w ) , [_ seq 1 ( ( +g ` w ) , ( NN X. { x } ) ) / s ]_ if ( 0 < n , ( s ` n ) , ( ( invg ` w ) ` ( s ` -u n ) ) ) ) ) )
29 zex 
 |-  ZZ e. _V
30 1 fvexi 
 |-  B e. _V
31 29 30 mpoex 
 |-  ( n e. ZZ , x e. B |-> if ( n = 0 , .0. , if ( 0 < n , ( seq 1 ( .+ , ( NN X. { x } ) ) ` n ) , ( I ` ( seq 1 ( .+ , ( NN X. { x } ) ) ` -u n ) ) ) ) ) e. _V
32 27 28 31 fvmpt 
 |-  ( G e. _V -> ( .g ` G ) = ( n e. ZZ , x e. B |-> if ( n = 0 , .0. , if ( 0 < n , ( seq 1 ( .+ , ( NN X. { x } ) ) ` n ) , ( I ` ( seq 1 ( .+ , ( NN X. { x } ) ) ` -u n ) ) ) ) ) )
33 fvprc 
 |-  ( -. G e. _V -> ( .g ` G ) = (/) )
34 eqid 
 |-  ( n e. ZZ , x e. B |-> if ( n = 0 , .0. , if ( 0 < n , ( seq 1 ( .+ , ( NN X. { x } ) ) ` n ) , ( I ` ( seq 1 ( .+ , ( NN X. { x } ) ) ` -u n ) ) ) ) ) = ( n e. ZZ , x e. B |-> if ( n = 0 , .0. , if ( 0 < n , ( seq 1 ( .+ , ( NN X. { x } ) ) ` n ) , ( I ` ( seq 1 ( .+ , ( NN X. { x } ) ) ` -u n ) ) ) ) )
35 3 fvexi 
 |-  .0. e. _V
36 fvex 
 |-  ( seq 1 ( .+ , ( NN X. { x } ) ) ` n ) e. _V
37 fvex 
 |-  ( I ` ( seq 1 ( .+ , ( NN X. { x } ) ) ` -u n ) ) e. _V
38 36 37 ifex 
 |-  if ( 0 < n , ( seq 1 ( .+ , ( NN X. { x } ) ) ` n ) , ( I ` ( seq 1 ( .+ , ( NN X. { x } ) ) ` -u n ) ) ) e. _V
39 35 38 ifex 
 |-  if ( n = 0 , .0. , if ( 0 < n , ( seq 1 ( .+ , ( NN X. { x } ) ) ` n ) , ( I ` ( seq 1 ( .+ , ( NN X. { x } ) ) ` -u n ) ) ) ) e. _V
40 34 39 fnmpoi 
 |-  ( n e. ZZ , x e. B |-> if ( n = 0 , .0. , if ( 0 < n , ( seq 1 ( .+ , ( NN X. { x } ) ) ` n ) , ( I ` ( seq 1 ( .+ , ( NN X. { x } ) ) ` -u n ) ) ) ) ) Fn ( ZZ X. B )
41 fvprc 
 |-  ( -. G e. _V -> ( Base ` G ) = (/) )
42 1 41 eqtrid 
 |-  ( -. G e. _V -> B = (/) )
43 42 xpeq2d 
 |-  ( -. G e. _V -> ( ZZ X. B ) = ( ZZ X. (/) ) )
44 xp0 
 |-  ( ZZ X. (/) ) = (/)
45 43 44 eqtrdi 
 |-  ( -. G e. _V -> ( ZZ X. B ) = (/) )
46 45 fneq2d 
 |-  ( -. G e. _V -> ( ( n e. ZZ , x e. B |-> if ( n = 0 , .0. , if ( 0 < n , ( seq 1 ( .+ , ( NN X. { x } ) ) ` n ) , ( I ` ( seq 1 ( .+ , ( NN X. { x } ) ) ` -u n ) ) ) ) ) Fn ( ZZ X. B ) <-> ( n e. ZZ , x e. B |-> if ( n = 0 , .0. , if ( 0 < n , ( seq 1 ( .+ , ( NN X. { x } ) ) ` n ) , ( I ` ( seq 1 ( .+ , ( NN X. { x } ) ) ` -u n ) ) ) ) ) Fn (/) ) )
47 40 46 mpbii 
 |-  ( -. G e. _V -> ( n e. ZZ , x e. B |-> if ( n = 0 , .0. , if ( 0 < n , ( seq 1 ( .+ , ( NN X. { x } ) ) ` n ) , ( I ` ( seq 1 ( .+ , ( NN X. { x } ) ) ` -u n ) ) ) ) ) Fn (/) )
48 fn0 
 |-  ( ( n e. ZZ , x e. B |-> if ( n = 0 , .0. , if ( 0 < n , ( seq 1 ( .+ , ( NN X. { x } ) ) ` n ) , ( I ` ( seq 1 ( .+ , ( NN X. { x } ) ) ` -u n ) ) ) ) ) Fn (/) <-> ( n e. ZZ , x e. B |-> if ( n = 0 , .0. , if ( 0 < n , ( seq 1 ( .+ , ( NN X. { x } ) ) ` n ) , ( I ` ( seq 1 ( .+ , ( NN X. { x } ) ) ` -u n ) ) ) ) ) = (/) )
49 47 48 sylib 
 |-  ( -. G e. _V -> ( n e. ZZ , x e. B |-> if ( n = 0 , .0. , if ( 0 < n , ( seq 1 ( .+ , ( NN X. { x } ) ) ` n ) , ( I ` ( seq 1 ( .+ , ( NN X. { x } ) ) ` -u n ) ) ) ) ) = (/) )
50 33 49 eqtr4d 
 |-  ( -. G e. _V -> ( .g ` G ) = ( n e. ZZ , x e. B |-> if ( n = 0 , .0. , if ( 0 < n , ( seq 1 ( .+ , ( NN X. { x } ) ) ` n ) , ( I ` ( seq 1 ( .+ , ( NN X. { x } ) ) ` -u n ) ) ) ) ) )
51 32 50 pm2.61i 
 |-  ( .g ` G ) = ( n e. ZZ , x e. B |-> if ( n = 0 , .0. , if ( 0 < n , ( seq 1 ( .+ , ( NN X. { x } ) ) ` n ) , ( I ` ( seq 1 ( .+ , ( NN X. { x } ) ) ` -u n ) ) ) ) )
52 5 51 eqtri 
 |-  .x. = ( n e. ZZ , x e. B |-> if ( n = 0 , .0. , if ( 0 < n , ( seq 1 ( .+ , ( NN X. { x } ) ) ` n ) , ( I ` ( seq 1 ( .+ , ( NN X. { x } ) ) ` -u n ) ) ) ) )