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

Metamath Proof Explorer

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 𝑇 → ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) )