Metamath Proof Explorer


Theorem lsmelvalx

Description: Subspace sum membership (for a group or vector space). Extended domain version of lsmelval . (Contributed by NM, 28-Jan-2014) (Revised by Mario Carneiro, 19-Apr-2016)

Ref Expression
Hypotheses lsmfval.v B = Base G
lsmfval.a + ˙ = + G
lsmfval.s ˙ = LSSum G
Assertion lsmelvalx G V T B U B X T ˙ U y T z U X = y + ˙ z

Proof

Step Hyp Ref Expression
1 lsmfval.v B = Base G
2 lsmfval.a + ˙ = + G
3 lsmfval.s ˙ = LSSum G
4 1 2 3 lsmvalx G V T B U B T ˙ U = ran y T , z U y + ˙ z
5 4 eleq2d G V T B U B X T ˙ U X ran y T , z U y + ˙ z
6 eqid y T , z U y + ˙ z = y T , z U y + ˙ z
7 ovex y + ˙ z V
8 6 7 elrnmpo X ran y T , z U y + ˙ z y T z U X = y + ˙ z
9 5 8 bitrdi G V T B U B X T ˙ U y T z U X = y + ˙ z