Metamath Proof Explorer


Theorem issubmnd

Description: Characterize a submonoid by closure properties. (Contributed by Mario Carneiro, 10-Jan-2015)

Ref Expression
Hypotheses issubmnd.b B=BaseG
issubmnd.p +˙=+G
issubmnd.z 0˙=0G
issubmnd.h H=G𝑠S
Assertion issubmnd GMndSB0˙SHMndxSySx+˙yS

Proof

Step Hyp Ref Expression
1 issubmnd.b B=BaseG
2 issubmnd.p +˙=+G
3 issubmnd.z 0˙=0G
4 issubmnd.h H=G𝑠S
5 simplr GMndSB0˙SHMndxSySHMnd
6 simprl GMndSB0˙SHMndxSySxS
7 simpll2 GMndSB0˙SHMndxSySSB
8 4 1 ressbas2 SBS=BaseH
9 7 8 syl GMndSB0˙SHMndxSySS=BaseH
10 6 9 eleqtrd GMndSB0˙SHMndxSySxBaseH
11 simprr GMndSB0˙SHMndxSySyS
12 11 9 eleqtrd GMndSB0˙SHMndxSySyBaseH
13 eqid BaseH=BaseH
14 eqid +H=+H
15 13 14 mndcl HMndxBaseHyBaseHx+HyBaseH
16 5 10 12 15 syl3anc GMndSB0˙SHMndxSySx+HyBaseH
17 1 fvexi BV
18 17 ssex SBSV
19 18 3ad2ant2 GMndSB0˙SSV
20 4 2 ressplusg SV+˙=+H
21 19 20 syl GMndSB0˙S+˙=+H
22 21 ad2antrr GMndSB0˙SHMndxSyS+˙=+H
23 22 oveqd GMndSB0˙SHMndxSySx+˙y=x+Hy
24 16 23 9 3eltr4d GMndSB0˙SHMndxSySx+˙yS
25 24 ralrimivva GMndSB0˙SHMndxSySx+˙yS
26 simpl2 GMndSB0˙SxSySx+˙ySSB
27 26 8 syl GMndSB0˙SxSySx+˙ySS=BaseH
28 21 adantr GMndSB0˙SxSySx+˙yS+˙=+H
29 ovrspc2v uSvSxSySx+˙ySu+˙vS
30 29 ancoms xSySx+˙ySuSvSu+˙vS
31 30 3impb xSySx+˙ySuSvSu+˙vS
32 31 3adant1l GMndSB0˙SxSySx+˙ySuSvSu+˙vS
33 simpl1 GMndSB0˙SxSySx+˙ySGMnd
34 26 sseld GMndSB0˙SxSySx+˙ySuSuB
35 26 sseld GMndSB0˙SxSySx+˙ySvSvB
36 26 sseld GMndSB0˙SxSySx+˙ySwSwB
37 34 35 36 3anim123d GMndSB0˙SxSySx+˙ySuSvSwSuBvBwB
38 37 imp GMndSB0˙SxSySx+˙ySuSvSwSuBvBwB
39 1 2 mndass GMnduBvBwBu+˙v+˙w=u+˙v+˙w
40 33 38 39 syl2an2r GMndSB0˙SxSySx+˙ySuSvSwSu+˙v+˙w=u+˙v+˙w
41 simpl3 GMndSB0˙SxSySx+˙yS0˙S
42 26 sselda GMndSB0˙SxSySx+˙ySuSuB
43 1 2 3 mndlid GMnduB0˙+˙u=u
44 33 42 43 syl2an2r GMndSB0˙SxSySx+˙ySuS0˙+˙u=u
45 1 2 3 mndrid GMnduBu+˙0˙=u
46 33 42 45 syl2an2r GMndSB0˙SxSySx+˙ySuSu+˙0˙=u
47 27 28 32 40 41 44 46 ismndd GMndSB0˙SxSySx+˙ySHMnd
48 25 47 impbida GMndSB0˙SHMndxSySx+˙yS