Metamath Proof Explorer

Theorem ofs2

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

Ref Expression
Assertion ofs2 ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐶 ∈ 𝑇 ∧ 𝐷 ∈ 𝑇 ) ) → ( ⟨“ 𝐴 𝐵 ”⟩ ∘f 𝑅 ⟨“ 𝐶 𝐷 ”⟩ ) = ⟨“ ( 𝐴 𝑅 𝐶 ) ( 𝐵 𝑅 𝐷 ) ”⟩ )

Proof

Step Hyp Ref Expression
1 df-s2 ⊢ ⟨“ 𝐴 𝐵 ”⟩ = ( ⟨“ 𝐴 ”⟩ ++ ⟨“ 𝐵 ”⟩ )
2 df-s2 ⊢ ⟨“ 𝐶 𝐷 ”⟩ = ( ⟨“ 𝐶 ”⟩ ++ ⟨“ 𝐷 ”⟩ )
3 1 2 oveq12i ⊢ ( ⟨“ 𝐴 𝐵 ”⟩ ∘f 𝑅 ⟨“ 𝐶 𝐷 ”⟩ ) = ( ( ⟨“ 𝐴 ”⟩ ++ ⟨“ 𝐵 ”⟩ ) ∘f 𝑅 ( ⟨“ 𝐶 ”⟩ ++ ⟨“ 𝐷 ”⟩ ) )
4 simpll ⊢ ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐶 ∈ 𝑇 ∧ 𝐷 ∈ 𝑇 ) ) → 𝐴 ∈ 𝑆 )
5 4 s1cld ⊢ ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐶 ∈ 𝑇 ∧ 𝐷 ∈ 𝑇 ) ) → ⟨“ 𝐴 ”⟩ ∈ Word 𝑆 )
6 simplr ⊢ ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐶 ∈ 𝑇 ∧ 𝐷 ∈ 𝑇 ) ) → 𝐵 ∈ 𝑆 )
7 6 s1cld ⊢ ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐶 ∈ 𝑇 ∧ 𝐷 ∈ 𝑇 ) ) → ⟨“ 𝐵 ”⟩ ∈ Word 𝑆 )
8 simprl ⊢ ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐶 ∈ 𝑇 ∧ 𝐷 ∈ 𝑇 ) ) → 𝐶 ∈ 𝑇 )
9 8 s1cld ⊢ ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐶 ∈ 𝑇 ∧ 𝐷 ∈ 𝑇 ) ) → ⟨“ 𝐶 ”⟩ ∈ Word 𝑇 )
10 simprr ⊢ ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐶 ∈ 𝑇 ∧ 𝐷 ∈ 𝑇 ) ) → 𝐷 ∈ 𝑇 )
11 10 s1cld ⊢ ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐶 ∈ 𝑇 ∧ 𝐷 ∈ 𝑇 ) ) → ⟨“ 𝐷 ”⟩ ∈ Word 𝑇 )
12 s1len ⊢ ( ♯ ‘ ⟨“ 𝐴 ”⟩ ) = 1
13 s1len ⊢ ( ♯ ‘ ⟨“ 𝐶 ”⟩ ) = 1
14 12 13 eqtr4i ⊢ ( ♯ ‘ ⟨“ 𝐴 ”⟩ ) = ( ♯ ‘ ⟨“ 𝐶 ”⟩ )
15 14 a1i ⊢ ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐶 ∈ 𝑇 ∧ 𝐷 ∈ 𝑇 ) ) → ( ♯ ‘ ⟨“ 𝐴 ”⟩ ) = ( ♯ ‘ ⟨“ 𝐶 ”⟩ ) )
16 s1len ⊢ ( ♯ ‘ ⟨“ 𝐵 ”⟩ ) = 1
17 s1len ⊢ ( ♯ ‘ ⟨“ 𝐷 ”⟩ ) = 1
18 16 17 eqtr4i ⊢ ( ♯ ‘ ⟨“ 𝐵 ”⟩ ) = ( ♯ ‘ ⟨“ 𝐷 ”⟩ )
19 18 a1i ⊢ ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐶 ∈ 𝑇 ∧ 𝐷 ∈ 𝑇 ) ) → ( ♯ ‘ ⟨“ 𝐵 ”⟩ ) = ( ♯ ‘ ⟨“ 𝐷 ”⟩ ) )
20 5 7 9 11 15 19 ofccat ⊢ ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐶 ∈ 𝑇 ∧ 𝐷 ∈ 𝑇 ) ) → ( ( ⟨“ 𝐴 ”⟩ ++ ⟨“ 𝐵 ”⟩ ) ∘f 𝑅 ( ⟨“ 𝐶 ”⟩ ++ ⟨“ 𝐷 ”⟩ ) ) = ( ( ⟨“ 𝐴 ”⟩ ∘f 𝑅 ⟨“ 𝐶 ”⟩ ) ++ ( ⟨“ 𝐵 ”⟩ ∘f 𝑅 ⟨“ 𝐷 ”⟩ ) ) )
21 3 20 syl5eq ⊢ ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐶 ∈ 𝑇 ∧ 𝐷 ∈ 𝑇 ) ) → ( ⟨“ 𝐴 𝐵 ”⟩ ∘f 𝑅 ⟨“ 𝐶 𝐷 ”⟩ ) = ( ( ⟨“ 𝐴 ”⟩ ∘f 𝑅 ⟨“ 𝐶 ”⟩ ) ++ ( ⟨“ 𝐵 ”⟩ ∘f 𝑅 ⟨“ 𝐷 ”⟩ ) ) )
22 ofs1 ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇 ) → ( ⟨“ 𝐴 ”⟩ ∘f 𝑅 ⟨“ 𝐶 ”⟩ ) = ⟨“ ( 𝐴 𝑅 𝐶 ) ”⟩ )
23 4 8 22 syl2anc ⊢ ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐶 ∈ 𝑇 ∧ 𝐷 ∈ 𝑇 ) ) → ( ⟨“ 𝐴 ”⟩ ∘f 𝑅 ⟨“ 𝐶 ”⟩ ) = ⟨“ ( 𝐴 𝑅 𝐶 ) ”⟩ )
24 ofs1 ⊢ ( ( 𝐵 ∈ 𝑆 ∧ 𝐷 ∈ 𝑇 ) → ( ⟨“ 𝐵 ”⟩ ∘f 𝑅 ⟨“ 𝐷 ”⟩ ) = ⟨“ ( 𝐵 𝑅 𝐷 ) ”⟩ )
25 6 10 24 syl2anc ⊢ ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐶 ∈ 𝑇 ∧ 𝐷 ∈ 𝑇 ) ) → ( ⟨“ 𝐵 ”⟩ ∘f 𝑅 ⟨“ 𝐷 ”⟩ ) = ⟨“ ( 𝐵 𝑅 𝐷 ) ”⟩ )
26 23 25 oveq12d ⊢ ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐶 ∈ 𝑇 ∧ 𝐷 ∈ 𝑇 ) ) → ( ( ⟨“ 𝐴 ”⟩ ∘f 𝑅 ⟨“ 𝐶 ”⟩ ) ++ ( ⟨“ 𝐵 ”⟩ ∘f 𝑅 ⟨“ 𝐷 ”⟩ ) ) = ( ⟨“ ( 𝐴 𝑅 𝐶 ) ”⟩ ++ ⟨“ ( 𝐵 𝑅 𝐷 ) ”⟩ ) )
27 df-s2 ⊢ ⟨“ ( 𝐴 𝑅 𝐶 ) ( 𝐵 𝑅 𝐷 ) ”⟩ = ( ⟨“ ( 𝐴 𝑅 𝐶 ) ”⟩ ++ ⟨“ ( 𝐵 𝑅 𝐷 ) ”⟩ )
28 26 27 eqtr4di ⊢ ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐶 ∈ 𝑇 ∧ 𝐷 ∈ 𝑇 ) ) → ( ( ⟨“ 𝐴 ”⟩ ∘f 𝑅 ⟨“ 𝐶 ”⟩ ) ++ ( ⟨“ 𝐵 ”⟩ ∘f 𝑅 ⟨“ 𝐷 ”⟩ ) ) = ⟨“ ( 𝐴 𝑅 𝐶 ) ( 𝐵 𝑅 𝐷 ) ”⟩ )
29 21 28 eqtrd ⊢ ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐶 ∈ 𝑇 ∧ 𝐷 ∈ 𝑇 ) ) → ( ⟨“ 𝐴 𝐵 ”⟩ ∘f 𝑅 ⟨“ 𝐶 𝐷 ”⟩ ) = ⟨“ ( 𝐴 𝑅 𝐶 ) ( 𝐵 𝑅 𝐷 ) ”⟩ )