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. } )