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