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 ⁡ Word I × 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 ⁡ Word I × 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 = Word I × 2 𝑜
8 7 adantr ⊢ A ∈ W ∧ B ∈ W → I ∈ V ∧ W = Word I × 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 = Word I × 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 ⊢ Base freeMnd ⁡ I × 2 𝑜 = Base freeMnd ⁡ I × 2 𝑜
18 10 17 frmdbas ⊢ I × 2 𝑜 ∈ V → Base freeMnd ⁡ I × 2 𝑜 = Word I × 2 𝑜
19 16 18 syl ⊢ A ∈ W ∧ B ∈ W → Base freeMnd ⁡ I × 2 𝑜 = Word I × 2 𝑜
20 13 19 eqtr4d ⊢ A ∈ W ∧ B ∈ W → W = Base freeMnd ⁡ I × 2 𝑜
21 1 3 efger ⊢ ∼ ˙ Er W
22 21 a1i ⊢ A ∈ W ∧ B ∈ W → ∼ ˙ Er W
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 = Base freeMnd ⁡ I × 2 𝑜
31 29 30 eleqtrd ⊢ A ∈ W ∧ B ∈ W ∧ b ∈ W ∧ d ∈ W → b ∈ Base freeMnd ⁡ 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 ∈ Base freeMnd ⁡ I × 2 𝑜
34 17 25 mndcl ⊢ freeMnd ⁡ I × 2 𝑜 ∈ Mnd ∧ b ∈ Base freeMnd ⁡ I × 2 𝑜 ∧ d ∈ Base freeMnd ⁡ I × 2 𝑜 → b + freeMnd ⁡ I × 2 𝑜 d ∈ Base freeMnd ⁡ I × 2 𝑜
35 28 31 33 34 syl3anc ⊢ A ∈ W ∧ B ∈ W ∧ b ∈ W ∧ d ∈ W → b + freeMnd ⁡ I × 2 𝑜 d ∈ Base freeMnd ⁡ 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 ∈ Base freeMnd ⁡ I × 2 𝑜
40 6 20 eleqtrd ⊢ A ∈ W ∧ B ∈ W → B ∈ Base freeMnd ⁡ I × 2 𝑜
41 10 17 25 frmdadd ⊢ A ∈ Base freeMnd ⁡ I × 2 𝑜 ∧ B ∈ Base freeMnd ⁡ 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 ∼ ˙