Step |
Hyp |
Ref |
Expression |
1 |
|
lsmcom.s |
|- .(+) = ( LSSum ` G ) |
2 |
|
simp2 |
|- ( ( G e. Abel /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) -> T e. ( SubGrp ` G ) ) |
3 |
|
simp3 |
|- ( ( G e. Abel /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) -> U e. ( SubGrp ` G ) ) |
4 |
|
eqid |
|- ( Cntz ` G ) = ( Cntz ` G ) |
5 |
|
simp1 |
|- ( ( G e. Abel /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) -> G e. Abel ) |
6 |
4 5 2 3
|
ablcntzd |
|- ( ( G e. Abel /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) -> T C_ ( ( Cntz ` G ) ` U ) ) |
7 |
1 4
|
lsmsubg |
|- ( ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) /\ T C_ ( ( Cntz ` G ) ` U ) ) -> ( T .(+) U ) e. ( SubGrp ` G ) ) |
8 |
2 3 6 7
|
syl3anc |
|- ( ( G e. Abel /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) -> ( T .(+) U ) e. ( SubGrp ` G ) ) |