Theorem pmtrdifwrdellem2

Description: Lemma 2 for pmtrdifwrdel . (Contributed by AV, 15-Jan-2019)

	Ref	Expression
Hypotheses	pmtrdifel.t	⊢ 𝑇 = ran ( pmTrsp ‘ ( 𝑁 ∖ { 𝐾 } ) )
	pmtrdifel.r	⊢ 𝑅 = ran ( pmTrsp ‘ 𝑁 )
	pmtrdifwrdel.0	⊢ 𝑈 = ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ↦ ( ( pmTrsp ‘ 𝑁 ) ‘ dom ( ( 𝑊 ‘ 𝑥 ) ∖ I ) ) )
Assertion	pmtrdifwrdellem2	⊢ ( 𝑊 ∈ Word 𝑇 → ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) )

Proof

Step	Hyp	Ref	Expression
1		pmtrdifel.t	⊢ 𝑇 = ran ( pmTrsp ‘ ( 𝑁 ∖ { 𝐾 } ) )
2		pmtrdifel.r	⊢ 𝑅 = ran ( pmTrsp ‘ 𝑁 )
3		pmtrdifwrdel.0	⊢ 𝑈 = ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ↦ ( ( pmTrsp ‘ 𝑁 ) ‘ dom ( ( 𝑊 ‘ 𝑥 ) ∖ I ) ) )
4		wrdsymbcl	⊢ ( ( 𝑊 ∈ Word 𝑇 ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊 ‘ 𝑥 ) ∈ 𝑇 )
5		eqid	⊢ ( ( pmTrsp ‘ 𝑁 ) ‘ dom ( ( 𝑊 ‘ 𝑥 ) ∖ I ) ) = ( ( pmTrsp ‘ 𝑁 ) ‘ dom ( ( 𝑊 ‘ 𝑥 ) ∖ I ) )
6	1 2 5	pmtrdifellem1	⊢ ( ( 𝑊 ‘ 𝑥 ) ∈ 𝑇 → ( ( pmTrsp ‘ 𝑁 ) ‘ dom ( ( 𝑊 ‘ 𝑥 ) ∖ I ) ) ∈ 𝑅 )
7	4 6	syl	⊢ ( ( 𝑊 ∈ Word 𝑇 ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( pmTrsp ‘ 𝑁 ) ‘ dom ( ( 𝑊 ‘ 𝑥 ) ∖ I ) ) ∈ 𝑅 )
8	7	ralrimiva	⊢ ( 𝑊 ∈ Word 𝑇 → ∀ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( pmTrsp ‘ 𝑁 ) ‘ dom ( ( 𝑊 ‘ 𝑥 ) ∖ I ) ) ∈ 𝑅 )
9	3	fnmpt	⊢ ( ∀ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( pmTrsp ‘ 𝑁 ) ‘ dom ( ( 𝑊 ‘ 𝑥 ) ∖ I ) ) ∈ 𝑅 → 𝑈 Fn ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
10		hashfn	⊢ ( 𝑈 Fn ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → ( ♯ ‘ 𝑈 ) = ( ♯ ‘ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) )
11	8 9 10	3syl	⊢ ( 𝑊 ∈ Word 𝑇 → ( ♯ ‘ 𝑈 ) = ( ♯ ‘ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) )
12		lencl	⊢ ( 𝑊 ∈ Word 𝑇 → ( ♯ ‘ 𝑊 ) ∈ ℕ0 )
13		hashfzo0	⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 → ( ♯ ‘ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) = ( ♯ ‘ 𝑊 ) )
14	12 13	syl	⊢ ( 𝑊 ∈ Word 𝑇 → ( ♯ ‘ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) = ( ♯ ‘ 𝑊 ) )
15	11 14	eqtr2d	⊢ ( 𝑊 ∈ Word 𝑇 → ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) )