This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ↔ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 + 𝑦 ) ∈ 𝑆 ) )