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 ‘ 𝐺 )
lsmssass.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
lsmssass.g ⊢ ( 𝜑 → 𝐺 ∈ Mnd )
lsmssass.r ⊢ ( 𝜑 → 𝑅 ⊆ 𝐵 )
lsmssass.t ⊢ ( 𝜑 → 𝑇 ⊆ 𝐵 )
lsmssass.u ⊢ ( 𝜑 → 𝑈 ⊆ 𝐵 )
Assertion lsmssass ( 𝜑 → ( ( 𝑅 ⊕ 𝑇 ) ⊕ 𝑈 ) = ( 𝑅 ⊕ ( 𝑇 ⊕ 𝑈 ) ) )

Proof

Step Hyp Ref Expression
1 lsmssass.p ⊢ ⊕ = ( LSSum ‘ 𝐺 )
2 lsmssass.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
3 lsmssass.g ⊢ ( 𝜑 → 𝐺 ∈ Mnd )
4 lsmssass.r ⊢ ( 𝜑 → 𝑅 ⊆ 𝐵 )
5 lsmssass.t ⊢ ( 𝜑 → 𝑇 ⊆ 𝐵 )
6 lsmssass.u ⊢ ( 𝜑 → 𝑈 ⊆ 𝐵 )
7 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
8 2 7 1 lsmvalx ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑅 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝐵 ) → ( 𝑅 ⊕ 𝑇 ) = ran ( 𝑎 ∈ 𝑅 , 𝑏 ∈ 𝑇 ↦ ( 𝑎 ( +g ‘ 𝐺 ) 𝑏 ) ) )
9 3 4 5 8 syl3anc ⊢ ( 𝜑 → ( 𝑅 ⊕ 𝑇 ) = ran ( 𝑎 ∈ 𝑅 , 𝑏 ∈ 𝑇 ↦ ( 𝑎 ( +g ‘ 𝐺 ) 𝑏 ) ) )
10 9 rexeqdv ⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ( 𝑅 ⊕ 𝑇 ) ∃ 𝑐 ∈ 𝑈 𝑥 = ( 𝑦 ( +g ‘ 𝐺 ) 𝑐 ) ↔ ∃ 𝑦 ∈ ran ( 𝑎 ∈ 𝑅 , 𝑏 ∈ 𝑇 ↦ ( 𝑎 ( +g ‘ 𝐺 ) 𝑏 ) ) ∃ 𝑐 ∈ 𝑈 𝑥 = ( 𝑦 ( +g ‘ 𝐺 ) 𝑐 ) ) )
11 ovex ⊢ ( 𝑎 ( +g ‘ 𝐺 ) 𝑏 ) ∈ V
12 11 rgen2w ⊢ ∀ 𝑎 ∈ 𝑅 ∀ 𝑏 ∈ 𝑇 ( 𝑎 ( +g ‘ 𝐺 ) 𝑏 ) ∈ V
13 eqid ⊢ ( 𝑎 ∈ 𝑅 , 𝑏 ∈ 𝑇 ↦ ( 𝑎 ( +g ‘ 𝐺 ) 𝑏 ) ) = ( 𝑎 ∈ 𝑅 , 𝑏 ∈ 𝑇 ↦ ( 𝑎 ( +g ‘ 𝐺 ) 𝑏 ) )
14 oveq1 ⊢ ( 𝑦 = ( 𝑎 ( +g ‘ 𝐺 ) 𝑏 ) → ( 𝑦 ( +g ‘ 𝐺 ) 𝑐 ) = ( ( 𝑎 ( +g ‘ 𝐺 ) 𝑏 ) ( +g ‘ 𝐺 ) 𝑐 ) )
15 14 eqeq2d ⊢ ( 𝑦 = ( 𝑎 ( +g ‘ 𝐺 ) 𝑏 ) → ( 𝑥 = ( 𝑦 ( +g ‘ 𝐺 ) 𝑐 ) ↔ 𝑥 = ( ( 𝑎 ( +g ‘ 𝐺 ) 𝑏 ) ( +g ‘ 𝐺 ) 𝑐 ) ) )
16 15 rexbidv ⊢ ( 𝑦 = ( 𝑎 ( +g ‘ 𝐺 ) 𝑏 ) → ( ∃ 𝑐 ∈ 𝑈 𝑥 = ( 𝑦 ( +g ‘ 𝐺 ) 𝑐 ) ↔ ∃ 𝑐 ∈ 𝑈 𝑥 = ( ( 𝑎 ( +g ‘ 𝐺 ) 𝑏 ) ( +g ‘ 𝐺 ) 𝑐 ) ) )
17 13 16 rexrnmpo ⊢ ( ∀ 𝑎 ∈ 𝑅 ∀ 𝑏 ∈ 𝑇 ( 𝑎 ( +g ‘ 𝐺 ) 𝑏 ) ∈ V → ( ∃ 𝑦 ∈ ran ( 𝑎 ∈ 𝑅 , 𝑏 ∈ 𝑇 ↦ ( 𝑎 ( +g ‘ 𝐺 ) 𝑏 ) ) ∃ 𝑐 ∈ 𝑈 𝑥 = ( 𝑦 ( +g ‘ 𝐺 ) 𝑐 ) ↔ ∃ 𝑎 ∈ 𝑅 ∃ 𝑏 ∈ 𝑇 ∃ 𝑐 ∈ 𝑈 𝑥 = ( ( 𝑎 ( +g ‘ 𝐺 ) 𝑏 ) ( +g ‘ 𝐺 ) 𝑐 ) ) )
18 12 17 ax-mp ⊢ ( ∃ 𝑦 ∈ ran ( 𝑎 ∈ 𝑅 , 𝑏 ∈ 𝑇 ↦ ( 𝑎 ( +g ‘ 𝐺 ) 𝑏 ) ) ∃ 𝑐 ∈ 𝑈 𝑥 = ( 𝑦 ( +g ‘ 𝐺 ) 𝑐 ) ↔ ∃ 𝑎 ∈ 𝑅 ∃ 𝑏 ∈ 𝑇 ∃ 𝑐 ∈ 𝑈 𝑥 = ( ( 𝑎 ( +g ‘ 𝐺 ) 𝑏 ) ( +g ‘ 𝐺 ) 𝑐 ) )
19 10 18 bitrdi ⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ( 𝑅 ⊕ 𝑇 ) ∃ 𝑐 ∈ 𝑈 𝑥 = ( 𝑦 ( +g ‘ 𝐺 ) 𝑐 ) ↔ ∃ 𝑎 ∈ 𝑅 ∃ 𝑏 ∈ 𝑇 ∃ 𝑐 ∈ 𝑈 𝑥 = ( ( 𝑎 ( +g ‘ 𝐺 ) 𝑏 ) ( +g ‘ 𝐺 ) 𝑐 ) ) )
20 2 7 1 lsmvalx ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑇 ⊆ 𝐵 ∧ 𝑈 ⊆ 𝐵 ) → ( 𝑇 ⊕ 𝑈 ) = ran ( 𝑏 ∈ 𝑇 , 𝑐 ∈ 𝑈 ↦ ( 𝑏 ( +g ‘ 𝐺 ) 𝑐 ) ) )
21 3 5 6 20 syl3anc ⊢ ( 𝜑 → ( 𝑇 ⊕ 𝑈 ) = ran ( 𝑏 ∈ 𝑇 , 𝑐 ∈ 𝑈 ↦ ( 𝑏 ( +g ‘ 𝐺 ) 𝑐 ) ) )
22 21 rexeqdv ⊢ ( 𝜑 → ( ∃ 𝑧 ∈ ( 𝑇 ⊕ 𝑈 ) 𝑥 = ( 𝑎 ( +g ‘ 𝐺 ) 𝑧 ) ↔ ∃ 𝑧 ∈ ran ( 𝑏 ∈ 𝑇 , 𝑐 ∈ 𝑈 ↦ ( 𝑏 ( +g ‘ 𝐺 ) 𝑐 ) ) 𝑥 = ( 𝑎 ( +g ‘ 𝐺 ) 𝑧 ) ) )
23 ovex ⊢ ( 𝑏 ( +g ‘ 𝐺 ) 𝑐 ) ∈ V
24 23 rgen2w ⊢ ∀ 𝑏 ∈ 𝑇 ∀ 𝑐 ∈ 𝑈 ( 𝑏 ( +g ‘ 𝐺 ) 𝑐 ) ∈ V
25 eqid ⊢ ( 𝑏 ∈ 𝑇 , 𝑐 ∈ 𝑈 ↦ ( 𝑏 ( +g ‘ 𝐺 ) 𝑐 ) ) = ( 𝑏 ∈ 𝑇 , 𝑐 ∈ 𝑈 ↦ ( 𝑏 ( +g ‘ 𝐺 ) 𝑐 ) )
26 oveq2 ⊢ ( 𝑧 = ( 𝑏 ( +g ‘ 𝐺 ) 𝑐 ) → ( 𝑎 ( +g ‘ 𝐺 ) 𝑧 ) = ( 𝑎 ( +g ‘ 𝐺 ) ( 𝑏 ( +g ‘ 𝐺 ) 𝑐 ) ) )
27 26 eqeq2d ⊢ ( 𝑧 = ( 𝑏 ( +g ‘ 𝐺 ) 𝑐 ) → ( 𝑥 = ( 𝑎 ( +g ‘ 𝐺 ) 𝑧 ) ↔ 𝑥 = ( 𝑎 ( +g ‘ 𝐺 ) ( 𝑏 ( +g ‘ 𝐺 ) 𝑐 ) ) ) )
28 25 27 rexrnmpo ⊢ ( ∀ 𝑏 ∈ 𝑇 ∀ 𝑐 ∈ 𝑈 ( 𝑏 ( +g ‘ 𝐺 ) 𝑐 ) ∈ V → ( ∃ 𝑧 ∈ ran ( 𝑏 ∈ 𝑇 , 𝑐 ∈ 𝑈 ↦ ( 𝑏 ( +g ‘ 𝐺 ) 𝑐 ) ) 𝑥 = ( 𝑎 ( +g ‘ 𝐺 ) 𝑧 ) ↔ ∃ 𝑏 ∈ 𝑇 ∃ 𝑐 ∈ 𝑈 𝑥 = ( 𝑎 ( +g ‘ 𝐺 ) ( 𝑏 ( +g ‘ 𝐺 ) 𝑐 ) ) ) )
29 24 28 ax-mp ⊢ ( ∃ 𝑧 ∈ ran ( 𝑏 ∈ 𝑇 , 𝑐 ∈ 𝑈 ↦ ( 𝑏 ( +g ‘ 𝐺 ) 𝑐 ) ) 𝑥 = ( 𝑎 ( +g ‘ 𝐺 ) 𝑧 ) ↔ ∃ 𝑏 ∈ 𝑇 ∃ 𝑐 ∈ 𝑈 𝑥 = ( 𝑎 ( +g ‘ 𝐺 ) ( 𝑏 ( +g ‘ 𝐺 ) 𝑐 ) ) )
30 22 29 bitrdi ⊢ ( 𝜑 → ( ∃ 𝑧 ∈ ( 𝑇 ⊕ 𝑈 ) 𝑥 = ( 𝑎 ( +g ‘ 𝐺 ) 𝑧 ) ↔ ∃ 𝑏 ∈ 𝑇 ∃ 𝑐 ∈ 𝑈 𝑥 = ( 𝑎 ( +g ‘ 𝐺 ) ( 𝑏 ( +g ‘ 𝐺 ) 𝑐 ) ) ) )
31 30 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑅 ) → ( ∃ 𝑧 ∈ ( 𝑇 ⊕ 𝑈 ) 𝑥 = ( 𝑎 ( +g ‘ 𝐺 ) 𝑧 ) ↔ ∃ 𝑏 ∈ 𝑇 ∃ 𝑐 ∈ 𝑈 𝑥 = ( 𝑎 ( +g ‘ 𝐺 ) ( 𝑏 ( +g ‘ 𝐺 ) 𝑐 ) ) ) )
32 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑅 ) ∧ ( 𝑏 ∈ 𝑇 ∧ 𝑐 ∈ 𝑈 ) ) → 𝐺 ∈ Mnd )
33 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑅 ) ∧ ( 𝑏 ∈ 𝑇 ∧ 𝑐 ∈ 𝑈 ) ) → 𝑅 ⊆ 𝐵 )
34 simplr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑅 ) ∧ ( 𝑏 ∈ 𝑇 ∧ 𝑐 ∈ 𝑈 ) ) → 𝑎 ∈ 𝑅 )
35 33 34 sseldd ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑅 ) ∧ ( 𝑏 ∈ 𝑇 ∧ 𝑐 ∈ 𝑈 ) ) → 𝑎 ∈ 𝐵 )
36 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑅 ) ∧ ( 𝑏 ∈ 𝑇 ∧ 𝑐 ∈ 𝑈 ) ) → 𝑇 ⊆ 𝐵 )
37 simprl ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑅 ) ∧ ( 𝑏 ∈ 𝑇 ∧ 𝑐 ∈ 𝑈 ) ) → 𝑏 ∈ 𝑇 )
38 36 37 sseldd ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑅 ) ∧ ( 𝑏 ∈ 𝑇 ∧ 𝑐 ∈ 𝑈 ) ) → 𝑏 ∈ 𝐵 )
39 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑅 ) ∧ ( 𝑏 ∈ 𝑇 ∧ 𝑐 ∈ 𝑈 ) ) → 𝑈 ⊆ 𝐵 )
40 simprr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑅 ) ∧ ( 𝑏 ∈ 𝑇 ∧ 𝑐 ∈ 𝑈 ) ) → 𝑐 ∈ 𝑈 )
41 39 40 sseldd ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑅 ) ∧ ( 𝑏 ∈ 𝑇 ∧ 𝑐 ∈ 𝑈 ) ) → 𝑐 ∈ 𝐵 )
42 2 7 mndass ⊢ ( ( 𝐺 ∈ Mnd ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) → ( ( 𝑎 ( +g ‘ 𝐺 ) 𝑏 ) ( +g ‘ 𝐺 ) 𝑐 ) = ( 𝑎 ( +g ‘ 𝐺 ) ( 𝑏 ( +g ‘ 𝐺 ) 𝑐 ) ) )
43 32 35 38 41 42 syl13anc ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑅 ) ∧ ( 𝑏 ∈ 𝑇 ∧ 𝑐 ∈ 𝑈 ) ) → ( ( 𝑎 ( +g ‘ 𝐺 ) 𝑏 ) ( +g ‘ 𝐺 ) 𝑐 ) = ( 𝑎 ( +g ‘ 𝐺 ) ( 𝑏 ( +g ‘ 𝐺 ) 𝑐 ) ) )
44 43 eqeq2d ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑅 ) ∧ ( 𝑏 ∈ 𝑇 ∧ 𝑐 ∈ 𝑈 ) ) → ( 𝑥 = ( ( 𝑎 ( +g ‘ 𝐺 ) 𝑏 ) ( +g ‘ 𝐺 ) 𝑐 ) ↔ 𝑥 = ( 𝑎 ( +g ‘ 𝐺 ) ( 𝑏 ( +g ‘ 𝐺 ) 𝑐 ) ) ) )
45 44 2rexbidva ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑅 ) → ( ∃ 𝑏 ∈ 𝑇 ∃ 𝑐 ∈ 𝑈 𝑥 = ( ( 𝑎 ( +g ‘ 𝐺 ) 𝑏 ) ( +g ‘ 𝐺 ) 𝑐 ) ↔ ∃ 𝑏 ∈ 𝑇 ∃ 𝑐 ∈ 𝑈 𝑥 = ( 𝑎 ( +g ‘ 𝐺 ) ( 𝑏 ( +g ‘ 𝐺 ) 𝑐 ) ) ) )
46 31 45 bitr4d ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑅 ) → ( ∃ 𝑧 ∈ ( 𝑇 ⊕ 𝑈 ) 𝑥 = ( 𝑎 ( +g ‘ 𝐺 ) 𝑧 ) ↔ ∃ 𝑏 ∈ 𝑇 ∃ 𝑐 ∈ 𝑈 𝑥 = ( ( 𝑎 ( +g ‘ 𝐺 ) 𝑏 ) ( +g ‘ 𝐺 ) 𝑐 ) ) )
47 46 rexbidva ⊢ ( 𝜑 → ( ∃ 𝑎 ∈ 𝑅 ∃ 𝑧 ∈ ( 𝑇 ⊕ 𝑈 ) 𝑥 = ( 𝑎 ( +g ‘ 𝐺 ) 𝑧 ) ↔ ∃ 𝑎 ∈ 𝑅 ∃ 𝑏 ∈ 𝑇 ∃ 𝑐 ∈ 𝑈 𝑥 = ( ( 𝑎 ( +g ‘ 𝐺 ) 𝑏 ) ( +g ‘ 𝐺 ) 𝑐 ) ) )
48 19 47 bitr4d ⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ( 𝑅 ⊕ 𝑇 ) ∃ 𝑐 ∈ 𝑈 𝑥 = ( 𝑦 ( +g ‘ 𝐺 ) 𝑐 ) ↔ ∃ 𝑎 ∈ 𝑅 ∃ 𝑧 ∈ ( 𝑇 ⊕ 𝑈 ) 𝑥 = ( 𝑎 ( +g ‘ 𝐺 ) 𝑧 ) ) )
49 2 1 lsmssv ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑅 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝐵 ) → ( 𝑅 ⊕ 𝑇 ) ⊆ 𝐵 )
50 3 4 5 49 syl3anc ⊢ ( 𝜑 → ( 𝑅 ⊕ 𝑇 ) ⊆ 𝐵 )
51 2 7 1 lsmelvalx ⊢ ( ( 𝐺 ∈ Mnd ∧ ( 𝑅 ⊕ 𝑇 ) ⊆ 𝐵 ∧ 𝑈 ⊆ 𝐵 ) → ( 𝑥 ∈ ( ( 𝑅 ⊕ 𝑇 ) ⊕ 𝑈 ) ↔ ∃ 𝑦 ∈ ( 𝑅 ⊕ 𝑇 ) ∃ 𝑐 ∈ 𝑈 𝑥 = ( 𝑦 ( +g ‘ 𝐺 ) 𝑐 ) ) )
52 3 50 6 51 syl3anc ⊢ ( 𝜑 → ( 𝑥 ∈ ( ( 𝑅 ⊕ 𝑇 ) ⊕ 𝑈 ) ↔ ∃ 𝑦 ∈ ( 𝑅 ⊕ 𝑇 ) ∃ 𝑐 ∈ 𝑈 𝑥 = ( 𝑦 ( +g ‘ 𝐺 ) 𝑐 ) ) )
53 2 1 lsmssv ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑇 ⊆ 𝐵 ∧ 𝑈 ⊆ 𝐵 ) → ( 𝑇 ⊕ 𝑈 ) ⊆ 𝐵 )
54 3 5 6 53 syl3anc ⊢ ( 𝜑 → ( 𝑇 ⊕ 𝑈 ) ⊆ 𝐵 )
55 2 7 1 lsmelvalx ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑅 ⊆ 𝐵 ∧ ( 𝑇 ⊕ 𝑈 ) ⊆ 𝐵 ) → ( 𝑥 ∈ ( 𝑅 ⊕ ( 𝑇 ⊕ 𝑈 ) ) ↔ ∃ 𝑎 ∈ 𝑅 ∃ 𝑧 ∈ ( 𝑇 ⊕ 𝑈 ) 𝑥 = ( 𝑎 ( +g ‘ 𝐺 ) 𝑧 ) ) )
56 3 4 54 55 syl3anc ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑅 ⊕ ( 𝑇 ⊕ 𝑈 ) ) ↔ ∃ 𝑎 ∈ 𝑅 ∃ 𝑧 ∈ ( 𝑇 ⊕ 𝑈 ) 𝑥 = ( 𝑎 ( +g ‘ 𝐺 ) 𝑧 ) ) )
57 48 52 56 3bitr4d ⊢ ( 𝜑 → ( 𝑥 ∈ ( ( 𝑅 ⊕ 𝑇 ) ⊕ 𝑈 ) ↔ 𝑥 ∈ ( 𝑅 ⊕ ( 𝑇 ⊕ 𝑈 ) ) ) )
58 57 eqrdv ⊢ ( 𝜑 → ( ( 𝑅 ⊕ 𝑇 ) ⊕ 𝑈 ) = ( 𝑅 ⊕ ( 𝑇 ⊕ 𝑈 ) ) )