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