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=BaseG
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=BaseG
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+Gb
9 3 4 5 8 syl3anc ⊢φ→R⊕˙T=ran⁡a∈R,b∈T⟼a+Gb
10 9 rexeqdv ⊢φ→∃y∈R⊕˙T∃c∈Ux=y+Gc↔∃y∈ran⁡a∈R,b∈T⟼a+Gb∃c∈Ux=y+Gc
11 ovex ⊢a+Gb∈V
12 11 rgen2w ⊢∀a∈R∀b∈Ta+Gb∈V
13 eqid ⊢a∈R,b∈T⟼a+Gb=a∈R,b∈T⟼a+Gb
14 oveq1 ⊢y=a+Gb→y+Gc=a+Gb+Gc
15 14 eqeq2d ⊢y=a+Gb→x=y+Gc↔x=a+Gb+Gc
16 15 rexbidv ⊢y=a+Gb→∃c∈Ux=y+Gc↔∃c∈Ux=a+Gb+Gc
17 13 16 rexrnmpo ⊢∀a∈R∀b∈Ta+Gb∈V→∃y∈ran⁡a∈R,b∈T⟼a+Gb∃c∈Ux=y+Gc↔∃a∈R∃b∈T∃c∈Ux=a+Gb+Gc
18 12 17 ax-mp ⊢∃y∈ran⁡a∈R,b∈T⟼a+Gb∃c∈Ux=y+Gc↔∃a∈R∃b∈T∃c∈Ux=a+Gb+Gc
19 10 18 bitrdi ⊢φ→∃y∈R⊕˙T∃c∈Ux=y+Gc↔∃a∈R∃b∈T∃c∈Ux=a+Gb+Gc
20 2 7 1 lsmvalx ⊢G∈Mnd∧T⊆B∧U⊆B→T⊕˙U=ran⁡b∈T,c∈U⟼b+Gc
21 3 5 6 20 syl3anc ⊢φ→T⊕˙U=ran⁡b∈T,c∈U⟼b+Gc
22 21 rexeqdv ⊢φ→∃z∈T⊕˙Ux=a+Gz↔∃z∈ran⁡b∈T,c∈U⟼b+Gcx=a+Gz
23 ovex ⊢b+Gc∈V
24 23 rgen2w ⊢∀b∈T∀c∈Ub+Gc∈V
25 eqid ⊢b∈T,c∈U⟼b+Gc=b∈T,c∈U⟼b+Gc
26 oveq2 ⊢z=b+Gc→a+Gz=a+Gb+Gc
27 26 eqeq2d ⊢z=b+Gc→x=a+Gz↔x=a+Gb+Gc
28 25 27 rexrnmpo ⊢∀b∈T∀c∈Ub+Gc∈V→∃z∈ran⁡b∈T,c∈U⟼b+Gcx=a+Gz↔∃b∈T∃c∈Ux=a+Gb+Gc
29 24 28 ax-mp ⊢∃z∈ran⁡b∈T,c∈U⟼b+Gcx=a+Gz↔∃b∈T∃c∈Ux=a+Gb+Gc
30 22 29 bitrdi ⊢φ→∃z∈T⊕˙Ux=a+Gz↔∃b∈T∃c∈Ux=a+Gb+Gc
31 30 adantr ⊢φ∧a∈R→∃z∈T⊕˙Ux=a+Gz↔∃b∈T∃c∈Ux=a+Gb+Gc
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+Gb+Gc=a+Gb+Gc
43 32 35 38 41 42 syl13anc ⊢φ∧a∈R∧b∈T∧c∈U→a+Gb+Gc=a+Gb+Gc
44 43 eqeq2d ⊢φ∧a∈R∧b∈T∧c∈U→x=a+Gb+Gc↔x=a+Gb+Gc
45 44 2rexbidva ⊢φ∧a∈R→∃b∈T∃c∈Ux=a+Gb+Gc↔∃b∈T∃c∈Ux=a+Gb+Gc
46 31 45 bitr4d ⊢φ∧a∈R→∃z∈T⊕˙Ux=a+Gz↔∃b∈T∃c∈Ux=a+Gb+Gc
47 46 rexbidva ⊢φ→∃a∈R∃z∈T⊕˙Ux=a+Gz↔∃a∈R∃b∈T∃c∈Ux=a+Gb+Gc
48 19 47 bitr4d ⊢φ→∃y∈R⊕˙T∃c∈Ux=y+Gc↔∃a∈R∃z∈T⊕˙Ux=a+Gz
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∈Ux=y+Gc
52 3 50 6 51 syl3anc ⊢φ→x∈R⊕˙T⊕˙U↔∃y∈R⊕˙T∃c∈Ux=y+Gc
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⊕˙Ux=a+Gz
56 3 4 54 55 syl3anc ⊢φ→x∈R⊕˙T⊕˙U↔∃a∈R∃z∈T⊕˙Ux=a+Gz
57 48 52 56 3bitr4d ⊢φ→x∈R⊕˙T⊕˙U↔x∈R⊕˙T⊕˙U
58 57 eqrdv ⊢φ→R⊕˙T⊕˙U=R⊕˙T⊕˙U