Metamath Proof Explorer

Theorem lsmsubm

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

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

Proof

Step Hyp Ref Expression
1 lsmsubg.p 
 |-  .(+) = ( LSSum ` G )
2 lsmsubg.z 
 |-  Z = ( Cntz ` G )
3 submrcl 
 |-  ( T e. ( SubMnd ` G ) -> G e. Mnd )
4 3 3ad2ant1 
 |-  ( ( T e. ( SubMnd ` G ) /\ U e. ( SubMnd ` G ) /\ T C_ ( Z ` U ) ) -> G e. Mnd )
5 eqid 
 |-  ( Base ` G ) = ( Base ` G )
6 5 submss 
 |-  ( T e. ( SubMnd ` G ) -> T C_ ( Base ` G ) )
7 6 3ad2ant1 
 |-  ( ( T e. ( SubMnd ` G ) /\ U e. ( SubMnd ` G ) /\ T C_ ( Z ` U ) ) -> T C_ ( Base ` G ) )
8 5 submss 
 |-  ( U e. ( SubMnd ` G ) -> U C_ ( Base ` G ) )
9 8 3ad2ant2 
 |-  ( ( T e. ( SubMnd ` G ) /\ U e. ( SubMnd ` G ) /\ T C_ ( Z ` U ) ) -> U C_ ( Base ` G ) )
10 5 1 lsmssv 
 |-  ( ( G e. Mnd /\ T C_ ( Base ` G ) /\ U C_ ( Base ` G ) ) -> ( T .(+) U ) C_ ( Base ` G ) )
11 4 7 9 10 syl3anc 
 |-  ( ( T e. ( SubMnd ` G ) /\ U e. ( SubMnd ` G ) /\ T C_ ( Z ` U ) ) -> ( T .(+) U ) C_ ( Base ` G ) )
12 simp2 
 |-  ( ( T e. ( SubMnd ` G ) /\ U e. ( SubMnd ` G ) /\ T C_ ( Z ` U ) ) -> U e. ( SubMnd ` G ) )
13 5 1 lsmub1x 
 |-  ( ( T C_ ( Base ` G ) /\ U e. ( SubMnd ` G ) ) -> T C_ ( T .(+) U ) )
14 7 12 13 syl2anc 
 |-  ( ( T e. ( SubMnd ` G ) /\ U e. ( SubMnd ` G ) /\ T C_ ( Z ` U ) ) -> T C_ ( T .(+) U ) )
15 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
16 15 subm0cl 
 |-  ( T e. ( SubMnd ` G ) -> ( 0g ` G ) e. T )
17 16 3ad2ant1 
 |-  ( ( T e. ( SubMnd ` G ) /\ U e. ( SubMnd ` G ) /\ T C_ ( Z ` U ) ) -> ( 0g ` G ) e. T )
18 14 17 sseldd 
 |-  ( ( T e. ( SubMnd ` G ) /\ U e. ( SubMnd ` G ) /\ T C_ ( Z ` U ) ) -> ( 0g ` G ) e. ( T .(+) U ) )
19 eqid 
 |-  ( +g ` G ) = ( +g ` G )
20 5 19 1 lsmelvalx 
 |-  ( ( G e. Mnd /\ T C_ ( Base ` G ) /\ U C_ ( Base ` G ) ) -> ( x e. ( T .(+) U ) <-> E. a e. T E. c e. U x = ( a ( +g ` G ) c ) ) )
21 4 7 9 20 syl3anc 
 |-  ( ( T e. ( SubMnd ` G ) /\ U e. ( SubMnd ` G ) /\ T C_ ( Z ` U ) ) -> ( x e. ( T .(+) U ) <-> E. a e. T E. c e. U x = ( a ( +g ` G ) c ) ) )
22 5 19 1 lsmelvalx 
 |-  ( ( G e. Mnd /\ T C_ ( Base ` G ) /\ U C_ ( Base ` G ) ) -> ( y e. ( T .(+) U ) <-> E. b e. T E. d e. U y = ( b ( +g ` G ) d ) ) )
23 4 7 9 22 syl3anc 
 |-  ( ( T e. ( SubMnd ` G ) /\ U e. ( SubMnd ` G ) /\ T C_ ( Z ` U ) ) -> ( y e. ( T .(+) U ) <-> E. b e. T E. d e. U y = ( b ( +g ` G ) d ) ) )
24 21 23 anbi12d 
 |-  ( ( T e. ( SubMnd ` G ) /\ U e. ( SubMnd ` G ) /\ T C_ ( Z ` U ) ) -> ( ( x e. ( T .(+) U ) /\ y e. ( T .(+) U ) ) <-> ( E. a e. T E. c e. U x = ( a ( +g ` G ) c ) /\ E. b e. T E. d e. U y = ( b ( +g ` G ) d ) ) ) )
25 reeanv 
 |-  ( E. a e. T E. b e. T ( E. c e. U x = ( a ( +g ` G ) c ) /\ E. d e. U y = ( b ( +g ` G ) d ) ) <-> ( E. a e. T E. c e. U x = ( a ( +g ` G ) c ) /\ E. b e. T E. d e. U y = ( b ( +g ` G ) d ) ) )
26 reeanv 
 |-  ( E. c e. U E. d e. U ( x = ( a ( +g ` G ) c ) /\ y = ( b ( +g ` G ) d ) ) <-> ( E. c e. U x = ( a ( +g ` G ) c ) /\ E. d e. U y = ( b ( +g ` G ) d ) ) )
27 4 adantr 
 |-  ( ( ( T e. ( SubMnd ` G ) /\ U e. ( SubMnd ` G ) /\ T C_ ( Z ` U ) ) /\ ( ( a e. T /\ b e. T ) /\ ( c e. U /\ d e. U ) ) ) -> G e. Mnd )
28 7 adantr 
 |-  ( ( ( T e. ( SubMnd ` G ) /\ U e. ( SubMnd ` G ) /\ T C_ ( Z ` U ) ) /\ ( ( a e. T /\ b e. T ) /\ ( c e. U /\ d e. U ) ) ) -> T C_ ( Base ` G ) )
29 simprll 
 |-  ( ( ( T e. ( SubMnd ` G ) /\ U e. ( SubMnd ` G ) /\ T C_ ( Z ` U ) ) /\ ( ( a e. T /\ b e. T ) /\ ( c e. U /\ d e. U ) ) ) -> a e. T )
30 28 29 sseldd 
 |-  ( ( ( T e. ( SubMnd ` G ) /\ U e. ( SubMnd ` G ) /\ T C_ ( Z ` U ) ) /\ ( ( a e. T /\ b e. T ) /\ ( c e. U /\ d e. U ) ) ) -> a e. ( Base ` G ) )
31 simprlr 
 |-  ( ( ( T e. ( SubMnd ` G ) /\ U e. ( SubMnd ` G ) /\ T C_ ( Z ` U ) ) /\ ( ( a e. T /\ b e. T ) /\ ( c e. U /\ d e. U ) ) ) -> b e. T )
32 28 31 sseldd 
 |-  ( ( ( T e. ( SubMnd ` G ) /\ U e. ( SubMnd ` G ) /\ T C_ ( Z ` U ) ) /\ ( ( a e. T /\ b e. T ) /\ ( c e. U /\ d e. U ) ) ) -> b e. ( Base ` G ) )
33 9 adantr 
 |-  ( ( ( T e. ( SubMnd ` G ) /\ U e. ( SubMnd ` G ) /\ T C_ ( Z ` U ) ) /\ ( ( a e. T /\ b e. T ) /\ ( c e. U /\ d e. U ) ) ) -> U C_ ( Base ` G ) )
34 simprrl 
 |-  ( ( ( T e. ( SubMnd ` G ) /\ U e. ( SubMnd ` G ) /\ T C_ ( Z ` U ) ) /\ ( ( a e. T /\ b e. T ) /\ ( c e. U /\ d e. U ) ) ) -> c e. U )
35 33 34 sseldd 
 |-  ( ( ( T e. ( SubMnd ` G ) /\ U e. ( SubMnd ` G ) /\ T C_ ( Z ` U ) ) /\ ( ( a e. T /\ b e. T ) /\ ( c e. U /\ d e. U ) ) ) -> c e. ( Base ` G ) )
36 simprrr 
 |-  ( ( ( T e. ( SubMnd ` G ) /\ U e. ( SubMnd ` G ) /\ T C_ ( Z ` U ) ) /\ ( ( a e. T /\ b e. T ) /\ ( c e. U /\ d e. U ) ) ) -> d e. U )
37 33 36 sseldd 
 |-  ( ( ( T e. ( SubMnd ` G ) /\ U e. ( SubMnd ` G ) /\ T C_ ( Z ` U ) ) /\ ( ( a e. T /\ b e. T ) /\ ( c e. U /\ d e. U ) ) ) -> d e. ( Base ` G ) )
38 simpl3 
 |-  ( ( ( T e. ( SubMnd ` G ) /\ U e. ( SubMnd ` G ) /\ T C_ ( Z ` U ) ) /\ ( ( a e. T /\ b e. T ) /\ ( c e. U /\ d e. U ) ) ) -> T C_ ( Z ` U ) )
39 38 31 sseldd 
 |-  ( ( ( T e. ( SubMnd ` G ) /\ U e. ( SubMnd ` G ) /\ T C_ ( Z ` U ) ) /\ ( ( a e. T /\ b e. T ) /\ ( c e. U /\ d e. U ) ) ) -> b e. ( Z ` U ) )
40 19 2 cntzi 
 |-  ( ( b e. ( Z ` U ) /\ c e. U ) -> ( b ( +g ` G ) c ) = ( c ( +g ` G ) b ) )
41 39 34 40 syl2anc 
 |-  ( ( ( T e. ( SubMnd ` G ) /\ U e. ( SubMnd ` G ) /\ T C_ ( Z ` U ) ) /\ ( ( a e. T /\ b e. T ) /\ ( c e. U /\ d e. U ) ) ) -> ( b ( +g ` G ) c ) = ( c ( +g ` G ) b ) )
42 5 19 27 30 32 35 37 41 mnd4g 
 |-  ( ( ( T e. ( SubMnd ` G ) /\ U e. ( SubMnd ` G ) /\ T C_ ( Z ` U ) ) /\ ( ( a e. T /\ b e. T ) /\ ( c e. U /\ d e. U ) ) ) -> ( ( a ( +g ` G ) b ) ( +g ` G ) ( c ( +g ` G ) d ) ) = ( ( a ( +g ` G ) c ) ( +g ` G ) ( b ( +g ` G ) d ) ) )
43 simpl1 
 |-  ( ( ( T e. ( SubMnd ` G ) /\ U e. ( SubMnd ` G ) /\ T C_ ( Z ` U ) ) /\ ( ( a e. T /\ b e. T ) /\ ( c e. U /\ d e. U ) ) ) -> T e. ( SubMnd ` G ) )
44 19 submcl 
 |-  ( ( T e. ( SubMnd ` G ) /\ a e. T /\ b e. T ) -> ( a ( +g ` G ) b ) e. T )
45 43 29 31 44 syl3anc 
 |-  ( ( ( T e. ( SubMnd ` G ) /\ U e. ( SubMnd ` G ) /\ T C_ ( Z ` U ) ) /\ ( ( a e. T /\ b e. T ) /\ ( c e. U /\ d e. U ) ) ) -> ( a ( +g ` G ) b ) e. T )
46 simpl2 
 |-  ( ( ( T e. ( SubMnd ` G ) /\ U e. ( SubMnd ` G ) /\ T C_ ( Z ` U ) ) /\ ( ( a e. T /\ b e. T ) /\ ( c e. U /\ d e. U ) ) ) -> U e. ( SubMnd ` G ) )
47 19 submcl 
 |-  ( ( U e. ( SubMnd ` G ) /\ c e. U /\ d e. U ) -> ( c ( +g ` G ) d ) e. U )
48 46 34 36 47 syl3anc 
 |-  ( ( ( T e. ( SubMnd ` G ) /\ U e. ( SubMnd ` G ) /\ T C_ ( Z ` U ) ) /\ ( ( a e. T /\ b e. T ) /\ ( c e. U /\ d e. U ) ) ) -> ( c ( +g ` G ) d ) e. U )
49 5 19 1 lsmelvalix 
 |-  ( ( ( G e. Mnd /\ T C_ ( Base ` G ) /\ U C_ ( Base ` G ) ) /\ ( ( a ( +g ` G ) b ) e. T /\ ( c ( +g ` G ) d ) e. U ) ) -> ( ( a ( +g ` G ) b ) ( +g ` G ) ( c ( +g ` G ) d ) ) e. ( T .(+) U ) )
50 27 28 33 45 48 49 syl32anc 
 |-  ( ( ( T e. ( SubMnd ` G ) /\ U e. ( SubMnd ` G ) /\ T C_ ( Z ` U ) ) /\ ( ( a e. T /\ b e. T ) /\ ( c e. U /\ d e. U ) ) ) -> ( ( a ( +g ` G ) b ) ( +g ` G ) ( c ( +g ` G ) d ) ) e. ( T .(+) U ) )
51 42 50 eqeltrrd 
 |-  ( ( ( T e. ( SubMnd ` G ) /\ U e. ( SubMnd ` G ) /\ T C_ ( Z ` U ) ) /\ ( ( a e. T /\ b e. T ) /\ ( c e. U /\ d e. U ) ) ) -> ( ( a ( +g ` G ) c ) ( +g ` G ) ( b ( +g ` G ) d ) ) e. ( T .(+) U ) )
52 oveq12 
 |-  ( ( x = ( a ( +g ` G ) c ) /\ y = ( b ( +g ` G ) d ) ) -> ( x ( +g ` G ) y ) = ( ( a ( +g ` G ) c ) ( +g ` G ) ( b ( +g ` G ) d ) ) )
53 52 eleq1d 
 |-  ( ( x = ( a ( +g ` G ) c ) /\ y = ( b ( +g ` G ) d ) ) -> ( ( x ( +g ` G ) y ) e. ( T .(+) U ) <-> ( ( a ( +g ` G ) c ) ( +g ` G ) ( b ( +g ` G ) d ) ) e. ( T .(+) U ) ) )
54 51 53 syl5ibrcom 
 |-  ( ( ( T e. ( SubMnd ` G ) /\ U e. ( SubMnd ` G ) /\ T C_ ( Z ` U ) ) /\ ( ( a e. T /\ b e. T ) /\ ( c e. U /\ d e. U ) ) ) -> ( ( x = ( a ( +g ` G ) c ) /\ y = ( b ( +g ` G ) d ) ) -> ( x ( +g ` G ) y ) e. ( T .(+) U ) ) )
55 54 anassrs 
 |-  ( ( ( ( T e. ( SubMnd ` G ) /\ U e. ( SubMnd ` G ) /\ T C_ ( Z ` U ) ) /\ ( a e. T /\ b e. T ) ) /\ ( c e. U /\ d e. U ) ) -> ( ( x = ( a ( +g ` G ) c ) /\ y = ( b ( +g ` G ) d ) ) -> ( x ( +g ` G ) y ) e. ( T .(+) U ) ) )
56 55 rexlimdvva 
 |-  ( ( ( T e. ( SubMnd ` G ) /\ U e. ( SubMnd ` G ) /\ T C_ ( Z ` U ) ) /\ ( a e. T /\ b e. T ) ) -> ( E. c e. U E. d e. U ( x = ( a ( +g ` G ) c ) /\ y = ( b ( +g ` G ) d ) ) -> ( x ( +g ` G ) y ) e. ( T .(+) U ) ) )
57 26 56 syl5bir 
 |-  ( ( ( T e. ( SubMnd ` G ) /\ U e. ( SubMnd ` G ) /\ T C_ ( Z ` U ) ) /\ ( a e. T /\ b e. T ) ) -> ( ( E. c e. U x = ( a ( +g ` G ) c ) /\ E. d e. U y = ( b ( +g ` G ) d ) ) -> ( x ( +g ` G ) y ) e. ( T .(+) U ) ) )
58 57 rexlimdvva 
 |-  ( ( T e. ( SubMnd ` G ) /\ U e. ( SubMnd ` G ) /\ T C_ ( Z ` U ) ) -> ( E. a e. T E. b e. T ( E. c e. U x = ( a ( +g ` G ) c ) /\ E. d e. U y = ( b ( +g ` G ) d ) ) -> ( x ( +g ` G ) y ) e. ( T .(+) U ) ) )
59 25 58 syl5bir 
 |-  ( ( T e. ( SubMnd ` G ) /\ U e. ( SubMnd ` G ) /\ T C_ ( Z ` U ) ) -> ( ( E. a e. T E. c e. U x = ( a ( +g ` G ) c ) /\ E. b e. T E. d e. U y = ( b ( +g ` G ) d ) ) -> ( x ( +g ` G ) y ) e. ( T .(+) U ) ) )
60 24 59 sylbid 
 |-  ( ( T e. ( SubMnd ` G ) /\ U e. ( SubMnd ` G ) /\ T C_ ( Z ` U ) ) -> ( ( x e. ( T .(+) U ) /\ y e. ( T .(+) U ) ) -> ( x ( +g ` G ) y ) e. ( T .(+) U ) ) )
61 60 ralrimivv 
 |-  ( ( T e. ( SubMnd ` G ) /\ U e. ( SubMnd ` G ) /\ T C_ ( Z ` U ) ) -> A. x e. ( T .(+) U ) A. y e. ( T .(+) U ) ( x ( +g ` G ) y ) e. ( T .(+) U ) )
62 5 15 19 issubm 
 |-  ( G e. Mnd -> ( ( T .(+) U ) e. ( SubMnd ` G ) <-> ( ( T .(+) U ) C_ ( Base ` G ) /\ ( 0g ` G ) e. ( T .(+) U ) /\ A. x e. ( T .(+) U ) A. y e. ( T .(+) U ) ( x ( +g ` G ) y ) e. ( T .(+) U ) ) ) )
63 4 62 syl 
 |-  ( ( T e. ( SubMnd ` G ) /\ U e. ( SubMnd ` G ) /\ T C_ ( Z ` U ) ) -> ( ( T .(+) U ) e. ( SubMnd ` G ) <-> ( ( T .(+) U ) C_ ( Base ` G ) /\ ( 0g ` G ) e. ( T .(+) U ) /\ A. x e. ( T .(+) U ) A. y e. ( T .(+) U ) ( x ( +g ` G ) y ) e. ( T .(+) U ) ) ) )
64 11 18 61 63 mpbir3and 
 |-  ( ( T e. ( SubMnd ` G ) /\ U e. ( SubMnd ` G ) /\ T C_ ( Z ` U ) ) -> ( T .(+) U ) e. ( SubMnd ` G ) )