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 e. Abel /\ ( Q e. ( SubGrp ` G ) /\ R e. ( SubGrp ` G ) ) /\ ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) ) -> ( ( Q .(+) R ) .(+) ( T .(+) U ) ) = ( ( Q .(+) T ) .(+) ( R .(+) U ) ) )

Proof

Step Hyp Ref Expression
1 lsmcom.s 
 |-  .(+) = ( LSSum ` G )
2 simp1 
 |-  ( ( G e. Abel /\ ( Q e. ( SubGrp ` G ) /\ R e. ( SubGrp ` G ) ) /\ ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) ) -> G e. Abel )
3 simp2r 
 |-  ( ( G e. Abel /\ ( Q e. ( SubGrp ` G ) /\ R e. ( SubGrp ` G ) ) /\ ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) ) -> R e. ( SubGrp ` G ) )
4 simp3l 
 |-  ( ( G e. Abel /\ ( Q e. ( SubGrp ` G ) /\ R e. ( SubGrp ` G ) ) /\ ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) ) -> T e. ( SubGrp ` G ) )
5 1 lsmcom 
 |-  ( ( G e. Abel /\ R e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) ) -> ( R .(+) T ) = ( T .(+) R ) )
6 2 3 4 5 syl3anc 
 |-  ( ( G e. Abel /\ ( Q e. ( SubGrp ` G ) /\ R e. ( SubGrp ` G ) ) /\ ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) ) -> ( R .(+) T ) = ( T .(+) R ) )
7 6 oveq2d 
 |-  ( ( G e. Abel /\ ( Q e. ( SubGrp ` G ) /\ R e. ( SubGrp ` G ) ) /\ ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) ) -> ( Q .(+) ( R .(+) T ) ) = ( Q .(+) ( T .(+) R ) ) )
8 simp2l 
 |-  ( ( G e. Abel /\ ( Q e. ( SubGrp ` G ) /\ R e. ( SubGrp ` G ) ) /\ ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) ) -> Q e. ( SubGrp ` G ) )
9 1 lsmass 
 |-  ( ( Q e. ( SubGrp ` G ) /\ R e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) ) -> ( ( Q .(+) R ) .(+) T ) = ( Q .(+) ( R .(+) T ) ) )
10 8 3 4 9 syl3anc 
 |-  ( ( G e. Abel /\ ( Q e. ( SubGrp ` G ) /\ R e. ( SubGrp ` G ) ) /\ ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) ) -> ( ( Q .(+) R ) .(+) T ) = ( Q .(+) ( R .(+) T ) ) )
11 1 lsmass 
 |-  ( ( Q e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) /\ R e. ( SubGrp ` G ) ) -> ( ( Q .(+) T ) .(+) R ) = ( Q .(+) ( T .(+) R ) ) )
12 8 4 3 11 syl3anc 
 |-  ( ( G e. Abel /\ ( Q e. ( SubGrp ` G ) /\ R e. ( SubGrp ` G ) ) /\ ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) ) -> ( ( Q .(+) T ) .(+) R ) = ( Q .(+) ( T .(+) R ) ) )
13 7 10 12 3eqtr4d 
 |-  ( ( G e. Abel /\ ( Q e. ( SubGrp ` G ) /\ R e. ( SubGrp ` G ) ) /\ ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) ) -> ( ( Q .(+) R ) .(+) T ) = ( ( Q .(+) T ) .(+) R ) )
14 13 oveq1d 
 |-  ( ( G e. Abel /\ ( Q e. ( SubGrp ` G ) /\ R e. ( SubGrp ` G ) ) /\ ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) ) -> ( ( ( Q .(+) R ) .(+) T ) .(+) U ) = ( ( ( Q .(+) T ) .(+) R ) .(+) U ) )
15 1 lsmsubg2 
 |-  ( ( G e. Abel /\ Q e. ( SubGrp ` G ) /\ R e. ( SubGrp ` G ) ) -> ( Q .(+) R ) e. ( SubGrp ` G ) )
16 2 8 3 15 syl3anc 
 |-  ( ( G e. Abel /\ ( Q e. ( SubGrp ` G ) /\ R e. ( SubGrp ` G ) ) /\ ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) ) -> ( Q .(+) R ) e. ( SubGrp ` G ) )
17 simp3r 
 |-  ( ( G e. Abel /\ ( Q e. ( SubGrp ` G ) /\ R e. ( SubGrp ` G ) ) /\ ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) ) -> U e. ( SubGrp ` G ) )
18 1 lsmass 
 |-  ( ( ( Q .(+) R ) e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) -> ( ( ( Q .(+) R ) .(+) T ) .(+) U ) = ( ( Q .(+) R ) .(+) ( T .(+) U ) ) )
19 16 4 17 18 syl3anc 
 |-  ( ( G e. Abel /\ ( Q e. ( SubGrp ` G ) /\ R e. ( SubGrp ` G ) ) /\ ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) ) -> ( ( ( Q .(+) R ) .(+) T ) .(+) U ) = ( ( Q .(+) R ) .(+) ( T .(+) U ) ) )
20 1 lsmsubg2 
 |-  ( ( G e. Abel /\ Q e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) ) -> ( Q .(+) T ) e. ( SubGrp ` G ) )
21 2 8 4 20 syl3anc 
 |-  ( ( G e. Abel /\ ( Q e. ( SubGrp ` G ) /\ R e. ( SubGrp ` G ) ) /\ ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) ) -> ( Q .(+) T ) e. ( SubGrp ` G ) )
22 1 lsmass 
 |-  ( ( ( Q .(+) T ) e. ( SubGrp ` G ) /\ R e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) -> ( ( ( Q .(+) T ) .(+) R ) .(+) U ) = ( ( Q .(+) T ) .(+) ( R .(+) U ) ) )
23 21 3 17 22 syl3anc 
 |-  ( ( G e. Abel /\ ( Q e. ( SubGrp ` G ) /\ R e. ( SubGrp ` G ) ) /\ ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) ) -> ( ( ( Q .(+) T ) .(+) R ) .(+) U ) = ( ( Q .(+) T ) .(+) ( R .(+) U ) ) )
24 14 19 23 3eqtr3d 
 |-  ( ( G e. Abel /\ ( Q e. ( SubGrp ` G ) /\ R e. ( SubGrp ` G ) ) /\ ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) ) -> ( ( Q .(+) R ) .(+) ( T .(+) U ) ) = ( ( Q .(+) T ) .(+) ( R .(+) U ) ) )