Metamath Proof Explorer

Theorem lsmmod

Description: The modular law holds for subgroup sum. Similar to part of Theorem 16.9 of MaedaMaeda p. 70. (Contributed by NM, 2-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2016)

Ref Expression
Hypothesis lsmmod.p 
|- .(+) = ( LSSum ` G )
Assertion lsmmod 
|- ( ( ( S e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) /\ S C_ U ) -> ( S .(+) ( T i^i U ) ) = ( ( S .(+) T ) i^i U ) )

Proof

Step Hyp Ref Expression
1 lsmmod.p 
 |-  .(+) = ( LSSum ` G )
2 simpl1 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) /\ S C_ U ) -> S e. ( SubGrp ` G ) )
3 simpl2 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) /\ S C_ U ) -> T e. ( SubGrp ` G ) )
4 inss1 
 |-  ( T i^i U ) C_ T
5 4 a1i 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) /\ S C_ U ) -> ( T i^i U ) C_ T )
6 1 lsmless2 
 |-  ( ( S e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) /\ ( T i^i U ) C_ T ) -> ( S .(+) ( T i^i U ) ) C_ ( S .(+) T ) )
7 2 3 5 6 syl3anc 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) /\ S C_ U ) -> ( S .(+) ( T i^i U ) ) C_ ( S .(+) T ) )
8 simpr 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) /\ S C_ U ) -> S C_ U )
9 inss2 
 |-  ( T i^i U ) C_ U
10 9 a1i 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) /\ S C_ U ) -> ( T i^i U ) C_ U )
11 subgrcl 
 |-  ( S e. ( SubGrp ` G ) -> G e. Grp )
12 eqid 
 |-  ( Base ` G ) = ( Base ` G )
13 12 subgacs 
 |-  ( G e. Grp -> ( SubGrp ` G ) e. ( ACS ` ( Base ` G ) ) )
14 acsmre 
 |-  ( ( SubGrp ` G ) e. ( ACS ` ( Base ` G ) ) -> ( SubGrp ` G ) e. ( Moore ` ( Base ` G ) ) )
15 2 11 13 14 4syl 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) /\ S C_ U ) -> ( SubGrp ` G ) e. ( Moore ` ( Base ` G ) ) )
16 simpl3 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) /\ S C_ U ) -> U e. ( SubGrp ` G ) )
17 mreincl 
 |-  ( ( ( SubGrp ` G ) e. ( Moore ` ( Base ` G ) ) /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) -> ( T i^i U ) e. ( SubGrp ` G ) )
18 15 3 16 17 syl3anc 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) /\ S C_ U ) -> ( T i^i U ) e. ( SubGrp ` G ) )
19 1 lsmlub 
 |-  ( ( S e. ( SubGrp ` G ) /\ ( T i^i U ) e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) -> ( ( S C_ U /\ ( T i^i U ) C_ U ) <-> ( S .(+) ( T i^i U ) ) C_ U ) )
20 2 18 16 19 syl3anc 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) /\ S C_ U ) -> ( ( S C_ U /\ ( T i^i U ) C_ U ) <-> ( S .(+) ( T i^i U ) ) C_ U ) )
21 8 10 20 mpbi2and 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) /\ S C_ U ) -> ( S .(+) ( T i^i U ) ) C_ U )
22 7 21 ssind 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) /\ S C_ U ) -> ( S .(+) ( T i^i U ) ) C_ ( ( S .(+) T ) i^i U ) )
23 elin 
 |-  ( x e. ( ( S .(+) T ) i^i U ) <-> ( x e. ( S .(+) T ) /\ x e. U ) )
24 eqid 
 |-  ( +g ` G ) = ( +g ` G )
25 24 1 lsmelval 
 |-  ( ( S e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) ) -> ( x e. ( S .(+) T ) <-> E. y e. S E. z e. T x = ( y ( +g ` G ) z ) ) )
26 2 3 25 syl2anc 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) /\ S C_ U ) -> ( x e. ( S .(+) T ) <-> E. y e. S E. z e. T x = ( y ( +g ` G ) z ) ) )
27 2 adantr 
 |-  ( ( ( ( S e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) /\ S C_ U ) /\ ( ( y e. S /\ z e. T ) /\ ( y ( +g ` G ) z ) e. U ) ) -> S e. ( SubGrp ` G ) )
28 18 adantr 
 |-  ( ( ( ( S e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) /\ S C_ U ) /\ ( ( y e. S /\ z e. T ) /\ ( y ( +g ` G ) z ) e. U ) ) -> ( T i^i U ) e. ( SubGrp ` G ) )
29 simprll 
 |-  ( ( ( ( S e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) /\ S C_ U ) /\ ( ( y e. S /\ z e. T ) /\ ( y ( +g ` G ) z ) e. U ) ) -> y e. S )
30 simprlr 
 |-  ( ( ( ( S e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) /\ S C_ U ) /\ ( ( y e. S /\ z e. T ) /\ ( y ( +g ` G ) z ) e. U ) ) -> z e. T )
31 27 11 syl 
 |-  ( ( ( ( S e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) /\ S C_ U ) /\ ( ( y e. S /\ z e. T ) /\ ( y ( +g ` G ) z ) e. U ) ) -> G e. Grp )
32 16 adantr 
 |-  ( ( ( ( S e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) /\ S C_ U ) /\ ( ( y e. S /\ z e. T ) /\ ( y ( +g ` G ) z ) e. U ) ) -> U e. ( SubGrp ` G ) )
33 12 subgss 
 |-  ( U e. ( SubGrp ` G ) -> U C_ ( Base ` G ) )
34 32 33 syl 
 |-  ( ( ( ( S e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) /\ S C_ U ) /\ ( ( y e. S /\ z e. T ) /\ ( y ( +g ` G ) z ) e. U ) ) -> U C_ ( Base ` G ) )
35 8 adantr 
 |-  ( ( ( ( S e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) /\ S C_ U ) /\ ( ( y e. S /\ z e. T ) /\ ( y ( +g ` G ) z ) e. U ) ) -> S C_ U )
36 35 29 sseldd 
 |-  ( ( ( ( S e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) /\ S C_ U ) /\ ( ( y e. S /\ z e. T ) /\ ( y ( +g ` G ) z ) e. U ) ) -> y e. U )
37 34 36 sseldd 
 |-  ( ( ( ( S e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) /\ S C_ U ) /\ ( ( y e. S /\ z e. T ) /\ ( y ( +g ` G ) z ) e. U ) ) -> y e. ( Base ` G ) )
38 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
39 eqid 
 |-  ( invg ` G ) = ( invg ` G )
40 12 24 38 39 grplinv 
 |-  ( ( G e. Grp /\ y e. ( Base ` G ) ) -> ( ( ( invg ` G ) ` y ) ( +g ` G ) y ) = ( 0g ` G ) )
41 31 37 40 syl2anc 
 |-  ( ( ( ( S e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) /\ S C_ U ) /\ ( ( y e. S /\ z e. T ) /\ ( y ( +g ` G ) z ) e. U ) ) -> ( ( ( invg ` G ) ` y ) ( +g ` G ) y ) = ( 0g ` G ) )
42 41 oveq1d 
 |-  ( ( ( ( S e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) /\ S C_ U ) /\ ( ( y e. S /\ z e. T ) /\ ( y ( +g ` G ) z ) e. U ) ) -> ( ( ( ( invg ` G ) ` y ) ( +g ` G ) y ) ( +g ` G ) z ) = ( ( 0g ` G ) ( +g ` G ) z ) )
43 39 subginvcl 
 |-  ( ( U e. ( SubGrp ` G ) /\ y e. U ) -> ( ( invg ` G ) ` y ) e. U )
44 32 36 43 syl2anc 
 |-  ( ( ( ( S e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) /\ S C_ U ) /\ ( ( y e. S /\ z e. T ) /\ ( y ( +g ` G ) z ) e. U ) ) -> ( ( invg ` G ) ` y ) e. U )
45 34 44 sseldd 
 |-  ( ( ( ( S e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) /\ S C_ U ) /\ ( ( y e. S /\ z e. T ) /\ ( y ( +g ` G ) z ) e. U ) ) -> ( ( invg ` G ) ` y ) e. ( Base ` G ) )
46 simpll2 
 |-  ( ( ( ( S e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) /\ S C_ U ) /\ ( ( y e. S /\ z e. T ) /\ ( y ( +g ` G ) z ) e. U ) ) -> T e. ( SubGrp ` G ) )
47 12 subgss 
 |-  ( T e. ( SubGrp ` G ) -> T C_ ( Base ` G ) )
48 46 47 syl 
 |-  ( ( ( ( S e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) /\ S C_ U ) /\ ( ( y e. S /\ z e. T ) /\ ( y ( +g ` G ) z ) e. U ) ) -> T C_ ( Base ` G ) )
49 48 30 sseldd 
 |-  ( ( ( ( S e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) /\ S C_ U ) /\ ( ( y e. S /\ z e. T ) /\ ( y ( +g ` G ) z ) e. U ) ) -> z e. ( Base ` G ) )
50 12 24 grpass 
 |-  ( ( G e. Grp /\ ( ( ( invg ` G ) ` y ) e. ( Base ` G ) /\ y e. ( Base ` G ) /\ z e. ( Base ` G ) ) ) -> ( ( ( ( invg ` G ) ` y ) ( +g ` G ) y ) ( +g ` G ) z ) = ( ( ( invg ` G ) ` y ) ( +g ` G ) ( y ( +g ` G ) z ) ) )
51 31 45 37 49 50 syl13anc 
 |-  ( ( ( ( S e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) /\ S C_ U ) /\ ( ( y e. S /\ z e. T ) /\ ( y ( +g ` G ) z ) e. U ) ) -> ( ( ( ( invg ` G ) ` y ) ( +g ` G ) y ) ( +g ` G ) z ) = ( ( ( invg ` G ) ` y ) ( +g ` G ) ( y ( +g ` G ) z ) ) )
52 12 24 38 grplid 
 |-  ( ( G e. Grp /\ z e. ( Base ` G ) ) -> ( ( 0g ` G ) ( +g ` G ) z ) = z )
53 31 49 52 syl2anc 
 |-  ( ( ( ( S e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) /\ S C_ U ) /\ ( ( y e. S /\ z e. T ) /\ ( y ( +g ` G ) z ) e. U ) ) -> ( ( 0g ` G ) ( +g ` G ) z ) = z )
54 42 51 53 3eqtr3d 
 |-  ( ( ( ( S e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) /\ S C_ U ) /\ ( ( y e. S /\ z e. T ) /\ ( y ( +g ` G ) z ) e. U ) ) -> ( ( ( invg ` G ) ` y ) ( +g ` G ) ( y ( +g ` G ) z ) ) = z )
55 simprr 
 |-  ( ( ( ( S e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) /\ S C_ U ) /\ ( ( y e. S /\ z e. T ) /\ ( y ( +g ` G ) z ) e. U ) ) -> ( y ( +g ` G ) z ) e. U )
56 24 subgcl 
 |-  ( ( U e. ( SubGrp ` G ) /\ ( ( invg ` G ) ` y ) e. U /\ ( y ( +g ` G ) z ) e. U ) -> ( ( ( invg ` G ) ` y ) ( +g ` G ) ( y ( +g ` G ) z ) ) e. U )
57 32 44 55 56 syl3anc 
 |-  ( ( ( ( S e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) /\ S C_ U ) /\ ( ( y e. S /\ z e. T ) /\ ( y ( +g ` G ) z ) e. U ) ) -> ( ( ( invg ` G ) ` y ) ( +g ` G ) ( y ( +g ` G ) z ) ) e. U )
58 54 57 eqeltrrd 
 |-  ( ( ( ( S e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) /\ S C_ U ) /\ ( ( y e. S /\ z e. T ) /\ ( y ( +g ` G ) z ) e. U ) ) -> z e. U )
59 30 58 elind 
 |-  ( ( ( ( S e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) /\ S C_ U ) /\ ( ( y e. S /\ z e. T ) /\ ( y ( +g ` G ) z ) e. U ) ) -> z e. ( T i^i U ) )
60 24 1 lsmelvali 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ ( T i^i U ) e. ( SubGrp ` G ) ) /\ ( y e. S /\ z e. ( T i^i U ) ) ) -> ( y ( +g ` G ) z ) e. ( S .(+) ( T i^i U ) ) )
61 27 28 29 59 60 syl22anc 
 |-  ( ( ( ( S e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) /\ S C_ U ) /\ ( ( y e. S /\ z e. T ) /\ ( y ( +g ` G ) z ) e. U ) ) -> ( y ( +g ` G ) z ) e. ( S .(+) ( T i^i U ) ) )
62 61 expr 
 |-  ( ( ( ( S e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) /\ S C_ U ) /\ ( y e. S /\ z e. T ) ) -> ( ( y ( +g ` G ) z ) e. U -> ( y ( +g ` G ) z ) e. ( S .(+) ( T i^i U ) ) ) )
63 eleq1 
 |-  ( x = ( y ( +g ` G ) z ) -> ( x e. U <-> ( y ( +g ` G ) z ) e. U ) )
64 eleq1 
 |-  ( x = ( y ( +g ` G ) z ) -> ( x e. ( S .(+) ( T i^i U ) ) <-> ( y ( +g ` G ) z ) e. ( S .(+) ( T i^i U ) ) ) )
65 63 64 imbi12d 
 |-  ( x = ( y ( +g ` G ) z ) -> ( ( x e. U -> x e. ( S .(+) ( T i^i U ) ) ) <-> ( ( y ( +g ` G ) z ) e. U -> ( y ( +g ` G ) z ) e. ( S .(+) ( T i^i U ) ) ) ) )
66 62 65 syl5ibrcom 
 |-  ( ( ( ( S e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) /\ S C_ U ) /\ ( y e. S /\ z e. T ) ) -> ( x = ( y ( +g ` G ) z ) -> ( x e. U -> x e. ( S .(+) ( T i^i U ) ) ) ) )
67 66 rexlimdvva 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) /\ S C_ U ) -> ( E. y e. S E. z e. T x = ( y ( +g ` G ) z ) -> ( x e. U -> x e. ( S .(+) ( T i^i U ) ) ) ) )
68 26 67 sylbid 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) /\ S C_ U ) -> ( x e. ( S .(+) T ) -> ( x e. U -> x e. ( S .(+) ( T i^i U ) ) ) ) )
69 68 impd 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) /\ S C_ U ) -> ( ( x e. ( S .(+) T ) /\ x e. U ) -> x e. ( S .(+) ( T i^i U ) ) ) )
70 23 69 syl5bi 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) /\ S C_ U ) -> ( x e. ( ( S .(+) T ) i^i U ) -> x e. ( S .(+) ( T i^i U ) ) ) )
71 70 ssrdv 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) /\ S C_ U ) -> ( ( S .(+) T ) i^i U ) C_ ( S .(+) ( T i^i U ) ) )
72 22 71 eqssd 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) /\ S C_ U ) -> ( S .(+) ( T i^i U ) ) = ( ( S .(+) T ) i^i U ) )