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