Metamath Proof Explorer

Theorem frgpadd

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

Ref Expression
Hypotheses frgpadd.w ⊒W=I⁑WordIΓ—2π‘œ
frgpadd.g ⊒G=freeGrp⁑I
frgpadd.r βŠ’βˆΌΛ™=~FG⁑I
frgpadd.n ⊒+Λ™=+G
Assertion frgpadd ⊒A∈W∧B∈Wβ†’AβˆΌΛ™+Λ™BβˆΌΛ™=A++BβˆΌΛ™

Proof

Step Hyp Ref Expression
1 frgpadd.w ⊒W=I⁑WordIΓ—2π‘œ
2 frgpadd.g ⊒G=freeGrp⁑I
3 frgpadd.r βŠ’βˆΌΛ™=~FG⁑I
4 frgpadd.n ⊒+Λ™=+G
5 simpl ⊒A∈W∧B∈Wβ†’A∈W
6 simpr ⊒A∈W∧B∈Wβ†’B∈W
7 1 efgrcl ⊒A∈Wβ†’I∈V∧W=WordIΓ—2π‘œ
8 7 adantr ⊒A∈W∧B∈Wβ†’I∈V∧W=WordIΓ—2π‘œ
9 8 simpld ⊒A∈W∧B∈Wβ†’I∈V
10 eqid ⊒freeMnd⁑IΓ—2π‘œ=freeMnd⁑IΓ—2π‘œ
11 2 10 3 frgpval ⊒I∈Vβ†’G=freeMnd⁑IΓ—2π‘œ/π‘ βˆΌΛ™
12 9 11 syl ⊒A∈W∧B∈Wβ†’G=freeMnd⁑IΓ—2π‘œ/π‘ βˆΌΛ™
13 8 simprd ⊒A∈W∧B∈Wβ†’W=WordIΓ—2π‘œ
14 2on ⊒2π‘œβˆˆOn
15 xpexg ⊒I∈V∧2π‘œβˆˆOnβ†’IΓ—2π‘œβˆˆV
16 9 14 15 sylancl ⊒A∈W∧B∈Wβ†’IΓ—2π‘œβˆˆV
17 eqid ⊒BasefreeMnd⁑IΓ—2π‘œ=BasefreeMnd⁑IΓ—2π‘œ
18 10 17 frmdbas ⊒IΓ—2π‘œβˆˆVβ†’BasefreeMnd⁑IΓ—2π‘œ=WordIΓ—2π‘œ
19 16 18 syl ⊒A∈W∧B∈Wβ†’BasefreeMnd⁑IΓ—2π‘œ=WordIΓ—2π‘œ
20 13 19 eqtr4d ⊒A∈W∧B∈Wβ†’W=BasefreeMnd⁑IΓ—2π‘œ
21 1 3 efger βŠ’βˆΌΛ™ErW
22 21 a1i ⊒A∈W∧B∈Wβ†’βˆΌΛ™ErW
23 10 frmdmnd ⊒IΓ—2π‘œβˆˆVβ†’freeMnd⁑IΓ—2π‘œβˆˆMnd
24 16 23 syl ⊒A∈W∧B∈Wβ†’freeMnd⁑IΓ—2π‘œβˆˆMnd
25 eqid ⊒+freeMnd⁑IΓ—2π‘œ=+freeMnd⁑IΓ—2π‘œ
26 2 10 3 25 frgpcpbl ⊒aβˆΌΛ™b∧cβˆΌΛ™dβ†’a+freeMnd⁑IΓ—2π‘œcβˆΌΛ™b+freeMnd⁑IΓ—2π‘œd
27 26 a1i ⊒A∈W∧B∈Wβ†’aβˆΌΛ™b∧cβˆΌΛ™dβ†’a+freeMnd⁑IΓ—2π‘œcβˆΌΛ™b+freeMnd⁑IΓ—2π‘œd
28 24 adantr ⊒A∈W∧B∈W∧b∈W∧d∈Wβ†’freeMnd⁑IΓ—2π‘œβˆˆMnd
29 simprl ⊒A∈W∧B∈W∧b∈W∧d∈Wβ†’b∈W
30 20 adantr ⊒A∈W∧B∈W∧b∈W∧d∈Wβ†’W=BasefreeMnd⁑IΓ—2π‘œ
31 29 30 eleqtrd ⊒A∈W∧B∈W∧b∈W∧d∈Wβ†’b∈BasefreeMnd⁑IΓ—2π‘œ
32 simprr ⊒A∈W∧B∈W∧b∈W∧d∈Wβ†’d∈W
33 32 30 eleqtrd ⊒A∈W∧B∈W∧b∈W∧d∈Wβ†’d∈BasefreeMnd⁑IΓ—2π‘œ
34 17 25 mndcl ⊒freeMnd⁑IΓ—2π‘œβˆˆMnd∧b∈BasefreeMnd⁑IΓ—2π‘œβˆ§d∈BasefreeMnd⁑IΓ—2π‘œβ†’b+freeMnd⁑IΓ—2π‘œd∈BasefreeMnd⁑IΓ—2π‘œ
35 28 31 33 34 syl3anc ⊒A∈W∧B∈W∧b∈W∧d∈Wβ†’b+freeMnd⁑IΓ—2π‘œd∈BasefreeMnd⁑IΓ—2π‘œ
36 35 30 eleqtrrd ⊒A∈W∧B∈W∧b∈W∧d∈Wβ†’b+freeMnd⁑IΓ—2π‘œd∈W
37 12 20 22 24 27 36 25 4 qusaddval ⊒A∈W∧B∈W∧A∈W∧B∈Wβ†’AβˆΌΛ™+Λ™BβˆΌΛ™=A+freeMnd⁑IΓ—2π‘œBβˆΌΛ™
38 5 6 37 mpd3an23 ⊒A∈W∧B∈Wβ†’AβˆΌΛ™+Λ™BβˆΌΛ™=A+freeMnd⁑IΓ—2π‘œBβˆΌΛ™
39 5 20 eleqtrd ⊒A∈W∧B∈Wβ†’A∈BasefreeMnd⁑IΓ—2π‘œ
40 6 20 eleqtrd ⊒A∈W∧B∈Wβ†’B∈BasefreeMnd⁑IΓ—2π‘œ
41 10 17 25 frmdadd ⊒A∈BasefreeMnd⁑IΓ—2π‘œβˆ§B∈BasefreeMnd⁑IΓ—2π‘œβ†’A+freeMnd⁑IΓ—2π‘œB=A++B
42 39 40 41 syl2anc ⊒A∈W∧B∈Wβ†’A+freeMnd⁑IΓ—2π‘œB=A++B
43 42 eceq1d ⊒A∈W∧B∈Wβ†’A+freeMnd⁑IΓ—2π‘œBβˆΌΛ™=A++BβˆΌΛ™
44 38 43 eqtrd ⊒A∈W∧B∈Wβ†’AβˆΌΛ™+Λ™BβˆΌΛ™=A++BβˆΌΛ™