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