Metamath Proof Explorer

Theorem lsmelvali

Description: Subgroup sum membership (for a left module or left vector space). (Contributed by NM, 4-Feb-2014) (Revised by Mario Carneiro, 19-Apr-2016)

Ref Expression
Hypotheses lsmelval.a 
|- .+ = ( +g ` G )
lsmelval.p 
|- .(+) = ( LSSum ` G )
Assertion lsmelvali 
|- ( ( ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) /\ ( X e. T /\ Y e. U ) ) -> ( X .+ Y ) e. ( T .(+) U ) )

Proof

Step Hyp Ref Expression
1 lsmelval.a 
 |-  .+ = ( +g ` G )
2 lsmelval.p 
 |-  .(+) = ( LSSum ` G )
3 subgrcl 
 |-  ( T e. ( SubGrp ` G ) -> G e. Grp )
4 3 adantr 
 |-  ( ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) -> G e. Grp )
5 eqid 
 |-  ( Base ` G ) = ( Base ` G )
6 5 subgss 
 |-  ( T e. ( SubGrp ` G ) -> T C_ ( Base ` G ) )
7 6 adantr 
 |-  ( ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) -> T C_ ( Base ` G ) )
8 5 subgss 
 |-  ( U e. ( SubGrp ` G ) -> U C_ ( Base ` G ) )
9 8 adantl 
 |-  ( ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) -> U C_ ( Base ` G ) )
10 4 7 9 3jca 
 |-  ( ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) -> ( G e. Grp /\ T C_ ( Base ` G ) /\ U C_ ( Base ` G ) ) )
11 5 1 2 lsmelvalix 
 |-  ( ( ( G e. Grp /\ T C_ ( Base ` G ) /\ U C_ ( Base ` G ) ) /\ ( X e. T /\ Y e. U ) ) -> ( X .+ Y ) e. ( T .(+) U ) )
12 10 11 sylan 
 |-  ( ( ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) /\ ( X e. T /\ Y e. U ) ) -> ( X .+ Y ) e. ( T .(+) U ) )