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 ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ∧ ( 𝐷 ∈ 𝑉 ∧ 𝐸 ∈ 𝑉 ∧ 𝐹 ∈ 𝑉 ) ) → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ = ⟨“ 𝐷 𝐸 𝐹 ”⟩ ↔ ( ⟨“ 𝐴 𝐵 ”⟩ = ⟨“ 𝐷 𝐸 ”⟩ ∧ ⟨“ 𝐶 ”⟩ = ⟨“ 𝐹 ”⟩ ) ) )