Metamath Proof Explorer

Theorem lenco

Description: Length of a mapped word is unchanged. (Contributed by Stefan O'Rear, 27-Aug-2015)

Ref Expression
Assertion lenco ( ( 𝑊 ∈ Word 𝐴 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ( ♯ ‘ ( 𝐹 ∘ 𝑊 ) ) = ( ♯ ‘ 𝑊 ) )

Proof

Step Hyp Ref Expression
1 simpr ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → 𝐹 : 𝐴 ⟶ 𝐵 )
2 wrdf ⊢ ( 𝑊 ∈ Word 𝐴 → 𝑊 : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ 𝐴 )
3 2 adantr ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → 𝑊 : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ 𝐴 )
4 fco ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑊 : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ 𝐴 ) → ( 𝐹 ∘ 𝑊 ) : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ 𝐵 )
5 1 3 4 syl2anc ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ( 𝐹 ∘ 𝑊 ) : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ 𝐵 )
6 ffn ⊢ ( ( 𝐹 ∘ 𝑊 ) : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ 𝐵 → ( 𝐹 ∘ 𝑊 ) Fn ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
7 hashfn ⊢ ( ( 𝐹 ∘ 𝑊 ) Fn ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → ( ♯ ‘ ( 𝐹 ∘ 𝑊 ) ) = ( ♯ ‘ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) )
8 5 6 7 3syl ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ( ♯ ‘ ( 𝐹 ∘ 𝑊 ) ) = ( ♯ ‘ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) )
9 ffn ⊢ ( 𝑊 : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ 𝐴 → 𝑊 Fn ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
10 hashfn ⊢ ( 𝑊 Fn ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → ( ♯ ‘ 𝑊 ) = ( ♯ ‘ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) )
11 3 9 10 3syl ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ( ♯ ‘ 𝑊 ) = ( ♯ ‘ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) )
12 8 11 eqtr4d ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ( ♯ ‘ ( 𝐹 ∘ 𝑊 ) ) = ( ♯ ‘ 𝑊 ) )