Metamath Proof Explorer


Theorem lsmssass

Description: Group sum is associative, subset version (see lsmass ). (Contributed by Thierry Arnoux, 1-Jun-2024)

Ref Expression
Hypotheses lsmssass.p ˙ = LSSum G
lsmssass.b B = Base G
lsmssass.g φ G Mnd
lsmssass.r φ R B
lsmssass.t φ T B
lsmssass.u φ U B
Assertion lsmssass φ R ˙ T ˙ U = R ˙ T ˙ U

Proof

Step Hyp Ref Expression
1 lsmssass.p ˙ = LSSum G
2 lsmssass.b B = Base G
3 lsmssass.g φ G Mnd
4 lsmssass.r φ R B
5 lsmssass.t φ T B
6 lsmssass.u φ U B
7 eqid + G = + G
8 2 7 1 lsmvalx G Mnd R B T B R ˙ T = ran a R , b T a + G b
9 3 4 5 8 syl3anc φ R ˙ T = ran a R , b T a + G b
10 9 rexeqdv φ y R ˙ T c U x = y + G c y ran a R , b T a + G b c U x = y + G c
11 ovex a + G b V
12 11 rgen2w a R b T a + G b V
13 eqid a R , b T a + G b = a R , b T a + G b
14 oveq1 y = a + G b y + G c = a + G b + G c
15 14 eqeq2d y = a + G b x = y + G c x = a + G b + G c
16 15 rexbidv y = a + G b c U x = y + G c c U x = a + G b + G c
17 13 16 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
18 12 17 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
19 10 18 bitrdi φ y R ˙ T c U x = y + G c a R b T c U x = a + G b + G c
20 2 7 1 lsmvalx G Mnd T B U B T ˙ U = ran b T , c U b + G c
21 3 5 6 20 syl3anc φ T ˙ U = ran b T , c U b + G c
22 21 rexeqdv φ z T ˙ U x = a + G z z ran b T , c U b + G c x = a + G z
23 ovex b + G c V
24 23 rgen2w b T c U b + G c V
25 eqid b T , c U b + G c = b T , c U b + G c
26 oveq2 z = b + G c a + G z = a + G b + G c
27 26 eqeq2d z = b + G c x = a + G z x = a + G b + G c
28 25 27 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
29 24 28 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
30 22 29 bitrdi φ z T ˙ U x = a + G z b T c U x = a + G b + G c
31 30 adantr φ a R z T ˙ U x = a + G z b T c U x = a + G b + G c
32 3 ad2antrr φ a R b T c U G Mnd
33 4 ad2antrr φ a R b T c U R B
34 simplr φ a R b T c U a R
35 33 34 sseldd φ a R b T c U a B
36 5 ad2antrr φ a R b T c U T B
37 simprl φ a R b T c U b T
38 36 37 sseldd φ a R b T c U b B
39 6 ad2antrr φ a R b T c U U B
40 simprr φ a R b T c U c U
41 39 40 sseldd φ a R b T c U c B
42 2 7 mndass G Mnd a B b B c B a + G b + G c = a + G b + G c
43 32 35 38 41 42 syl13anc φ a R b T c U a + G b + G c = a + G b + G c
44 43 eqeq2d φ a R b T c U x = a + G b + G c x = a + G b + G c
45 44 2rexbidva φ a R b T c U x = a + G b + G c b T c U x = a + G b + G c
46 31 45 bitr4d φ a R z T ˙ U x = a + G z b T c U x = a + G b + G c
47 46 rexbidva φ a R z T ˙ U x = a + G z a R b T c U x = a + G b + G c
48 19 47 bitr4d φ y R ˙ T c U x = y + G c a R z T ˙ U x = a + G z
49 2 1 lsmssv G Mnd R B T B R ˙ T B
50 3 4 5 49 syl3anc φ R ˙ T B
51 2 7 1 lsmelvalx G Mnd R ˙ T B U B x R ˙ T ˙ U y R ˙ T c U x = y + G c
52 3 50 6 51 syl3anc φ x R ˙ T ˙ U y R ˙ T c U x = y + G c
53 2 1 lsmssv G Mnd T B U B T ˙ U B
54 3 5 6 53 syl3anc φ T ˙ U B
55 2 7 1 lsmelvalx G Mnd R B T ˙ U B x R ˙ T ˙ U a R z T ˙ U x = a + G z
56 3 4 54 55 syl3anc φ x R ˙ T ˙ U a R z T ˙ U x = a + G z
57 48 52 56 3bitr4d φ x R ˙ T ˙ U x R ˙ T ˙ U
58 57 eqrdv φ R ˙ T ˙ U = R ˙ T ˙ U