Metamath Proof Explorer

Theorem frgpcpbl

Description: Compatibility of the group operation with the free group equivalence relation. (Contributed by Mario Carneiro, 1-Oct-2015) (Revised by Mario Carneiro, 27-Feb-2016)

Ref Expression
Hypotheses frgpval.m ⊢ G = freeGrp ⁡ I
frgpval.b ⊢ M = freeMnd ⁡ I × 2 𝑜
frgpval.r ⊢ ∼ ˙ = ~ FG ⁡ I
frgpcpbl.p ⊢ + ˙ = + M
Assertion frgpcpbl ⊢ A ∼ ˙ C ∧ B ∼ ˙ D → A + ˙ B ∼ ˙ C + ˙ D

Proof

Step Hyp Ref Expression
1 frgpval.m ⊢ G = freeGrp ⁡ I
2 frgpval.b ⊢ M = freeMnd ⁡ I × 2 𝑜
3 frgpval.r ⊢ ∼ ˙ = ~ FG ⁡ I
4 frgpcpbl.p ⊢ + ˙ = + M
5 eqid ⊢ I ⁡ Word I × 2 𝑜 = I ⁡ Word I × 2 𝑜
6 eqid ⊢ y ∈ I , z ∈ 2 𝑜 ⟼ y 1 𝑜 ∖ z = y ∈ I , z ∈ 2 𝑜 ⟼ y 1 𝑜 ∖ z
7 eqid ⊢ v ∈ I ⁡ Word I × 2 𝑜 ⟼ n ∈ 0 … v , w ∈ I × 2 𝑜 ⟼ v splice n n ⟨“ w y ∈ I , z ∈ 2 𝑜 ⟼ y 1 𝑜 ∖ z ⁡ w ”⟩ = v ∈ I ⁡ Word I × 2 𝑜 ⟼ n ∈ 0 … v , w ∈ I × 2 𝑜 ⟼ v splice n n ⟨“ w y ∈ I , z ∈ 2 𝑜 ⟼ y 1 𝑜 ∖ z ⁡ w ”⟩
8 eqid ⊢ I ⁡ Word I × 2 𝑜 ∖ ⋃ x ∈ I ⁡ Word I × 2 𝑜 ran ⁡ v ∈ I ⁡ Word I × 2 𝑜 ⟼ n ∈ 0 … v , w ∈ I × 2 𝑜 ⟼ v splice n n ⟨“ w y ∈ I , z ∈ 2 𝑜 ⟼ y 1 𝑜 ∖ z ⁡ w ”⟩ ⁡ x = I ⁡ Word I × 2 𝑜 ∖ ⋃ x ∈ I ⁡ Word I × 2 𝑜 ran ⁡ v ∈ I ⁡ Word I × 2 𝑜 ⟼ n ∈ 0 … v , w ∈ I × 2 𝑜 ⟼ v splice n n ⟨“ w y ∈ I , z ∈ 2 𝑜 ⟼ y 1 𝑜 ∖ z ⁡ w ”⟩ ⁡ x
9 eqid ⊢ m ∈ t ∈ Word I ⁡ Word I × 2 𝑜 ∖ ∅ | t ⁡ 0 ∈ I ⁡ Word I × 2 𝑜 ∖ ⋃ x ∈ I ⁡ Word I × 2 𝑜 ran ⁡ v ∈ I ⁡ Word I × 2 𝑜 ⟼ n ∈ 0 … v , w ∈ I × 2 𝑜 ⟼ v splice n n ⟨“ w y ∈ I , z ∈ 2 𝑜 ⟼ y 1 𝑜 ∖ z ⁡ w ”⟩ ⁡ x ∧ ∀ k ∈ 1 ..^ t t ⁡ k ∈ ran ⁡ v ∈ I ⁡ Word I × 2 𝑜 ⟼ n ∈ 0 … v , w ∈ I × 2 𝑜 ⟼ v splice n n ⟨“ w y ∈ I , z ∈ 2 𝑜 ⟼ y 1 𝑜 ∖ z ⁡ w ”⟩ ⁡ t ⁡ k − 1 ⟼ m ⁡ m − 1 = m ∈ t ∈ Word I ⁡ Word I × 2 𝑜 ∖ ∅ | t ⁡ 0 ∈ I ⁡ Word I × 2 𝑜 ∖ ⋃ x ∈ I ⁡ Word I × 2 𝑜 ran ⁡ v ∈ I ⁡ Word I × 2 𝑜 ⟼ n ∈ 0 … v , w ∈ I × 2 𝑜 ⟼ v splice n n ⟨“ w y ∈ I , z ∈ 2 𝑜 ⟼ y 1 𝑜 ∖ z ⁡ w ”⟩ ⁡ x ∧ ∀ k ∈ 1 ..^ t t ⁡ k ∈ ran ⁡ v ∈ I ⁡ Word I × 2 𝑜 ⟼ n ∈ 0 … v , w ∈ I × 2 𝑜 ⟼ v splice n n ⟨“ w y ∈ I , z ∈ 2 𝑜 ⟼ y 1 𝑜 ∖ z ⁡ w ”⟩ ⁡ t ⁡ k − 1 ⟼ m ⁡ m − 1
10 5 3 6 7 8 9 efgcpbl2 ⊢ A ∼ ˙ C ∧ B ∼ ˙ D → A ++ B ∼ ˙ C ++ D
11 5 3 efger ⊢ ∼ ˙ Er I ⁡ Word I × 2 𝑜
12 11 a1i ⊢ A ∼ ˙ C ∧ B ∼ ˙ D → ∼ ˙ Er I ⁡ Word I × 2 𝑜
13 simpl ⊢ A ∼ ˙ C ∧ B ∼ ˙ D → A ∼ ˙ C
14 12 13 ercl ⊢ A ∼ ˙ C ∧ B ∼ ˙ D → A ∈ I ⁡ Word I × 2 𝑜
15 5 efgrcl ⊢ A ∈ I ⁡ Word I × 2 𝑜 → I ∈ V ∧ I ⁡ Word I × 2 𝑜 = Word I × 2 𝑜
16 14 15 syl ⊢ A ∼ ˙ C ∧ B ∼ ˙ D → I ∈ V ∧ I ⁡ Word I × 2 𝑜 = Word I × 2 𝑜
17 16 simprd ⊢ A ∼ ˙ C ∧ B ∼ ˙ D → I ⁡ Word I × 2 𝑜 = Word I × 2 𝑜
18 16 simpld ⊢ A ∼ ˙ C ∧ B ∼ ˙ D → I ∈ V
19 2on ⊢ 2 𝑜 ∈ On
20 xpexg ⊢ I ∈ V ∧ 2 𝑜 ∈ On → I × 2 𝑜 ∈ V
21 18 19 20 sylancl ⊢ A ∼ ˙ C ∧ B ∼ ˙ D → I × 2 𝑜 ∈ V
22 eqid ⊢ Base M = Base M
23 2 22 frmdbas ⊢ I × 2 𝑜 ∈ V → Base M = Word I × 2 𝑜
24 21 23 syl ⊢ A ∼ ˙ C ∧ B ∼ ˙ D → Base M = Word I × 2 𝑜
25 17 24 eqtr4d ⊢ A ∼ ˙ C ∧ B ∼ ˙ D → I ⁡ Word I × 2 𝑜 = Base M
26 14 25 eleqtrd ⊢ A ∼ ˙ C ∧ B ∼ ˙ D → A ∈ Base M
27 simpr ⊢ A ∼ ˙ C ∧ B ∼ ˙ D → B ∼ ˙ D
28 12 27 ercl ⊢ A ∼ ˙ C ∧ B ∼ ˙ D → B ∈ I ⁡ Word I × 2 𝑜
29 28 25 eleqtrd ⊢ A ∼ ˙ C ∧ B ∼ ˙ D → B ∈ Base M
30 2 22 4 frmdadd ⊢ A ∈ Base M ∧ B ∈ Base M → A + ˙ B = A ++ B
31 26 29 30 syl2anc ⊢ A ∼ ˙ C ∧ B ∼ ˙ D → A + ˙ B = A ++ B
32 12 13 ercl2 ⊢ A ∼ ˙ C ∧ B ∼ ˙ D → C ∈ I ⁡ Word I × 2 𝑜
33 32 25 eleqtrd ⊢ A ∼ ˙ C ∧ B ∼ ˙ D → C ∈ Base M
34 12 27 ercl2 ⊢ A ∼ ˙ C ∧ B ∼ ˙ D → D ∈ I ⁡ Word I × 2 𝑜
35 34 25 eleqtrd ⊢ A ∼ ˙ C ∧ B ∼ ˙ D → D ∈ Base M
36 2 22 4 frmdadd ⊢ C ∈ Base M ∧ D ∈ Base M → C + ˙ D = C ++ D
37 33 35 36 syl2anc ⊢ A ∼ ˙ C ∧ B ∼ ˙ D → C + ˙ D = C ++ D
38 10 31 37 3brtr4d ⊢ A ∼ ˙ C ∧ B ∼ ˙ D → A + ˙ B ∼ ˙ C + ˙ D