lenco

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

		Ref	Expression
	Assertion	lenco	$⊢ (W \in Word A \land F : A ⟶ B) \to \|F \circ W\| = \|W\|$

Step	Hyp	Ref	Expression
1		simpr	$⊢ (W \in Word A \land F : A ⟶ B) \to F : A ⟶ B$
2		wrdf	$⊢ W \in Word A \to W : (0 ..^\|W\|) ⟶ A$
3	2	adantr	$⊢ (W \in Word A \land F : A ⟶ B) \to W : (0 ..^\|W\|) ⟶ A$
4		fco	$⊢ (F : A ⟶ B \land W : (0 ..^\|W\|) ⟶ A) \to (F \circ W) : (0 ..^\|W\|) ⟶ B$
5	1 3 4	syl2anc	$⊢ (W \in Word A \land F : A ⟶ B) \to (F \circ W) : (0 ..^\|W\|) ⟶ B$
6		ffn	$⊢ (F \circ W) : (0 ..^\|W\|) ⟶ B \to (F \circ W) Fn (0 ..^\|W\|)$
7		hashfn	$⊢ (F \circ W) Fn (0 ..^\|W\|) \to \|F \circ W\| = \|(0 ..^\|W\|)\|$
8	5 6 7	3syl	$⊢ (W \in Word A \land F : A ⟶ B) \to \|F \circ W\| = \|(0 ..^\|W\|)\|$
9		ffn	$⊢ W : (0 ..^\|W\|) ⟶ A \to W Fn (0 ..^\|W\|)$
10		hashfn	$⊢ W Fn (0 ..^\|W\|) \to \|W\| = \|(0 ..^\|W\|)\|$
11	3 9 10	3syl	$⊢ (W \in Word A \land F : A ⟶ B) \to \|W\| = \|(0 ..^\|W\|)\|$
12	8 11	eqtr4d	$⊢ (W \in Word A \land F : A ⟶ B) \to \|F \circ W\| = \|W\|$

Metamath Proof Explorer