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