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 𝑅 )