Metamath Proof Explorer

Theorem lsmsubg

Description: The sum of two commuting subgroups is a subgroup. (Contributed by Mario Carneiro, 19-Apr-2016)

Ref Expression
Hypotheses lsmsubg.p 
|- .(+) = ( LSSum ` G )
lsmsubg.z 
|- Z = ( Cntz ` G )
Assertion lsmsubg 
|- ( ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) /\ T C_ ( Z ` U ) ) -> ( T .(+) U ) e. ( SubGrp ` G ) )

Proof

Step Hyp Ref Expression
1 lsmsubg.p 
 |-  .(+) = ( LSSum ` G )
2 lsmsubg.z 
 |-  Z = ( Cntz ` G )
3 simp1 
 |-  ( ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) /\ T C_ ( Z ` U ) ) -> T e. ( SubGrp ` G ) )
4 subgsubm 
 |-  ( T e. ( SubGrp ` G ) -> T e. ( SubMnd ` G ) )
5 3 4 syl 
 |-  ( ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) /\ T C_ ( Z ` U ) ) -> T e. ( SubMnd ` G ) )
6 simp2 
 |-  ( ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) /\ T C_ ( Z ` U ) ) -> U e. ( SubGrp ` G ) )
7 subgsubm 
 |-  ( U e. ( SubGrp ` G ) -> U e. ( SubMnd ` G ) )
8 6 7 syl 
 |-  ( ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) /\ T C_ ( Z ` U ) ) -> U e. ( SubMnd ` G ) )
9 simp3 
 |-  ( ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) /\ T C_ ( Z ` U ) ) -> T C_ ( Z ` U ) )
10 1 2 lsmsubm 
 |-  ( ( T e. ( SubMnd ` G ) /\ U e. ( SubMnd ` G ) /\ T C_ ( Z ` U ) ) -> ( T .(+) U ) e. ( SubMnd ` G ) )
11 5 8 9 10 syl3anc 
 |-  ( ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) /\ T C_ ( Z ` U ) ) -> ( T .(+) U ) e. ( SubMnd ` G ) )
12 eqid 
 |-  ( +g ` G ) = ( +g ` G )
13 12 1 lsmelval 
 |-  ( ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) -> ( x e. ( T .(+) U ) <-> E. a e. T E. b e. U x = ( a ( +g ` G ) b ) ) )
14 13 3adant3 
 |-  ( ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) /\ T C_ ( Z ` U ) ) -> ( x e. ( T .(+) U ) <-> E. a e. T E. b e. U x = ( a ( +g ` G ) b ) ) )
15 3 adantr 
 |-  ( ( ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) /\ T C_ ( Z ` U ) ) /\ ( a e. T /\ b e. U ) ) -> T e. ( SubGrp ` G ) )
16 subgrcl 
 |-  ( T e. ( SubGrp ` G ) -> G e. Grp )
17 15 16 syl 
 |-  ( ( ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) /\ T C_ ( Z ` U ) ) /\ ( a e. T /\ b e. U ) ) -> G e. Grp )
18 eqid 
 |-  ( Base ` G ) = ( Base ` G )
19 18 subgss 
 |-  ( T e. ( SubGrp ` G ) -> T C_ ( Base ` G ) )
20 15 19 syl 
 |-  ( ( ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) /\ T C_ ( Z ` U ) ) /\ ( a e. T /\ b e. U ) ) -> T C_ ( Base ` G ) )
21 simprl 
 |-  ( ( ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) /\ T C_ ( Z ` U ) ) /\ ( a e. T /\ b e. U ) ) -> a e. T )
22 20 21 sseldd 
 |-  ( ( ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) /\ T C_ ( Z ` U ) ) /\ ( a e. T /\ b e. U ) ) -> a e. ( Base ` G ) )
23 6 adantr 
 |-  ( ( ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) /\ T C_ ( Z ` U ) ) /\ ( a e. T /\ b e. U ) ) -> U e. ( SubGrp ` G ) )
24 18 subgss 
 |-  ( U e. ( SubGrp ` G ) -> U C_ ( Base ` G ) )
25 23 24 syl 
 |-  ( ( ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) /\ T C_ ( Z ` U ) ) /\ ( a e. T /\ b e. U ) ) -> U C_ ( Base ` G ) )
26 simprr 
 |-  ( ( ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) /\ T C_ ( Z ` U ) ) /\ ( a e. T /\ b e. U ) ) -> b e. U )
27 25 26 sseldd 
 |-  ( ( ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) /\ T C_ ( Z ` U ) ) /\ ( a e. T /\ b e. U ) ) -> b e. ( Base ` G ) )
28 eqid 
 |-  ( invg ` G ) = ( invg ` G )
29 18 12 28 grpinvadd 
 |-  ( ( G e. Grp /\ a e. ( Base ` G ) /\ b e. ( Base ` G ) ) -> ( ( invg ` G ) ` ( a ( +g ` G ) b ) ) = ( ( ( invg ` G ) ` b ) ( +g ` G ) ( ( invg ` G ) ` a ) ) )
30 17 22 27 29 syl3anc 
 |-  ( ( ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) /\ T C_ ( Z ` U ) ) /\ ( a e. T /\ b e. U ) ) -> ( ( invg ` G ) ` ( a ( +g ` G ) b ) ) = ( ( ( invg ` G ) ` b ) ( +g ` G ) ( ( invg ` G ) ` a ) ) )
31 9 adantr 
 |-  ( ( ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) /\ T C_ ( Z ` U ) ) /\ ( a e. T /\ b e. U ) ) -> T C_ ( Z ` U ) )
32 28 subginvcl 
 |-  ( ( T e. ( SubGrp ` G ) /\ a e. T ) -> ( ( invg ` G ) ` a ) e. T )
33 15 21 32 syl2anc 
 |-  ( ( ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) /\ T C_ ( Z ` U ) ) /\ ( a e. T /\ b e. U ) ) -> ( ( invg ` G ) ` a ) e. T )
34 31 33 sseldd 
 |-  ( ( ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) /\ T C_ ( Z ` U ) ) /\ ( a e. T /\ b e. U ) ) -> ( ( invg ` G ) ` a ) e. ( Z ` U ) )
35 28 subginvcl 
 |-  ( ( U e. ( SubGrp ` G ) /\ b e. U ) -> ( ( invg ` G ) ` b ) e. U )
36 23 26 35 syl2anc 
 |-  ( ( ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) /\ T C_ ( Z ` U ) ) /\ ( a e. T /\ b e. U ) ) -> ( ( invg ` G ) ` b ) e. U )
37 12 2 cntzi 
 |-  ( ( ( ( invg ` G ) ` a ) e. ( Z ` U ) /\ ( ( invg ` G ) ` b ) e. U ) -> ( ( ( invg ` G ) ` a ) ( +g ` G ) ( ( invg ` G ) ` b ) ) = ( ( ( invg ` G ) ` b ) ( +g ` G ) ( ( invg ` G ) ` a ) ) )
38 34 36 37 syl2anc 
 |-  ( ( ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) /\ T C_ ( Z ` U ) ) /\ ( a e. T /\ b e. U ) ) -> ( ( ( invg ` G ) ` a ) ( +g ` G ) ( ( invg ` G ) ` b ) ) = ( ( ( invg ` G ) ` b ) ( +g ` G ) ( ( invg ` G ) ` a ) ) )
39 30 38 eqtr4d 
 |-  ( ( ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) /\ T C_ ( Z ` U ) ) /\ ( a e. T /\ b e. U ) ) -> ( ( invg ` G ) ` ( a ( +g ` G ) b ) ) = ( ( ( invg ` G ) ` a ) ( +g ` G ) ( ( invg ` G ) ` b ) ) )
40 12 1 lsmelvali 
 |-  ( ( ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) /\ ( ( ( invg ` G ) ` a ) e. T /\ ( ( invg ` G ) ` b ) e. U ) ) -> ( ( ( invg ` G ) ` a ) ( +g ` G ) ( ( invg ` G ) ` b ) ) e. ( T .(+) U ) )
41 15 23 33 36 40 syl22anc 
 |-  ( ( ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) /\ T C_ ( Z ` U ) ) /\ ( a e. T /\ b e. U ) ) -> ( ( ( invg ` G ) ` a ) ( +g ` G ) ( ( invg ` G ) ` b ) ) e. ( T .(+) U ) )
42 39 41 eqeltrd 
 |-  ( ( ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) /\ T C_ ( Z ` U ) ) /\ ( a e. T /\ b e. U ) ) -> ( ( invg ` G ) ` ( a ( +g ` G ) b ) ) e. ( T .(+) U ) )
43 fveq2 
 |-  ( x = ( a ( +g ` G ) b ) -> ( ( invg ` G ) ` x ) = ( ( invg ` G ) ` ( a ( +g ` G ) b ) ) )
44 43 eleq1d 
 |-  ( x = ( a ( +g ` G ) b ) -> ( ( ( invg ` G ) ` x ) e. ( T .(+) U ) <-> ( ( invg ` G ) ` ( a ( +g ` G ) b ) ) e. ( T .(+) U ) ) )
45 42 44 syl5ibrcom 
 |-  ( ( ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) /\ T C_ ( Z ` U ) ) /\ ( a e. T /\ b e. U ) ) -> ( x = ( a ( +g ` G ) b ) -> ( ( invg ` G ) ` x ) e. ( T .(+) U ) ) )
46 45 rexlimdvva 
 |-  ( ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) /\ T C_ ( Z ` U ) ) -> ( E. a e. T E. b e. U x = ( a ( +g ` G ) b ) -> ( ( invg ` G ) ` x ) e. ( T .(+) U ) ) )
47 14 46 sylbid 
 |-  ( ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) /\ T C_ ( Z ` U ) ) -> ( x e. ( T .(+) U ) -> ( ( invg ` G ) ` x ) e. ( T .(+) U ) ) )
48 47 ralrimiv 
 |-  ( ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) /\ T C_ ( Z ` U ) ) -> A. x e. ( T .(+) U ) ( ( invg ` G ) ` x ) e. ( T .(+) U ) )
49 3 16 syl 
 |-  ( ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) /\ T C_ ( Z ` U ) ) -> G e. Grp )
50 28 issubg3 
 |-  ( G e. Grp -> ( ( T .(+) U ) e. ( SubGrp ` G ) <-> ( ( T .(+) U ) e. ( SubMnd ` G ) /\ A. x e. ( T .(+) U ) ( ( invg ` G ) ` x ) e. ( T .(+) U ) ) ) )
51 49 50 syl 
 |-  ( ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) /\ T C_ ( Z ` U ) ) -> ( ( T .(+) U ) e. ( SubGrp ` G ) <-> ( ( T .(+) U ) e. ( SubMnd ` G ) /\ A. x e. ( T .(+) U ) ( ( invg ` G ) ` x ) e. ( T .(+) U ) ) ) )
52 11 48 51 mpbir2and 
 |-  ( ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) /\ T C_ ( Z ` U ) ) -> ( T .(+) U ) e. ( SubGrp ` G ) )