Metamath Proof Explorer

Theorem lsm4

Description: Commutative/associative law for subgroup sum. (Contributed by NM, 26-Sep-2014) (Revised by Mario Carneiro, 19-Apr-2016)

Ref Expression
Hypothesis lsmcom.s ⊢ ⊕ = ( LSSum ‘ 𝐺 )
Assertion lsm4 ( ( 𝐺 ∈ Abel ∧ ( 𝑄 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑅 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) ) → ( ( 𝑄 ⊕ 𝑅 ) ⊕ ( 𝑇 ⊕ 𝑈 ) ) = ( ( 𝑄 ⊕ 𝑇 ) ⊕ ( 𝑅 ⊕ 𝑈 ) ) )

Proof

Step Hyp Ref Expression
1 lsmcom.s ⊢ ⊕ = ( LSSum ‘ 𝐺 )
2 simp1 ⊢ ( ( 𝐺 ∈ Abel ∧ ( 𝑄 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑅 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) ) → 𝐺 ∈ Abel )
3 simp2r ⊢ ( ( 𝐺 ∈ Abel ∧ ( 𝑄 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑅 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) ) → 𝑅 ∈ ( SubGrp ‘ 𝐺 ) )
4 simp3l ⊢ ( ( 𝐺 ∈ Abel ∧ ( 𝑄 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑅 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) ) → 𝑇 ∈ ( SubGrp ‘ 𝐺 ) )
5 1 lsmcom ⊢ ( ( 𝐺 ∈ Abel ∧ 𝑅 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ) → ( 𝑅 ⊕ 𝑇 ) = ( 𝑇 ⊕ 𝑅 ) )
6 2 3 4 5 syl3anc ⊢ ( ( 𝐺 ∈ Abel ∧ ( 𝑄 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑅 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) ) → ( 𝑅 ⊕ 𝑇 ) = ( 𝑇 ⊕ 𝑅 ) )
7 6 oveq2d ⊢ ( ( 𝐺 ∈ Abel ∧ ( 𝑄 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑅 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) ) → ( 𝑄 ⊕ ( 𝑅 ⊕ 𝑇 ) ) = ( 𝑄 ⊕ ( 𝑇 ⊕ 𝑅 ) ) )
8 simp2l ⊢ ( ( 𝐺 ∈ Abel ∧ ( 𝑄 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑅 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) ) → 𝑄 ∈ ( SubGrp ‘ 𝐺 ) )
9 1 lsmass ⊢ ( ( 𝑄 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑅 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ) → ( ( 𝑄 ⊕ 𝑅 ) ⊕ 𝑇 ) = ( 𝑄 ⊕ ( 𝑅 ⊕ 𝑇 ) ) )
10 8 3 4 9 syl3anc ⊢ ( ( 𝐺 ∈ Abel ∧ ( 𝑄 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑅 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) ) → ( ( 𝑄 ⊕ 𝑅 ) ⊕ 𝑇 ) = ( 𝑄 ⊕ ( 𝑅 ⊕ 𝑇 ) ) )
11 1 lsmass ⊢ ( ( 𝑄 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑅 ∈ ( SubGrp ‘ 𝐺 ) ) → ( ( 𝑄 ⊕ 𝑇 ) ⊕ 𝑅 ) = ( 𝑄 ⊕ ( 𝑇 ⊕ 𝑅 ) ) )
12 8 4 3 11 syl3anc ⊢ ( ( 𝐺 ∈ Abel ∧ ( 𝑄 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑅 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) ) → ( ( 𝑄 ⊕ 𝑇 ) ⊕ 𝑅 ) = ( 𝑄 ⊕ ( 𝑇 ⊕ 𝑅 ) ) )
13 7 10 12 3eqtr4d ⊢ ( ( 𝐺 ∈ Abel ∧ ( 𝑄 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑅 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) ) → ( ( 𝑄 ⊕ 𝑅 ) ⊕ 𝑇 ) = ( ( 𝑄 ⊕ 𝑇 ) ⊕ 𝑅 ) )
14 13 oveq1d ⊢ ( ( 𝐺 ∈ Abel ∧ ( 𝑄 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑅 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) ) → ( ( ( 𝑄 ⊕ 𝑅 ) ⊕ 𝑇 ) ⊕ 𝑈 ) = ( ( ( 𝑄 ⊕ 𝑇 ) ⊕ 𝑅 ) ⊕ 𝑈 ) )
15 1 lsmsubg2 ⊢ ( ( 𝐺 ∈ Abel ∧ 𝑄 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑅 ∈ ( SubGrp ‘ 𝐺 ) ) → ( 𝑄 ⊕ 𝑅 ) ∈ ( SubGrp ‘ 𝐺 ) )
16 2 8 3 15 syl3anc ⊢ ( ( 𝐺 ∈ Abel ∧ ( 𝑄 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑅 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) ) → ( 𝑄 ⊕ 𝑅 ) ∈ ( SubGrp ‘ 𝐺 ) )
17 simp3r ⊢ ( ( 𝐺 ∈ Abel ∧ ( 𝑄 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑅 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) ) → 𝑈 ∈ ( SubGrp ‘ 𝐺 ) )
18 1 lsmass ⊢ ( ( ( 𝑄 ⊕ 𝑅 ) ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) → ( ( ( 𝑄 ⊕ 𝑅 ) ⊕ 𝑇 ) ⊕ 𝑈 ) = ( ( 𝑄 ⊕ 𝑅 ) ⊕ ( 𝑇 ⊕ 𝑈 ) ) )
19 16 4 17 18 syl3anc ⊢ ( ( 𝐺 ∈ Abel ∧ ( 𝑄 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑅 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) ) → ( ( ( 𝑄 ⊕ 𝑅 ) ⊕ 𝑇 ) ⊕ 𝑈 ) = ( ( 𝑄 ⊕ 𝑅 ) ⊕ ( 𝑇 ⊕ 𝑈 ) ) )
20 1 lsmsubg2 ⊢ ( ( 𝐺 ∈ Abel ∧ 𝑄 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ) → ( 𝑄 ⊕ 𝑇 ) ∈ ( SubGrp ‘ 𝐺 ) )
21 2 8 4 20 syl3anc ⊢ ( ( 𝐺 ∈ Abel ∧ ( 𝑄 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑅 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) ) → ( 𝑄 ⊕ 𝑇 ) ∈ ( SubGrp ‘ 𝐺 ) )
22 1 lsmass ⊢ ( ( ( 𝑄 ⊕ 𝑇 ) ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑅 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) → ( ( ( 𝑄 ⊕ 𝑇 ) ⊕ 𝑅 ) ⊕ 𝑈 ) = ( ( 𝑄 ⊕ 𝑇 ) ⊕ ( 𝑅 ⊕ 𝑈 ) ) )
23 21 3 17 22 syl3anc ⊢ ( ( 𝐺 ∈ Abel ∧ ( 𝑄 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑅 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) ) → ( ( ( 𝑄 ⊕ 𝑇 ) ⊕ 𝑅 ) ⊕ 𝑈 ) = ( ( 𝑄 ⊕ 𝑇 ) ⊕ ( 𝑅 ⊕ 𝑈 ) ) )
24 14 19 23 3eqtr3d ⊢ ( ( 𝐺 ∈ Abel ∧ ( 𝑄 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑅 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) ) → ( ( 𝑄 ⊕ 𝑅 ) ⊕ ( 𝑇 ⊕ 𝑈 ) ) = ( ( 𝑄 ⊕ 𝑇 ) ⊕ ( 𝑅 ⊕ 𝑈 ) ) )