Metamath Proof Explorer


Theorem lsmfval

Description: The subgroup sum function (for a group or vector space). (Contributed by NM, 28-Jan-2014) (Revised by Mario Carneiro, 19-Apr-2016)

Ref Expression
Hypotheses lsmfval.v
|- B = ( Base ` G )
lsmfval.a
|- .+ = ( +g ` G )
lsmfval.s
|- .(+) = ( LSSum ` G )
Assertion lsmfval
|- ( G e. V -> .(+) = ( t e. ~P B , u e. ~P B |-> ran ( x e. t , y e. u |-> ( x .+ y ) ) ) )

Proof

Step Hyp Ref Expression
1 lsmfval.v
 |-  B = ( Base ` G )
2 lsmfval.a
 |-  .+ = ( +g ` G )
3 lsmfval.s
 |-  .(+) = ( LSSum ` G )
4 elex
 |-  ( G e. V -> G e. _V )
5 fveq2
 |-  ( w = G -> ( Base ` w ) = ( Base ` G ) )
6 5 1 eqtr4di
 |-  ( w = G -> ( Base ` w ) = B )
7 6 pweqd
 |-  ( w = G -> ~P ( Base ` w ) = ~P B )
8 fveq2
 |-  ( w = G -> ( +g ` w ) = ( +g ` G ) )
9 8 2 eqtr4di
 |-  ( w = G -> ( +g ` w ) = .+ )
10 9 oveqd
 |-  ( w = G -> ( x ( +g ` w ) y ) = ( x .+ y ) )
11 10 mpoeq3dv
 |-  ( w = G -> ( x e. t , y e. u |-> ( x ( +g ` w ) y ) ) = ( x e. t , y e. u |-> ( x .+ y ) ) )
12 11 rneqd
 |-  ( w = G -> ran ( x e. t , y e. u |-> ( x ( +g ` w ) y ) ) = ran ( x e. t , y e. u |-> ( x .+ y ) ) )
13 7 7 12 mpoeq123dv
 |-  ( w = G -> ( t e. ~P ( Base ` w ) , u e. ~P ( Base ` w ) |-> ran ( x e. t , y e. u |-> ( x ( +g ` w ) y ) ) ) = ( t e. ~P B , u e. ~P B |-> ran ( x e. t , y e. u |-> ( x .+ y ) ) ) )
14 df-lsm
 |-  LSSum = ( w e. _V |-> ( t e. ~P ( Base ` w ) , u e. ~P ( Base ` w ) |-> ran ( x e. t , y e. u |-> ( x ( +g ` w ) y ) ) ) )
15 1 fvexi
 |-  B e. _V
16 15 pwex
 |-  ~P B e. _V
17 16 16 mpoex
 |-  ( t e. ~P B , u e. ~P B |-> ran ( x e. t , y e. u |-> ( x .+ y ) ) ) e. _V
18 13 14 17 fvmpt
 |-  ( G e. _V -> ( LSSum ` G ) = ( t e. ~P B , u e. ~P B |-> ran ( x e. t , y e. u |-> ( x .+ y ) ) ) )
19 4 18 syl
 |-  ( G e. V -> ( LSSum ` G ) = ( t e. ~P B , u e. ~P B |-> ran ( x e. t , y e. u |-> ( x .+ y ) ) ) )
20 3 19 eqtrid
 |-  ( G e. V -> .(+) = ( t e. ~P B , u e. ~P B |-> ran ( x e. t , y e. u |-> ( x .+ y ) ) ) )