Metamath Proof Explorer

Theorem frmdss2

Description: A subset of generators is contained in a submonoid iff the set of words on the generators is in the submonoid. This can be viewed as an elementary way of saying "the monoidal closure of J is Word J ". (Contributed by Mario Carneiro, 2-Oct-2015)

Ref Expression
Hypotheses frmdmnd.m ⊢ 𝑀 = ( freeMnd ‘ 𝐼 )
frmdgsum.u ⊢ 𝑈 = ( varFMnd ‘ 𝐼 )
Assertion frmdss2 ( ( 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ∧ 𝐴 ∈ ( SubMnd ‘ 𝑀 ) ) → ( ( 𝑈 “ 𝐽 ) ⊆ 𝐴 ↔ Word 𝐽 ⊆ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 frmdmnd.m ⊢ 𝑀 = ( freeMnd ‘ 𝐼 )
2 frmdgsum.u ⊢ 𝑈 = ( varFMnd ‘ 𝐼 )
3 simpl1 ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ∧ 𝐴 ∈ ( SubMnd ‘ 𝑀 ) ) ∧ ( ( 𝑈 “ 𝐽 ) ⊆ 𝐴 ∧ 𝑥 ∈ Word 𝐽 ) ) → 𝐼 ∈ 𝑉 )
4 simpl2 ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ∧ 𝐴 ∈ ( SubMnd ‘ 𝑀 ) ) ∧ ( ( 𝑈 “ 𝐽 ) ⊆ 𝐴 ∧ 𝑥 ∈ Word 𝐽 ) ) → 𝐽 ⊆ 𝐼 )
5 sswrd ⊢ ( 𝐽 ⊆ 𝐼 → Word 𝐽 ⊆ Word 𝐼 )
6 4 5 syl ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ∧ 𝐴 ∈ ( SubMnd ‘ 𝑀 ) ) ∧ ( ( 𝑈 “ 𝐽 ) ⊆ 𝐴 ∧ 𝑥 ∈ Word 𝐽 ) ) → Word 𝐽 ⊆ Word 𝐼 )
7 simprr ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ∧ 𝐴 ∈ ( SubMnd ‘ 𝑀 ) ) ∧ ( ( 𝑈 “ 𝐽 ) ⊆ 𝐴 ∧ 𝑥 ∈ Word 𝐽 ) ) → 𝑥 ∈ Word 𝐽 )
8 6 7 sseldd ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ∧ 𝐴 ∈ ( SubMnd ‘ 𝑀 ) ) ∧ ( ( 𝑈 “ 𝐽 ) ⊆ 𝐴 ∧ 𝑥 ∈ Word 𝐽 ) ) → 𝑥 ∈ Word 𝐼 )
9 1 2 frmdgsum ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word 𝐼 ) → ( 𝑀 Σg ( 𝑈 ∘ 𝑥 ) ) = 𝑥 )
10 3 8 9 syl2anc ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ∧ 𝐴 ∈ ( SubMnd ‘ 𝑀 ) ) ∧ ( ( 𝑈 “ 𝐽 ) ⊆ 𝐴 ∧ 𝑥 ∈ Word 𝐽 ) ) → ( 𝑀 Σg ( 𝑈 ∘ 𝑥 ) ) = 𝑥 )
11 simpl3 ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ∧ 𝐴 ∈ ( SubMnd ‘ 𝑀 ) ) ∧ ( ( 𝑈 “ 𝐽 ) ⊆ 𝐴 ∧ 𝑥 ∈ Word 𝐽 ) ) → 𝐴 ∈ ( SubMnd ‘ 𝑀 ) )
12 wrdf ⊢ ( 𝑥 ∈ Word 𝐽 → 𝑥 : ( 0 ..^ ( ♯ ‘ 𝑥 ) ) ⟶ 𝐽 )
13 12 ad2antll ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ∧ 𝐴 ∈ ( SubMnd ‘ 𝑀 ) ) ∧ ( ( 𝑈 “ 𝐽 ) ⊆ 𝐴 ∧ 𝑥 ∈ Word 𝐽 ) ) → 𝑥 : ( 0 ..^ ( ♯ ‘ 𝑥 ) ) ⟶ 𝐽 )
14 13 frnd ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ∧ 𝐴 ∈ ( SubMnd ‘ 𝑀 ) ) ∧ ( ( 𝑈 “ 𝐽 ) ⊆ 𝐴 ∧ 𝑥 ∈ Word 𝐽 ) ) → ran 𝑥 ⊆ 𝐽 )
15 cores ⊢ ( ran 𝑥 ⊆ 𝐽 → ( ( 𝑈 ↾ 𝐽 ) ∘ 𝑥 ) = ( 𝑈 ∘ 𝑥 ) )
16 14 15 syl ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ∧ 𝐴 ∈ ( SubMnd ‘ 𝑀 ) ) ∧ ( ( 𝑈 “ 𝐽 ) ⊆ 𝐴 ∧ 𝑥 ∈ Word 𝐽 ) ) → ( ( 𝑈 ↾ 𝐽 ) ∘ 𝑥 ) = ( 𝑈 ∘ 𝑥 ) )
17 2 vrmdf ⊢ ( 𝐼 ∈ 𝑉 → 𝑈 : 𝐼 ⟶ Word 𝐼 )
18 17 3ad2ant1 ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ∧ 𝐴 ∈ ( SubMnd ‘ 𝑀 ) ) → 𝑈 : 𝐼 ⟶ Word 𝐼 )
19 18 ffnd ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ∧ 𝐴 ∈ ( SubMnd ‘ 𝑀 ) ) → 𝑈 Fn 𝐼 )
20 fnssres ⊢ ( ( 𝑈 Fn 𝐼 ∧ 𝐽 ⊆ 𝐼 ) → ( 𝑈 ↾ 𝐽 ) Fn 𝐽 )
21 19 4 20 syl2an2r ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ∧ 𝐴 ∈ ( SubMnd ‘ 𝑀 ) ) ∧ ( ( 𝑈 “ 𝐽 ) ⊆ 𝐴 ∧ 𝑥 ∈ Word 𝐽 ) ) → ( 𝑈 ↾ 𝐽 ) Fn 𝐽 )
22 df-ima ⊢ ( 𝑈 “ 𝐽 ) = ran ( 𝑈 ↾ 𝐽 )
23 simprl ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ∧ 𝐴 ∈ ( SubMnd ‘ 𝑀 ) ) ∧ ( ( 𝑈 “ 𝐽 ) ⊆ 𝐴 ∧ 𝑥 ∈ Word 𝐽 ) ) → ( 𝑈 “ 𝐽 ) ⊆ 𝐴 )
24 22 23 eqsstrrid ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ∧ 𝐴 ∈ ( SubMnd ‘ 𝑀 ) ) ∧ ( ( 𝑈 “ 𝐽 ) ⊆ 𝐴 ∧ 𝑥 ∈ Word 𝐽 ) ) → ran ( 𝑈 ↾ 𝐽 ) ⊆ 𝐴 )
25 df-f ⊢ ( ( 𝑈 ↾ 𝐽 ) : 𝐽 ⟶ 𝐴 ↔ ( ( 𝑈 ↾ 𝐽 ) Fn 𝐽 ∧ ran ( 𝑈 ↾ 𝐽 ) ⊆ 𝐴 ) )
26 21 24 25 sylanbrc ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ∧ 𝐴 ∈ ( SubMnd ‘ 𝑀 ) ) ∧ ( ( 𝑈 “ 𝐽 ) ⊆ 𝐴 ∧ 𝑥 ∈ Word 𝐽 ) ) → ( 𝑈 ↾ 𝐽 ) : 𝐽 ⟶ 𝐴 )
27 wrdco ⊢ ( ( 𝑥 ∈ Word 𝐽 ∧ ( 𝑈 ↾ 𝐽 ) : 𝐽 ⟶ 𝐴 ) → ( ( 𝑈 ↾ 𝐽 ) ∘ 𝑥 ) ∈ Word 𝐴 )
28 7 26 27 syl2anc ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ∧ 𝐴 ∈ ( SubMnd ‘ 𝑀 ) ) ∧ ( ( 𝑈 “ 𝐽 ) ⊆ 𝐴 ∧ 𝑥 ∈ Word 𝐽 ) ) → ( ( 𝑈 ↾ 𝐽 ) ∘ 𝑥 ) ∈ Word 𝐴 )
29 16 28 eqeltrrd ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ∧ 𝐴 ∈ ( SubMnd ‘ 𝑀 ) ) ∧ ( ( 𝑈 “ 𝐽 ) ⊆ 𝐴 ∧ 𝑥 ∈ Word 𝐽 ) ) → ( 𝑈 ∘ 𝑥 ) ∈ Word 𝐴 )
30 gsumwsubmcl ⊢ ( ( 𝐴 ∈ ( SubMnd ‘ 𝑀 ) ∧ ( 𝑈 ∘ 𝑥 ) ∈ Word 𝐴 ) → ( 𝑀 Σg ( 𝑈 ∘ 𝑥 ) ) ∈ 𝐴 )
31 11 29 30 syl2anc ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ∧ 𝐴 ∈ ( SubMnd ‘ 𝑀 ) ) ∧ ( ( 𝑈 “ 𝐽 ) ⊆ 𝐴 ∧ 𝑥 ∈ Word 𝐽 ) ) → ( 𝑀 Σg ( 𝑈 ∘ 𝑥 ) ) ∈ 𝐴 )
32 10 31 eqeltrrd ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ∧ 𝐴 ∈ ( SubMnd ‘ 𝑀 ) ) ∧ ( ( 𝑈 “ 𝐽 ) ⊆ 𝐴 ∧ 𝑥 ∈ Word 𝐽 ) ) → 𝑥 ∈ 𝐴 )
33 32 expr ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ∧ 𝐴 ∈ ( SubMnd ‘ 𝑀 ) ) ∧ ( 𝑈 “ 𝐽 ) ⊆ 𝐴 ) → ( 𝑥 ∈ Word 𝐽 → 𝑥 ∈ 𝐴 ) )
34 33 ssrdv ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ∧ 𝐴 ∈ ( SubMnd ‘ 𝑀 ) ) ∧ ( 𝑈 “ 𝐽 ) ⊆ 𝐴 ) → Word 𝐽 ⊆ 𝐴 )
35 34 ex ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ∧ 𝐴 ∈ ( SubMnd ‘ 𝑀 ) ) → ( ( 𝑈 “ 𝐽 ) ⊆ 𝐴 → Word 𝐽 ⊆ 𝐴 ) )
36 simpl1 ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ∧ 𝐴 ∈ ( SubMnd ‘ 𝑀 ) ) ∧ 𝑥 ∈ 𝐽 ) → 𝐼 ∈ 𝑉 )
37 simp2 ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ∧ 𝐴 ∈ ( SubMnd ‘ 𝑀 ) ) → 𝐽 ⊆ 𝐼 )
38 37 sselda ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ∧ 𝐴 ∈ ( SubMnd ‘ 𝑀 ) ) ∧ 𝑥 ∈ 𝐽 ) → 𝑥 ∈ 𝐼 )
39 2 vrmdval ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑥 ∈ 𝐼 ) → ( 𝑈 ‘ 𝑥 ) = ⟨“ 𝑥 ”⟩ )
40 36 38 39 syl2anc ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ∧ 𝐴 ∈ ( SubMnd ‘ 𝑀 ) ) ∧ 𝑥 ∈ 𝐽 ) → ( 𝑈 ‘ 𝑥 ) = ⟨“ 𝑥 ”⟩ )
41 simpr ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ∧ 𝐴 ∈ ( SubMnd ‘ 𝑀 ) ) ∧ 𝑥 ∈ 𝐽 ) → 𝑥 ∈ 𝐽 )
42 41 s1cld ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ∧ 𝐴 ∈ ( SubMnd ‘ 𝑀 ) ) ∧ 𝑥 ∈ 𝐽 ) → ⟨“ 𝑥 ”⟩ ∈ Word 𝐽 )
43 40 42 eqeltrd ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ∧ 𝐴 ∈ ( SubMnd ‘ 𝑀 ) ) ∧ 𝑥 ∈ 𝐽 ) → ( 𝑈 ‘ 𝑥 ) ∈ Word 𝐽 )
44 43 ralrimiva ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ∧ 𝐴 ∈ ( SubMnd ‘ 𝑀 ) ) → ∀ 𝑥 ∈ 𝐽 ( 𝑈 ‘ 𝑥 ) ∈ Word 𝐽 )
45 18 ffund ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ∧ 𝐴 ∈ ( SubMnd ‘ 𝑀 ) ) → Fun 𝑈 )
46 18 fdmd ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ∧ 𝐴 ∈ ( SubMnd ‘ 𝑀 ) ) → dom 𝑈 = 𝐼 )
47 37 46 sseqtrrd ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ∧ 𝐴 ∈ ( SubMnd ‘ 𝑀 ) ) → 𝐽 ⊆ dom 𝑈 )
48 funimass4 ⊢ ( ( Fun 𝑈 ∧ 𝐽 ⊆ dom 𝑈 ) → ( ( 𝑈 “ 𝐽 ) ⊆ Word 𝐽 ↔ ∀ 𝑥 ∈ 𝐽 ( 𝑈 ‘ 𝑥 ) ∈ Word 𝐽 ) )
49 45 47 48 syl2anc ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ∧ 𝐴 ∈ ( SubMnd ‘ 𝑀 ) ) → ( ( 𝑈 “ 𝐽 ) ⊆ Word 𝐽 ↔ ∀ 𝑥 ∈ 𝐽 ( 𝑈 ‘ 𝑥 ) ∈ Word 𝐽 ) )
50 44 49 mpbird ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ∧ 𝐴 ∈ ( SubMnd ‘ 𝑀 ) ) → ( 𝑈 “ 𝐽 ) ⊆ Word 𝐽 )
51 sstr2 ⊢ ( ( 𝑈 “ 𝐽 ) ⊆ Word 𝐽 → ( Word 𝐽 ⊆ 𝐴 → ( 𝑈 “ 𝐽 ) ⊆ 𝐴 ) )
52 50 51 syl ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ∧ 𝐴 ∈ ( SubMnd ‘ 𝑀 ) ) → ( Word 𝐽 ⊆ 𝐴 → ( 𝑈 “ 𝐽 ) ⊆ 𝐴 ) )
53 35 52 impbid ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ∧ 𝐴 ∈ ( SubMnd ‘ 𝑀 ) ) → ( ( 𝑈 “ 𝐽 ) ⊆ 𝐴 ↔ Word 𝐽 ⊆ 𝐴 ) )