Metamath Proof Explorer


Theorem lsmdisj

Description: Disjointness from a subgroup sum. (Contributed by Mario Carneiro, 21-Apr-2016)

Ref Expression
Hypotheses lsmcntz.p
|- .(+) = ( LSSum ` G )
lsmcntz.s
|- ( ph -> S e. ( SubGrp ` G ) )
lsmcntz.t
|- ( ph -> T e. ( SubGrp ` G ) )
lsmcntz.u
|- ( ph -> U e. ( SubGrp ` G ) )
lsmdisj.o
|- .0. = ( 0g ` G )
lsmdisj.i
|- ( ph -> ( ( S .(+) T ) i^i U ) = { .0. } )
Assertion lsmdisj
|- ( ph -> ( ( S i^i U ) = { .0. } /\ ( T i^i U ) = { .0. } ) )

Proof

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 1 lsmub1
 |-  ( ( S e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) ) -> S C_ ( S .(+) T ) )
8 2 3 7 syl2anc
 |-  ( ph -> S C_ ( S .(+) T ) )
9 8 ssrind
 |-  ( ph -> ( S i^i U ) C_ ( ( S .(+) T ) i^i U ) )
10 9 6 sseqtrd
 |-  ( ph -> ( S i^i U ) C_ { .0. } )
11 5 subg0cl
 |-  ( S e. ( SubGrp ` G ) -> .0. e. S )
12 2 11 syl
 |-  ( ph -> .0. e. S )
13 5 subg0cl
 |-  ( U e. ( SubGrp ` G ) -> .0. e. U )
14 4 13 syl
 |-  ( ph -> .0. e. U )
15 12 14 elind
 |-  ( ph -> .0. e. ( S i^i U ) )
16 15 snssd
 |-  ( ph -> { .0. } C_ ( S i^i U ) )
17 10 16 eqssd
 |-  ( ph -> ( S i^i U ) = { .0. } )
18 1 lsmub2
 |-  ( ( S e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) ) -> T C_ ( S .(+) T ) )
19 2 3 18 syl2anc
 |-  ( ph -> T C_ ( S .(+) T ) )
20 19 ssrind
 |-  ( ph -> ( T i^i U ) C_ ( ( S .(+) T ) i^i U ) )
21 20 6 sseqtrd
 |-  ( ph -> ( T i^i U ) C_ { .0. } )
22 5 subg0cl
 |-  ( T e. ( SubGrp ` G ) -> .0. e. T )
23 3 22 syl
 |-  ( ph -> .0. e. T )
24 23 14 elind
 |-  ( ph -> .0. e. ( T i^i U ) )
25 24 snssd
 |-  ( ph -> { .0. } C_ ( T i^i U ) )
26 21 25 eqssd
 |-  ( ph -> ( T i^i U ) = { .0. } )
27 17 26 jca
 |-  ( ph -> ( ( S i^i U ) = { .0. } /\ ( T i^i U ) = { .0. } ) )