# Metamath Proof Explorer

## Theorem frgp0

Description: The free group is a group. (Contributed by Mario Carneiro, 1-Oct-2015) (Revised by Mario Carneiro, 27-Feb-2016)

Ref Expression
Hypotheses frgp0.m ${⊢}{G}=\mathrm{freeGrp}\left({I}\right)$
frgp0.r
Assertion frgp0

### Proof

Step Hyp Ref Expression
1 frgp0.m ${⊢}{G}=\mathrm{freeGrp}\left({I}\right)$
2 frgp0.r
3 eqid ${⊢}\mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)=\mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)$
4 1 3 2 frgpval
5 2on ${⊢}{2}_{𝑜}\in \mathrm{On}$
6 xpexg ${⊢}\left({I}\in {V}\wedge {2}_{𝑜}\in \mathrm{On}\right)\to {I}×{2}_{𝑜}\in \mathrm{V}$
7 5 6 mpan2 ${⊢}{I}\in {V}\to {I}×{2}_{𝑜}\in \mathrm{V}$
8 eqid ${⊢}{\mathrm{Base}}_{\mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)}={\mathrm{Base}}_{\mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)}$
9 3 8 frmdbas ${⊢}{I}×{2}_{𝑜}\in \mathrm{V}\to {\mathrm{Base}}_{\mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)}=\mathrm{Word}\left({I}×{2}_{𝑜}\right)$
10 7 9 syl ${⊢}{I}\in {V}\to {\mathrm{Base}}_{\mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)}=\mathrm{Word}\left({I}×{2}_{𝑜}\right)$
11 10 eqcomd ${⊢}{I}\in {V}\to \mathrm{Word}\left({I}×{2}_{𝑜}\right)={\mathrm{Base}}_{\mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)}$
12 eqidd ${⊢}{I}\in {V}\to {+}_{\mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)}={+}_{\mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)}$
13 eqid ${⊢}\mathrm{I}\left(\mathrm{Word}\left({I}×{2}_{𝑜}\right)\right)=\mathrm{I}\left(\mathrm{Word}\left({I}×{2}_{𝑜}\right)\right)$
14 13 2 efger
15 wrdexg ${⊢}{I}×{2}_{𝑜}\in \mathrm{V}\to \mathrm{Word}\left({I}×{2}_{𝑜}\right)\in \mathrm{V}$
16 fvi ${⊢}\mathrm{Word}\left({I}×{2}_{𝑜}\right)\in \mathrm{V}\to \mathrm{I}\left(\mathrm{Word}\left({I}×{2}_{𝑜}\right)\right)=\mathrm{Word}\left({I}×{2}_{𝑜}\right)$
17 7 15 16 3syl ${⊢}{I}\in {V}\to \mathrm{I}\left(\mathrm{Word}\left({I}×{2}_{𝑜}\right)\right)=\mathrm{Word}\left({I}×{2}_{𝑜}\right)$
18 ereq2
19 17 18 syl
20 14 19 mpbii
21 fvexd ${⊢}{I}\in {V}\to \mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)\in \mathrm{V}$
22 eqid ${⊢}{+}_{\mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)}={+}_{\mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)}$
23 1 3 2 22 frgpcpbl
24 23 a1i
25 3 frmdmnd ${⊢}{I}×{2}_{𝑜}\in \mathrm{V}\to \mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)\in \mathrm{Mnd}$
26 7 25 syl ${⊢}{I}\in {V}\to \mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)\in \mathrm{Mnd}$
27 26 3ad2ant1 ${⊢}\left({I}\in {V}\wedge {x}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\wedge {y}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\right)\to \mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)\in \mathrm{Mnd}$
28 simp2 ${⊢}\left({I}\in {V}\wedge {x}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\wedge {y}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\right)\to {x}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)$
29 11 3ad2ant1 ${⊢}\left({I}\in {V}\wedge {x}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\wedge {y}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\right)\to \mathrm{Word}\left({I}×{2}_{𝑜}\right)={\mathrm{Base}}_{\mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)}$
30 28 29 eleqtrd ${⊢}\left({I}\in {V}\wedge {x}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\wedge {y}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\right)\to {x}\in {\mathrm{Base}}_{\mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)}$
31 simp3 ${⊢}\left({I}\in {V}\wedge {x}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\wedge {y}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\right)\to {y}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)$
32 31 29 eleqtrd ${⊢}\left({I}\in {V}\wedge {x}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\wedge {y}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\right)\to {y}\in {\mathrm{Base}}_{\mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)}$
33 8 22 mndcl ${⊢}\left(\mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)\in \mathrm{Mnd}\wedge {x}\in {\mathrm{Base}}_{\mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)}\wedge {y}\in {\mathrm{Base}}_{\mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)}\right)\to {x}{+}_{\mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)}{y}\in {\mathrm{Base}}_{\mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)}$
34 27 30 32 33 syl3anc ${⊢}\left({I}\in {V}\wedge {x}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\wedge {y}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\right)\to {x}{+}_{\mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)}{y}\in {\mathrm{Base}}_{\mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)}$
35 34 29 eleqtrrd ${⊢}\left({I}\in {V}\wedge {x}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\wedge {y}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\right)\to {x}{+}_{\mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)}{y}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)$
37 26 adantr ${⊢}\left({I}\in {V}\wedge \left({x}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\wedge {y}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\wedge {z}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\right)\right)\to \mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)\in \mathrm{Mnd}$
38 34 3adant3r3 ${⊢}\left({I}\in {V}\wedge \left({x}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\wedge {y}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\wedge {z}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\right)\right)\to {x}{+}_{\mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)}{y}\in {\mathrm{Base}}_{\mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)}$
39 simpr3 ${⊢}\left({I}\in {V}\wedge \left({x}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\wedge {y}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\wedge {z}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\right)\right)\to {z}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)$
40 11 adantr ${⊢}\left({I}\in {V}\wedge \left({x}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\wedge {y}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\wedge {z}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\right)\right)\to \mathrm{Word}\left({I}×{2}_{𝑜}\right)={\mathrm{Base}}_{\mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)}$
41 39 40 eleqtrd ${⊢}\left({I}\in {V}\wedge \left({x}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\wedge {y}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\wedge {z}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\right)\right)\to {z}\in {\mathrm{Base}}_{\mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)}$
42 8 22 mndcl ${⊢}\left(\mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)\in \mathrm{Mnd}\wedge {x}{+}_{\mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)}{y}\in {\mathrm{Base}}_{\mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)}\wedge {z}\in {\mathrm{Base}}_{\mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)}\right)\to \left({x}{+}_{\mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)}{y}\right){+}_{\mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)}{z}\in {\mathrm{Base}}_{\mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)}$
43 37 38 41 42 syl3anc ${⊢}\left({I}\in {V}\wedge \left({x}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\wedge {y}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\wedge {z}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\right)\right)\to \left({x}{+}_{\mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)}{y}\right){+}_{\mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)}{z}\in {\mathrm{Base}}_{\mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)}$
44 43 40 eleqtrrd ${⊢}\left({I}\in {V}\wedge \left({x}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\wedge {y}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\wedge {z}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\right)\right)\to \left({x}{+}_{\mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)}{y}\right){+}_{\mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)}{z}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)$
45 36 44 erref
46 30 3adant3r3 ${⊢}\left({I}\in {V}\wedge \left({x}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\wedge {y}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\wedge {z}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\right)\right)\to {x}\in {\mathrm{Base}}_{\mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)}$
47 32 3adant3r3 ${⊢}\left({I}\in {V}\wedge \left({x}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\wedge {y}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\wedge {z}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\right)\right)\to {y}\in {\mathrm{Base}}_{\mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)}$
48 8 22 mndass ${⊢}\left(\mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)\in \mathrm{Mnd}\wedge \left({x}\in {\mathrm{Base}}_{\mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)}\wedge {y}\in {\mathrm{Base}}_{\mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)}\wedge {z}\in {\mathrm{Base}}_{\mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)}\right)\right)\to \left({x}{+}_{\mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)}{y}\right){+}_{\mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)}{z}={x}{+}_{\mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)}\left({y}{+}_{\mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)}{z}\right)$
49 37 46 47 41 48 syl13anc ${⊢}\left({I}\in {V}\wedge \left({x}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\wedge {y}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\wedge {z}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\right)\right)\to \left({x}{+}_{\mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)}{y}\right){+}_{\mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)}{z}={x}{+}_{\mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)}\left({y}{+}_{\mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)}{z}\right)$
50 45 49 breqtrd
51 wrd0 ${⊢}\varnothing \in \mathrm{Word}\left({I}×{2}_{𝑜}\right)$
52 51 a1i ${⊢}{I}\in {V}\to \varnothing \in \mathrm{Word}\left({I}×{2}_{𝑜}\right)$
53 51 11 eleqtrid ${⊢}{I}\in {V}\to \varnothing \in {\mathrm{Base}}_{\mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)}$
54 53 adantr ${⊢}\left({I}\in {V}\wedge {x}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\right)\to \varnothing \in {\mathrm{Base}}_{\mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)}$
55 11 eleq2d ${⊢}{I}\in {V}\to \left({x}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)↔{x}\in {\mathrm{Base}}_{\mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)}\right)$
56 55 biimpa ${⊢}\left({I}\in {V}\wedge {x}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\right)\to {x}\in {\mathrm{Base}}_{\mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)}$
57 3 8 22 frmdadd ${⊢}\left(\varnothing \in {\mathrm{Base}}_{\mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)}\wedge {x}\in {\mathrm{Base}}_{\mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)}\right)\to \varnothing {+}_{\mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)}{x}=\varnothing \mathrm{++}{x}$
58 54 56 57 syl2anc ${⊢}\left({I}\in {V}\wedge {x}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\right)\to \varnothing {+}_{\mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)}{x}=\varnothing \mathrm{++}{x}$
59 ccatlid ${⊢}{x}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\to \varnothing \mathrm{++}{x}={x}$
60 59 adantl ${⊢}\left({I}\in {V}\wedge {x}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\right)\to \varnothing \mathrm{++}{x}={x}$
61 58 60 eqtrd ${⊢}\left({I}\in {V}\wedge {x}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\right)\to \varnothing {+}_{\mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)}{x}={x}$
63 simpr ${⊢}\left({I}\in {V}\wedge {x}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\right)\to {x}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)$
64 62 63 erref
65 61 64 eqbrtrd
66 revcl ${⊢}{x}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\to \mathrm{reverse}\left({x}\right)\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)$
67 66 adantl ${⊢}\left({I}\in {V}\wedge {x}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\right)\to \mathrm{reverse}\left({x}\right)\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)$
68 eqid ${⊢}\left({y}\in {I},{z}\in {2}_{𝑜}⟼⟨{y},{1}_{𝑜}\setminus {z}⟩\right)=\left({y}\in {I},{z}\in {2}_{𝑜}⟼⟨{y},{1}_{𝑜}\setminus {z}⟩\right)$
69 68 efgmf ${⊢}\left({y}\in {I},{z}\in {2}_{𝑜}⟼⟨{y},{1}_{𝑜}\setminus {z}⟩\right):{I}×{2}_{𝑜}⟶{I}×{2}_{𝑜}$
70 69 a1i ${⊢}\left({I}\in {V}\wedge {x}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\right)\to \left({y}\in {I},{z}\in {2}_{𝑜}⟼⟨{y},{1}_{𝑜}\setminus {z}⟩\right):{I}×{2}_{𝑜}⟶{I}×{2}_{𝑜}$
71 wrdco ${⊢}\left(\mathrm{reverse}\left({x}\right)\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\wedge \left({y}\in {I},{z}\in {2}_{𝑜}⟼⟨{y},{1}_{𝑜}\setminus {z}⟩\right):{I}×{2}_{𝑜}⟶{I}×{2}_{𝑜}\right)\to \left({y}\in {I},{z}\in {2}_{𝑜}⟼⟨{y},{1}_{𝑜}\setminus {z}⟩\right)\circ \mathrm{reverse}\left({x}\right)\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)$
72 67 70 71 syl2anc ${⊢}\left({I}\in {V}\wedge {x}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\right)\to \left({y}\in {I},{z}\in {2}_{𝑜}⟼⟨{y},{1}_{𝑜}\setminus {z}⟩\right)\circ \mathrm{reverse}\left({x}\right)\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)$
73 11 adantr ${⊢}\left({I}\in {V}\wedge {x}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\right)\to \mathrm{Word}\left({I}×{2}_{𝑜}\right)={\mathrm{Base}}_{\mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)}$
74 72 73 eleqtrd ${⊢}\left({I}\in {V}\wedge {x}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\right)\to \left({y}\in {I},{z}\in {2}_{𝑜}⟼⟨{y},{1}_{𝑜}\setminus {z}⟩\right)\circ \mathrm{reverse}\left({x}\right)\in {\mathrm{Base}}_{\mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)}$
75 3 8 22 frmdadd ${⊢}\left(\left({y}\in {I},{z}\in {2}_{𝑜}⟼⟨{y},{1}_{𝑜}\setminus {z}⟩\right)\circ \mathrm{reverse}\left({x}\right)\in {\mathrm{Base}}_{\mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)}\wedge {x}\in {\mathrm{Base}}_{\mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)}\right)\to \left(\left({y}\in {I},{z}\in {2}_{𝑜}⟼⟨{y},{1}_{𝑜}\setminus {z}⟩\right)\circ \mathrm{reverse}\left({x}\right)\right){+}_{\mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)}{x}=\left(\left({y}\in {I},{z}\in {2}_{𝑜}⟼⟨{y},{1}_{𝑜}\setminus {z}⟩\right)\circ \mathrm{reverse}\left({x}\right)\right)\mathrm{++}{x}$
76 74 56 75 syl2anc ${⊢}\left({I}\in {V}\wedge {x}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\right)\to \left(\left({y}\in {I},{z}\in {2}_{𝑜}⟼⟨{y},{1}_{𝑜}\setminus {z}⟩\right)\circ \mathrm{reverse}\left({x}\right)\right){+}_{\mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)}{x}=\left(\left({y}\in {I},{z}\in {2}_{𝑜}⟼⟨{y},{1}_{𝑜}\setminus {z}⟩\right)\circ \mathrm{reverse}\left({x}\right)\right)\mathrm{++}{x}$
77 17 eleq2d ${⊢}{I}\in {V}\to \left({x}\in \mathrm{I}\left(\mathrm{Word}\left({I}×{2}_{𝑜}\right)\right)↔{x}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\right)$
78 77 biimpar ${⊢}\left({I}\in {V}\wedge {x}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\right)\to {x}\in \mathrm{I}\left(\mathrm{Word}\left({I}×{2}_{𝑜}\right)\right)$
79 eqid ${⊢}\left({v}\in \mathrm{I}\left(\mathrm{Word}\left({I}×{2}_{𝑜}\right)\right)⟼\left({n}\in \left(0\dots \left|{v}\right|\right),{w}\in \left({I}×{2}_{𝑜}\right)⟼{v}\mathrm{splice}⟨{n},{n},⟨“{w}\left({y}\in {I},{z}\in {2}_{𝑜}⟼⟨{y},{1}_{𝑜}\setminus {z}⟩\right)\left({w}\right)”⟩⟩\right)\right)=\left({v}\in \mathrm{I}\left(\mathrm{Word}\left({I}×{2}_{𝑜}\right)\right)⟼\left({n}\in \left(0\dots \left|{v}\right|\right),{w}\in \left({I}×{2}_{𝑜}\right)⟼{v}\mathrm{splice}⟨{n},{n},⟨“{w}\left({y}\in {I},{z}\in {2}_{𝑜}⟼⟨{y},{1}_{𝑜}\setminus {z}⟩\right)\left({w}\right)”⟩⟩\right)\right)$
80 13 2 68 79 efginvrel1
81 78 80 syl
82 76 81 eqbrtrd
83 4 11 12 20 21 24 35 50 52 65 72 82 qusgrp2