This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) ) ) )