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

Metamath Proof Explorer

Theorem pmtrdifwrdellem1

Description: Lemma 1 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 pmtrdifwrdellem1 ( 𝑊 ∈ Word 𝑇 → 𝑈 ∈ 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 3 fmptd ⊢ ( 𝑊 ∈ Word 𝑇 → 𝑈 : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ 𝑅 )
9 iswrdi ⊢ ( 𝑈 : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ 𝑅 → 𝑈 ∈ Word 𝑅 )
10 8 9 syl ⊢ ( 𝑊 ∈ Word 𝑇 → 𝑈 ∈ Word 𝑅 )