Metamath Proof Explorer

Theorem mulgfval

Description: Group multiple (exponentiation) operation. For a shorter proof using ax-rep , see mulgfvalALT . (Contributed by Mario Carneiro, 11-Dec-2014) Remove dependency on ax-rep . (Revised by Rohan Ridenour, 17-Aug-2023)

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 mulgfval 
|- .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 fvex 
 |-  ( +g ` w ) e. _V
12 1z 
 |-  1 e. ZZ
13 11 12 seqexw 
 |-  seq 1 ( ( +g ` w ) , ( NN X. { x } ) ) e. _V
14 13 a1i 
 |-  ( w = G -> seq 1 ( ( +g ` w ) , ( NN X. { x } ) ) e. _V )
15 id 
 |-  ( s = seq 1 ( ( +g ` w ) , ( NN X. { x } ) ) -> s = seq 1 ( ( +g ` w ) , ( NN X. { x } ) ) )
16 fveq2 
 |-  ( w = G -> ( +g ` w ) = ( +g ` G ) )
17 16 2 eqtr4di 
 |-  ( w = G -> ( +g ` w ) = .+ )
18 17 seqeq2d 
 |-  ( w = G -> seq 1 ( ( +g ` w ) , ( NN X. { x } ) ) = seq 1 ( .+ , ( NN X. { x } ) ) )
19 15 18 sylan9eqr 
 |-  ( ( w = G /\ s = seq 1 ( ( +g ` w ) , ( NN X. { x } ) ) ) -> s = seq 1 ( .+ , ( NN X. { x } ) ) )
20 19 fveq1d 
 |-  ( ( w = G /\ s = seq 1 ( ( +g ` w ) , ( NN X. { x } ) ) ) -> ( s ` n ) = ( seq 1 ( .+ , ( NN X. { x } ) ) ` n ) )
21 simpl 
 |-  ( ( w = G /\ s = seq 1 ( ( +g ` w ) , ( NN X. { x } ) ) ) -> w = G )
22 21 fveq2d 
 |-  ( ( w = G /\ s = seq 1 ( ( +g ` w ) , ( NN X. { x } ) ) ) -> ( invg ` w ) = ( invg ` G ) )
23 22 4 eqtr4di 
 |-  ( ( w = G /\ s = seq 1 ( ( +g ` w ) , ( NN X. { x } ) ) ) -> ( invg ` w ) = I )
24 19 fveq1d 
 |-  ( ( w = G /\ s = seq 1 ( ( +g ` w ) , ( NN X. { x } ) ) ) -> ( s ` -u n ) = ( seq 1 ( .+ , ( NN X. { x } ) ) ` -u n ) )
25 23 24 fveq12d 
 |-  ( ( w = G /\ s = seq 1 ( ( +g ` w ) , ( NN X. { x } ) ) ) -> ( ( invg ` w ) ` ( s ` -u n ) ) = ( I ` ( seq 1 ( .+ , ( NN X. { x } ) ) ` -u n ) ) )
26 20 25 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 ) ) ) )
27 14 26 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 ) ) ) )
28 10 27 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 ) ) ) ) )
29 6 8 28 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 ) ) ) ) ) )
30 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 ) ) ) ) ) )
31 zex 
 |-  ZZ e. _V
32 1 fvexi 
 |-  B e. _V
33 snex 
 |-  { .0. } e. _V
34 2 fvexi 
 |-  .+ e. _V
35 34 rnex 
 |-  ran .+ e. _V
36 35 32 unex 
 |-  ( ran .+ u. B ) e. _V
37 4 fvexi 
 |-  I e. _V
38 37 rnex 
 |-  ran I e. _V
39 p0ex 
 |-  { (/) } e. _V
40 38 39 unex 
 |-  ( ran I u. { (/) } ) e. _V
41 36 40 unex 
 |-  ( ( ran .+ u. B ) u. ( ran I u. { (/) } ) ) e. _V
42 33 41 unex 
 |-  ( { .0. } u. ( ( ran .+ u. B ) u. ( ran I u. { (/) } ) ) ) e. _V
43 ssun1 
 |-  { .0. } C_ ( { .0. } u. ( ( ran .+ u. B ) u. ( ran I u. { (/) } ) ) )
44 3 fvexi 
 |-  .0. e. _V
45 44 snid 
 |-  .0. e. { .0. }
46 43 45 sselii 
 |-  .0. e. ( { .0. } u. ( ( ran .+ u. B ) u. ( ran I u. { (/) } ) ) )
47 46 a1i 
 |-  ( ( n e. ZZ /\ x e. B ) -> .0. e. ( { .0. } u. ( ( ran .+ u. B ) u. ( ran I u. { (/) } ) ) ) )
48 ssun2 
 |-  B C_ ( ran .+ u. B )
49 ssun1 
 |-  ( ran .+ u. B ) C_ ( ( ran .+ u. B ) u. ( ran I u. { (/) } ) )
50 48 49 sstri 
 |-  B C_ ( ( ran .+ u. B ) u. ( ran I u. { (/) } ) )
51 ssun2 
 |-  ( ( ran .+ u. B ) u. ( ran I u. { (/) } ) ) C_ ( { .0. } u. ( ( ran .+ u. B ) u. ( ran I u. { (/) } ) ) )
52 50 51 sstri 
 |-  B C_ ( { .0. } u. ( ( ran .+ u. B ) u. ( ran I u. { (/) } ) ) )
53 fveq2 
 |-  ( n = 1 -> ( seq 1 ( .+ , ( NN X. { x } ) ) ` n ) = ( seq 1 ( .+ , ( NN X. { x } ) ) ` 1 ) )
54 53 adantl 
 |-  ( ( x e. B /\ n = 1 ) -> ( seq 1 ( .+ , ( NN X. { x } ) ) ` n ) = ( seq 1 ( .+ , ( NN X. { x } ) ) ` 1 ) )
55 seq1 
 |-  ( 1 e. ZZ -> ( seq 1 ( .+ , ( NN X. { x } ) ) ` 1 ) = ( ( NN X. { x } ) ` 1 ) )
56 12 55 ax-mp 
 |-  ( seq 1 ( .+ , ( NN X. { x } ) ) ` 1 ) = ( ( NN X. { x } ) ` 1 )
57 1nn 
 |-  1 e. NN
58 vex 
 |-  x e. _V
59 58 fvconst2 
 |-  ( 1 e. NN -> ( ( NN X. { x } ) ` 1 ) = x )
60 57 59 ax-mp 
 |-  ( ( NN X. { x } ) ` 1 ) = x
61 60 eleq1i 
 |-  ( ( ( NN X. { x } ) ` 1 ) e. B <-> x e. B )
62 61 biimpri 
 |-  ( x e. B -> ( ( NN X. { x } ) ` 1 ) e. B )
63 56 62 eqeltrid 
 |-  ( x e. B -> ( seq 1 ( .+ , ( NN X. { x } ) ) ` 1 ) e. B )
64 63 adantr 
 |-  ( ( x e. B /\ n = 1 ) -> ( seq 1 ( .+ , ( NN X. { x } ) ) ` 1 ) e. B )
65 54 64 eqeltrd 
 |-  ( ( x e. B /\ n = 1 ) -> ( seq 1 ( .+ , ( NN X. { x } ) ) ` n ) e. B )
66 52 65 sseldi 
 |-  ( ( x e. B /\ n = 1 ) -> ( seq 1 ( .+ , ( NN X. { x } ) ) ` n ) e. ( { .0. } u. ( ( ran .+ u. B ) u. ( ran I u. { (/) } ) ) ) )
67 66 ad4ant24 
 |-  ( ( ( ( n e. ZZ /\ x e. B ) /\ n e. ( ZZ>= ` 1 ) ) /\ n = 1 ) -> ( seq 1 ( .+ , ( NN X. { x } ) ) ` n ) e. ( { .0. } u. ( ( ran .+ u. B ) u. ( ran I u. { (/) } ) ) ) )
68 zcn 
 |-  ( n e. ZZ -> n e. CC )
69 npcan1 
 |-  ( n e. CC -> ( ( n - 1 ) + 1 ) = n )
70 68 69 syl 
 |-  ( n e. ZZ -> ( ( n - 1 ) + 1 ) = n )
71 70 fveq2d 
 |-  ( n e. ZZ -> ( seq 1 ( .+ , ( NN X. { x } ) ) ` ( ( n - 1 ) + 1 ) ) = ( seq 1 ( .+ , ( NN X. { x } ) ) ` n ) )
72 71 adantr 
 |-  ( ( n e. ZZ /\ ( n - 1 ) e. ( ZZ>= ` 1 ) ) -> ( seq 1 ( .+ , ( NN X. { x } ) ) ` ( ( n - 1 ) + 1 ) ) = ( seq 1 ( .+ , ( NN X. { x } ) ) ` n ) )
73 seqp1 
 |-  ( ( n - 1 ) e. ( ZZ>= ` 1 ) -> ( seq 1 ( .+ , ( NN X. { x } ) ) ` ( ( n - 1 ) + 1 ) ) = ( ( seq 1 ( .+ , ( NN X. { x } ) ) ` ( n - 1 ) ) .+ ( ( NN X. { x } ) ` ( ( n - 1 ) + 1 ) ) ) )
74 ssun1 
 |-  ran .+ C_ ( ran .+ u. B )
75 ssun2 
 |-  { (/) } C_ ( ran I u. { (/) } )
76 unss12 
 |-  ( ( ran .+ C_ ( ran .+ u. B ) /\ { (/) } C_ ( ran I u. { (/) } ) ) -> ( ran .+ u. { (/) } ) C_ ( ( ran .+ u. B ) u. ( ran I u. { (/) } ) ) )
77 74 75 76 mp2an 
 |-  ( ran .+ u. { (/) } ) C_ ( ( ran .+ u. B ) u. ( ran I u. { (/) } ) )
78 77 51 sstri 
 |-  ( ran .+ u. { (/) } ) C_ ( { .0. } u. ( ( ran .+ u. B ) u. ( ran I u. { (/) } ) ) )
79 df-ov 
 |-  ( ( seq 1 ( .+ , ( NN X. { x } ) ) ` ( n - 1 ) ) .+ ( ( NN X. { x } ) ` ( ( n - 1 ) + 1 ) ) ) = ( .+ ` <. ( seq 1 ( .+ , ( NN X. { x } ) ) ` ( n - 1 ) ) , ( ( NN X. { x } ) ` ( ( n - 1 ) + 1 ) ) >. )
80 fvrn0 
 |-  ( .+ ` <. ( seq 1 ( .+ , ( NN X. { x } ) ) ` ( n - 1 ) ) , ( ( NN X. { x } ) ` ( ( n - 1 ) + 1 ) ) >. ) e. ( ran .+ u. { (/) } )
81 79 80 eqeltri 
 |-  ( ( seq 1 ( .+ , ( NN X. { x } ) ) ` ( n - 1 ) ) .+ ( ( NN X. { x } ) ` ( ( n - 1 ) + 1 ) ) ) e. ( ran .+ u. { (/) } )
82 78 81 sselii 
 |-  ( ( seq 1 ( .+ , ( NN X. { x } ) ) ` ( n - 1 ) ) .+ ( ( NN X. { x } ) ` ( ( n - 1 ) + 1 ) ) ) e. ( { .0. } u. ( ( ran .+ u. B ) u. ( ran I u. { (/) } ) ) )
83 73 82 eqeltrdi 
 |-  ( ( n - 1 ) e. ( ZZ>= ` 1 ) -> ( seq 1 ( .+ , ( NN X. { x } ) ) ` ( ( n - 1 ) + 1 ) ) e. ( { .0. } u. ( ( ran .+ u. B ) u. ( ran I u. { (/) } ) ) ) )
84 83 adantl 
 |-  ( ( n e. ZZ /\ ( n - 1 ) e. ( ZZ>= ` 1 ) ) -> ( seq 1 ( .+ , ( NN X. { x } ) ) ` ( ( n - 1 ) + 1 ) ) e. ( { .0. } u. ( ( ran .+ u. B ) u. ( ran I u. { (/) } ) ) ) )
85 72 84 eqeltrrd 
 |-  ( ( n e. ZZ /\ ( n - 1 ) e. ( ZZ>= ` 1 ) ) -> ( seq 1 ( .+ , ( NN X. { x } ) ) ` n ) e. ( { .0. } u. ( ( ran .+ u. B ) u. ( ran I u. { (/) } ) ) ) )
86 85 ad4ant14 
 |-  ( ( ( ( n e. ZZ /\ x e. B ) /\ n e. ( ZZ>= ` 1 ) ) /\ ( n - 1 ) e. ( ZZ>= ` 1 ) ) -> ( seq 1 ( .+ , ( NN X. { x } ) ) ` n ) e. ( { .0. } u. ( ( ran .+ u. B ) u. ( ran I u. { (/) } ) ) ) )
87 uzm1 
 |-  ( n e. ( ZZ>= ` 1 ) -> ( n = 1 \/ ( n - 1 ) e. ( ZZ>= ` 1 ) ) )
88 87 adantl 
 |-  ( ( ( n e. ZZ /\ x e. B ) /\ n e. ( ZZ>= ` 1 ) ) -> ( n = 1 \/ ( n - 1 ) e. ( ZZ>= ` 1 ) ) )
89 67 86 88 mpjaodan 
 |-  ( ( ( n e. ZZ /\ x e. B ) /\ n e. ( ZZ>= ` 1 ) ) -> ( seq 1 ( .+ , ( NN X. { x } ) ) ` n ) e. ( { .0. } u. ( ( ran .+ u. B ) u. ( ran I u. { (/) } ) ) ) )
90 simpr 
 |-  ( ( ( n e. ZZ /\ x e. B ) /\ -. n e. ( ZZ>= ` 1 ) ) -> -. n e. ( ZZ>= ` 1 ) )
91 seqfn 
 |-  ( 1 e. ZZ -> seq 1 ( .+ , ( NN X. { x } ) ) Fn ( ZZ>= ` 1 ) )
92 12 91 ax-mp 
 |-  seq 1 ( .+ , ( NN X. { x } ) ) Fn ( ZZ>= ` 1 )
93 92 fndmi 
 |-  dom seq 1 ( .+ , ( NN X. { x } ) ) = ( ZZ>= ` 1 )
94 93 eleq2i 
 |-  ( n e. dom seq 1 ( .+ , ( NN X. { x } ) ) <-> n e. ( ZZ>= ` 1 ) )
95 90 94 sylnibr 
 |-  ( ( ( n e. ZZ /\ x e. B ) /\ -. n e. ( ZZ>= ` 1 ) ) -> -. n e. dom seq 1 ( .+ , ( NN X. { x } ) ) )
96 ndmfv 
 |-  ( -. n e. dom seq 1 ( .+ , ( NN X. { x } ) ) -> ( seq 1 ( .+ , ( NN X. { x } ) ) ` n ) = (/) )
97 95 96 syl 
 |-  ( ( ( n e. ZZ /\ x e. B ) /\ -. n e. ( ZZ>= ` 1 ) ) -> ( seq 1 ( .+ , ( NN X. { x } ) ) ` n ) = (/) )
98 ssun2 
 |-  ( ran I u. { (/) } ) C_ ( ( ran .+ u. B ) u. ( ran I u. { (/) } ) )
99 75 98 sstri 
 |-  { (/) } C_ ( ( ran .+ u. B ) u. ( ran I u. { (/) } ) )
100 99 51 sstri 
 |-  { (/) } C_ ( { .0. } u. ( ( ran .+ u. B ) u. ( ran I u. { (/) } ) ) )
101 0ex 
 |-  (/) e. _V
102 101 snid 
 |-  (/) e. { (/) }
103 100 102 sselii 
 |-  (/) e. ( { .0. } u. ( ( ran .+ u. B ) u. ( ran I u. { (/) } ) ) )
104 103 a1i 
 |-  ( ( ( n e. ZZ /\ x e. B ) /\ -. n e. ( ZZ>= ` 1 ) ) -> (/) e. ( { .0. } u. ( ( ran .+ u. B ) u. ( ran I u. { (/) } ) ) ) )
105 97 104 eqeltrd 
 |-  ( ( ( n e. ZZ /\ x e. B ) /\ -. n e. ( ZZ>= ` 1 ) ) -> ( seq 1 ( .+ , ( NN X. { x } ) ) ` n ) e. ( { .0. } u. ( ( ran .+ u. B ) u. ( ran I u. { (/) } ) ) ) )
106 89 105 pm2.61dan 
 |-  ( ( n e. ZZ /\ x e. B ) -> ( seq 1 ( .+ , ( NN X. { x } ) ) ` n ) e. ( { .0. } u. ( ( ran .+ u. B ) u. ( ran I u. { (/) } ) ) ) )
107 98 51 sstri 
 |-  ( ran I u. { (/) } ) C_ ( { .0. } u. ( ( ran .+ u. B ) u. ( ran I u. { (/) } ) ) )
108 fvrn0 
 |-  ( I ` ( seq 1 ( .+ , ( NN X. { x } ) ) ` -u n ) ) e. ( ran I u. { (/) } )
109 107 108 sselii 
 |-  ( I ` ( seq 1 ( .+ , ( NN X. { x } ) ) ` -u n ) ) e. ( { .0. } u. ( ( ran .+ u. B ) u. ( ran I u. { (/) } ) ) )
110 109 a1i 
 |-  ( ( n e. ZZ /\ x e. B ) -> ( I ` ( seq 1 ( .+ , ( NN X. { x } ) ) ` -u n ) ) e. ( { .0. } u. ( ( ran .+ u. B ) u. ( ran I u. { (/) } ) ) ) )
111 106 110 ifcld 
 |-  ( ( n e. ZZ /\ x e. B ) -> if ( 0 < n , ( seq 1 ( .+ , ( NN X. { x } ) ) ` n ) , ( I ` ( seq 1 ( .+ , ( NN X. { x } ) ) ` -u n ) ) ) e. ( { .0. } u. ( ( ran .+ u. B ) u. ( ran I u. { (/) } ) ) ) )
112 47 111 ifcld 
 |-  ( ( 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. ( { .0. } u. ( ( ran .+ u. B ) u. ( ran I u. { (/) } ) ) ) )
113 112 rgen2 
 |-  A. n e. ZZ A. 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. ( { .0. } u. ( ( ran .+ u. B ) u. ( ran I u. { (/) } ) ) )
114 31 32 42 113 mpoexw 
 |-  ( 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
115 29 30 114 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 ) ) ) ) ) )
116 fvprc 
 |-  ( -. G e. _V -> ( .g ` G ) = (/) )
117 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 ) ) ) ) )
118 fvex 
 |-  ( seq 1 ( .+ , ( NN X. { x } ) ) ` n ) e. _V
119 fvex 
 |-  ( I ` ( seq 1 ( .+ , ( NN X. { x } ) ) ` -u n ) ) e. _V
120 118 119 ifex 
 |-  if ( 0 < n , ( seq 1 ( .+ , ( NN X. { x } ) ) ` n ) , ( I ` ( seq 1 ( .+ , ( NN X. { x } ) ) ` -u n ) ) ) e. _V
121 44 120 ifex 
 |-  if ( n = 0 , .0. , if ( 0 < n , ( seq 1 ( .+ , ( NN X. { x } ) ) ` n ) , ( I ` ( seq 1 ( .+ , ( NN X. { x } ) ) ` -u n ) ) ) ) e. _V
122 117 121 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 )
123 fvprc 
 |-  ( -. G e. _V -> ( Base ` G ) = (/) )
124 1 123 syl5eq 
 |-  ( -. G e. _V -> B = (/) )
125 124 xpeq2d 
 |-  ( -. G e. _V -> ( ZZ X. B ) = ( ZZ X. (/) ) )
126 xp0 
 |-  ( ZZ X. (/) ) = (/)
127 125 126 syl6eq 
 |-  ( -. G e. _V -> ( ZZ X. B ) = (/) )
128 127 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 (/) ) )
129 122 128 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 (/) )
130 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 ) ) ) ) ) = (/) )
131 129 130 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 ) ) ) ) ) = (/) )
132 116 131 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 ) ) ) ) ) )
133 115 132 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 ) ) ) ) )
134 5 133 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 ) ) ) ) )