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 |
|
lsmdisjr.i |
|- ( ph -> ( S i^i ( T .(+) U ) ) = { .0. } ) |
7 |
|
lsmdisj2r.i |
|- ( ph -> ( T i^i U ) = { .0. } ) |
8 |
|
lsmdisj3r.z |
|- Z = ( Cntz ` G ) |
9 |
|
lsmdisj3r.s |
|- ( ph -> T C_ ( Z ` U ) ) |
10 |
1 8
|
lsmcom2 |
|- ( ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) /\ T C_ ( Z ` U ) ) -> ( T .(+) U ) = ( U .(+) T ) ) |
11 |
3 4 9 10
|
syl3anc |
|- ( ph -> ( T .(+) U ) = ( U .(+) T ) ) |
12 |
11
|
ineq2d |
|- ( ph -> ( S i^i ( T .(+) U ) ) = ( S i^i ( U .(+) T ) ) ) |
13 |
12 6
|
eqtr3d |
|- ( ph -> ( S i^i ( U .(+) T ) ) = { .0. } ) |
14 |
|
incom |
|- ( U i^i T ) = ( T i^i U ) |
15 |
14 7
|
syl5eq |
|- ( ph -> ( U i^i T ) = { .0. } ) |
16 |
1 2 4 3 5 13 15
|
lsmdisj2r |
|- ( ph -> ( ( S .(+) T ) i^i U ) = { .0. } ) |