Metamath Proof Explorer

Theorem lsmass

Description: Subgroup sum is associative. (Contributed by NM, 2-Mar-2014) (Revised by Mario Carneiro, 19-Apr-2016)

Ref Expression
Hypothesis lsmub1.p 
|- .(+) = ( LSSum ` G )
Assertion lsmass 
|- ( ( R e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) -> ( ( R .(+) T ) .(+) U ) = ( R .(+) ( T .(+) U ) ) )

Proof

Step Hyp Ref Expression
1 lsmub1.p 
 |-  .(+) = ( LSSum ` G )
2 eqid 
 |-  ( Base ` G ) = ( Base ` G )
3 eqid 
 |-  ( +g ` G ) = ( +g ` G )
4 2 3 1 lsmval 
 |-  ( ( R e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) ) -> ( R .(+) T ) = ran ( a e. R , b e. T |-> ( a ( +g ` G ) b ) ) )
5 4 3adant3 
 |-  ( ( R e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) -> ( R .(+) T ) = ran ( a e. R , b e. T |-> ( a ( +g ` G ) b ) ) )
6 5 rexeqdv 
 |-  ( ( R e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) -> ( E. y e. ( R .(+) T ) E. c e. U x = ( y ( +g ` G ) c ) <-> E. y e. ran ( a e. R , b e. T |-> ( a ( +g ` G ) b ) ) E. c e. U x = ( y ( +g ` G ) c ) ) )
7 ovex 
 |-  ( a ( +g ` G ) b ) e. _V
8 7 rgen2w 
 |-  A. a e. R A. b e. T ( a ( +g ` G ) b ) e. _V
9 eqid 
 |-  ( a e. R , b e. T |-> ( a ( +g ` G ) b ) ) = ( a e. R , b e. T |-> ( a ( +g ` G ) b ) )
10 oveq1 
 |-  ( y = ( a ( +g ` G ) b ) -> ( y ( +g ` G ) c ) = ( ( a ( +g ` G ) b ) ( +g ` G ) c ) )
11 10 eqeq2d 
 |-  ( y = ( a ( +g ` G ) b ) -> ( x = ( y ( +g ` G ) c ) <-> x = ( ( a ( +g ` G ) b ) ( +g ` G ) c ) ) )
12 11 rexbidv 
 |-  ( y = ( a ( +g ` G ) b ) -> ( E. c e. U x = ( y ( +g ` G ) c ) <-> E. c e. U x = ( ( a ( +g ` G ) b ) ( +g ` G ) c ) ) )
13 9 12 rexrnmpo 
 |-  ( A. a e. R A. b e. T ( a ( +g ` G ) b ) e. _V -> ( E. y e. ran ( a e. R , b e. T |-> ( a ( +g ` G ) b ) ) E. c e. U x = ( y ( +g ` G ) c ) <-> E. a e. R E. b e. T E. c e. U x = ( ( a ( +g ` G ) b ) ( +g ` G ) c ) ) )
14 8 13 ax-mp 
 |-  ( E. y e. ran ( a e. R , b e. T |-> ( a ( +g ` G ) b ) ) E. c e. U x = ( y ( +g ` G ) c ) <-> E. a e. R E. b e. T E. c e. U x = ( ( a ( +g ` G ) b ) ( +g ` G ) c ) )
15 6 14 bitrdi 
 |-  ( ( R e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) -> ( E. y e. ( R .(+) T ) E. c e. U x = ( y ( +g ` G ) c ) <-> E. a e. R E. b e. T E. c e. U x = ( ( a ( +g ` G ) b ) ( +g ` G ) c ) ) )
16 2 3 1 lsmval 
 |-  ( ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) -> ( T .(+) U ) = ran ( b e. T , c e. U |-> ( b ( +g ` G ) c ) ) )
17 16 3adant1 
 |-  ( ( R e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) -> ( T .(+) U ) = ran ( b e. T , c e. U |-> ( b ( +g ` G ) c ) ) )
18 17 rexeqdv 
 |-  ( ( R e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) -> ( E. z e. ( T .(+) U ) x = ( a ( +g ` G ) z ) <-> E. z e. ran ( b e. T , c e. U |-> ( b ( +g ` G ) c ) ) x = ( a ( +g ` G ) z ) ) )
19 ovex 
 |-  ( b ( +g ` G ) c ) e. _V
20 19 rgen2w 
 |-  A. b e. T A. c e. U ( b ( +g ` G ) c ) e. _V
21 eqid 
 |-  ( b e. T , c e. U |-> ( b ( +g ` G ) c ) ) = ( b e. T , c e. U |-> ( b ( +g ` G ) c ) )
22 oveq2 
 |-  ( z = ( b ( +g ` G ) c ) -> ( a ( +g ` G ) z ) = ( a ( +g ` G ) ( b ( +g ` G ) c ) ) )
23 22 eqeq2d 
 |-  ( z = ( b ( +g ` G ) c ) -> ( x = ( a ( +g ` G ) z ) <-> x = ( a ( +g ` G ) ( b ( +g ` G ) c ) ) ) )
24 21 23 rexrnmpo 
 |-  ( A. b e. T A. c e. U ( b ( +g ` G ) c ) e. _V -> ( E. z e. ran ( b e. T , c e. U |-> ( b ( +g ` G ) c ) ) x = ( a ( +g ` G ) z ) <-> E. b e. T E. c e. U x = ( a ( +g ` G ) ( b ( +g ` G ) c ) ) ) )
25 20 24 ax-mp 
 |-  ( E. z e. ran ( b e. T , c e. U |-> ( b ( +g ` G ) c ) ) x = ( a ( +g ` G ) z ) <-> E. b e. T E. c e. U x = ( a ( +g ` G ) ( b ( +g ` G ) c ) ) )
26 18 25 bitrdi 
 |-  ( ( R e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) -> ( E. z e. ( T .(+) U ) x = ( a ( +g ` G ) z ) <-> E. b e. T E. c e. U x = ( a ( +g ` G ) ( b ( +g ` G ) c ) ) ) )
27 26 adantr 
 |-  ( ( ( R e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) /\ a e. R ) -> ( E. z e. ( T .(+) U ) x = ( a ( +g ` G ) z ) <-> E. b e. T E. c e. U x = ( a ( +g ` G ) ( b ( +g ` G ) c ) ) ) )
28 subgrcl 
 |-  ( R e. ( SubGrp ` G ) -> G e. Grp )
29 28 3ad2ant1 
 |-  ( ( R e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) -> G e. Grp )
30 29 ad2antrr 
 |-  ( ( ( ( R e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) /\ a e. R ) /\ ( b e. T /\ c e. U ) ) -> G e. Grp )
31 2 subgss 
 |-  ( R e. ( SubGrp ` G ) -> R C_ ( Base ` G ) )
32 31 3ad2ant1 
 |-  ( ( R e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) -> R C_ ( Base ` G ) )
33 32 ad2antrr 
 |-  ( ( ( ( R e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) /\ a e. R ) /\ ( b e. T /\ c e. U ) ) -> R C_ ( Base ` G ) )
34 simplr 
 |-  ( ( ( ( R e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) /\ a e. R ) /\ ( b e. T /\ c e. U ) ) -> a e. R )
35 33 34 sseldd 
 |-  ( ( ( ( R e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) /\ a e. R ) /\ ( b e. T /\ c e. U ) ) -> a e. ( Base ` G ) )
36 2 subgss 
 |-  ( T e. ( SubGrp ` G ) -> T C_ ( Base ` G ) )
37 36 3ad2ant2 
 |-  ( ( R e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) -> T C_ ( Base ` G ) )
38 37 ad2antrr 
 |-  ( ( ( ( R e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) /\ a e. R ) /\ ( b e. T /\ c e. U ) ) -> T C_ ( Base ` G ) )
39 simprl 
 |-  ( ( ( ( R e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) /\ a e. R ) /\ ( b e. T /\ c e. U ) ) -> b e. T )
40 38 39 sseldd 
 |-  ( ( ( ( R e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) /\ a e. R ) /\ ( b e. T /\ c e. U ) ) -> b e. ( Base ` G ) )
41 2 subgss 
 |-  ( U e. ( SubGrp ` G ) -> U C_ ( Base ` G ) )
42 41 3ad2ant3 
 |-  ( ( R e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) -> U C_ ( Base ` G ) )
43 42 ad2antrr 
 |-  ( ( ( ( R e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) /\ a e. R ) /\ ( b e. T /\ c e. U ) ) -> U C_ ( Base ` G ) )
44 simprr 
 |-  ( ( ( ( R e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) /\ a e. R ) /\ ( b e. T /\ c e. U ) ) -> c e. U )
45 43 44 sseldd 
 |-  ( ( ( ( R e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) /\ a e. R ) /\ ( b e. T /\ c e. U ) ) -> c e. ( Base ` G ) )
46 2 3 grpass 
 |-  ( ( G e. Grp /\ ( a e. ( Base ` G ) /\ b e. ( Base ` G ) /\ c e. ( Base ` G ) ) ) -> ( ( a ( +g ` G ) b ) ( +g ` G ) c ) = ( a ( +g ` G ) ( b ( +g ` G ) c ) ) )
47 30 35 40 45 46 syl13anc 
 |-  ( ( ( ( R e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) /\ a e. R ) /\ ( b e. T /\ c e. U ) ) -> ( ( a ( +g ` G ) b ) ( +g ` G ) c ) = ( a ( +g ` G ) ( b ( +g ` G ) c ) ) )
48 47 eqeq2d 
 |-  ( ( ( ( R e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) /\ a e. R ) /\ ( b e. T /\ c e. U ) ) -> ( x = ( ( a ( +g ` G ) b ) ( +g ` G ) c ) <-> x = ( a ( +g ` G ) ( b ( +g ` G ) c ) ) ) )
49 48 2rexbidva 
 |-  ( ( ( R e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) /\ a e. R ) -> ( E. b e. T E. c e. U x = ( ( a ( +g ` G ) b ) ( +g ` G ) c ) <-> E. b e. T E. c e. U x = ( a ( +g ` G ) ( b ( +g ` G ) c ) ) ) )
50 27 49 bitr4d 
 |-  ( ( ( R e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) /\ a e. R ) -> ( E. z e. ( T .(+) U ) x = ( a ( +g ` G ) z ) <-> E. b e. T E. c e. U x = ( ( a ( +g ` G ) b ) ( +g ` G ) c ) ) )
51 50 rexbidva 
 |-  ( ( R e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) -> ( E. a e. R E. z e. ( T .(+) U ) x = ( a ( +g ` G ) z ) <-> E. a e. R E. b e. T E. c e. U x = ( ( a ( +g ` G ) b ) ( +g ` G ) c ) ) )
52 15 51 bitr4d 
 |-  ( ( R e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) -> ( E. y e. ( R .(+) T ) E. c e. U x = ( y ( +g ` G ) c ) <-> E. a e. R E. z e. ( T .(+) U ) x = ( a ( +g ` G ) z ) ) )
53 grpmnd 
 |-  ( G e. Grp -> G e. Mnd )
54 29 53 syl 
 |-  ( ( R e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) -> G e. Mnd )
55 2 1 lsmssv 
 |-  ( ( G e. Mnd /\ R C_ ( Base ` G ) /\ T C_ ( Base ` G ) ) -> ( R .(+) T ) C_ ( Base ` G ) )
56 54 32 37 55 syl3anc 
 |-  ( ( R e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) -> ( R .(+) T ) C_ ( Base ` G ) )
57 2 3 1 lsmelvalx 
 |-  ( ( G e. Grp /\ ( R .(+) T ) C_ ( Base ` G ) /\ U C_ ( Base ` G ) ) -> ( x e. ( ( R .(+) T ) .(+) U ) <-> E. y e. ( R .(+) T ) E. c e. U x = ( y ( +g ` G ) c ) ) )
58 29 56 42 57 syl3anc 
 |-  ( ( R e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) -> ( x e. ( ( R .(+) T ) .(+) U ) <-> E. y e. ( R .(+) T ) E. c e. U x = ( y ( +g ` G ) c ) ) )
59 2 1 lsmssv 
 |-  ( ( G e. Mnd /\ T C_ ( Base ` G ) /\ U C_ ( Base ` G ) ) -> ( T .(+) U ) C_ ( Base ` G ) )
60 54 37 42 59 syl3anc 
 |-  ( ( R e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) -> ( T .(+) U ) C_ ( Base ` G ) )
61 2 3 1 lsmelvalx 
 |-  ( ( G e. Grp /\ R C_ ( Base ` G ) /\ ( T .(+) U ) C_ ( Base ` G ) ) -> ( x e. ( R .(+) ( T .(+) U ) ) <-> E. a e. R E. z e. ( T .(+) U ) x = ( a ( +g ` G ) z ) ) )
62 29 32 60 61 syl3anc 
 |-  ( ( R e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) -> ( x e. ( R .(+) ( T .(+) U ) ) <-> E. a e. R E. z e. ( T .(+) U ) x = ( a ( +g ` G ) z ) ) )
63 52 58 62 3bitr4d 
 |-  ( ( R e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) -> ( x e. ( ( R .(+) T ) .(+) U ) <-> x e. ( R .(+) ( T .(+) U ) ) ) )
64 63 eqrdv 
 |-  ( ( R e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) -> ( ( R .(+) T ) .(+) U ) = ( R .(+) ( T .(+) U ) ) )