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 29 grpmndd
 |-  ( ( R e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) -> G e. Mnd )
54 2 1 lsmssv
 |-  ( ( G e. Mnd /\ R C_ ( Base ` G ) /\ T C_ ( Base ` G ) ) -> ( R .(+) T ) C_ ( Base ` G ) )
55 53 32 37 54 syl3anc
 |-  ( ( R e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) -> ( R .(+) T ) C_ ( Base ` G ) )
56 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 ) ) )
57 29 55 42 56 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 ) ) )
58 2 1 lsmssv
 |-  ( ( G e. Mnd /\ T C_ ( Base ` G ) /\ U C_ ( Base ` G ) ) -> ( T .(+) U ) C_ ( Base ` G ) )
59 53 37 42 58 syl3anc
 |-  ( ( R e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) -> ( T .(+) U ) C_ ( Base ` G ) )
60 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 ) ) )
61 29 32 59 60 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 ) ) )
62 52 57 61 3bitr4d
 |-  ( ( R e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) -> ( x e. ( ( R .(+) T ) .(+) U ) <-> x e. ( R .(+) ( T .(+) U ) ) ) )
63 62 eqrdv
 |-  ( ( R e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) -> ( ( R .(+) T ) .(+) U ) = ( R .(+) ( T .(+) U ) ) )