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

Metamath Proof Explorer

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 ..^ ( ♯ ‘ 𝑊 ) ) ∀ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑛 ) )