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