Metamath Proof Explorer


Theorem ofcs2

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

Ref Expression
Assertion ofcs2 ( ( 𝐴𝑆𝐵𝑆𝐶𝑇 ) → ( ⟨“ 𝐴 𝐵 ”⟩ ∘f/c 𝑅 𝐶 ) = ⟨“ ( 𝐴 𝑅 𝐶 ) ( 𝐵 𝑅 𝐶 ) ”⟩ )

Proof

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 𝑅 𝐶 ) = ⟨“ ( 𝐴 𝑅 𝐶 ) ( 𝐵 𝑅 𝐶 ) ”⟩ )