Step |
Hyp |
Ref |
Expression |
1 |
|
df-s2 |
⊢ 〈“ 𝐴 𝐵 ”〉 = ( 〈“ 𝐴 ”〉 ++ 〈“ 𝐵 ”〉 ) |
2 |
1
|
oveq1i |
⊢ ( 〈“ 𝐴 𝐵 ”〉 ∘f/c 𝑅 𝐶 ) = ( ( 〈“ 𝐴 ”〉 ++ 〈“ 𝐵 ”〉 ) ∘f/c 𝑅 𝐶 ) |
3 |
|
simp1 |
⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇 ) → 𝐴 ∈ 𝑆 ) |
4 |
3
|
s1cld |
⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇 ) → 〈“ 𝐴 ”〉 ∈ Word 𝑆 ) |
5 |
|
simp2 |
⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇 ) → 𝐵 ∈ 𝑆 ) |
6 |
5
|
s1cld |
⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇 ) → 〈“ 𝐵 ”〉 ∈ Word 𝑆 ) |
7 |
|
simp3 |
⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇 ) → 𝐶 ∈ 𝑇 ) |
8 |
4 6 7
|
ofcccat |
⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇 ) → ( ( 〈“ 𝐴 ”〉 ++ 〈“ 𝐵 ”〉 ) ∘f/c 𝑅 𝐶 ) = ( ( 〈“ 𝐴 ”〉 ∘f/c 𝑅 𝐶 ) ++ ( 〈“ 𝐵 ”〉 ∘f/c 𝑅 𝐶 ) ) ) |
9 |
2 8
|
syl5eq |
⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇 ) → ( 〈“ 𝐴 𝐵 ”〉 ∘f/c 𝑅 𝐶 ) = ( ( 〈“ 𝐴 ”〉 ∘f/c 𝑅 𝐶 ) ++ ( 〈“ 𝐵 ”〉 ∘f/c 𝑅 𝐶 ) ) ) |
10 |
|
ofcs1 |
⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇 ) → ( 〈“ 𝐴 ”〉 ∘f/c 𝑅 𝐶 ) = 〈“ ( 𝐴 𝑅 𝐶 ) ”〉 ) |
11 |
3 7 10
|
syl2anc |
⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇 ) → ( 〈“ 𝐴 ”〉 ∘f/c 𝑅 𝐶 ) = 〈“ ( 𝐴 𝑅 𝐶 ) ”〉 ) |
12 |
|
ofcs1 |
⊢ ( ( 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇 ) → ( 〈“ 𝐵 ”〉 ∘f/c 𝑅 𝐶 ) = 〈“ ( 𝐵 𝑅 𝐶 ) ”〉 ) |
13 |
5 7 12
|
syl2anc |
⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇 ) → ( 〈“ 𝐵 ”〉 ∘f/c 𝑅 𝐶 ) = 〈“ ( 𝐵 𝑅 𝐶 ) ”〉 ) |
14 |
11 13
|
oveq12d |
⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇 ) → ( ( 〈“ 𝐴 ”〉 ∘f/c 𝑅 𝐶 ) ++ ( 〈“ 𝐵 ”〉 ∘f/c 𝑅 𝐶 ) ) = ( 〈“ ( 𝐴 𝑅 𝐶 ) ”〉 ++ 〈“ ( 𝐵 𝑅 𝐶 ) ”〉 ) ) |
15 |
|
df-s2 |
⊢ 〈“ ( 𝐴 𝑅 𝐶 ) ( 𝐵 𝑅 𝐶 ) ”〉 = ( 〈“ ( 𝐴 𝑅 𝐶 ) ”〉 ++ 〈“ ( 𝐵 𝑅 𝐶 ) ”〉 ) |
16 |
14 15
|
eqtr4di |
⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇 ) → ( ( 〈“ 𝐴 ”〉 ∘f/c 𝑅 𝐶 ) ++ ( 〈“ 𝐵 ”〉 ∘f/c 𝑅 𝐶 ) ) = 〈“ ( 𝐴 𝑅 𝐶 ) ( 𝐵 𝑅 𝐶 ) ”〉 ) |
17 |
9 16
|
eqtrd |
⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇 ) → ( 〈“ 𝐴 𝐵 ”〉 ∘f/c 𝑅 𝐶 ) = 〈“ ( 𝐴 𝑅 𝐶 ) ( 𝐵 𝑅 𝐶 ) ”〉 ) |