# Metamath Proof Explorer

## Theorem efgi

Description: Value of the free group construction. (Contributed by Mario Carneiro, 27-Sep-2015) (Revised by Mario Carneiro, 27-Feb-2016)

Ref Expression
Hypotheses efgval.w ${⊢}{W}=\mathrm{I}\left(\mathrm{Word}\left({I}×{2}_{𝑜}\right)\right)$
efgval.r
Assertion efgi

### Proof

Step Hyp Ref Expression
1 efgval.w ${⊢}{W}=\mathrm{I}\left(\mathrm{Word}\left({I}×{2}_{𝑜}\right)\right)$
2 efgval.r
3 fveq2 ${⊢}{u}={A}\to \left|{u}\right|=\left|{A}\right|$
4 3 oveq2d ${⊢}{u}={A}\to \left(0\dots \left|{u}\right|\right)=\left(0\dots \left|{A}\right|\right)$
5 id ${⊢}{u}={A}\to {u}={A}$
6 oveq1 ${⊢}{u}={A}\to {u}\mathrm{splice}⟨{i},{i},⟨“⟨{a},{b}⟩⟨{a},{1}_{𝑜}\setminus {b}⟩”⟩⟩={A}\mathrm{splice}⟨{i},{i},⟨“⟨{a},{b}⟩⟨{a},{1}_{𝑜}\setminus {b}⟩”⟩⟩$
7 5 6 breq12d ${⊢}{u}={A}\to \left({u}{r}\left({u}\mathrm{splice}⟨{i},{i},⟨“⟨{a},{b}⟩⟨{a},{1}_{𝑜}\setminus {b}⟩”⟩⟩\right)↔{A}{r}\left({A}\mathrm{splice}⟨{i},{i},⟨“⟨{a},{b}⟩⟨{a},{1}_{𝑜}\setminus {b}⟩”⟩⟩\right)\right)$
8 7 2ralbidv ${⊢}{u}={A}\to \left(\forall {a}\in {I}\phantom{\rule{.4em}{0ex}}\forall {b}\in {2}_{𝑜}\phantom{\rule{.4em}{0ex}}{u}{r}\left({u}\mathrm{splice}⟨{i},{i},⟨“⟨{a},{b}⟩⟨{a},{1}_{𝑜}\setminus {b}⟩”⟩⟩\right)↔\forall {a}\in {I}\phantom{\rule{.4em}{0ex}}\forall {b}\in {2}_{𝑜}\phantom{\rule{.4em}{0ex}}{A}{r}\left({A}\mathrm{splice}⟨{i},{i},⟨“⟨{a},{b}⟩⟨{a},{1}_{𝑜}\setminus {b}⟩”⟩⟩\right)\right)$
9 4 8 raleqbidv ${⊢}{u}={A}\to \left(\forall {i}\in \left(0\dots \left|{u}\right|\right)\phantom{\rule{.4em}{0ex}}\forall {a}\in {I}\phantom{\rule{.4em}{0ex}}\forall {b}\in {2}_{𝑜}\phantom{\rule{.4em}{0ex}}{u}{r}\left({u}\mathrm{splice}⟨{i},{i},⟨“⟨{a},{b}⟩⟨{a},{1}_{𝑜}\setminus {b}⟩”⟩⟩\right)↔\forall {i}\in \left(0\dots \left|{A}\right|\right)\phantom{\rule{.4em}{0ex}}\forall {a}\in {I}\phantom{\rule{.4em}{0ex}}\forall {b}\in {2}_{𝑜}\phantom{\rule{.4em}{0ex}}{A}{r}\left({A}\mathrm{splice}⟨{i},{i},⟨“⟨{a},{b}⟩⟨{a},{1}_{𝑜}\setminus {b}⟩”⟩⟩\right)\right)$
10 9 rspcv ${⊢}{A}\in {W}\to \left(\forall {u}\in {W}\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(0\dots \left|{u}\right|\right)\phantom{\rule{.4em}{0ex}}\forall {a}\in {I}\phantom{\rule{.4em}{0ex}}\forall {b}\in {2}_{𝑜}\phantom{\rule{.4em}{0ex}}{u}{r}\left({u}\mathrm{splice}⟨{i},{i},⟨“⟨{a},{b}⟩⟨{a},{1}_{𝑜}\setminus {b}⟩”⟩⟩\right)\to \forall {i}\in \left(0\dots \left|{A}\right|\right)\phantom{\rule{.4em}{0ex}}\forall {a}\in {I}\phantom{\rule{.4em}{0ex}}\forall {b}\in {2}_{𝑜}\phantom{\rule{.4em}{0ex}}{A}{r}\left({A}\mathrm{splice}⟨{i},{i},⟨“⟨{a},{b}⟩⟨{a},{1}_{𝑜}\setminus {b}⟩”⟩⟩\right)\right)$
11 oteq1 ${⊢}{i}={N}\to ⟨{i},{i},⟨“⟨{a},{b}⟩⟨{a},{1}_{𝑜}\setminus {b}⟩”⟩⟩=⟨{N},{i},⟨“⟨{a},{b}⟩⟨{a},{1}_{𝑜}\setminus {b}⟩”⟩⟩$
12 oteq2 ${⊢}{i}={N}\to ⟨{N},{i},⟨“⟨{a},{b}⟩⟨{a},{1}_{𝑜}\setminus {b}⟩”⟩⟩=⟨{N},{N},⟨“⟨{a},{b}⟩⟨{a},{1}_{𝑜}\setminus {b}⟩”⟩⟩$
13 11 12 eqtrd ${⊢}{i}={N}\to ⟨{i},{i},⟨“⟨{a},{b}⟩⟨{a},{1}_{𝑜}\setminus {b}⟩”⟩⟩=⟨{N},{N},⟨“⟨{a},{b}⟩⟨{a},{1}_{𝑜}\setminus {b}⟩”⟩⟩$
14 13 oveq2d ${⊢}{i}={N}\to {A}\mathrm{splice}⟨{i},{i},⟨“⟨{a},{b}⟩⟨{a},{1}_{𝑜}\setminus {b}⟩”⟩⟩={A}\mathrm{splice}⟨{N},{N},⟨“⟨{a},{b}⟩⟨{a},{1}_{𝑜}\setminus {b}⟩”⟩⟩$
15 14 breq2d ${⊢}{i}={N}\to \left({A}{r}\left({A}\mathrm{splice}⟨{i},{i},⟨“⟨{a},{b}⟩⟨{a},{1}_{𝑜}\setminus {b}⟩”⟩⟩\right)↔{A}{r}\left({A}\mathrm{splice}⟨{N},{N},⟨“⟨{a},{b}⟩⟨{a},{1}_{𝑜}\setminus {b}⟩”⟩⟩\right)\right)$
16 15 2ralbidv ${⊢}{i}={N}\to \left(\forall {a}\in {I}\phantom{\rule{.4em}{0ex}}\forall {b}\in {2}_{𝑜}\phantom{\rule{.4em}{0ex}}{A}{r}\left({A}\mathrm{splice}⟨{i},{i},⟨“⟨{a},{b}⟩⟨{a},{1}_{𝑜}\setminus {b}⟩”⟩⟩\right)↔\forall {a}\in {I}\phantom{\rule{.4em}{0ex}}\forall {b}\in {2}_{𝑜}\phantom{\rule{.4em}{0ex}}{A}{r}\left({A}\mathrm{splice}⟨{N},{N},⟨“⟨{a},{b}⟩⟨{a},{1}_{𝑜}\setminus {b}⟩”⟩⟩\right)\right)$
17 16 rspcv ${⊢}{N}\in \left(0\dots \left|{A}\right|\right)\to \left(\forall {i}\in \left(0\dots \left|{A}\right|\right)\phantom{\rule{.4em}{0ex}}\forall {a}\in {I}\phantom{\rule{.4em}{0ex}}\forall {b}\in {2}_{𝑜}\phantom{\rule{.4em}{0ex}}{A}{r}\left({A}\mathrm{splice}⟨{i},{i},⟨“⟨{a},{b}⟩⟨{a},{1}_{𝑜}\setminus {b}⟩”⟩⟩\right)\to \forall {a}\in {I}\phantom{\rule{.4em}{0ex}}\forall {b}\in {2}_{𝑜}\phantom{\rule{.4em}{0ex}}{A}{r}\left({A}\mathrm{splice}⟨{N},{N},⟨“⟨{a},{b}⟩⟨{a},{1}_{𝑜}\setminus {b}⟩”⟩⟩\right)\right)$
18 10 17 sylan9 ${⊢}\left({A}\in {W}\wedge {N}\in \left(0\dots \left|{A}\right|\right)\right)\to \left(\forall {u}\in {W}\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(0\dots \left|{u}\right|\right)\phantom{\rule{.4em}{0ex}}\forall {a}\in {I}\phantom{\rule{.4em}{0ex}}\forall {b}\in {2}_{𝑜}\phantom{\rule{.4em}{0ex}}{u}{r}\left({u}\mathrm{splice}⟨{i},{i},⟨“⟨{a},{b}⟩⟨{a},{1}_{𝑜}\setminus {b}⟩”⟩⟩\right)\to \forall {a}\in {I}\phantom{\rule{.4em}{0ex}}\forall {b}\in {2}_{𝑜}\phantom{\rule{.4em}{0ex}}{A}{r}\left({A}\mathrm{splice}⟨{N},{N},⟨“⟨{a},{b}⟩⟨{a},{1}_{𝑜}\setminus {b}⟩”⟩⟩\right)\right)$
19 opeq1 ${⊢}{a}={J}\to ⟨{a},{b}⟩=⟨{J},{b}⟩$
20 opeq1 ${⊢}{a}={J}\to ⟨{a},{1}_{𝑜}\setminus {b}⟩=⟨{J},{1}_{𝑜}\setminus {b}⟩$
21 19 20 s2eqd ${⊢}{a}={J}\to ⟨“⟨{a},{b}⟩⟨{a},{1}_{𝑜}\setminus {b}⟩”⟩=⟨“⟨{J},{b}⟩⟨{J},{1}_{𝑜}\setminus {b}⟩”⟩$
22 21 oteq3d ${⊢}{a}={J}\to ⟨{N},{N},⟨“⟨{a},{b}⟩⟨{a},{1}_{𝑜}\setminus {b}⟩”⟩⟩=⟨{N},{N},⟨“⟨{J},{b}⟩⟨{J},{1}_{𝑜}\setminus {b}⟩”⟩⟩$
23 22 oveq2d ${⊢}{a}={J}\to {A}\mathrm{splice}⟨{N},{N},⟨“⟨{a},{b}⟩⟨{a},{1}_{𝑜}\setminus {b}⟩”⟩⟩={A}\mathrm{splice}⟨{N},{N},⟨“⟨{J},{b}⟩⟨{J},{1}_{𝑜}\setminus {b}⟩”⟩⟩$
24 23 breq2d ${⊢}{a}={J}\to \left({A}{r}\left({A}\mathrm{splice}⟨{N},{N},⟨“⟨{a},{b}⟩⟨{a},{1}_{𝑜}\setminus {b}⟩”⟩⟩\right)↔{A}{r}\left({A}\mathrm{splice}⟨{N},{N},⟨“⟨{J},{b}⟩⟨{J},{1}_{𝑜}\setminus {b}⟩”⟩⟩\right)\right)$
25 opeq2 ${⊢}{b}={K}\to ⟨{J},{b}⟩=⟨{J},{K}⟩$
26 difeq2 ${⊢}{b}={K}\to {1}_{𝑜}\setminus {b}={1}_{𝑜}\setminus {K}$
27 26 opeq2d ${⊢}{b}={K}\to ⟨{J},{1}_{𝑜}\setminus {b}⟩=⟨{J},{1}_{𝑜}\setminus {K}⟩$
28 25 27 s2eqd ${⊢}{b}={K}\to ⟨“⟨{J},{b}⟩⟨{J},{1}_{𝑜}\setminus {b}⟩”⟩=⟨“⟨{J},{K}⟩⟨{J},{1}_{𝑜}\setminus {K}⟩”⟩$
29 28 oteq3d ${⊢}{b}={K}\to ⟨{N},{N},⟨“⟨{J},{b}⟩⟨{J},{1}_{𝑜}\setminus {b}⟩”⟩⟩=⟨{N},{N},⟨“⟨{J},{K}⟩⟨{J},{1}_{𝑜}\setminus {K}⟩”⟩⟩$
30 29 oveq2d ${⊢}{b}={K}\to {A}\mathrm{splice}⟨{N},{N},⟨“⟨{J},{b}⟩⟨{J},{1}_{𝑜}\setminus {b}⟩”⟩⟩={A}\mathrm{splice}⟨{N},{N},⟨“⟨{J},{K}⟩⟨{J},{1}_{𝑜}\setminus {K}⟩”⟩⟩$
31 30 breq2d ${⊢}{b}={K}\to \left({A}{r}\left({A}\mathrm{splice}⟨{N},{N},⟨“⟨{J},{b}⟩⟨{J},{1}_{𝑜}\setminus {b}⟩”⟩⟩\right)↔{A}{r}\left({A}\mathrm{splice}⟨{N},{N},⟨“⟨{J},{K}⟩⟨{J},{1}_{𝑜}\setminus {K}⟩”⟩⟩\right)\right)$
32 df-br ${⊢}{A}{r}\left({A}\mathrm{splice}⟨{N},{N},⟨“⟨{J},{K}⟩⟨{J},{1}_{𝑜}\setminus {K}⟩”⟩⟩\right)↔⟨{A},{A}\mathrm{splice}⟨{N},{N},⟨“⟨{J},{K}⟩⟨{J},{1}_{𝑜}\setminus {K}⟩”⟩⟩⟩\in {r}$
33 31 32 syl6bb ${⊢}{b}={K}\to \left({A}{r}\left({A}\mathrm{splice}⟨{N},{N},⟨“⟨{J},{b}⟩⟨{J},{1}_{𝑜}\setminus {b}⟩”⟩⟩\right)↔⟨{A},{A}\mathrm{splice}⟨{N},{N},⟨“⟨{J},{K}⟩⟨{J},{1}_{𝑜}\setminus {K}⟩”⟩⟩⟩\in {r}\right)$
34 24 33 rspc2v ${⊢}\left({J}\in {I}\wedge {K}\in {2}_{𝑜}\right)\to \left(\forall {a}\in {I}\phantom{\rule{.4em}{0ex}}\forall {b}\in {2}_{𝑜}\phantom{\rule{.4em}{0ex}}{A}{r}\left({A}\mathrm{splice}⟨{N},{N},⟨“⟨{a},{b}⟩⟨{a},{1}_{𝑜}\setminus {b}⟩”⟩⟩\right)\to ⟨{A},{A}\mathrm{splice}⟨{N},{N},⟨“⟨{J},{K}⟩⟨{J},{1}_{𝑜}\setminus {K}⟩”⟩⟩⟩\in {r}\right)$
35 18 34 sylan9 ${⊢}\left(\left({A}\in {W}\wedge {N}\in \left(0\dots \left|{A}\right|\right)\right)\wedge \left({J}\in {I}\wedge {K}\in {2}_{𝑜}\right)\right)\to \left(\forall {u}\in {W}\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(0\dots \left|{u}\right|\right)\phantom{\rule{.4em}{0ex}}\forall {a}\in {I}\phantom{\rule{.4em}{0ex}}\forall {b}\in {2}_{𝑜}\phantom{\rule{.4em}{0ex}}{u}{r}\left({u}\mathrm{splice}⟨{i},{i},⟨“⟨{a},{b}⟩⟨{a},{1}_{𝑜}\setminus {b}⟩”⟩⟩\right)\to ⟨{A},{A}\mathrm{splice}⟨{N},{N},⟨“⟨{J},{K}⟩⟨{J},{1}_{𝑜}\setminus {K}⟩”⟩⟩⟩\in {r}\right)$
36 35 adantld ${⊢}\left(\left({A}\in {W}\wedge {N}\in \left(0\dots \left|{A}\right|\right)\right)\wedge \left({J}\in {I}\wedge {K}\in {2}_{𝑜}\right)\right)\to \left(\left({r}\mathrm{Er}{W}\wedge \forall {u}\in {W}\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(0\dots \left|{u}\right|\right)\phantom{\rule{.4em}{0ex}}\forall {a}\in {I}\phantom{\rule{.4em}{0ex}}\forall {b}\in {2}_{𝑜}\phantom{\rule{.4em}{0ex}}{u}{r}\left({u}\mathrm{splice}⟨{i},{i},⟨“⟨{a},{b}⟩⟨{a},{1}_{𝑜}\setminus {b}⟩”⟩⟩\right)\right)\to ⟨{A},{A}\mathrm{splice}⟨{N},{N},⟨“⟨{J},{K}⟩⟨{J},{1}_{𝑜}\setminus {K}⟩”⟩⟩⟩\in {r}\right)$
37 36 alrimiv ${⊢}\left(\left({A}\in {W}\wedge {N}\in \left(0\dots \left|{A}\right|\right)\right)\wedge \left({J}\in {I}\wedge {K}\in {2}_{𝑜}\right)\right)\to \forall {r}\phantom{\rule{.4em}{0ex}}\left(\left({r}\mathrm{Er}{W}\wedge \forall {u}\in {W}\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(0\dots \left|{u}\right|\right)\phantom{\rule{.4em}{0ex}}\forall {a}\in {I}\phantom{\rule{.4em}{0ex}}\forall {b}\in {2}_{𝑜}\phantom{\rule{.4em}{0ex}}{u}{r}\left({u}\mathrm{splice}⟨{i},{i},⟨“⟨{a},{b}⟩⟨{a},{1}_{𝑜}\setminus {b}⟩”⟩⟩\right)\right)\to ⟨{A},{A}\mathrm{splice}⟨{N},{N},⟨“⟨{J},{K}⟩⟨{J},{1}_{𝑜}\setminus {K}⟩”⟩⟩⟩\in {r}\right)$
38 opex ${⊢}⟨{A},{A}\mathrm{splice}⟨{N},{N},⟨“⟨{J},{K}⟩⟨{J},{1}_{𝑜}\setminus {K}⟩”⟩⟩⟩\in \mathrm{V}$
39 38 elintab ${⊢}⟨{A},{A}\mathrm{splice}⟨{N},{N},⟨“⟨{J},{K}⟩⟨{J},{1}_{𝑜}\setminus {K}⟩”⟩⟩⟩\in \bigcap \left\{{r}|\left({r}\mathrm{Er}{W}\wedge \forall {u}\in {W}\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(0\dots \left|{u}\right|\right)\phantom{\rule{.4em}{0ex}}\forall {a}\in {I}\phantom{\rule{.4em}{0ex}}\forall {b}\in {2}_{𝑜}\phantom{\rule{.4em}{0ex}}{u}{r}\left({u}\mathrm{splice}⟨{i},{i},⟨“⟨{a},{b}⟩⟨{a},{1}_{𝑜}\setminus {b}⟩”⟩⟩\right)\right)\right\}↔\forall {r}\phantom{\rule{.4em}{0ex}}\left(\left({r}\mathrm{Er}{W}\wedge \forall {u}\in {W}\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(0\dots \left|{u}\right|\right)\phantom{\rule{.4em}{0ex}}\forall {a}\in {I}\phantom{\rule{.4em}{0ex}}\forall {b}\in {2}_{𝑜}\phantom{\rule{.4em}{0ex}}{u}{r}\left({u}\mathrm{splice}⟨{i},{i},⟨“⟨{a},{b}⟩⟨{a},{1}_{𝑜}\setminus {b}⟩”⟩⟩\right)\right)\to ⟨{A},{A}\mathrm{splice}⟨{N},{N},⟨“⟨{J},{K}⟩⟨{J},{1}_{𝑜}\setminus {K}⟩”⟩⟩⟩\in {r}\right)$
40 37 39 sylibr ${⊢}\left(\left({A}\in {W}\wedge {N}\in \left(0\dots \left|{A}\right|\right)\right)\wedge \left({J}\in {I}\wedge {K}\in {2}_{𝑜}\right)\right)\to ⟨{A},{A}\mathrm{splice}⟨{N},{N},⟨“⟨{J},{K}⟩⟨{J},{1}_{𝑜}\setminus {K}⟩”⟩⟩⟩\in \bigcap \left\{{r}|\left({r}\mathrm{Er}{W}\wedge \forall {u}\in {W}\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(0\dots \left|{u}\right|\right)\phantom{\rule{.4em}{0ex}}\forall {a}\in {I}\phantom{\rule{.4em}{0ex}}\forall {b}\in {2}_{𝑜}\phantom{\rule{.4em}{0ex}}{u}{r}\left({u}\mathrm{splice}⟨{i},{i},⟨“⟨{a},{b}⟩⟨{a},{1}_{𝑜}\setminus {b}⟩”⟩⟩\right)\right)\right\}$
41 1 2 efgval
42 40 41 eleqtrrdi
43 df-br
44 42 43 sylibr