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 sselid
 |-  ( ( 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 eqtrid
 |-  ( -. G e. _V -> B = (/) )
125 124 xpeq2d
 |-  ( -. G e. _V -> ( ZZ X. B ) = ( ZZ X. (/) ) )
126 xp0
 |-  ( ZZ X. (/) ) = (/)
127 125 126 eqtrdi
 |-  ( -. 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 ) ) ) ) )