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 = Base G
issubmnd.p + ˙ = + G
issubmnd.z 0 ˙ = 0 G
issubmnd.h H = G 𝑠 S
Assertion issubmnd G Mnd S B 0 ˙ S H Mnd x S y S x + ˙ y S

Proof

Step Hyp Ref Expression
1 issubmnd.b B = Base G
2 issubmnd.p + ˙ = + G
3 issubmnd.z 0 ˙ = 0 G
4 issubmnd.h H = G 𝑠 S
5 simplr G Mnd S B 0 ˙ S H Mnd x S y S H Mnd
6 simprl G Mnd S B 0 ˙ S H Mnd x S y S x S
7 simpll2 G Mnd S B 0 ˙ S H Mnd x S y S S B
8 4 1 ressbas2 S B S = Base H
9 7 8 syl G Mnd S B 0 ˙ S H Mnd x S y S S = Base H
10 6 9 eleqtrd G Mnd S B 0 ˙ S H Mnd x S y S x Base H
11 simprr G Mnd S B 0 ˙ S H Mnd x S y S y S
12 11 9 eleqtrd G Mnd S B 0 ˙ S H Mnd x S y S y Base H
13 eqid Base H = Base H
14 eqid + H = + H
15 13 14 mndcl H Mnd x Base H y Base H x + H y Base H
16 5 10 12 15 syl3anc G Mnd S B 0 ˙ S H Mnd x S y S x + H y Base H
17 1 fvexi B V
18 17 ssex S B S V
19 18 3ad2ant2 G Mnd S B 0 ˙ S S V
20 4 2 ressplusg S V + ˙ = + H
21 19 20 syl G Mnd S B 0 ˙ S + ˙ = + H
22 21 ad2antrr G Mnd S B 0 ˙ S H Mnd x S y S + ˙ = + H
23 22 oveqd G Mnd S B 0 ˙ S H Mnd x S y S x + ˙ y = x + H y
24 16 23 9 3eltr4d G Mnd S B 0 ˙ S H Mnd x S y S x + ˙ y S
25 24 ralrimivva G Mnd S B 0 ˙ S H Mnd x S y S x + ˙ y S
26 simpl2 G Mnd S B 0 ˙ S x S y S x + ˙ y S S B
27 26 8 syl G Mnd S B 0 ˙ S x S y S x + ˙ y S S = Base H
28 21 adantr G Mnd S B 0 ˙ S x S y S x + ˙ y S + ˙ = + H
29 ovrspc2v u S v S x S y S x + ˙ y S u + ˙ v S
30 29 ancoms x S y S x + ˙ y S u S v S u + ˙ v S
31 30 3impb x S y S x + ˙ y S u S v S u + ˙ v S
32 31 3adant1l G Mnd S B 0 ˙ S x S y S x + ˙ y S u S v S u + ˙ v S
33 simpl1 G Mnd S B 0 ˙ S x S y S x + ˙ y S G Mnd
34 26 sseld G Mnd S B 0 ˙ S x S y S x + ˙ y S u S u B
35 26 sseld G Mnd S B 0 ˙ S x S y S x + ˙ y S v S v B
36 26 sseld G Mnd S B 0 ˙ S x S y S x + ˙ y S w S w B
37 34 35 36 3anim123d G Mnd S B 0 ˙ S x S y S x + ˙ y S u S v S w S u B v B w B
38 37 imp G Mnd S B 0 ˙ S x S y S x + ˙ y S u S v S w S u B v B w B
39 1 2 mndass G Mnd u B v B w B u + ˙ v + ˙ w = u + ˙ v + ˙ w
40 33 38 39 syl2an2r G Mnd S B 0 ˙ S x S y S x + ˙ y S u S v S w S u + ˙ v + ˙ w = u + ˙ v + ˙ w
41 simpl3 G Mnd S B 0 ˙ S x S y S x + ˙ y S 0 ˙ S
42 26 sselda G Mnd S B 0 ˙ S x S y S x + ˙ y S u S u B
43 1 2 3 mndlid G Mnd u B 0 ˙ + ˙ u = u
44 33 42 43 syl2an2r G Mnd S B 0 ˙ S x S y S x + ˙ y S u S 0 ˙ + ˙ u = u
45 1 2 3 mndrid G Mnd u B u + ˙ 0 ˙ = u
46 33 42 45 syl2an2r G Mnd S B 0 ˙ S x S y S x + ˙ y S u S u + ˙ 0 ˙ = u
47 27 28 32 40 41 44 46 ismndd G Mnd S B 0 ˙ S x S y S x + ˙ y S H Mnd
48 25 47 impbida G Mnd S B 0 ˙ S H Mnd x S y S x + ˙ y S