Metamath Proof Explorer

Theorem lsmvalx

Description: Subspace sum value (for a group or vector space). Extended domain version of lsmval . (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 lsmvalx 
|- ( ( G e. V /\ T C_ B /\ U C_ B ) -> ( T .(+) U ) = 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 1 2 3 lsmfval 
 |-  ( G e. V -> .(+) = ( t e. ~P B , u e. ~P B |-> ran ( x e. t , y e. u |-> ( x .+ y ) ) ) )
5 4 oveqd 
 |-  ( G e. V -> ( T .(+) U ) = ( T ( t e. ~P B , u e. ~P B |-> ran ( x e. t , y e. u |-> ( x .+ y ) ) ) U ) )
6 1 fvexi 
 |-  B e. _V
7 6 elpw2 
 |-  ( T e. ~P B <-> T C_ B )
8 6 elpw2 
 |-  ( U e. ~P B <-> U C_ B )
9 mpoexga 
 |-  ( ( T e. ~P B /\ U e. ~P B ) -> ( x e. T , y e. U |-> ( x .+ y ) ) e. _V )
10 rnexg 
 |-  ( ( x e. T , y e. U |-> ( x .+ y ) ) e. _V -> ran ( x e. T , y e. U |-> ( x .+ y ) ) e. _V )
11 9 10 syl 
 |-  ( ( T e. ~P B /\ U e. ~P B ) -> ran ( x e. T , y e. U |-> ( x .+ y ) ) e. _V )
12 mpoeq12 
 |-  ( ( t = T /\ u = U ) -> ( x e. t , y e. u |-> ( x .+ y ) ) = ( x e. T , y e. U |-> ( x .+ y ) ) )
13 12 rneqd 
 |-  ( ( t = T /\ u = U ) -> ran ( x e. t , y e. u |-> ( x .+ y ) ) = ran ( x e. T , y e. U |-> ( x .+ y ) ) )
14 eqid 
 |-  ( t e. ~P B , u e. ~P B |-> ran ( x e. t , y e. u |-> ( x .+ y ) ) ) = ( t e. ~P B , u e. ~P B |-> ran ( x e. t , y e. u |-> ( x .+ y ) ) )
15 13 14 ovmpoga 
 |-  ( ( T e. ~P B /\ U e. ~P B /\ ran ( x e. T , y e. U |-> ( x .+ y ) ) e. _V ) -> ( T ( t e. ~P B , u e. ~P B |-> ran ( x e. t , y e. u |-> ( x .+ y ) ) ) U ) = ran ( x e. T , y e. U |-> ( x .+ y ) ) )
16 11 15 mpd3an3 
 |-  ( ( T e. ~P B /\ U e. ~P B ) -> ( T ( t e. ~P B , u e. ~P B |-> ran ( x e. t , y e. u |-> ( x .+ y ) ) ) U ) = ran ( x e. T , y e. U |-> ( x .+ y ) ) )
17 7 8 16 syl2anbr 
 |-  ( ( T C_ B /\ U C_ B ) -> ( T ( t e. ~P B , u e. ~P B |-> ran ( x e. t , y e. u |-> ( x .+ y ) ) ) U ) = ran ( x e. T , y e. U |-> ( x .+ y ) ) )
18 5 17 sylan9eq 
 |-  ( ( G e. V /\ ( T C_ B /\ U C_ B ) ) -> ( T .(+) U ) = ran ( x e. T , y e. U |-> ( x .+ y ) ) )
19 18 3impb 
 |-  ( ( G e. V /\ T C_ B /\ U C_ B ) -> ( T .(+) U ) = ran ( x e. T , y e. U |-> ( x .+ y ) ) )