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