Theorem pmtrdifwrdellem3

Description: Lemma 3 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	pmtrdifwrdellem3	⊢ ( 𝑊 ∈ Word 𝑇 → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∀ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑛 ) )

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	pmtrdifellem3	⊢ ( ( 𝑊 ‘ 𝑖 ) ∈ 𝑇 → ∀ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( ( pmTrsp ‘ 𝑁 ) ‘ dom ( ( 𝑊 ‘ 𝑖 ) ∖ I ) ) ‘ 𝑛 ) )
7	4 6	syl	⊢ ( ( 𝑊 ∈ Word 𝑇 ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ∀ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( ( pmTrsp ‘ 𝑁 ) ‘ dom ( ( 𝑊 ‘ 𝑖 ) ∖ I ) ) ‘ 𝑛 ) )
8		fveq2	⊢ ( 𝑥 = 𝑖 → ( 𝑊 ‘ 𝑥 ) = ( 𝑊 ‘ 𝑖 ) )
9	8	difeq1d	⊢ ( 𝑥 = 𝑖 → ( ( 𝑊 ‘ 𝑥 ) ∖ I ) = ( ( 𝑊 ‘ 𝑖 ) ∖ I ) )
10	9	dmeqd	⊢ ( 𝑥 = 𝑖 → dom ( ( 𝑊 ‘ 𝑥 ) ∖ I ) = dom ( ( 𝑊 ‘ 𝑖 ) ∖ I ) )
11	10	fveq2d	⊢ ( 𝑥 = 𝑖 → ( ( pmTrsp ‘ 𝑁 ) ‘ dom ( ( 𝑊 ‘ 𝑥 ) ∖ I ) ) = ( ( pmTrsp ‘ 𝑁 ) ‘ dom ( ( 𝑊 ‘ 𝑖 ) ∖ I ) ) )
12		simpr	⊢ ( ( 𝑊 ∈ Word 𝑇 ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
13		fvexd	⊢ ( ( 𝑊 ∈ Word 𝑇 ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( pmTrsp ‘ 𝑁 ) ‘ dom ( ( 𝑊 ‘ 𝑖 ) ∖ I ) ) ∈ V )
14	3 11 12 13	fvmptd3	⊢ ( ( 𝑊 ∈ Word 𝑇 ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝑈 ‘ 𝑖 ) = ( ( pmTrsp ‘ 𝑁 ) ‘ dom ( ( 𝑊 ‘ 𝑖 ) ∖ I ) ) )
15	14	fveq1d	⊢ ( ( 𝑊 ∈ Word 𝑇 ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( ( pmTrsp ‘ 𝑁 ) ‘ dom ( ( 𝑊 ‘ 𝑖 ) ∖ I ) ) ‘ 𝑛 ) )
16	15	eqeq2d	⊢ ( ( 𝑊 ∈ Word 𝑇 ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( ( 𝑊 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑛 ) ↔ ( ( 𝑊 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( ( pmTrsp ‘ 𝑁 ) ‘ dom ( ( 𝑊 ‘ 𝑖 ) ∖ I ) ) ‘ 𝑛 ) ) )
17	16	ralbidv	⊢ ( ( 𝑊 ∈ Word 𝑇 ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ∀ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑛 ) ↔ ∀ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( ( pmTrsp ‘ 𝑁 ) ‘ dom ( ( 𝑊 ‘ 𝑖 ) ∖ I ) ) ‘ 𝑛 ) ) )
18	7 17	mpbird	⊢ ( ( 𝑊 ∈ Word 𝑇 ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ∀ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑛 ) )
19	18	ralrimiva	⊢ ( 𝑊 ∈ Word 𝑇 → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∀ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑛 ) )