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⁡WordI×2𝑜=I⁡WordI×2𝑜
6 eqid ⊢y∈I,z∈2𝑜⟼y1𝑜∖z=y∈I,z∈2𝑜⟼y1𝑜∖z
7 eqid ⊢v∈I⁡WordI×2𝑜⟼n∈0…v,w∈I×2𝑜⟼vsplicenn⟨“wy∈I,z∈2𝑜⟼y1𝑜∖z⁡w”⟩=v∈I⁡WordI×2𝑜⟼n∈0…v,w∈I×2𝑜⟼vsplicenn⟨“wy∈I,z∈2𝑜⟼y1𝑜∖z⁡w”⟩
8 eqid ⊢I⁡WordI×2𝑜∖⋃x∈I⁡WordI×2𝑜ran⁡v∈I⁡WordI×2𝑜⟼n∈0…v,w∈I×2𝑜⟼vsplicenn⟨“wy∈I,z∈2𝑜⟼y1𝑜∖z⁡w”⟩⁡x=I⁡WordI×2𝑜∖⋃x∈I⁡WordI×2𝑜ran⁡v∈I⁡WordI×2𝑜⟼n∈0…v,w∈I×2𝑜⟼vsplicenn⟨“wy∈I,z∈2𝑜⟼y1𝑜∖z⁡w”⟩⁡x
9 eqid ⊢m∈t∈WordI⁡WordI×2𝑜∖∅|t⁡0∈I⁡WordI×2𝑜∖⋃x∈I⁡WordI×2𝑜ran⁡v∈I⁡WordI×2𝑜⟼n∈0…v,w∈I×2𝑜⟼vsplicenn⟨“wy∈I,z∈2𝑜⟼y1𝑜∖z⁡w”⟩⁡x∧∀k∈1..^tt⁡k∈ran⁡v∈I⁡WordI×2𝑜⟼n∈0…v,w∈I×2𝑜⟼vsplicenn⟨“wy∈I,z∈2𝑜⟼y1𝑜∖z⁡w”⟩⁡t⁡k−1⟼m⁡m−1=m∈t∈WordI⁡WordI×2𝑜∖∅|t⁡0∈I⁡WordI×2𝑜∖⋃x∈I⁡WordI×2𝑜ran⁡v∈I⁡WordI×2𝑜⟼n∈0…v,w∈I×2𝑜⟼vsplicenn⟨“wy∈I,z∈2𝑜⟼y1𝑜∖z⁡w”⟩⁡x∧∀k∈1..^tt⁡k∈ran⁡v∈I⁡WordI×2𝑜⟼n∈0…v,w∈I×2𝑜⟼vsplicenn⟨“wy∈I,z∈2𝑜⟼y1𝑜∖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 ⊢∼˙ErI⁡WordI×2𝑜
12 11 a1i ⊢A∼˙C∧B∼˙D→∼˙ErI⁡WordI×2𝑜
13 simpl ⊢A∼˙C∧B∼˙D→A∼˙C
14 12 13 ercl ⊢A∼˙C∧B∼˙D→A∈I⁡WordI×2𝑜
15 5 efgrcl ⊢A∈I⁡WordI×2𝑜→I∈V∧I⁡WordI×2𝑜=WordI×2𝑜
16 14 15 syl ⊢A∼˙C∧B∼˙D→I∈V∧I⁡WordI×2𝑜=WordI×2𝑜
17 16 simprd ⊢A∼˙C∧B∼˙D→I⁡WordI×2𝑜=WordI×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 ⊢BaseM=BaseM
23 2 22 frmdbas ⊢I×2𝑜∈V→BaseM=WordI×2𝑜
24 21 23 syl ⊢A∼˙C∧B∼˙D→BaseM=WordI×2𝑜
25 17 24 eqtr4d ⊢A∼˙C∧B∼˙D→I⁡WordI×2𝑜=BaseM
26 14 25 eleqtrd ⊢A∼˙C∧B∼˙D→A∈BaseM
27 simpr ⊢A∼˙C∧B∼˙D→B∼˙D
28 12 27 ercl ⊢A∼˙C∧B∼˙D→B∈I⁡WordI×2𝑜
29 28 25 eleqtrd ⊢A∼˙C∧B∼˙D→B∈BaseM
30 2 22 4 frmdadd ⊢A∈BaseM∧B∈BaseM→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⁡WordI×2𝑜
33 32 25 eleqtrd ⊢A∼˙C∧B∼˙D→C∈BaseM
34 12 27 ercl2 ⊢A∼˙C∧B∼˙D→D∈I⁡WordI×2𝑜
35 34 25 eleqtrd ⊢A∼˙C∧B∼˙D→D∈BaseM
36 2 22 4 frmdadd ⊢C∈BaseM∧D∈BaseM→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