Metamath Proof Explorer

Theorem ofcs2

Description: Letterwise operations on a double letter word. (Contributed by Thierry Arnoux, 9-Oct-2018)

Ref Expression
Assertion ofcs2 ⊢ A ∈ S ∧ B ∈ S ∧ C ∈ T → ⟨“ AB ”⟩ ∘ fc ⁡ R C = ⟨“ A R CB R C ”⟩

Proof

Step Hyp Ref Expression
1 df-s2 ⊢ ⟨“ AB ”⟩ = ⟨“ A ”⟩ ++ ⟨“ B ”⟩
2 1 oveq1i ⊢ ⟨“ AB ”⟩ ∘ fc ⁡ R C = ⟨“ A ”⟩ ++ ⟨“ B ”⟩ ∘ fc ⁡ R C
3 simp1 ⊢ A ∈ S ∧ B ∈ S ∧ C ∈ T → A ∈ S
4 3 s1cld ⊢ A ∈ S ∧ B ∈ S ∧ C ∈ T → ⟨“ A ”⟩ ∈ Word S
5 simp2 ⊢ A ∈ S ∧ B ∈ S ∧ C ∈ T → B ∈ S
6 5 s1cld ⊢ A ∈ S ∧ B ∈ S ∧ C ∈ T → ⟨“ B ”⟩ ∈ Word S
7 simp3 ⊢ A ∈ S ∧ B ∈ S ∧ C ∈ T → C ∈ T
8 4 6 7 ofcccat ⊢ A ∈ S ∧ B ∈ S ∧ C ∈ T → ⟨“ A ”⟩ ++ ⟨“ B ”⟩ ∘ fc ⁡ R C = ⟨“ A ”⟩ ∘ fc ⁡ R C ++ ⟨“ B ”⟩ ∘ fc ⁡ R C
9 2 8 syl5eq ⊢ A ∈ S ∧ B ∈ S ∧ C ∈ T → ⟨“ AB ”⟩ ∘ fc ⁡ R C = ⟨“ A ”⟩ ∘ fc ⁡ R C ++ ⟨“ B ”⟩ ∘ fc ⁡ R C
10 ofcs1 ⊢ A ∈ S ∧ C ∈ T → ⟨“ A ”⟩ ∘ fc ⁡ R C = ⟨“ A R C ”⟩
11 3 7 10 syl2anc ⊢ A ∈ S ∧ B ∈ S ∧ C ∈ T → ⟨“ A ”⟩ ∘ fc ⁡ R C = ⟨“ A R C ”⟩
12 ofcs1 ⊢ B ∈ S ∧ C ∈ T → ⟨“ B ”⟩ ∘ fc ⁡ R C = ⟨“ B R C ”⟩
13 5 7 12 syl2anc ⊢ A ∈ S ∧ B ∈ S ∧ C ∈ T → ⟨“ B ”⟩ ∘ fc ⁡ R C = ⟨“ B R C ”⟩
14 11 13 oveq12d ⊢ A ∈ S ∧ B ∈ S ∧ C ∈ T → ⟨“ A ”⟩ ∘ fc ⁡ R C ++ ⟨“ B ”⟩ ∘ fc ⁡ R C = ⟨“ A R C ”⟩ ++ ⟨“ B R C ”⟩
15 df-s2 ⊢ ⟨“ A R CB R C ”⟩ = ⟨“ A R C ”⟩ ++ ⟨“ B R C ”⟩
16 14 15 eqtr4di ⊢ A ∈ S ∧ B ∈ S ∧ C ∈ T → ⟨“ A ”⟩ ∘ fc ⁡ R C ++ ⟨“ B ”⟩ ∘ fc ⁡ R C = ⟨“ A R CB R C ”⟩
17 9 16 eqtrd ⊢ A ∈ S ∧ B ∈ S ∧ C ∈ T → ⟨“ AB ”⟩ ∘ fc ⁡ R C = ⟨“ A R CB R C ”⟩