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	eqtrid	⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇 ) → ( ⟨“ 𝐴 𝐵 ”⟩ ∘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 𝑅 𝐶 ) = ⟨“ ( 𝐴 𝑅 𝐶 ) ( 𝐵 𝑅 𝐶 ) ”⟩ )