Metamath Proof Explorer


Theorem issubmnd

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

Ref Expression
Hypotheses issubmnd.b 𝐵 = ( Base ‘ 𝐺 )
issubmnd.p + = ( +g𝐺 )
issubmnd.z 0 = ( 0g𝐺 )
issubmnd.h 𝐻 = ( 𝐺s 𝑆 )
Assertion issubmnd ( ( 𝐺 ∈ Mnd ∧ 𝑆𝐵0𝑆 ) → ( 𝐻 ∈ Mnd ↔ ∀ 𝑥𝑆𝑦𝑆 ( 𝑥 + 𝑦 ) ∈ 𝑆 ) )

Proof

Step Hyp Ref Expression
1 issubmnd.b 𝐵 = ( Base ‘ 𝐺 )
2 issubmnd.p + = ( +g𝐺 )
3 issubmnd.z 0 = ( 0g𝐺 )
4 issubmnd.h 𝐻 = ( 𝐺s 𝑆 )
5 simplr ( ( ( ( 𝐺 ∈ Mnd ∧ 𝑆𝐵0𝑆 ) ∧ 𝐻 ∈ Mnd ) ∧ ( 𝑥𝑆𝑦𝑆 ) ) → 𝐻 ∈ Mnd )
6 simprl ( ( ( ( 𝐺 ∈ Mnd ∧ 𝑆𝐵0𝑆 ) ∧ 𝐻 ∈ Mnd ) ∧ ( 𝑥𝑆𝑦𝑆 ) ) → 𝑥𝑆 )
7 simpll2 ( ( ( ( 𝐺 ∈ Mnd ∧ 𝑆𝐵0𝑆 ) ∧ 𝐻 ∈ Mnd ) ∧ ( 𝑥𝑆𝑦𝑆 ) ) → 𝑆𝐵 )
8 4 1 ressbas2 ( 𝑆𝐵𝑆 = ( Base ‘ 𝐻 ) )
9 7 8 syl ( ( ( ( 𝐺 ∈ Mnd ∧ 𝑆𝐵0𝑆 ) ∧ 𝐻 ∈ Mnd ) ∧ ( 𝑥𝑆𝑦𝑆 ) ) → 𝑆 = ( Base ‘ 𝐻 ) )
10 6 9 eleqtrd ( ( ( ( 𝐺 ∈ Mnd ∧ 𝑆𝐵0𝑆 ) ∧ 𝐻 ∈ Mnd ) ∧ ( 𝑥𝑆𝑦𝑆 ) ) → 𝑥 ∈ ( Base ‘ 𝐻 ) )
11 simprr ( ( ( ( 𝐺 ∈ Mnd ∧ 𝑆𝐵0𝑆 ) ∧ 𝐻 ∈ Mnd ) ∧ ( 𝑥𝑆𝑦𝑆 ) ) → 𝑦𝑆 )
12 11 9 eleqtrd ( ( ( ( 𝐺 ∈ Mnd ∧ 𝑆𝐵0𝑆 ) ∧ 𝐻 ∈ Mnd ) ∧ ( 𝑥𝑆𝑦𝑆 ) ) → 𝑦 ∈ ( Base ‘ 𝐻 ) )
13 eqid ( Base ‘ 𝐻 ) = ( Base ‘ 𝐻 )
14 eqid ( +g𝐻 ) = ( +g𝐻 )
15 13 14 mndcl ( ( 𝐻 ∈ Mnd ∧ 𝑥 ∈ ( Base ‘ 𝐻 ) ∧ 𝑦 ∈ ( Base ‘ 𝐻 ) ) → ( 𝑥 ( +g𝐻 ) 𝑦 ) ∈ ( Base ‘ 𝐻 ) )
16 5 10 12 15 syl3anc ( ( ( ( 𝐺 ∈ Mnd ∧ 𝑆𝐵0𝑆 ) ∧ 𝐻 ∈ Mnd ) ∧ ( 𝑥𝑆𝑦𝑆 ) ) → ( 𝑥 ( +g𝐻 ) 𝑦 ) ∈ ( Base ‘ 𝐻 ) )
17 1 fvexi 𝐵 ∈ V
18 17 ssex ( 𝑆𝐵𝑆 ∈ V )
19 18 3ad2ant2 ( ( 𝐺 ∈ Mnd ∧ 𝑆𝐵0𝑆 ) → 𝑆 ∈ V )
20 4 2 ressplusg ( 𝑆 ∈ V → + = ( +g𝐻 ) )
21 19 20 syl ( ( 𝐺 ∈ Mnd ∧ 𝑆𝐵0𝑆 ) → + = ( +g𝐻 ) )
22 21 ad2antrr ( ( ( ( 𝐺 ∈ Mnd ∧ 𝑆𝐵0𝑆 ) ∧ 𝐻 ∈ Mnd ) ∧ ( 𝑥𝑆𝑦𝑆 ) ) → + = ( +g𝐻 ) )
23 22 oveqd ( ( ( ( 𝐺 ∈ Mnd ∧ 𝑆𝐵0𝑆 ) ∧ 𝐻 ∈ Mnd ) ∧ ( 𝑥𝑆𝑦𝑆 ) ) → ( 𝑥 + 𝑦 ) = ( 𝑥 ( +g𝐻 ) 𝑦 ) )
24 16 23 9 3eltr4d ( ( ( ( 𝐺 ∈ Mnd ∧ 𝑆𝐵0𝑆 ) ∧ 𝐻 ∈ Mnd ) ∧ ( 𝑥𝑆𝑦𝑆 ) ) → ( 𝑥 + 𝑦 ) ∈ 𝑆 )
25 24 ralrimivva ( ( ( 𝐺 ∈ Mnd ∧ 𝑆𝐵0𝑆 ) ∧ 𝐻 ∈ Mnd ) → ∀ 𝑥𝑆𝑦𝑆 ( 𝑥 + 𝑦 ) ∈ 𝑆 )
26 simpl2 ( ( ( 𝐺 ∈ Mnd ∧ 𝑆𝐵0𝑆 ) ∧ ∀ 𝑥𝑆𝑦𝑆 ( 𝑥 + 𝑦 ) ∈ 𝑆 ) → 𝑆𝐵 )
27 26 8 syl ( ( ( 𝐺 ∈ Mnd ∧ 𝑆𝐵0𝑆 ) ∧ ∀ 𝑥𝑆𝑦𝑆 ( 𝑥 + 𝑦 ) ∈ 𝑆 ) → 𝑆 = ( Base ‘ 𝐻 ) )
28 21 adantr ( ( ( 𝐺 ∈ Mnd ∧ 𝑆𝐵0𝑆 ) ∧ ∀ 𝑥𝑆𝑦𝑆 ( 𝑥 + 𝑦 ) ∈ 𝑆 ) → + = ( +g𝐻 ) )
29 ovrspc2v ( ( ( 𝑢𝑆𝑣𝑆 ) ∧ ∀ 𝑥𝑆𝑦𝑆 ( 𝑥 + 𝑦 ) ∈ 𝑆 ) → ( 𝑢 + 𝑣 ) ∈ 𝑆 )
30 29 ancoms ( ( ∀ 𝑥𝑆𝑦𝑆 ( 𝑥 + 𝑦 ) ∈ 𝑆 ∧ ( 𝑢𝑆𝑣𝑆 ) ) → ( 𝑢 + 𝑣 ) ∈ 𝑆 )
31 30 3impb ( ( ∀ 𝑥𝑆𝑦𝑆 ( 𝑥 + 𝑦 ) ∈ 𝑆𝑢𝑆𝑣𝑆 ) → ( 𝑢 + 𝑣 ) ∈ 𝑆 )
32 31 3adant1l ( ( ( ( 𝐺 ∈ Mnd ∧ 𝑆𝐵0𝑆 ) ∧ ∀ 𝑥𝑆𝑦𝑆 ( 𝑥 + 𝑦 ) ∈ 𝑆 ) ∧ 𝑢𝑆𝑣𝑆 ) → ( 𝑢 + 𝑣 ) ∈ 𝑆 )
33 simpl1 ( ( ( 𝐺 ∈ Mnd ∧ 𝑆𝐵0𝑆 ) ∧ ∀ 𝑥𝑆𝑦𝑆 ( 𝑥 + 𝑦 ) ∈ 𝑆 ) → 𝐺 ∈ Mnd )
34 26 sseld ( ( ( 𝐺 ∈ Mnd ∧ 𝑆𝐵0𝑆 ) ∧ ∀ 𝑥𝑆𝑦𝑆 ( 𝑥 + 𝑦 ) ∈ 𝑆 ) → ( 𝑢𝑆𝑢𝐵 ) )
35 26 sseld ( ( ( 𝐺 ∈ Mnd ∧ 𝑆𝐵0𝑆 ) ∧ ∀ 𝑥𝑆𝑦𝑆 ( 𝑥 + 𝑦 ) ∈ 𝑆 ) → ( 𝑣𝑆𝑣𝐵 ) )
36 26 sseld ( ( ( 𝐺 ∈ Mnd ∧ 𝑆𝐵0𝑆 ) ∧ ∀ 𝑥𝑆𝑦𝑆 ( 𝑥 + 𝑦 ) ∈ 𝑆 ) → ( 𝑤𝑆𝑤𝐵 ) )
37 34 35 36 3anim123d ( ( ( 𝐺 ∈ Mnd ∧ 𝑆𝐵0𝑆 ) ∧ ∀ 𝑥𝑆𝑦𝑆 ( 𝑥 + 𝑦 ) ∈ 𝑆 ) → ( ( 𝑢𝑆𝑣𝑆𝑤𝑆 ) → ( 𝑢𝐵𝑣𝐵𝑤𝐵 ) ) )
38 37 imp ( ( ( ( 𝐺 ∈ Mnd ∧ 𝑆𝐵0𝑆 ) ∧ ∀ 𝑥𝑆𝑦𝑆 ( 𝑥 + 𝑦 ) ∈ 𝑆 ) ∧ ( 𝑢𝑆𝑣𝑆𝑤𝑆 ) ) → ( 𝑢𝐵𝑣𝐵𝑤𝐵 ) )
39 1 2 mndass ( ( 𝐺 ∈ Mnd ∧ ( 𝑢𝐵𝑣𝐵𝑤𝐵 ) ) → ( ( 𝑢 + 𝑣 ) + 𝑤 ) = ( 𝑢 + ( 𝑣 + 𝑤 ) ) )
40 33 38 39 syl2an2r ( ( ( ( 𝐺 ∈ Mnd ∧ 𝑆𝐵0𝑆 ) ∧ ∀ 𝑥𝑆𝑦𝑆 ( 𝑥 + 𝑦 ) ∈ 𝑆 ) ∧ ( 𝑢𝑆𝑣𝑆𝑤𝑆 ) ) → ( ( 𝑢 + 𝑣 ) + 𝑤 ) = ( 𝑢 + ( 𝑣 + 𝑤 ) ) )
41 simpl3 ( ( ( 𝐺 ∈ Mnd ∧ 𝑆𝐵0𝑆 ) ∧ ∀ 𝑥𝑆𝑦𝑆 ( 𝑥 + 𝑦 ) ∈ 𝑆 ) → 0𝑆 )
42 26 sselda ( ( ( ( 𝐺 ∈ Mnd ∧ 𝑆𝐵0𝑆 ) ∧ ∀ 𝑥𝑆𝑦𝑆 ( 𝑥 + 𝑦 ) ∈ 𝑆 ) ∧ 𝑢𝑆 ) → 𝑢𝐵 )
43 1 2 3 mndlid ( ( 𝐺 ∈ Mnd ∧ 𝑢𝐵 ) → ( 0 + 𝑢 ) = 𝑢 )
44 33 42 43 syl2an2r ( ( ( ( 𝐺 ∈ Mnd ∧ 𝑆𝐵0𝑆 ) ∧ ∀ 𝑥𝑆𝑦𝑆 ( 𝑥 + 𝑦 ) ∈ 𝑆 ) ∧ 𝑢𝑆 ) → ( 0 + 𝑢 ) = 𝑢 )
45 1 2 3 mndrid ( ( 𝐺 ∈ Mnd ∧ 𝑢𝐵 ) → ( 𝑢 + 0 ) = 𝑢 )
46 33 42 45 syl2an2r ( ( ( ( 𝐺 ∈ Mnd ∧ 𝑆𝐵0𝑆 ) ∧ ∀ 𝑥𝑆𝑦𝑆 ( 𝑥 + 𝑦 ) ∈ 𝑆 ) ∧ 𝑢𝑆 ) → ( 𝑢 + 0 ) = 𝑢 )
47 27 28 32 40 41 44 46 ismndd ( ( ( 𝐺 ∈ Mnd ∧ 𝑆𝐵0𝑆 ) ∧ ∀ 𝑥𝑆𝑦𝑆 ( 𝑥 + 𝑦 ) ∈ 𝑆 ) → 𝐻 ∈ Mnd )
48 25 47 impbida ( ( 𝐺 ∈ Mnd ∧ 𝑆𝐵0𝑆 ) → ( 𝐻 ∈ Mnd ↔ ∀ 𝑥𝑆𝑦𝑆 ( 𝑥 + 𝑦 ) ∈ 𝑆 ) )