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 ( ( 𝐴 𝐶𝐵 𝐷 ) → ( 𝐴 + 𝐵 ) ( 𝐶 + 𝐷 ) )