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