Metamath Proof Explorer


Theorem s3eqs2s1eq

Description: Two length 3 words are equal iff the corresponding length 2 words and singleton words consisting of their symbols are equal. (Contributed by AV, 4-Jan-2022)

Ref Expression
Assertion s3eqs2s1eq ( ( ( 𝐴𝑉𝐵𝑉𝐶𝑉 ) ∧ ( 𝐷𝑉𝐸𝑉𝐹𝑉 ) ) → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ = ⟨“ 𝐷 𝐸 𝐹 ”⟩ ↔ ( ⟨“ 𝐴 𝐵 ”⟩ = ⟨“ 𝐷 𝐸 ”⟩ ∧ ⟨“ 𝐶 ”⟩ = ⟨“ 𝐹 ”⟩ ) ) )

Proof

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