Metamath Proof Explorer

Theorem s2eq2s1eq

Description: Two length 2 words are equal iff the corresponding singleton words consisting of their symbols are equal. (Contributed by Alexander van der Vekens, 24-Sep-2018)

Ref Expression
Assertion s2eq2s1eq ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ) ) → ( ⟨“ 𝐴 𝐵 ”⟩ = ⟨“ 𝐶 𝐷 ”⟩ ↔ ( ⟨“ 𝐴 ”⟩ = ⟨“ 𝐶 ”⟩ ∧ ⟨“ 𝐵 ”⟩ = ⟨“ 𝐷 ”⟩ ) ) )

Proof

Step Hyp Ref Expression
1 df-s2 ⊢ ⟨“ 𝐴 𝐵 ”⟩ = ( ⟨“ 𝐴 ”⟩ ++ ⟨“ 𝐵 ”⟩ )
2 1 a1i ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ) ) → ⟨“ 𝐴 𝐵 ”⟩ = ( ⟨“ 𝐴 ”⟩ ++ ⟨“ 𝐵 ”⟩ ) )
3 df-s2 ⊢ ⟨“ 𝐶 𝐷 ”⟩ = ( ⟨“ 𝐶 ”⟩ ++ ⟨“ 𝐷 ”⟩ )
4 3 a1i ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ) ) → ⟨“ 𝐶 𝐷 ”⟩ = ( ⟨“ 𝐶 ”⟩ ++ ⟨“ 𝐷 ”⟩ ) )
5 2 4 eqeq12d ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ) ) → ( ⟨“ 𝐴 𝐵 ”⟩ = ⟨“ 𝐶 𝐷 ”⟩ ↔ ( ⟨“ 𝐴 ”⟩ ++ ⟨“ 𝐵 ”⟩ ) = ( ⟨“ 𝐶 ”⟩ ++ ⟨“ 𝐷 ”⟩ ) ) )
6 s1cl ⊢ ( 𝐴 ∈ 𝑉 → ⟨“ 𝐴 ”⟩ ∈ Word 𝑉 )
7 s1cl ⊢ ( 𝐵 ∈ 𝑉 → ⟨“ 𝐵 ”⟩ ∈ Word 𝑉 )
8 6 7 anim12i ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( ⟨“ 𝐴 ”⟩ ∈ Word 𝑉 ∧ ⟨“ 𝐵 ”⟩ ∈ Word 𝑉 ) )
9 8 adantr ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ) ) → ( ⟨“ 𝐴 ”⟩ ∈ Word 𝑉 ∧ ⟨“ 𝐵 ”⟩ ∈ Word 𝑉 ) )
10 s1cl ⊢ ( 𝐶 ∈ 𝑉 → ⟨“ 𝐶 ”⟩ ∈ Word 𝑉 )
11 s1cl ⊢ ( 𝐷 ∈ 𝑉 → ⟨“ 𝐷 ”⟩ ∈ Word 𝑉 )
12 10 11 anim12i ⊢ ( ( 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ) → ( ⟨“ 𝐶 ”⟩ ∈ Word 𝑉 ∧ ⟨“ 𝐷 ”⟩ ∈ Word 𝑉 ) )
13 12 adantl ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ) ) → ( ⟨“ 𝐶 ”⟩ ∈ Word 𝑉 ∧ ⟨“ 𝐷 ”⟩ ∈ Word 𝑉 ) )
14 s1len ⊢ ( ♯ ‘ ⟨“ 𝐴 ”⟩ ) = 1
15 s1len ⊢ ( ♯ ‘ ⟨“ 𝐶 ”⟩ ) = 1
16 14 15 eqtr4i ⊢ ( ♯ ‘ ⟨“ 𝐴 ”⟩ ) = ( ♯ ‘ ⟨“ 𝐶 ”⟩ )
17 16 a1i ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ) ) → ( ♯ ‘ ⟨“ 𝐴 ”⟩ ) = ( ♯ ‘ ⟨“ 𝐶 ”⟩ ) )
18 ccatopth ⊢ ( ( ( ⟨“ 𝐴 ”⟩ ∈ Word 𝑉 ∧ ⟨“ 𝐵 ”⟩ ∈ Word 𝑉 ) ∧ ( ⟨“ 𝐶 ”⟩ ∈ Word 𝑉 ∧ ⟨“ 𝐷 ”⟩ ∈ Word 𝑉 ) ∧ ( ♯ ‘ ⟨“ 𝐴 ”⟩ ) = ( ♯ ‘ ⟨“ 𝐶 ”⟩ ) ) → ( ( ⟨“ 𝐴 ”⟩ ++ ⟨“ 𝐵 ”⟩ ) = ( ⟨“ 𝐶 ”⟩ ++ ⟨“ 𝐷 ”⟩ ) ↔ ( ⟨“ 𝐴 ”⟩ = ⟨“ 𝐶 ”⟩ ∧ ⟨“ 𝐵 ”⟩ = ⟨“ 𝐷 ”⟩ ) ) )
19 9 13 17 18 syl3anc ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ) ) → ( ( ⟨“ 𝐴 ”⟩ ++ ⟨“ 𝐵 ”⟩ ) = ( ⟨“ 𝐶 ”⟩ ++ ⟨“ 𝐷 ”⟩ ) ↔ ( ⟨“ 𝐴 ”⟩ = ⟨“ 𝐶 ”⟩ ∧ ⟨“ 𝐵 ”⟩ = ⟨“ 𝐷 ”⟩ ) ) )
20 5 19 bitrd ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ) ) → ( ⟨“ 𝐴 𝐵 ”⟩ = ⟨“ 𝐶 𝐷 ”⟩ ↔ ( ⟨“ 𝐴 ”⟩ = ⟨“ 𝐶 ”⟩ ∧ ⟨“ 𝐵 ”⟩ = ⟨“ 𝐷 ”⟩ ) ) )