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 = I Word I × 2 𝑜
efgval.r ˙ = ~ FG I
Assertion efgval ˙ = r | r Er W x W n 0 x y I z 2 𝑜 x r x splice n n ⟨“ y z y 1 𝑜 z ”⟩

Proof

Step Hyp Ref Expression
1 efgval.w W = I Word I × 2 𝑜
2 efgval.r ˙ = ~ FG I
3 vex i V
4 2on 2 𝑜 On
5 4 elexi 2 𝑜 V
6 3 5 xpex i × 2 𝑜 V
7 wrdexg i × 2 𝑜 V Word i × 2 𝑜 V
8 fvi Word i × 2 𝑜 V I Word i × 2 𝑜 = Word i × 2 𝑜
9 6 7 8 mp2b I Word i × 2 𝑜 = Word i × 2 𝑜
10 xpeq1 i = I i × 2 𝑜 = I × 2 𝑜
11 wrdeq i × 2 𝑜 = I × 2 𝑜 Word i × 2 𝑜 = Word I × 2 𝑜
12 10 11 syl i = I Word i × 2 𝑜 = Word I × 2 𝑜
13 12 fveq2d i = I I Word i × 2 𝑜 = I Word I × 2 𝑜
14 9 13 eqtr3id i = I Word i × 2 𝑜 = I Word I × 2 𝑜
15 14 1 eqtr4di i = I Word i × 2 𝑜 = W
16 ereq2 Word i × 2 𝑜 = W r Er Word i × 2 𝑜 r Er W
17 15 16 syl i = I r Er Word i × 2 𝑜 r Er W
18 raleq i = I y i z 2 𝑜 x r x splice n n ⟨“ y z y 1 𝑜 z ”⟩ y I z 2 𝑜 x r x splice n n ⟨“ y z y 1 𝑜 z ”⟩
19 18 ralbidv i = I n 0 x y i z 2 𝑜 x r x splice n n ⟨“ y z y 1 𝑜 z ”⟩ n 0 x y I z 2 𝑜 x r x splice n n ⟨“ y z y 1 𝑜 z ”⟩
20 15 19 raleqbidv i = I x Word i × 2 𝑜 n 0 x y i z 2 𝑜 x r x splice n n ⟨“ y z y 1 𝑜 z ”⟩ x W n 0 x y I z 2 𝑜 x r x splice n n ⟨“ y z y 1 𝑜 z ”⟩
21 17 20 anbi12d i = I r Er Word i × 2 𝑜 x Word i × 2 𝑜 n 0 x y i z 2 𝑜 x r x splice n n ⟨“ y z y 1 𝑜 z ”⟩ r Er W x W n 0 x y I z 2 𝑜 x r x splice n n ⟨“ y z y 1 𝑜 z ”⟩
22 21 abbidv i = I r | r Er Word i × 2 𝑜 x Word i × 2 𝑜 n 0 x y i z 2 𝑜 x r x splice n n ⟨“ y z y 1 𝑜 z ”⟩ = r | r Er W x W n 0 x y I z 2 𝑜 x r x splice n n ⟨“ y z y 1 𝑜 z ”⟩
23 22 inteqd i = I r | r Er Word i × 2 𝑜 x Word i × 2 𝑜 n 0 x y i z 2 𝑜 x r x splice n n ⟨“ y z y 1 𝑜 z ”⟩ = r | r Er W x W n 0 x y I z 2 𝑜 x r x splice n n ⟨“ y z y 1 𝑜 z ”⟩
24 df-efg ~ FG = i V r | r Er Word i × 2 𝑜 x Word i × 2 𝑜 n 0 x y i z 2 𝑜 x r x splice n n ⟨“ y z y 1 𝑜 z ”⟩
25 1 efglem r r Er W x W n 0 x y I z 2 𝑜 x r x splice n n ⟨“ y z y 1 𝑜 z ”⟩
26 intexab r r Er W x W n 0 x y I z 2 𝑜 x r x splice n n ⟨“ y z y 1 𝑜 z ”⟩ r | r Er W x W n 0 x y I z 2 𝑜 x r x splice n n ⟨“ y z y 1 𝑜 z ”⟩ V
27 25 26 mpbi r | r Er W x W n 0 x y I z 2 𝑜 x r x splice n n ⟨“ y z y 1 𝑜 z ”⟩ V
28 23 24 27 fvmpt I V ~ FG I = r | r Er W x W n 0 x y I z 2 𝑜 x r x splice n n ⟨“ y z y 1 𝑜 z ”⟩
29 fvprc ¬ I V ~ FG I =
30 abn0 r | r Er W x W n 0 x y I z 2 𝑜 x r x splice n n ⟨“ y z y 1 𝑜 z ”⟩ r r Er W x W n 0 x y I z 2 𝑜 x r x splice n n ⟨“ y z y 1 𝑜 z ”⟩
31 25 30 mpbir r | r Er W x W n 0 x y I z 2 𝑜 x r x splice n n ⟨“ y z y 1 𝑜 z ”⟩
32 intssuni r | r Er W x W n 0 x y I z 2 𝑜 x r x splice n n ⟨“ y z y 1 𝑜 z ”⟩ r | r Er W x W n 0 x y I z 2 𝑜 x r x splice n n ⟨“ y z y 1 𝑜 z ”⟩ r | r Er W x W n 0 x y I z 2 𝑜 x r x splice n n ⟨“ y z y 1 𝑜 z ”⟩
33 31 32 ax-mp r | r Er W x W n 0 x y I z 2 𝑜 x r x splice n n ⟨“ y z y 1 𝑜 z ”⟩ r | r Er W x W n 0 x y I z 2 𝑜 x r x splice n n ⟨“ y z y 1 𝑜 z ”⟩
34 erssxp r Er W r W × W
35 1 efgrcl x W I V W = Word I × 2 𝑜
36 35 simpld x W I V
37 36 con3i ¬ I V ¬ x W
38 37 eq0rdv ¬ I V W =
39 38 xpeq2d ¬ I V W × W = W ×
40 xp0 W × =
41 39 40 eqtrdi ¬ I V W × W =
42 ss0b W × W W × W =
43 41 42 sylibr ¬ I V W × W
44 34 43 sylan9ssr ¬ I V r Er W r
45 44 ex ¬ I V r Er W r
46 45 adantrd ¬ I V r Er W x W n 0 x y I z 2 𝑜 x r x splice n n ⟨“ y z y 1 𝑜 z ”⟩ r
47 46 alrimiv ¬ I V r r Er W x W n 0 x y I z 2 𝑜 x r x splice n n ⟨“ y z y 1 𝑜 z ”⟩ r
48 sseq1 w = r w r
49 48 ralab2 w r | r Er W x W n 0 x y I z 2 𝑜 x r x splice n n ⟨“ y z y 1 𝑜 z ”⟩ w r r Er W x W n 0 x y I z 2 𝑜 x r x splice n n ⟨“ y z y 1 𝑜 z ”⟩ r
50 47 49 sylibr ¬ I V w r | r Er W x W n 0 x y I z 2 𝑜 x r x splice n n ⟨“ y z y 1 𝑜 z ”⟩ w
51 unissb r | r Er W x W n 0 x y I z 2 𝑜 x r x splice n n ⟨“ y z y 1 𝑜 z ”⟩ w r | r Er W x W n 0 x y I z 2 𝑜 x r x splice n n ⟨“ y z y 1 𝑜 z ”⟩ w
52 50 51 sylibr ¬ I V r | r Er W x W n 0 x y I z 2 𝑜 x r x splice n n ⟨“ y z y 1 𝑜 z ”⟩
53 33 52 sstrid ¬ I V r | r Er W x W n 0 x y I z 2 𝑜 x r x splice n n ⟨“ y z y 1 𝑜 z ”⟩
54 ss0 r | r Er W x W n 0 x y I z 2 𝑜 x r x splice n n ⟨“ y z y 1 𝑜 z ”⟩ r | r Er W x W n 0 x y I z 2 𝑜 x r x splice n n ⟨“ y z y 1 𝑜 z ”⟩ =
55 53 54 syl ¬ I V r | r Er W x W n 0 x y I z 2 𝑜 x r x splice n n ⟨“ y z y 1 𝑜 z ”⟩ =
56 29 55 eqtr4d ¬ I V ~ FG I = r | r Er W x W n 0 x y I z 2 𝑜 x r x splice n n ⟨“ y z y 1 𝑜 z ”⟩
57 28 56 pm2.61i ~ FG I = r | r Er W x W n 0 x y I z 2 𝑜 x r x splice n n ⟨“ y z y 1 𝑜 z ”⟩
58 2 57 eqtri ˙ = r | r Er W x W n 0 x y I z 2 𝑜 x r x splice n n ⟨“ y z y 1 𝑜 z ”⟩