This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem clwlkclwwlklem2a3

Description: Lemma 3 for clwlkclwwlklem2a . (Contributed by Alexander van der Vekens, 21-Jun-2018)

Ref Expression
Hypothesis clwlkclwwlklem2.f ⊢ 𝐹 = ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ if ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ 0 ) } ) ) )
Assertion clwlkclwwlklem2a3 ( ( 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = ( lastS ‘ 𝑃 ) )

Proof

Step Hyp Ref Expression
1 clwlkclwwlklem2.f ⊢ 𝐹 = ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ if ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ 0 ) } ) ) )
2 lsw ⊢ ( 𝑃 ∈ Word 𝑉 → ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 1 ) ) )
3 2 adantr ⊢ ( ( 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 1 ) ) )
4 1 clwlkclwwlklem2a2 ⊢ ( ( 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( ♯ ‘ 𝐹 ) = ( ( ♯ ‘ 𝑃 ) − 1 ) )
5 4 eqcomd ⊢ ( ( 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( ( ♯ ‘ 𝑃 ) − 1 ) = ( ♯ ‘ 𝐹 ) )
6 5 fveq2d ⊢ ( ( 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 1 ) ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) )
7 3 6 eqtr2d ⊢ ( ( 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = ( lastS ‘ 𝑃 ) )