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 ) )