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⁡G
Assertion lsm4 ⊢G∈Abel∧Q∈SubGrp⁡G∧R∈SubGrp⁡G∧T∈SubGrp⁡G∧U∈SubGrp⁡G→Q⊕˙R⊕˙T⊕˙U=Q⊕˙T⊕˙R⊕˙U

Proof

Step Hyp Ref Expression
1 lsmcom.s ⊢⊕˙=LSSum⁡G
2 simp1 ⊢G∈Abel∧Q∈SubGrp⁡G∧R∈SubGrp⁡G∧T∈SubGrp⁡G∧U∈SubGrp⁡G→G∈Abel
3 simp2r ⊢G∈Abel∧Q∈SubGrp⁡G∧R∈SubGrp⁡G∧T∈SubGrp⁡G∧U∈SubGrp⁡G→R∈SubGrp⁡G
4 simp3l ⊢G∈Abel∧Q∈SubGrp⁡G∧R∈SubGrp⁡G∧T∈SubGrp⁡G∧U∈SubGrp⁡G→T∈SubGrp⁡G
5 1 lsmcom ⊢G∈Abel∧R∈SubGrp⁡G∧T∈SubGrp⁡G→R⊕˙T=T⊕˙R
6 2 3 4 5 syl3anc ⊢G∈Abel∧Q∈SubGrp⁡G∧R∈SubGrp⁡G∧T∈SubGrp⁡G∧U∈SubGrp⁡G→R⊕˙T=T⊕˙R
7 6 oveq2d ⊢G∈Abel∧Q∈SubGrp⁡G∧R∈SubGrp⁡G∧T∈SubGrp⁡G∧U∈SubGrp⁡G→Q⊕˙R⊕˙T=Q⊕˙T⊕˙R
8 simp2l ⊢G∈Abel∧Q∈SubGrp⁡G∧R∈SubGrp⁡G∧T∈SubGrp⁡G∧U∈SubGrp⁡G→Q∈SubGrp⁡G
9 1 lsmass ⊢Q∈SubGrp⁡G∧R∈SubGrp⁡G∧T∈SubGrp⁡G→Q⊕˙R⊕˙T=Q⊕˙R⊕˙T
10 8 3 4 9 syl3anc ⊢G∈Abel∧Q∈SubGrp⁡G∧R∈SubGrp⁡G∧T∈SubGrp⁡G∧U∈SubGrp⁡G→Q⊕˙R⊕˙T=Q⊕˙R⊕˙T
11 1 lsmass ⊢Q∈SubGrp⁡G∧T∈SubGrp⁡G∧R∈SubGrp⁡G→Q⊕˙T⊕˙R=Q⊕˙T⊕˙R
12 8 4 3 11 syl3anc ⊢G∈Abel∧Q∈SubGrp⁡G∧R∈SubGrp⁡G∧T∈SubGrp⁡G∧U∈SubGrp⁡G→Q⊕˙T⊕˙R=Q⊕˙T⊕˙R
13 7 10 12 3eqtr4d ⊢G∈Abel∧Q∈SubGrp⁡G∧R∈SubGrp⁡G∧T∈SubGrp⁡G∧U∈SubGrp⁡G→Q⊕˙R⊕˙T=Q⊕˙T⊕˙R
14 13 oveq1d ⊢G∈Abel∧Q∈SubGrp⁡G∧R∈SubGrp⁡G∧T∈SubGrp⁡G∧U∈SubGrp⁡G→Q⊕˙R⊕˙T⊕˙U=Q⊕˙T⊕˙R⊕˙U
15 1 lsmsubg2 ⊢G∈Abel∧Q∈SubGrp⁡G∧R∈SubGrp⁡G→Q⊕˙R∈SubGrp⁡G
16 2 8 3 15 syl3anc ⊢G∈Abel∧Q∈SubGrp⁡G∧R∈SubGrp⁡G∧T∈SubGrp⁡G∧U∈SubGrp⁡G→Q⊕˙R∈SubGrp⁡G
17 simp3r ⊢G∈Abel∧Q∈SubGrp⁡G∧R∈SubGrp⁡G∧T∈SubGrp⁡G∧U∈SubGrp⁡G→U∈SubGrp⁡G
18 1 lsmass ⊢Q⊕˙R∈SubGrp⁡G∧T∈SubGrp⁡G∧U∈SubGrp⁡G→Q⊕˙R⊕˙T⊕˙U=Q⊕˙R⊕˙T⊕˙U
19 16 4 17 18 syl3anc ⊢G∈Abel∧Q∈SubGrp⁡G∧R∈SubGrp⁡G∧T∈SubGrp⁡G∧U∈SubGrp⁡G→Q⊕˙R⊕˙T⊕˙U=Q⊕˙R⊕˙T⊕˙U
20 1 lsmsubg2 ⊢G∈Abel∧Q∈SubGrp⁡G∧T∈SubGrp⁡G→Q⊕˙T∈SubGrp⁡G
21 2 8 4 20 syl3anc ⊢G∈Abel∧Q∈SubGrp⁡G∧R∈SubGrp⁡G∧T∈SubGrp⁡G∧U∈SubGrp⁡G→Q⊕˙T∈SubGrp⁡G
22 1 lsmass ⊢Q⊕˙T∈SubGrp⁡G∧R∈SubGrp⁡G∧U∈SubGrp⁡G→Q⊕˙T⊕˙R⊕˙U=Q⊕˙T⊕˙R⊕˙U
23 21 3 17 22 syl3anc ⊢G∈Abel∧Q∈SubGrp⁡G∧R∈SubGrp⁡G∧T∈SubGrp⁡G∧U∈SubGrp⁡G→Q⊕˙T⊕˙R⊕˙U=Q⊕˙T⊕˙R⊕˙U
24 14 19 23 3eqtr3d ⊢G∈Abel∧Q∈SubGrp⁡G∧R∈SubGrp⁡G∧T∈SubGrp⁡G∧U∈SubGrp⁡G→Q⊕˙R⊕˙T⊕˙U=Q⊕˙T⊕˙R⊕˙U