Metamath Proof Explorer


Theorem lsmdisj2

Description: Association of the disjointness constraint in a subgroup sum. (Contributed by Mario Carneiro, 22-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. } )
lsmdisj2.i
|- ( ph -> ( S i^i T ) = { .0. } )
Assertion lsmdisj2
|- ( ph -> ( T i^i ( S .(+) 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 lsmdisj2.i
 |-  ( ph -> ( S i^i T ) = { .0. } )
8 eqid
 |-  ( +g ` G ) = ( +g ` G )
9 8 1 lsmelval
 |-  ( ( S e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) -> ( x e. ( S .(+) U ) <-> E. s e. S E. u e. U x = ( s ( +g ` G ) u ) ) )
10 2 4 9 syl2anc
 |-  ( ph -> ( x e. ( S .(+) U ) <-> E. s e. S E. u e. U x = ( s ( +g ` G ) u ) ) )
11 simplrl
 |-  ( ( ( ph /\ ( s e. S /\ u e. U ) ) /\ ( s ( +g ` G ) u ) e. T ) -> s e. S )
12 subgrcl
 |-  ( S e. ( SubGrp ` G ) -> G e. Grp )
13 2 12 syl
 |-  ( ph -> G e. Grp )
14 13 ad2antrr
 |-  ( ( ( ph /\ ( s e. S /\ u e. U ) ) /\ ( s ( +g ` G ) u ) e. T ) -> G e. Grp )
15 2 ad2antrr
 |-  ( ( ( ph /\ ( s e. S /\ u e. U ) ) /\ ( s ( +g ` G ) u ) e. T ) -> S e. ( SubGrp ` G ) )
16 eqid
 |-  ( Base ` G ) = ( Base ` G )
17 16 subgss
 |-  ( S e. ( SubGrp ` G ) -> S C_ ( Base ` G ) )
18 15 17 syl
 |-  ( ( ( ph /\ ( s e. S /\ u e. U ) ) /\ ( s ( +g ` G ) u ) e. T ) -> S C_ ( Base ` G ) )
19 18 11 sseldd
 |-  ( ( ( ph /\ ( s e. S /\ u e. U ) ) /\ ( s ( +g ` G ) u ) e. T ) -> s e. ( Base ` G ) )
20 eqid
 |-  ( invg ` G ) = ( invg ` G )
21 16 8 5 20 grplinv
 |-  ( ( G e. Grp /\ s e. ( Base ` G ) ) -> ( ( ( invg ` G ) ` s ) ( +g ` G ) s ) = .0. )
22 14 19 21 syl2anc
 |-  ( ( ( ph /\ ( s e. S /\ u e. U ) ) /\ ( s ( +g ` G ) u ) e. T ) -> ( ( ( invg ` G ) ` s ) ( +g ` G ) s ) = .0. )
23 22 oveq1d
 |-  ( ( ( ph /\ ( s e. S /\ u e. U ) ) /\ ( s ( +g ` G ) u ) e. T ) -> ( ( ( ( invg ` G ) ` s ) ( +g ` G ) s ) ( +g ` G ) u ) = ( .0. ( +g ` G ) u ) )
24 20 subginvcl
 |-  ( ( S e. ( SubGrp ` G ) /\ s e. S ) -> ( ( invg ` G ) ` s ) e. S )
25 15 11 24 syl2anc
 |-  ( ( ( ph /\ ( s e. S /\ u e. U ) ) /\ ( s ( +g ` G ) u ) e. T ) -> ( ( invg ` G ) ` s ) e. S )
26 18 25 sseldd
 |-  ( ( ( ph /\ ( s e. S /\ u e. U ) ) /\ ( s ( +g ` G ) u ) e. T ) -> ( ( invg ` G ) ` s ) e. ( Base ` G ) )
27 4 ad2antrr
 |-  ( ( ( ph /\ ( s e. S /\ u e. U ) ) /\ ( s ( +g ` G ) u ) e. T ) -> U e. ( SubGrp ` G ) )
28 16 subgss
 |-  ( U e. ( SubGrp ` G ) -> U C_ ( Base ` G ) )
29 27 28 syl
 |-  ( ( ( ph /\ ( s e. S /\ u e. U ) ) /\ ( s ( +g ` G ) u ) e. T ) -> U C_ ( Base ` G ) )
30 simplrr
 |-  ( ( ( ph /\ ( s e. S /\ u e. U ) ) /\ ( s ( +g ` G ) u ) e. T ) -> u e. U )
31 29 30 sseldd
 |-  ( ( ( ph /\ ( s e. S /\ u e. U ) ) /\ ( s ( +g ` G ) u ) e. T ) -> u e. ( Base ` G ) )
32 16 8 grpass
 |-  ( ( G e. Grp /\ ( ( ( invg ` G ) ` s ) e. ( Base ` G ) /\ s e. ( Base ` G ) /\ u e. ( Base ` G ) ) ) -> ( ( ( ( invg ` G ) ` s ) ( +g ` G ) s ) ( +g ` G ) u ) = ( ( ( invg ` G ) ` s ) ( +g ` G ) ( s ( +g ` G ) u ) ) )
33 14 26 19 31 32 syl13anc
 |-  ( ( ( ph /\ ( s e. S /\ u e. U ) ) /\ ( s ( +g ` G ) u ) e. T ) -> ( ( ( ( invg ` G ) ` s ) ( +g ` G ) s ) ( +g ` G ) u ) = ( ( ( invg ` G ) ` s ) ( +g ` G ) ( s ( +g ` G ) u ) ) )
34 16 8 5 grplid
 |-  ( ( G e. Grp /\ u e. ( Base ` G ) ) -> ( .0. ( +g ` G ) u ) = u )
35 14 31 34 syl2anc
 |-  ( ( ( ph /\ ( s e. S /\ u e. U ) ) /\ ( s ( +g ` G ) u ) e. T ) -> ( .0. ( +g ` G ) u ) = u )
36 23 33 35 3eqtr3d
 |-  ( ( ( ph /\ ( s e. S /\ u e. U ) ) /\ ( s ( +g ` G ) u ) e. T ) -> ( ( ( invg ` G ) ` s ) ( +g ` G ) ( s ( +g ` G ) u ) ) = u )
37 3 ad2antrr
 |-  ( ( ( ph /\ ( s e. S /\ u e. U ) ) /\ ( s ( +g ` G ) u ) e. T ) -> T e. ( SubGrp ` G ) )
38 simpr
 |-  ( ( ( ph /\ ( s e. S /\ u e. U ) ) /\ ( s ( +g ` G ) u ) e. T ) -> ( s ( +g ` G ) u ) e. T )
39 8 1 lsmelvali
 |-  ( ( ( S e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) ) /\ ( ( ( invg ` G ) ` s ) e. S /\ ( s ( +g ` G ) u ) e. T ) ) -> ( ( ( invg ` G ) ` s ) ( +g ` G ) ( s ( +g ` G ) u ) ) e. ( S .(+) T ) )
40 15 37 25 38 39 syl22anc
 |-  ( ( ( ph /\ ( s e. S /\ u e. U ) ) /\ ( s ( +g ` G ) u ) e. T ) -> ( ( ( invg ` G ) ` s ) ( +g ` G ) ( s ( +g ` G ) u ) ) e. ( S .(+) T ) )
41 36 40 eqeltrrd
 |-  ( ( ( ph /\ ( s e. S /\ u e. U ) ) /\ ( s ( +g ` G ) u ) e. T ) -> u e. ( S .(+) T ) )
42 41 30 elind
 |-  ( ( ( ph /\ ( s e. S /\ u e. U ) ) /\ ( s ( +g ` G ) u ) e. T ) -> u e. ( ( S .(+) T ) i^i U ) )
43 6 ad2antrr
 |-  ( ( ( ph /\ ( s e. S /\ u e. U ) ) /\ ( s ( +g ` G ) u ) e. T ) -> ( ( S .(+) T ) i^i U ) = { .0. } )
44 42 43 eleqtrd
 |-  ( ( ( ph /\ ( s e. S /\ u e. U ) ) /\ ( s ( +g ` G ) u ) e. T ) -> u e. { .0. } )
45 elsni
 |-  ( u e. { .0. } -> u = .0. )
46 44 45 syl
 |-  ( ( ( ph /\ ( s e. S /\ u e. U ) ) /\ ( s ( +g ` G ) u ) e. T ) -> u = .0. )
47 46 oveq2d
 |-  ( ( ( ph /\ ( s e. S /\ u e. U ) ) /\ ( s ( +g ` G ) u ) e. T ) -> ( s ( +g ` G ) u ) = ( s ( +g ` G ) .0. ) )
48 16 8 5 grprid
 |-  ( ( G e. Grp /\ s e. ( Base ` G ) ) -> ( s ( +g ` G ) .0. ) = s )
49 14 19 48 syl2anc
 |-  ( ( ( ph /\ ( s e. S /\ u e. U ) ) /\ ( s ( +g ` G ) u ) e. T ) -> ( s ( +g ` G ) .0. ) = s )
50 47 49 eqtrd
 |-  ( ( ( ph /\ ( s e. S /\ u e. U ) ) /\ ( s ( +g ` G ) u ) e. T ) -> ( s ( +g ` G ) u ) = s )
51 50 38 eqeltrrd
 |-  ( ( ( ph /\ ( s e. S /\ u e. U ) ) /\ ( s ( +g ` G ) u ) e. T ) -> s e. T )
52 11 51 elind
 |-  ( ( ( ph /\ ( s e. S /\ u e. U ) ) /\ ( s ( +g ` G ) u ) e. T ) -> s e. ( S i^i T ) )
53 7 ad2antrr
 |-  ( ( ( ph /\ ( s e. S /\ u e. U ) ) /\ ( s ( +g ` G ) u ) e. T ) -> ( S i^i T ) = { .0. } )
54 52 53 eleqtrd
 |-  ( ( ( ph /\ ( s e. S /\ u e. U ) ) /\ ( s ( +g ` G ) u ) e. T ) -> s e. { .0. } )
55 elsni
 |-  ( s e. { .0. } -> s = .0. )
56 54 55 syl
 |-  ( ( ( ph /\ ( s e. S /\ u e. U ) ) /\ ( s ( +g ` G ) u ) e. T ) -> s = .0. )
57 56 46 oveq12d
 |-  ( ( ( ph /\ ( s e. S /\ u e. U ) ) /\ ( s ( +g ` G ) u ) e. T ) -> ( s ( +g ` G ) u ) = ( .0. ( +g ` G ) .0. ) )
58 16 5 grpidcl
 |-  ( G e. Grp -> .0. e. ( Base ` G ) )
59 16 8 5 grplid
 |-  ( ( G e. Grp /\ .0. e. ( Base ` G ) ) -> ( .0. ( +g ` G ) .0. ) = .0. )
60 13 58 59 syl2anc2
 |-  ( ph -> ( .0. ( +g ` G ) .0. ) = .0. )
61 60 ad2antrr
 |-  ( ( ( ph /\ ( s e. S /\ u e. U ) ) /\ ( s ( +g ` G ) u ) e. T ) -> ( .0. ( +g ` G ) .0. ) = .0. )
62 57 61 eqtrd
 |-  ( ( ( ph /\ ( s e. S /\ u e. U ) ) /\ ( s ( +g ` G ) u ) e. T ) -> ( s ( +g ` G ) u ) = .0. )
63 62 ex
 |-  ( ( ph /\ ( s e. S /\ u e. U ) ) -> ( ( s ( +g ` G ) u ) e. T -> ( s ( +g ` G ) u ) = .0. ) )
64 eleq1
 |-  ( x = ( s ( +g ` G ) u ) -> ( x e. T <-> ( s ( +g ` G ) u ) e. T ) )
65 eqeq1
 |-  ( x = ( s ( +g ` G ) u ) -> ( x = .0. <-> ( s ( +g ` G ) u ) = .0. ) )
66 64 65 imbi12d
 |-  ( x = ( s ( +g ` G ) u ) -> ( ( x e. T -> x = .0. ) <-> ( ( s ( +g ` G ) u ) e. T -> ( s ( +g ` G ) u ) = .0. ) ) )
67 63 66 syl5ibrcom
 |-  ( ( ph /\ ( s e. S /\ u e. U ) ) -> ( x = ( s ( +g ` G ) u ) -> ( x e. T -> x = .0. ) ) )
68 67 rexlimdvva
 |-  ( ph -> ( E. s e. S E. u e. U x = ( s ( +g ` G ) u ) -> ( x e. T -> x = .0. ) ) )
69 10 68 sylbid
 |-  ( ph -> ( x e. ( S .(+) U ) -> ( x e. T -> x = .0. ) ) )
70 69 impcomd
 |-  ( ph -> ( ( x e. T /\ x e. ( S .(+) U ) ) -> x = .0. ) )
71 elin
 |-  ( x e. ( T i^i ( S .(+) U ) ) <-> ( x e. T /\ x e. ( S .(+) U ) ) )
72 velsn
 |-  ( x e. { .0. } <-> x = .0. )
73 70 71 72 3imtr4g
 |-  ( ph -> ( x e. ( T i^i ( S .(+) U ) ) -> x e. { .0. } ) )
74 73 ssrdv
 |-  ( ph -> ( T i^i ( S .(+) U ) ) C_ { .0. } )
75 5 subg0cl
 |-  ( T e. ( SubGrp ` G ) -> .0. e. T )
76 3 75 syl
 |-  ( ph -> .0. e. T )
77 1 lsmub1
 |-  ( ( S e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) -> S C_ ( S .(+) U ) )
78 2 4 77 syl2anc
 |-  ( ph -> S C_ ( S .(+) U ) )
79 5 subg0cl
 |-  ( S e. ( SubGrp ` G ) -> .0. e. S )
80 2 79 syl
 |-  ( ph -> .0. e. S )
81 78 80 sseldd
 |-  ( ph -> .0. e. ( S .(+) U ) )
82 76 81 elind
 |-  ( ph -> .0. e. ( T i^i ( S .(+) U ) ) )
83 82 snssd
 |-  ( ph -> { .0. } C_ ( T i^i ( S .(+) U ) ) )
84 74 83 eqssd
 |-  ( ph -> ( T i^i ( S .(+) U ) ) = { .0. } )