# Metamath Proof Explorer

Description: Addition in the free group is given by concatenation. (Contributed by Mario Carneiro, 1-Oct-2015)

Ref Expression
Hypotheses frgpadd.w ${⊢}{W}=\mathrm{I}\left(\mathrm{Word}\left({I}×{2}_{𝑜}\right)\right)$
frgpadd.g ${⊢}{G}=\mathrm{freeGrp}\left({I}\right)$

### Proof

Step Hyp Ref Expression
1 frgpadd.w ${⊢}{W}=\mathrm{I}\left(\mathrm{Word}\left({I}×{2}_{𝑜}\right)\right)$
2 frgpadd.g ${⊢}{G}=\mathrm{freeGrp}\left({I}\right)$
5 simpl ${⊢}\left({A}\in {W}\wedge {B}\in {W}\right)\to {A}\in {W}$
6 simpr ${⊢}\left({A}\in {W}\wedge {B}\in {W}\right)\to {B}\in {W}$
7 1 efgrcl ${⊢}{A}\in {W}\to \left({I}\in \mathrm{V}\wedge {W}=\mathrm{Word}\left({I}×{2}_{𝑜}\right)\right)$
8 7 adantr ${⊢}\left({A}\in {W}\wedge {B}\in {W}\right)\to \left({I}\in \mathrm{V}\wedge {W}=\mathrm{Word}\left({I}×{2}_{𝑜}\right)\right)$
9 8 simpld ${⊢}\left({A}\in {W}\wedge {B}\in {W}\right)\to {I}\in \mathrm{V}$
10 eqid ${⊢}\mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)=\mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)$
11 2 10 3 frgpval
12 9 11 syl
13 8 simprd ${⊢}\left({A}\in {W}\wedge {B}\in {W}\right)\to {W}=\mathrm{Word}\left({I}×{2}_{𝑜}\right)$
14 2on ${⊢}{2}_{𝑜}\in \mathrm{On}$
15 xpexg ${⊢}\left({I}\in \mathrm{V}\wedge {2}_{𝑜}\in \mathrm{On}\right)\to {I}×{2}_{𝑜}\in \mathrm{V}$
16 9 14 15 sylancl ${⊢}\left({A}\in {W}\wedge {B}\in {W}\right)\to {I}×{2}_{𝑜}\in \mathrm{V}$
17 eqid ${⊢}{\mathrm{Base}}_{\mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)}={\mathrm{Base}}_{\mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)}$
18 10 17 frmdbas ${⊢}{I}×{2}_{𝑜}\in \mathrm{V}\to {\mathrm{Base}}_{\mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)}=\mathrm{Word}\left({I}×{2}_{𝑜}\right)$
19 16 18 syl ${⊢}\left({A}\in {W}\wedge {B}\in {W}\right)\to {\mathrm{Base}}_{\mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)}=\mathrm{Word}\left({I}×{2}_{𝑜}\right)$
20 13 19 eqtr4d ${⊢}\left({A}\in {W}\wedge {B}\in {W}\right)\to {W}={\mathrm{Base}}_{\mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)}$
21 1 3 efger
22 21 a1i
23 10 frmdmnd ${⊢}{I}×{2}_{𝑜}\in \mathrm{V}\to \mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)\in \mathrm{Mnd}$
24 16 23 syl ${⊢}\left({A}\in {W}\wedge {B}\in {W}\right)\to \mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)\in \mathrm{Mnd}$
25 eqid ${⊢}{+}_{\mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)}={+}_{\mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)}$
26 2 10 3 25 frgpcpbl
27 26 a1i
28 24 adantr ${⊢}\left(\left({A}\in {W}\wedge {B}\in {W}\right)\wedge \left({b}\in {W}\wedge {d}\in {W}\right)\right)\to \mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)\in \mathrm{Mnd}$
29 simprl ${⊢}\left(\left({A}\in {W}\wedge {B}\in {W}\right)\wedge \left({b}\in {W}\wedge {d}\in {W}\right)\right)\to {b}\in {W}$
30 20 adantr ${⊢}\left(\left({A}\in {W}\wedge {B}\in {W}\right)\wedge \left({b}\in {W}\wedge {d}\in {W}\right)\right)\to {W}={\mathrm{Base}}_{\mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)}$
31 29 30 eleqtrd ${⊢}\left(\left({A}\in {W}\wedge {B}\in {W}\right)\wedge \left({b}\in {W}\wedge {d}\in {W}\right)\right)\to {b}\in {\mathrm{Base}}_{\mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)}$
32 simprr ${⊢}\left(\left({A}\in {W}\wedge {B}\in {W}\right)\wedge \left({b}\in {W}\wedge {d}\in {W}\right)\right)\to {d}\in {W}$
33 32 30 eleqtrd ${⊢}\left(\left({A}\in {W}\wedge {B}\in {W}\right)\wedge \left({b}\in {W}\wedge {d}\in {W}\right)\right)\to {d}\in {\mathrm{Base}}_{\mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)}$
34 17 25 mndcl ${⊢}\left(\mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)\in \mathrm{Mnd}\wedge {b}\in {\mathrm{Base}}_{\mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)}\wedge {d}\in {\mathrm{Base}}_{\mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)}\right)\to {b}{+}_{\mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)}{d}\in {\mathrm{Base}}_{\mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)}$
35 28 31 33 34 syl3anc ${⊢}\left(\left({A}\in {W}\wedge {B}\in {W}\right)\wedge \left({b}\in {W}\wedge {d}\in {W}\right)\right)\to {b}{+}_{\mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)}{d}\in {\mathrm{Base}}_{\mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)}$
36 35 30 eleqtrrd ${⊢}\left(\left({A}\in {W}\wedge {B}\in {W}\right)\wedge \left({b}\in {W}\wedge {d}\in {W}\right)\right)\to {b}{+}_{\mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)}{d}\in {W}$
37 12 20 22 24 27 36 25 4 qusaddval
38 5 6 37 mpd3an23
39 5 20 eleqtrd ${⊢}\left({A}\in {W}\wedge {B}\in {W}\right)\to {A}\in {\mathrm{Base}}_{\mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)}$
40 6 20 eleqtrd ${⊢}\left({A}\in {W}\wedge {B}\in {W}\right)\to {B}\in {\mathrm{Base}}_{\mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)}$
41 10 17 25 frmdadd ${⊢}\left({A}\in {\mathrm{Base}}_{\mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)}\wedge {B}\in {\mathrm{Base}}_{\mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)}\right)\to {A}{+}_{\mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)}{B}={A}\mathrm{++}{B}$
42 39 40 41 syl2anc ${⊢}\left({A}\in {W}\wedge {B}\in {W}\right)\to {A}{+}_{\mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)}{B}={A}\mathrm{++}{B}$
43 42 eceq1d
44 38 43 eqtrd