Metamath Proof Explorer


Theorem efgval

Description: Value of the free group construction. (Contributed by Mario Carneiro, 1-Oct-2015)

Ref Expression
Hypotheses efgval.w W=IWordI×2𝑜
efgval.r ˙=~FGI
Assertion efgval ˙=r|rErWxWn0xyIz2𝑜xrxsplicenn⟨“yzy1𝑜z”⟩

Proof

Step Hyp Ref Expression
1 efgval.w W=IWordI×2𝑜
2 efgval.r ˙=~FGI
3 vex iV
4 2on 2𝑜On
5 4 elexi 2𝑜V
6 3 5 xpex i×2𝑜V
7 wrdexg i×2𝑜VWordi×2𝑜V
8 fvi Wordi×2𝑜VIWordi×2𝑜=Wordi×2𝑜
9 6 7 8 mp2b IWordi×2𝑜=Wordi×2𝑜
10 xpeq1 i=Ii×2𝑜=I×2𝑜
11 wrdeq i×2𝑜=I×2𝑜Wordi×2𝑜=WordI×2𝑜
12 10 11 syl i=IWordi×2𝑜=WordI×2𝑜
13 12 fveq2d i=IIWordi×2𝑜=IWordI×2𝑜
14 9 13 eqtr3id i=IWordi×2𝑜=IWordI×2𝑜
15 14 1 eqtr4di i=IWordi×2𝑜=W
16 ereq2 Wordi×2𝑜=WrErWordi×2𝑜rErW
17 15 16 syl i=IrErWordi×2𝑜rErW
18 raleq i=Iyiz2𝑜xrxsplicenn⟨“yzy1𝑜z”⟩yIz2𝑜xrxsplicenn⟨“yzy1𝑜z”⟩
19 18 ralbidv i=In0xyiz2𝑜xrxsplicenn⟨“yzy1𝑜z”⟩n0xyIz2𝑜xrxsplicenn⟨“yzy1𝑜z”⟩
20 15 19 raleqbidv i=IxWordi×2𝑜n0xyiz2𝑜xrxsplicenn⟨“yzy1𝑜z”⟩xWn0xyIz2𝑜xrxsplicenn⟨“yzy1𝑜z”⟩
21 17 20 anbi12d i=IrErWordi×2𝑜xWordi×2𝑜n0xyiz2𝑜xrxsplicenn⟨“yzy1𝑜z”⟩rErWxWn0xyIz2𝑜xrxsplicenn⟨“yzy1𝑜z”⟩
22 21 abbidv i=Ir|rErWordi×2𝑜xWordi×2𝑜n0xyiz2𝑜xrxsplicenn⟨“yzy1𝑜z”⟩=r|rErWxWn0xyIz2𝑜xrxsplicenn⟨“yzy1𝑜z”⟩
23 22 inteqd i=Ir|rErWordi×2𝑜xWordi×2𝑜n0xyiz2𝑜xrxsplicenn⟨“yzy1𝑜z”⟩=r|rErWxWn0xyIz2𝑜xrxsplicenn⟨“yzy1𝑜z”⟩
24 df-efg ~FG=iVr|rErWordi×2𝑜xWordi×2𝑜n0xyiz2𝑜xrxsplicenn⟨“yzy1𝑜z”⟩
25 1 efglem rrErWxWn0xyIz2𝑜xrxsplicenn⟨“yzy1𝑜z”⟩
26 intexab rrErWxWn0xyIz2𝑜xrxsplicenn⟨“yzy1𝑜z”⟩r|rErWxWn0xyIz2𝑜xrxsplicenn⟨“yzy1𝑜z”⟩V
27 25 26 mpbi r|rErWxWn0xyIz2𝑜xrxsplicenn⟨“yzy1𝑜z”⟩V
28 23 24 27 fvmpt IV~FGI=r|rErWxWn0xyIz2𝑜xrxsplicenn⟨“yzy1𝑜z”⟩
29 fvprc ¬IV~FGI=
30 abn0 r|rErWxWn0xyIz2𝑜xrxsplicenn⟨“yzy1𝑜z”⟩rrErWxWn0xyIz2𝑜xrxsplicenn⟨“yzy1𝑜z”⟩
31 25 30 mpbir r|rErWxWn0xyIz2𝑜xrxsplicenn⟨“yzy1𝑜z”⟩
32 intssuni r|rErWxWn0xyIz2𝑜xrxsplicenn⟨“yzy1𝑜z”⟩r|rErWxWn0xyIz2𝑜xrxsplicenn⟨“yzy1𝑜z”⟩r|rErWxWn0xyIz2𝑜xrxsplicenn⟨“yzy1𝑜z”⟩
33 31 32 ax-mp r|rErWxWn0xyIz2𝑜xrxsplicenn⟨“yzy1𝑜z”⟩r|rErWxWn0xyIz2𝑜xrxsplicenn⟨“yzy1𝑜z”⟩
34 erssxp rErWrW×W
35 1 efgrcl xWIVW=WordI×2𝑜
36 35 simpld xWIV
37 36 con3i ¬IV¬xW
38 37 eq0rdv ¬IVW=
39 38 xpeq2d ¬IVW×W=W×
40 xp0 W×=
41 39 40 eqtrdi ¬IVW×W=
42 ss0b W×WW×W=
43 41 42 sylibr ¬IVW×W
44 34 43 sylan9ssr ¬IVrErWr
45 44 ex ¬IVrErWr
46 45 adantrd ¬IVrErWxWn0xyIz2𝑜xrxsplicenn⟨“yzy1𝑜z”⟩r
47 46 alrimiv ¬IVrrErWxWn0xyIz2𝑜xrxsplicenn⟨“yzy1𝑜z”⟩r
48 sseq1 w=rwr
49 48 ralab2 wr|rErWxWn0xyIz2𝑜xrxsplicenn⟨“yzy1𝑜z”⟩wrrErWxWn0xyIz2𝑜xrxsplicenn⟨“yzy1𝑜z”⟩r
50 47 49 sylibr ¬IVwr|rErWxWn0xyIz2𝑜xrxsplicenn⟨“yzy1𝑜z”⟩w
51 unissb r|rErWxWn0xyIz2𝑜xrxsplicenn⟨“yzy1𝑜z”⟩wr|rErWxWn0xyIz2𝑜xrxsplicenn⟨“yzy1𝑜z”⟩w
52 50 51 sylibr ¬IVr|rErWxWn0xyIz2𝑜xrxsplicenn⟨“yzy1𝑜z”⟩
53 33 52 sstrid ¬IVr|rErWxWn0xyIz2𝑜xrxsplicenn⟨“yzy1𝑜z”⟩
54 ss0 r|rErWxWn0xyIz2𝑜xrxsplicenn⟨“yzy1𝑜z”⟩r|rErWxWn0xyIz2𝑜xrxsplicenn⟨“yzy1𝑜z”⟩=
55 53 54 syl ¬IVr|rErWxWn0xyIz2𝑜xrxsplicenn⟨“yzy1𝑜z”⟩=
56 29 55 eqtr4d ¬IV~FGI=r|rErWxWn0xyIz2𝑜xrxsplicenn⟨“yzy1𝑜z”⟩
57 28 56 pm2.61i ~FGI=r|rErWxWn0xyIz2𝑜xrxsplicenn⟨“yzy1𝑜z”⟩
58 2 57 eqtri ˙=r|rErWxWn0xyIz2𝑜xrxsplicenn⟨“yzy1𝑜z”⟩