Metamath Proof Explorer

Theorem frmdsssubm

Description: The set of words taking values in a subset is a (free) submonoid of the free monoid. (Contributed by Mario Carneiro, 27-Sep-2015) (Revised by Mario Carneiro, 27-Feb-2016)

Ref Expression
Hypothesis frmdmnd.m ⊢ 𝑀 = ( freeMnd ‘ 𝐼 )
Assertion frmdsssubm ( ( 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) → Word 𝐽 ∈ ( SubMnd ‘ 𝑀 ) )

Proof

Step Hyp Ref Expression
1 frmdmnd.m ⊢ 𝑀 = ( freeMnd ‘ 𝐼 )
2 sswrd ⊢ ( 𝐽 ⊆ 𝐼 → Word 𝐽 ⊆ Word 𝐼 )
3 2 adantl ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) → Word 𝐽 ⊆ Word 𝐼 )
4 eqid ⊢ ( Base ‘ 𝑀 ) = ( Base ‘ 𝑀 )
5 1 4 frmdbas ⊢ ( 𝐼 ∈ 𝑉 → ( Base ‘ 𝑀 ) = Word 𝐼 )
6 5 adantr ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) → ( Base ‘ 𝑀 ) = Word 𝐼 )
7 3 6 sseqtrrd ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) → Word 𝐽 ⊆ ( Base ‘ 𝑀 ) )
8 wrd0 ⊢ ∅ ∈ Word 𝐽
9 8 a1i ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) → ∅ ∈ Word 𝐽 )
10 7 sselda ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑥 ∈ Word 𝐽 ) → 𝑥 ∈ ( Base ‘ 𝑀 ) )
11 7 sselda ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ Word 𝐽 ) → 𝑦 ∈ ( Base ‘ 𝑀 ) )
12 10 11 anim12dan ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ ( 𝑥 ∈ Word 𝐽 ∧ 𝑦 ∈ Word 𝐽 ) ) → ( 𝑥 ∈ ( Base ‘ 𝑀 ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) )
13 eqid ⊢ ( +g ‘ 𝑀 ) = ( +g ‘ 𝑀 )
14 1 4 13 frmdadd ⊢ ( ( 𝑥 ∈ ( Base ‘ 𝑀 ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) → ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) = ( 𝑥 ++ 𝑦 ) )
15 12 14 syl ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ ( 𝑥 ∈ Word 𝐽 ∧ 𝑦 ∈ Word 𝐽 ) ) → ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) = ( 𝑥 ++ 𝑦 ) )
16 ccatcl ⊢ ( ( 𝑥 ∈ Word 𝐽 ∧ 𝑦 ∈ Word 𝐽 ) → ( 𝑥 ++ 𝑦 ) ∈ Word 𝐽 )
17 16 adantl ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ ( 𝑥 ∈ Word 𝐽 ∧ 𝑦 ∈ Word 𝐽 ) ) → ( 𝑥 ++ 𝑦 ) ∈ Word 𝐽 )
18 15 17 eqeltrd ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ ( 𝑥 ∈ Word 𝐽 ∧ 𝑦 ∈ Word 𝐽 ) ) → ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ∈ Word 𝐽 )
19 18 ralrimivva ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) → ∀ 𝑥 ∈ Word 𝐽 ∀ 𝑦 ∈ Word 𝐽 ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ∈ Word 𝐽 )
20 1 frmdmnd ⊢ ( 𝐼 ∈ 𝑉 → 𝑀 ∈ Mnd )
21 20 adantr ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) → 𝑀 ∈ Mnd )
22 1 frmd0 ⊢ ∅ = ( 0g ‘ 𝑀 )
23 4 22 13 issubm ⊢ ( 𝑀 ∈ Mnd → ( Word 𝐽 ∈ ( SubMnd ‘ 𝑀 ) ↔ ( Word 𝐽 ⊆ ( Base ‘ 𝑀 ) ∧ ∅ ∈ Word 𝐽 ∧ ∀ 𝑥 ∈ Word 𝐽 ∀ 𝑦 ∈ Word 𝐽 ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ∈ Word 𝐽 ) ) )
24 21 23 syl ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) → ( Word 𝐽 ∈ ( SubMnd ‘ 𝑀 ) ↔ ( Word 𝐽 ⊆ ( Base ‘ 𝑀 ) ∧ ∅ ∈ Word 𝐽 ∧ ∀ 𝑥 ∈ Word 𝐽 ∀ 𝑦 ∈ Word 𝐽 ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ∈ Word 𝐽 ) ) )
25 7 9 19 24 mpbir3and ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) → Word 𝐽 ∈ ( SubMnd ‘ 𝑀 ) )