Metamath Proof Explorer

Theorem subglsm

Description: The subgroup sum evaluated within a subgroup. (Contributed by Mario Carneiro, 27-Apr-2016)

Ref Expression
Hypotheses subglsm.h 
|- H = ( G |`s S )
subglsm.s 
|- .(+) = ( LSSum ` G )
subglsm.a 
|- A = ( LSSum ` H )
Assertion subglsm 
|- ( ( S e. ( SubGrp ` G ) /\ T C_ S /\ U C_ S ) -> ( T .(+) U ) = ( T A U ) )

Proof

Step Hyp Ref Expression
1 subglsm.h 
 |-  H = ( G |`s S )
2 subglsm.s 
 |-  .(+) = ( LSSum ` G )
3 subglsm.a 
 |-  A = ( LSSum ` H )
4 simp11 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ T C_ S /\ U C_ S ) /\ x e. T /\ y e. U ) -> S e. ( SubGrp ` G ) )
5 eqid 
 |-  ( +g ` G ) = ( +g ` G )
6 1 5 ressplusg 
 |-  ( S e. ( SubGrp ` G ) -> ( +g ` G ) = ( +g ` H ) )
7 4 6 syl 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ T C_ S /\ U C_ S ) /\ x e. T /\ y e. U ) -> ( +g ` G ) = ( +g ` H ) )
8 7 oveqd 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ T C_ S /\ U C_ S ) /\ x e. T /\ y e. U ) -> ( x ( +g ` G ) y ) = ( x ( +g ` H ) y ) )
9 8 mpoeq3dva 
 |-  ( ( S e. ( SubGrp ` G ) /\ T C_ S /\ U C_ S ) -> ( x e. T , y e. U |-> ( x ( +g ` G ) y ) ) = ( x e. T , y e. U |-> ( x ( +g ` H ) y ) ) )
10 9 rneqd 
 |-  ( ( S e. ( SubGrp ` G ) /\ T C_ S /\ U C_ S ) -> ran ( x e. T , y e. U |-> ( x ( +g ` G ) y ) ) = ran ( x e. T , y e. U |-> ( x ( +g ` H ) y ) ) )
11 subgrcl 
 |-  ( S e. ( SubGrp ` G ) -> G e. Grp )
12 11 3ad2ant1 
 |-  ( ( S e. ( SubGrp ` G ) /\ T C_ S /\ U C_ S ) -> G e. Grp )
13 simp2 
 |-  ( ( S e. ( SubGrp ` G ) /\ T C_ S /\ U C_ S ) -> T C_ S )
14 eqid 
 |-  ( Base ` G ) = ( Base ` G )
15 14 subgss 
 |-  ( S e. ( SubGrp ` G ) -> S C_ ( Base ` G ) )
16 15 3ad2ant1 
 |-  ( ( S e. ( SubGrp ` G ) /\ T C_ S /\ U C_ S ) -> S C_ ( Base ` G ) )
17 13 16 sstrd 
 |-  ( ( S e. ( SubGrp ` G ) /\ T C_ S /\ U C_ S ) -> T C_ ( Base ` G ) )
18 simp3 
 |-  ( ( S e. ( SubGrp ` G ) /\ T C_ S /\ U C_ S ) -> U C_ S )
19 18 16 sstrd 
 |-  ( ( S e. ( SubGrp ` G ) /\ T C_ S /\ U C_ S ) -> U C_ ( Base ` G ) )
20 14 5 2 lsmvalx 
 |-  ( ( G e. Grp /\ T C_ ( Base ` G ) /\ U C_ ( Base ` G ) ) -> ( T .(+) U ) = ran ( x e. T , y e. U |-> ( x ( +g ` G ) y ) ) )
21 12 17 19 20 syl3anc 
 |-  ( ( S e. ( SubGrp ` G ) /\ T C_ S /\ U C_ S ) -> ( T .(+) U ) = ran ( x e. T , y e. U |-> ( x ( +g ` G ) y ) ) )
22 1 subggrp 
 |-  ( S e. ( SubGrp ` G ) -> H e. Grp )
23 22 3ad2ant1 
 |-  ( ( S e. ( SubGrp ` G ) /\ T C_ S /\ U C_ S ) -> H e. Grp )
24 1 subgbas 
 |-  ( S e. ( SubGrp ` G ) -> S = ( Base ` H ) )
25 24 3ad2ant1 
 |-  ( ( S e. ( SubGrp ` G ) /\ T C_ S /\ U C_ S ) -> S = ( Base ` H ) )
26 13 25 sseqtrd 
 |-  ( ( S e. ( SubGrp ` G ) /\ T C_ S /\ U C_ S ) -> T C_ ( Base ` H ) )
27 18 25 sseqtrd 
 |-  ( ( S e. ( SubGrp ` G ) /\ T C_ S /\ U C_ S ) -> U C_ ( Base ` H ) )
28 eqid 
 |-  ( Base ` H ) = ( Base ` H )
29 eqid 
 |-  ( +g ` H ) = ( +g ` H )
30 28 29 3 lsmvalx 
 |-  ( ( H e. Grp /\ T C_ ( Base ` H ) /\ U C_ ( Base ` H ) ) -> ( T A U ) = ran ( x e. T , y e. U |-> ( x ( +g ` H ) y ) ) )
31 23 26 27 30 syl3anc 
 |-  ( ( S e. ( SubGrp ` G ) /\ T C_ S /\ U C_ S ) -> ( T A U ) = ran ( x e. T , y e. U |-> ( x ( +g ` H ) y ) ) )
32 10 21 31 3eqtr4d 
 |-  ( ( S e. ( SubGrp ` G ) /\ T C_ S /\ U C_ S ) -> ( T .(+) U ) = ( T A U ) )