Metamath Proof Explorer


Theorem wrdl1s1

Description: A word of length 1 is a singleton word consisting of the first symbol of the word. (Contributed by AV, 22-Jul-2018) (Proof shortened by AV, 14-Oct-2018)

Ref Expression
Assertion wrdl1s1 ( 𝑆𝑉 → ( 𝑊 = ⟨“ 𝑆 ”⟩ ↔ ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 1 ∧ ( 𝑊 ‘ 0 ) = 𝑆 ) ) )

Proof

Step Hyp Ref Expression
1 s1cl ( 𝑆𝑉 → ⟨“ 𝑆 ”⟩ ∈ Word 𝑉 )
2 s1len ( ♯ ‘ ⟨“ 𝑆 ”⟩ ) = 1
3 2 a1i ( 𝑆𝑉 → ( ♯ ‘ ⟨“ 𝑆 ”⟩ ) = 1 )
4 s1fv ( 𝑆𝑉 → ( ⟨“ 𝑆 ”⟩ ‘ 0 ) = 𝑆 )
5 1 3 4 3jca ( 𝑆𝑉 → ( ⟨“ 𝑆 ”⟩ ∈ Word 𝑉 ∧ ( ♯ ‘ ⟨“ 𝑆 ”⟩ ) = 1 ∧ ( ⟨“ 𝑆 ”⟩ ‘ 0 ) = 𝑆 ) )
6 eleq1 ( 𝑊 = ⟨“ 𝑆 ”⟩ → ( 𝑊 ∈ Word 𝑉 ↔ ⟨“ 𝑆 ”⟩ ∈ Word 𝑉 ) )
7 fveqeq2 ( 𝑊 = ⟨“ 𝑆 ”⟩ → ( ( ♯ ‘ 𝑊 ) = 1 ↔ ( ♯ ‘ ⟨“ 𝑆 ”⟩ ) = 1 ) )
8 fveq1 ( 𝑊 = ⟨“ 𝑆 ”⟩ → ( 𝑊 ‘ 0 ) = ( ⟨“ 𝑆 ”⟩ ‘ 0 ) )
9 8 eqeq1d ( 𝑊 = ⟨“ 𝑆 ”⟩ → ( ( 𝑊 ‘ 0 ) = 𝑆 ↔ ( ⟨“ 𝑆 ”⟩ ‘ 0 ) = 𝑆 ) )
10 6 7 9 3anbi123d ( 𝑊 = ⟨“ 𝑆 ”⟩ → ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 1 ∧ ( 𝑊 ‘ 0 ) = 𝑆 ) ↔ ( ⟨“ 𝑆 ”⟩ ∈ Word 𝑉 ∧ ( ♯ ‘ ⟨“ 𝑆 ”⟩ ) = 1 ∧ ( ⟨“ 𝑆 ”⟩ ‘ 0 ) = 𝑆 ) ) )
11 5 10 syl5ibrcom ( 𝑆𝑉 → ( 𝑊 = ⟨“ 𝑆 ”⟩ → ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 1 ∧ ( 𝑊 ‘ 0 ) = 𝑆 ) ) )
12 eqs1 ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 1 ) → 𝑊 = ⟨“ ( 𝑊 ‘ 0 ) ”⟩ )
13 s1eq ( ( 𝑊 ‘ 0 ) = 𝑆 → ⟨“ ( 𝑊 ‘ 0 ) ”⟩ = ⟨“ 𝑆 ”⟩ )
14 13 eqeq2d ( ( 𝑊 ‘ 0 ) = 𝑆 → ( 𝑊 = ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ↔ 𝑊 = ⟨“ 𝑆 ”⟩ ) )
15 12 14 syl5ibcom ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 1 ) → ( ( 𝑊 ‘ 0 ) = 𝑆𝑊 = ⟨“ 𝑆 ”⟩ ) )
16 15 3impia ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 1 ∧ ( 𝑊 ‘ 0 ) = 𝑆 ) → 𝑊 = ⟨“ 𝑆 ”⟩ )
17 11 16 impbid1 ( 𝑆𝑉 → ( 𝑊 = ⟨“ 𝑆 ”⟩ ↔ ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 1 ∧ ( 𝑊 ‘ 0 ) = 𝑆 ) ) )