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 ⊢ 𝐺 = ( freeGrp ‘ 𝐼 )
frgpval.b ⊢ 𝑀 = ( freeMnd ‘ ( 𝐼 × 2o ) )
frgpval.r ⊢ ∼ = ( ~FG ‘ 𝐼 )
frgpcpbl.p ⊢ + = ( +g ‘ 𝑀 )
Assertion frgpcpbl ( ( 𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷 ) → ( 𝐴 + 𝐵 ) ∼ ( 𝐶 + 𝐷 ) )

Proof

Step Hyp Ref Expression
1 frgpval.m ⊢ 𝐺 = ( freeGrp ‘ 𝐼 )
2 frgpval.b ⊢ 𝑀 = ( freeMnd ‘ ( 𝐼 × 2o ) )
3 frgpval.r ⊢ ∼ = ( ~FG ‘ 𝐼 )
4 frgpcpbl.p ⊢ + = ( +g ‘ 𝑀 )
5 eqid ⊢ ( I ‘ Word ( 𝐼 × 2o ) ) = ( I ‘ Word ( 𝐼 × 2o ) )
6 eqid ⊢ ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2o ↦ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ ) = ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2o ↦ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ )
7 eqid ⊢ ( 𝑣 ∈ ( I ‘ Word ( 𝐼 × 2o ) ) ↦ ( 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑣 ) ) , 𝑤 ∈ ( 𝐼 × 2o ) ↦ ( 𝑣 splice ⟨ 𝑛 , 𝑛 , ⟨“ 𝑤 ( ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2o ↦ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ ) ‘ 𝑤 ) ”⟩ ⟩ ) ) ) = ( 𝑣 ∈ ( I ‘ Word ( 𝐼 × 2o ) ) ↦ ( 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑣 ) ) , 𝑤 ∈ ( 𝐼 × 2o ) ↦ ( 𝑣 splice ⟨ 𝑛 , 𝑛 , ⟨“ 𝑤 ( ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2o ↦ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ ) ‘ 𝑤 ) ”⟩ ⟩ ) ) )
8 eqid ⊢ ( ( I ‘ Word ( 𝐼 × 2o ) ) ∖ ∪ 𝑥 ∈ ( I ‘ Word ( 𝐼 × 2o ) ) ran ( ( 𝑣 ∈ ( I ‘ Word ( 𝐼 × 2o ) ) ↦ ( 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑣 ) ) , 𝑤 ∈ ( 𝐼 × 2o ) ↦ ( 𝑣 splice ⟨ 𝑛 , 𝑛 , ⟨“ 𝑤 ( ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2o ↦ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ ) ‘ 𝑤 ) ”⟩ ⟩ ) ) ) ‘ 𝑥 ) ) = ( ( I ‘ Word ( 𝐼 × 2o ) ) ∖ ∪ 𝑥 ∈ ( I ‘ Word ( 𝐼 × 2o ) ) ran ( ( 𝑣 ∈ ( I ‘ Word ( 𝐼 × 2o ) ) ↦ ( 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑣 ) ) , 𝑤 ∈ ( 𝐼 × 2o ) ↦ ( 𝑣 splice ⟨ 𝑛 , 𝑛 , ⟨“ 𝑤 ( ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2o ↦ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ ) ‘ 𝑤 ) ”⟩ ⟩ ) ) ) ‘ 𝑥 ) )
9 eqid ⊢ ( 𝑚 ∈ { 𝑡 ∈ ( Word ( I ‘ Word ( 𝐼 × 2o ) ) ∖ { ∅ } ) ∣ ( ( 𝑡 ‘ 0 ) ∈ ( ( I ‘ Word ( 𝐼 × 2o ) ) ∖ ∪ 𝑥 ∈ ( I ‘ Word ( 𝐼 × 2o ) ) ran ( ( 𝑣 ∈ ( I ‘ Word ( 𝐼 × 2o ) ) ↦ ( 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑣 ) ) , 𝑤 ∈ ( 𝐼 × 2o ) ↦ ( 𝑣 splice ⟨ 𝑛 , 𝑛 , ⟨“ 𝑤 ( ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2o ↦ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ ) ‘ 𝑤 ) ”⟩ ⟩ ) ) ) ‘ 𝑥 ) ) ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝑡 ) ) ( 𝑡 ‘ 𝑘 ) ∈ ran ( ( 𝑣 ∈ ( I ‘ Word ( 𝐼 × 2o ) ) ↦ ( 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑣 ) ) , 𝑤 ∈ ( 𝐼 × 2o ) ↦ ( 𝑣 splice ⟨ 𝑛 , 𝑛 , ⟨“ 𝑤 ( ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2o ↦ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ ) ‘ 𝑤 ) ”⟩ ⟩ ) ) ) ‘ ( 𝑡 ‘ ( 𝑘 − 1 ) ) ) ) } ↦ ( 𝑚 ‘ ( ( ♯ ‘ 𝑚 ) − 1 ) ) ) = ( 𝑚 ∈ { 𝑡 ∈ ( Word ( I ‘ Word ( 𝐼 × 2o ) ) ∖ { ∅ } ) ∣ ( ( 𝑡 ‘ 0 ) ∈ ( ( I ‘ Word ( 𝐼 × 2o ) ) ∖ ∪ 𝑥 ∈ ( I ‘ Word ( 𝐼 × 2o ) ) ran ( ( 𝑣 ∈ ( I ‘ Word ( 𝐼 × 2o ) ) ↦ ( 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑣 ) ) , 𝑤 ∈ ( 𝐼 × 2o ) ↦ ( 𝑣 splice ⟨ 𝑛 , 𝑛 , ⟨“ 𝑤 ( ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2o ↦ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ ) ‘ 𝑤 ) ”⟩ ⟩ ) ) ) ‘ 𝑥 ) ) ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝑡 ) ) ( 𝑡 ‘ 𝑘 ) ∈ ran ( ( 𝑣 ∈ ( I ‘ Word ( 𝐼 × 2o ) ) ↦ ( 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑣 ) ) , 𝑤 ∈ ( 𝐼 × 2o ) ↦ ( 𝑣 splice ⟨ 𝑛 , 𝑛 , ⟨“ 𝑤 ( ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2o ↦ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ ) ‘ 𝑤 ) ”⟩ ⟩ ) ) ) ‘ ( 𝑡 ‘ ( 𝑘 − 1 ) ) ) ) } ↦ ( 𝑚 ‘ ( ( ♯ ‘ 𝑚 ) − 1 ) ) )
10 5 3 6 7 8 9 efgcpbl2 ⊢ ( ( 𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷 ) → ( 𝐴 ++ 𝐵 ) ∼ ( 𝐶 ++ 𝐷 ) )
11 5 3 efger ⊢ ∼ Er ( I ‘ Word ( 𝐼 × 2o ) )
12 11 a1i ⊢ ( ( 𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷 ) → ∼ Er ( I ‘ Word ( 𝐼 × 2o ) ) )
13 simpl ⊢ ( ( 𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷 ) → 𝐴 ∼ 𝐶 )
14 12 13 ercl ⊢ ( ( 𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷 ) → 𝐴 ∈ ( I ‘ Word ( 𝐼 × 2o ) ) )
15 5 efgrcl ⊢ ( 𝐴 ∈ ( I ‘ Word ( 𝐼 × 2o ) ) → ( 𝐼 ∈ V ∧ ( I ‘ Word ( 𝐼 × 2o ) ) = Word ( 𝐼 × 2o ) ) )
16 14 15 syl ⊢ ( ( 𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷 ) → ( 𝐼 ∈ V ∧ ( I ‘ Word ( 𝐼 × 2o ) ) = Word ( 𝐼 × 2o ) ) )
17 16 simprd ⊢ ( ( 𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷 ) → ( I ‘ Word ( 𝐼 × 2o ) ) = Word ( 𝐼 × 2o ) )
18 16 simpld ⊢ ( ( 𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷 ) → 𝐼 ∈ V )
19 2on ⊢ 2o ∈ On
20 xpexg ⊢ ( ( 𝐼 ∈ V ∧ 2o ∈ On ) → ( 𝐼 × 2o ) ∈ V )
21 18 19 20 sylancl ⊢ ( ( 𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷 ) → ( 𝐼 × 2o ) ∈ V )
22 eqid ⊢ ( Base ‘ 𝑀 ) = ( Base ‘ 𝑀 )
23 2 22 frmdbas ⊢ ( ( 𝐼 × 2o ) ∈ V → ( Base ‘ 𝑀 ) = Word ( 𝐼 × 2o ) )
24 21 23 syl ⊢ ( ( 𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷 ) → ( Base ‘ 𝑀 ) = Word ( 𝐼 × 2o ) )
25 17 24 eqtr4d ⊢ ( ( 𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷 ) → ( I ‘ Word ( 𝐼 × 2o ) ) = ( Base ‘ 𝑀 ) )
26 14 25 eleqtrd ⊢ ( ( 𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷 ) → 𝐴 ∈ ( Base ‘ 𝑀 ) )
27 simpr ⊢ ( ( 𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷 ) → 𝐵 ∼ 𝐷 )
28 12 27 ercl ⊢ ( ( 𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷 ) → 𝐵 ∈ ( I ‘ Word ( 𝐼 × 2o ) ) )
29 28 25 eleqtrd ⊢ ( ( 𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷 ) → 𝐵 ∈ ( Base ‘ 𝑀 ) )
30 2 22 4 frmdadd ⊢ ( ( 𝐴 ∈ ( Base ‘ 𝑀 ) ∧ 𝐵 ∈ ( Base ‘ 𝑀 ) ) → ( 𝐴 + 𝐵 ) = ( 𝐴 ++ 𝐵 ) )
31 26 29 30 syl2anc ⊢ ( ( 𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷 ) → ( 𝐴 + 𝐵 ) = ( 𝐴 ++ 𝐵 ) )
32 12 13 ercl2 ⊢ ( ( 𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷 ) → 𝐶 ∈ ( I ‘ Word ( 𝐼 × 2o ) ) )
33 32 25 eleqtrd ⊢ ( ( 𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷 ) → 𝐶 ∈ ( Base ‘ 𝑀 ) )
34 12 27 ercl2 ⊢ ( ( 𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷 ) → 𝐷 ∈ ( I ‘ Word ( 𝐼 × 2o ) ) )
35 34 25 eleqtrd ⊢ ( ( 𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷 ) → 𝐷 ∈ ( Base ‘ 𝑀 ) )
36 2 22 4 frmdadd ⊢ ( ( 𝐶 ∈ ( Base ‘ 𝑀 ) ∧ 𝐷 ∈ ( Base ‘ 𝑀 ) ) → ( 𝐶 + 𝐷 ) = ( 𝐶 ++ 𝐷 ) )
37 33 35 36 syl2anc ⊢ ( ( 𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷 ) → ( 𝐶 + 𝐷 ) = ( 𝐶 ++ 𝐷 ) )
38 10 31 37 3brtr4d ⊢ ( ( 𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷 ) → ( 𝐴 + 𝐵 ) ∼ ( 𝐶 + 𝐷 ) )