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 ( 𝜑 → ( ( 𝑅 𝑇 ) 𝑈 ) = ( 𝑅 ( 𝑇 𝑈 ) ) )