Step |
Hyp |
Ref |
Expression |
1 |
|
lsmcntz.p |
|- .(+) = ( LSSum ` G ) |
2 |
|
lsmcntz.s |
|- ( ph -> S e. ( SubGrp ` G ) ) |
3 |
|
lsmcntz.t |
|- ( ph -> T e. ( SubGrp ` G ) ) |
4 |
|
lsmcntz.u |
|- ( ph -> U e. ( SubGrp ` G ) ) |
5 |
|
lsmdisj.o |
|- .0. = ( 0g ` G ) |
6 |
|
lsmdisj.i |
|- ( ph -> ( ( S .(+) T ) i^i U ) = { .0. } ) |
7 |
|
lsmdisj2.i |
|- ( ph -> ( S i^i T ) = { .0. } ) |
8 |
|
lsmdisj3.z |
|- Z = ( Cntz ` G ) |
9 |
|
lsmdisj3.s |
|- ( ph -> S C_ ( Z ` T ) ) |
10 |
1 8
|
lsmcom2 |
|- ( ( S e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) /\ S C_ ( Z ` T ) ) -> ( S .(+) T ) = ( T .(+) S ) ) |
11 |
2 3 9 10
|
syl3anc |
|- ( ph -> ( S .(+) T ) = ( T .(+) S ) ) |
12 |
11
|
ineq1d |
|- ( ph -> ( ( S .(+) T ) i^i U ) = ( ( T .(+) S ) i^i U ) ) |
13 |
12 6
|
eqtr3d |
|- ( ph -> ( ( T .(+) S ) i^i U ) = { .0. } ) |
14 |
|
incom |
|- ( T i^i S ) = ( S i^i T ) |
15 |
14 7
|
syl5eq |
|- ( ph -> ( T i^i S ) = { .0. } ) |
16 |
1 3 2 4 5 13 15
|
lsmdisj2 |
|- ( ph -> ( S i^i ( T .(+) U ) ) = { .0. } ) |