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 ⊢ 𝑊 = ( I ‘ Word ( 𝐼 × 2o ) )
frgpadd.g ⊢ 𝐺 = ( freeGrp ‘ 𝐼 )
frgpadd.r ⊢ ∼ = ( ~FG ‘ 𝐼 )
frgpadd.n ⊢ + = ( +g ‘ 𝐺 )
Assertion frgpadd ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) → ( [ 𝐴 ] ∼ + [ 𝐵 ] ∼ ) = [ ( 𝐴 ++ 𝐵 ) ] ∼ )

Proof

Step Hyp Ref Expression
1 frgpadd.w ⊢ 𝑊 = ( I ‘ Word ( 𝐼 × 2o ) )
2 frgpadd.g ⊢ 𝐺 = ( freeGrp ‘ 𝐼 )
3 frgpadd.r ⊢ ∼ = ( ~FG ‘ 𝐼 )
4 frgpadd.n ⊢ + = ( +g ‘ 𝐺 )
5 simpl ⊢ ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) → 𝐴 ∈ 𝑊 )
6 simpr ⊢ ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) → 𝐵 ∈ 𝑊 )
7 1 efgrcl ⊢ ( 𝐴 ∈ 𝑊 → ( 𝐼 ∈ V ∧ 𝑊 = Word ( 𝐼 × 2o ) ) )
8 7 adantr ⊢ ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐼 ∈ V ∧ 𝑊 = Word ( 𝐼 × 2o ) ) )
9 8 simpld ⊢ ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) → 𝐼 ∈ V )
10 eqid ⊢ ( freeMnd ‘ ( 𝐼 × 2o ) ) = ( freeMnd ‘ ( 𝐼 × 2o ) )
11 2 10 3 frgpval ⊢ ( 𝐼 ∈ V → 𝐺 = ( ( freeMnd ‘ ( 𝐼 × 2o ) ) /s ∼ ) )
12 9 11 syl ⊢ ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) → 𝐺 = ( ( freeMnd ‘ ( 𝐼 × 2o ) ) /s ∼ ) )
13 8 simprd ⊢ ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) → 𝑊 = Word ( 𝐼 × 2o ) )
14 2on ⊢ 2o ∈ On
15 xpexg ⊢ ( ( 𝐼 ∈ V ∧ 2o ∈ On ) → ( 𝐼 × 2o ) ∈ V )
16 9 14 15 sylancl ⊢ ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐼 × 2o ) ∈ V )
17 eqid ⊢ ( Base ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) ) = ( Base ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) )
18 10 17 frmdbas ⊢ ( ( 𝐼 × 2o ) ∈ V → ( Base ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) ) = Word ( 𝐼 × 2o ) )
19 16 18 syl ⊢ ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) → ( Base ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) ) = Word ( 𝐼 × 2o ) )
20 13 19 eqtr4d ⊢ ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) → 𝑊 = ( Base ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) ) )
21 1 3 efger ⊢ ∼ Er 𝑊
22 21 a1i ⊢ ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) → ∼ Er 𝑊 )
23 10 frmdmnd ⊢ ( ( 𝐼 × 2o ) ∈ V → ( freeMnd ‘ ( 𝐼 × 2o ) ) ∈ Mnd )
24 16 23 syl ⊢ ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) → ( freeMnd ‘ ( 𝐼 × 2o ) ) ∈ Mnd )
25 eqid ⊢ ( +g ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) ) = ( +g ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) )
26 2 10 3 25 frgpcpbl ⊢ ( ( 𝑎 ∼ 𝑏 ∧ 𝑐 ∼ 𝑑 ) → ( 𝑎 ( +g ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) ) 𝑐 ) ∼ ( 𝑏 ( +g ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) ) 𝑑 ) )
27 26 a1i ⊢ ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) → ( ( 𝑎 ∼ 𝑏 ∧ 𝑐 ∼ 𝑑 ) → ( 𝑎 ( +g ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) ) 𝑐 ) ∼ ( 𝑏 ( +g ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) ) 𝑑 ) ) )
28 24 adantr ⊢ ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝑏 ∈ 𝑊 ∧ 𝑑 ∈ 𝑊 ) ) → ( freeMnd ‘ ( 𝐼 × 2o ) ) ∈ Mnd )
29 simprl ⊢ ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝑏 ∈ 𝑊 ∧ 𝑑 ∈ 𝑊 ) ) → 𝑏 ∈ 𝑊 )
30 20 adantr ⊢ ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝑏 ∈ 𝑊 ∧ 𝑑 ∈ 𝑊 ) ) → 𝑊 = ( Base ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) ) )
31 29 30 eleqtrd ⊢ ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝑏 ∈ 𝑊 ∧ 𝑑 ∈ 𝑊 ) ) → 𝑏 ∈ ( Base ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) ) )
32 simprr ⊢ ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝑏 ∈ 𝑊 ∧ 𝑑 ∈ 𝑊 ) ) → 𝑑 ∈ 𝑊 )
33 32 30 eleqtrd ⊢ ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝑏 ∈ 𝑊 ∧ 𝑑 ∈ 𝑊 ) ) → 𝑑 ∈ ( Base ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) ) )
34 17 25 mndcl ⊢ ( ( ( freeMnd ‘ ( 𝐼 × 2o ) ) ∈ Mnd ∧ 𝑏 ∈ ( Base ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) ) ∧ 𝑑 ∈ ( Base ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) ) ) → ( 𝑏 ( +g ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) ) 𝑑 ) ∈ ( Base ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) ) )
35 28 31 33 34 syl3anc ⊢ ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝑏 ∈ 𝑊 ∧ 𝑑 ∈ 𝑊 ) ) → ( 𝑏 ( +g ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) ) 𝑑 ) ∈ ( Base ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) ) )
36 35 30 eleqtrrd ⊢ ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝑏 ∈ 𝑊 ∧ 𝑑 ∈ 𝑊 ) ) → ( 𝑏 ( +g ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) ) 𝑑 ) ∈ 𝑊 )
37 12 20 22 24 27 36 25 4 qusaddval ⊢ ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) → ( [ 𝐴 ] ∼ + [ 𝐵 ] ∼ ) = [ ( 𝐴 ( +g ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) ) 𝐵 ) ] ∼ )
38 5 6 37 mpd3an23 ⊢ ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) → ( [ 𝐴 ] ∼ + [ 𝐵 ] ∼ ) = [ ( 𝐴 ( +g ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) ) 𝐵 ) ] ∼ )
39 5 20 eleqtrd ⊢ ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) → 𝐴 ∈ ( Base ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) ) )
40 6 20 eleqtrd ⊢ ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) → 𝐵 ∈ ( Base ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) ) )
41 10 17 25 frmdadd ⊢ ( ( 𝐴 ∈ ( Base ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) ) ∧ 𝐵 ∈ ( Base ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) ) ) → ( 𝐴 ( +g ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) ) 𝐵 ) = ( 𝐴 ++ 𝐵 ) )
42 39 40 41 syl2anc ⊢ ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 ( +g ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) ) 𝐵 ) = ( 𝐴 ++ 𝐵 ) )
43 42 eceq1d ⊢ ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) → [ ( 𝐴 ( +g ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) ) 𝐵 ) ] ∼ = [ ( 𝐴 ++ 𝐵 ) ] ∼ )
44 38 43 eqtrd ⊢ ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) → ( [ 𝐴 ] ∼ + [ 𝐵 ] ∼ ) = [ ( 𝐴 ++ 𝐵 ) ] ∼ )