Database
REAL AND COMPLEX NUMBERS
Words over a set
Mapping words by a function
lenco
Next ⟩
s1co
Metamath Proof Explorer
Ascii
Unicode
Theorem
lenco
Description:
Length of a mapped word is unchanged.
(Contributed by
Stefan O'Rear
, 27-Aug-2015)
Ref
Expression
Assertion
lenco
⊢
W
∈
Word
A
∧
F
:
A
⟶
B
→
F
∘
W
=
W
Proof
Step
Hyp
Ref
Expression
1
simpr
⊢
W
∈
Word
A
∧
F
:
A
⟶
B
→
F
:
A
⟶
B
2
wrdf
⊢
W
∈
Word
A
→
W
:
0
..^
W
⟶
A
3
2
adantr
⊢
W
∈
Word
A
∧
F
:
A
⟶
B
→
W
:
0
..^
W
⟶
A
4
fco
⊢
F
:
A
⟶
B
∧
W
:
0
..^
W
⟶
A
→
F
∘
W
:
0
..^
W
⟶
B
5
1
3
4
syl2anc
⊢
W
∈
Word
A
∧
F
:
A
⟶
B
→
F
∘
W
:
0
..^
W
⟶
B
6
ffn
⊢
F
∘
W
:
0
..^
W
⟶
B
→
F
∘
W
Fn
0
..^
W
7
hashfn
⊢
F
∘
W
Fn
0
..^
W
→
F
∘
W
=
0
..^
W
8
5
6
7
3syl
⊢
W
∈
Word
A
∧
F
:
A
⟶
B
→
F
∘
W
=
0
..^
W
9
ffn
⊢
W
:
0
..^
W
⟶
A
→
W
Fn
0
..^
W
10
hashfn
⊢
W
Fn
0
..^
W
→
W
=
0
..^
W
11
3
9
10
3syl
⊢
W
∈
Word
A
∧
F
:
A
⟶
B
→
W
=
0
..^
W
12
8
11
eqtr4d
⊢
W
∈
Word
A
∧
F
:
A
⟶
B
→
F
∘
W
=
W