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 |
|
eqid |
|- ( oppG ` G ) = ( oppG ` G ) |
9 |
8 1
|
oppglsm |
|- ( U ( LSSum ` ( oppG ` G ) ) S ) = ( S .(+) U ) |
10 |
9
|
ineq2i |
|- ( T i^i ( U ( LSSum ` ( oppG ` G ) ) S ) ) = ( T i^i ( S .(+) U ) ) |
11 |
|
incom |
|- ( T i^i ( S .(+) U ) ) = ( ( S .(+) U ) i^i T ) |
12 |
10 11
|
eqtri |
|- ( T i^i ( U ( LSSum ` ( oppG ` G ) ) S ) ) = ( ( S .(+) U ) i^i T ) |
13 |
|
eqid |
|- ( LSSum ` ( oppG ` G ) ) = ( LSSum ` ( oppG ` G ) ) |
14 |
8
|
oppgsubg |
|- ( SubGrp ` G ) = ( SubGrp ` ( oppG ` G ) ) |
15 |
4 14
|
eleqtrdi |
|- ( ph -> U e. ( SubGrp ` ( oppG ` G ) ) ) |
16 |
3 14
|
eleqtrdi |
|- ( ph -> T e. ( SubGrp ` ( oppG ` G ) ) ) |
17 |
2 14
|
eleqtrdi |
|- ( ph -> S e. ( SubGrp ` ( oppG ` G ) ) ) |
18 |
8 5
|
oppgid |
|- .0. = ( 0g ` ( oppG ` G ) ) |
19 |
8 1
|
oppglsm |
|- ( U ( LSSum ` ( oppG ` G ) ) T ) = ( T .(+) U ) |
20 |
19
|
ineq1i |
|- ( ( U ( LSSum ` ( oppG ` G ) ) T ) i^i S ) = ( ( T .(+) U ) i^i S ) |
21 |
|
incom |
|- ( ( T .(+) U ) i^i S ) = ( S i^i ( T .(+) U ) ) |
22 |
20 21
|
eqtri |
|- ( ( U ( LSSum ` ( oppG ` G ) ) T ) i^i S ) = ( S i^i ( T .(+) U ) ) |
23 |
22 6
|
syl5eq |
|- ( ph -> ( ( U ( LSSum ` ( oppG ` G ) ) T ) i^i S ) = { .0. } ) |
24 |
|
incom |
|- ( T i^i U ) = ( U i^i T ) |
25 |
24 7
|
eqtr3id |
|- ( ph -> ( U i^i T ) = { .0. } ) |
26 |
13 15 16 17 18 23 25
|
lsmdisj2 |
|- ( ph -> ( T i^i ( U ( LSSum ` ( oppG ` G ) ) S ) ) = { .0. } ) |
27 |
12 26
|
eqtr3id |
|- ( ph -> ( ( S .(+) U ) i^i T ) = { .0. } ) |