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
|- M = ( freeMnd ` I )
frmdgsum.u
|- U = ( varFMnd ` I )
Assertion frmdss2
|- ( ( I e. V /\ J C_ I /\ A e. ( SubMnd ` M ) ) -> ( ( U " J ) C_ A <-> Word J C_ A ) )

Proof

Step Hyp Ref Expression
1 frmdmnd.m
 |-  M = ( freeMnd ` I )
2 frmdgsum.u
 |-  U = ( varFMnd ` I )
3 simpl1
 |-  ( ( ( I e. V /\ J C_ I /\ A e. ( SubMnd ` M ) ) /\ ( ( U " J ) C_ A /\ x e. Word J ) ) -> I e. V )
4 simpl2
 |-  ( ( ( I e. V /\ J C_ I /\ A e. ( SubMnd ` M ) ) /\ ( ( U " J ) C_ A /\ x e. Word J ) ) -> J C_ I )
5 sswrd
 |-  ( J C_ I -> Word J C_ Word I )
6 4 5 syl
 |-  ( ( ( I e. V /\ J C_ I /\ A e. ( SubMnd ` M ) ) /\ ( ( U " J ) C_ A /\ x e. Word J ) ) -> Word J C_ Word I )
7 simprr
 |-  ( ( ( I e. V /\ J C_ I /\ A e. ( SubMnd ` M ) ) /\ ( ( U " J ) C_ A /\ x e. Word J ) ) -> x e. Word J )
8 6 7 sseldd
 |-  ( ( ( I e. V /\ J C_ I /\ A e. ( SubMnd ` M ) ) /\ ( ( U " J ) C_ A /\ x e. Word J ) ) -> x e. Word I )
9 1 2 frmdgsum
 |-  ( ( I e. V /\ x e. Word I ) -> ( M gsum ( U o. x ) ) = x )
10 3 8 9 syl2anc
 |-  ( ( ( I e. V /\ J C_ I /\ A e. ( SubMnd ` M ) ) /\ ( ( U " J ) C_ A /\ x e. Word J ) ) -> ( M gsum ( U o. x ) ) = x )
11 simpl3
 |-  ( ( ( I e. V /\ J C_ I /\ A e. ( SubMnd ` M ) ) /\ ( ( U " J ) C_ A /\ x e. Word J ) ) -> A e. ( SubMnd ` M ) )
12 wrdf
 |-  ( x e. Word J -> x : ( 0 ..^ ( # ` x ) ) --> J )
13 12 ad2antll
 |-  ( ( ( I e. V /\ J C_ I /\ A e. ( SubMnd ` M ) ) /\ ( ( U " J ) C_ A /\ x e. Word J ) ) -> x : ( 0 ..^ ( # ` x ) ) --> J )
14 13 frnd
 |-  ( ( ( I e. V /\ J C_ I /\ A e. ( SubMnd ` M ) ) /\ ( ( U " J ) C_ A /\ x e. Word J ) ) -> ran x C_ J )
15 cores
 |-  ( ran x C_ J -> ( ( U |` J ) o. x ) = ( U o. x ) )
16 14 15 syl
 |-  ( ( ( I e. V /\ J C_ I /\ A e. ( SubMnd ` M ) ) /\ ( ( U " J ) C_ A /\ x e. Word J ) ) -> ( ( U |` J ) o. x ) = ( U o. x ) )
17 2 vrmdf
 |-  ( I e. V -> U : I --> Word I )
18 17 3ad2ant1
 |-  ( ( I e. V /\ J C_ I /\ A e. ( SubMnd ` M ) ) -> U : I --> Word I )
19 18 ffnd
 |-  ( ( I e. V /\ J C_ I /\ A e. ( SubMnd ` M ) ) -> U Fn I )
20 fnssres
 |-  ( ( U Fn I /\ J C_ I ) -> ( U |` J ) Fn J )
21 19 4 20 syl2an2r
 |-  ( ( ( I e. V /\ J C_ I /\ A e. ( SubMnd ` M ) ) /\ ( ( U " J ) C_ A /\ x e. Word J ) ) -> ( U |` J ) Fn J )
22 df-ima
 |-  ( U " J ) = ran ( U |` J )
23 simprl
 |-  ( ( ( I e. V /\ J C_ I /\ A e. ( SubMnd ` M ) ) /\ ( ( U " J ) C_ A /\ x e. Word J ) ) -> ( U " J ) C_ A )
24 22 23 eqsstrrid
 |-  ( ( ( I e. V /\ J C_ I /\ A e. ( SubMnd ` M ) ) /\ ( ( U " J ) C_ A /\ x e. Word J ) ) -> ran ( U |` J ) C_ A )
25 df-f
 |-  ( ( U |` J ) : J --> A <-> ( ( U |` J ) Fn J /\ ran ( U |` J ) C_ A ) )
26 21 24 25 sylanbrc
 |-  ( ( ( I e. V /\ J C_ I /\ A e. ( SubMnd ` M ) ) /\ ( ( U " J ) C_ A /\ x e. Word J ) ) -> ( U |` J ) : J --> A )
27 wrdco
 |-  ( ( x e. Word J /\ ( U |` J ) : J --> A ) -> ( ( U |` J ) o. x ) e. Word A )
28 7 26 27 syl2anc
 |-  ( ( ( I e. V /\ J C_ I /\ A e. ( SubMnd ` M ) ) /\ ( ( U " J ) C_ A /\ x e. Word J ) ) -> ( ( U |` J ) o. x ) e. Word A )
29 16 28 eqeltrrd
 |-  ( ( ( I e. V /\ J C_ I /\ A e. ( SubMnd ` M ) ) /\ ( ( U " J ) C_ A /\ x e. Word J ) ) -> ( U o. x ) e. Word A )
30 gsumwsubmcl
 |-  ( ( A e. ( SubMnd ` M ) /\ ( U o. x ) e. Word A ) -> ( M gsum ( U o. x ) ) e. A )
31 11 29 30 syl2anc
 |-  ( ( ( I e. V /\ J C_ I /\ A e. ( SubMnd ` M ) ) /\ ( ( U " J ) C_ A /\ x e. Word J ) ) -> ( M gsum ( U o. x ) ) e. A )
32 10 31 eqeltrrd
 |-  ( ( ( I e. V /\ J C_ I /\ A e. ( SubMnd ` M ) ) /\ ( ( U " J ) C_ A /\ x e. Word J ) ) -> x e. A )
33 32 expr
 |-  ( ( ( I e. V /\ J C_ I /\ A e. ( SubMnd ` M ) ) /\ ( U " J ) C_ A ) -> ( x e. Word J -> x e. A ) )
34 33 ssrdv
 |-  ( ( ( I e. V /\ J C_ I /\ A e. ( SubMnd ` M ) ) /\ ( U " J ) C_ A ) -> Word J C_ A )
35 34 ex
 |-  ( ( I e. V /\ J C_ I /\ A e. ( SubMnd ` M ) ) -> ( ( U " J ) C_ A -> Word J C_ A ) )
36 simpl1
 |-  ( ( ( I e. V /\ J C_ I /\ A e. ( SubMnd ` M ) ) /\ x e. J ) -> I e. V )
37 simp2
 |-  ( ( I e. V /\ J C_ I /\ A e. ( SubMnd ` M ) ) -> J C_ I )
38 37 sselda
 |-  ( ( ( I e. V /\ J C_ I /\ A e. ( SubMnd ` M ) ) /\ x e. J ) -> x e. I )
39 2 vrmdval
 |-  ( ( I e. V /\ x e. I ) -> ( U ` x ) = <" x "> )
40 36 38 39 syl2anc
 |-  ( ( ( I e. V /\ J C_ I /\ A e. ( SubMnd ` M ) ) /\ x e. J ) -> ( U ` x ) = <" x "> )
41 simpr
 |-  ( ( ( I e. V /\ J C_ I /\ A e. ( SubMnd ` M ) ) /\ x e. J ) -> x e. J )
42 41 s1cld
 |-  ( ( ( I e. V /\ J C_ I /\ A e. ( SubMnd ` M ) ) /\ x e. J ) -> <" x "> e. Word J )
43 40 42 eqeltrd
 |-  ( ( ( I e. V /\ J C_ I /\ A e. ( SubMnd ` M ) ) /\ x e. J ) -> ( U ` x ) e. Word J )
44 43 ralrimiva
 |-  ( ( I e. V /\ J C_ I /\ A e. ( SubMnd ` M ) ) -> A. x e. J ( U ` x ) e. Word J )
45 18 ffund
 |-  ( ( I e. V /\ J C_ I /\ A e. ( SubMnd ` M ) ) -> Fun U )
46 18 fdmd
 |-  ( ( I e. V /\ J C_ I /\ A e. ( SubMnd ` M ) ) -> dom U = I )
47 37 46 sseqtrrd
 |-  ( ( I e. V /\ J C_ I /\ A e. ( SubMnd ` M ) ) -> J C_ dom U )
48 funimass4
 |-  ( ( Fun U /\ J C_ dom U ) -> ( ( U " J ) C_ Word J <-> A. x e. J ( U ` x ) e. Word J ) )
49 45 47 48 syl2anc
 |-  ( ( I e. V /\ J C_ I /\ A e. ( SubMnd ` M ) ) -> ( ( U " J ) C_ Word J <-> A. x e. J ( U ` x ) e. Word J ) )
50 44 49 mpbird
 |-  ( ( I e. V /\ J C_ I /\ A e. ( SubMnd ` M ) ) -> ( U " J ) C_ Word J )
51 sstr2
 |-  ( ( U " J ) C_ Word J -> ( Word J C_ A -> ( U " J ) C_ A ) )
52 50 51 syl
 |-  ( ( I e. V /\ J C_ I /\ A e. ( SubMnd ` M ) ) -> ( Word J C_ A -> ( U " J ) C_ A ) )
53 35 52 impbid
 |-  ( ( I e. V /\ J C_ I /\ A e. ( SubMnd ` M ) ) -> ( ( U " J ) C_ A <-> Word J C_ A ) )