Metamath Proof Explorer

Theorem pmtrdifwrdel2lem1

Description: Lemma 1 for pmtrdifwrdel2 . (Contributed by AV, 31-Jan-2019)

Ref Expression
Hypotheses pmtrdifel.t ⊢ 𝑇 = ran ( pmTrsp ‘ ( 𝑁 ∖ { 𝐾 } ) )
pmtrdifel.r ⊢ 𝑅 = ran ( pmTrsp ‘ 𝑁 )
pmtrdifwrdel.0 ⊢ 𝑈 = ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ↦ ( ( pmTrsp ‘ 𝑁 ) ‘ dom ( ( 𝑊 ‘ 𝑥 ) ∖ I ) ) )
Assertion pmtrdifwrdel2lem1 ( ( 𝑊 ∈ 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 simpr ⊢ ( ( ( 𝑊 ∈ Word 𝑇 ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
5 fvex ⊢ ( ( pmTrsp ‘ 𝑁 ) ‘ dom ( ( 𝑊 ‘ 𝑖 ) ∖ I ) ) ∈ V
6 fveq2 ⊢ ( 𝑥 = 𝑖 → ( 𝑊 ‘ 𝑥 ) = ( 𝑊 ‘ 𝑖 ) )
7 6 difeq1d ⊢ ( 𝑥 = 𝑖 → ( ( 𝑊 ‘ 𝑥 ) ∖ I ) = ( ( 𝑊 ‘ 𝑖 ) ∖ I ) )
8 7 dmeqd ⊢ ( 𝑥 = 𝑖 → dom ( ( 𝑊 ‘ 𝑥 ) ∖ I ) = dom ( ( 𝑊 ‘ 𝑖 ) ∖ I ) )
9 8 fveq2d ⊢ ( 𝑥 = 𝑖 → ( ( pmTrsp ‘ 𝑁 ) ‘ dom ( ( 𝑊 ‘ 𝑥 ) ∖ I ) ) = ( ( pmTrsp ‘ 𝑁 ) ‘ dom ( ( 𝑊 ‘ 𝑖 ) ∖ I ) ) )
10 9 3 fvmptg ⊢ ( ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∧ ( ( pmTrsp ‘ 𝑁 ) ‘ dom ( ( 𝑊 ‘ 𝑖 ) ∖ I ) ) ∈ V ) → ( 𝑈 ‘ 𝑖 ) = ( ( pmTrsp ‘ 𝑁 ) ‘ dom ( ( 𝑊 ‘ 𝑖 ) ∖ I ) ) )
11 4 5 10 sylancl ⊢ ( ( ( 𝑊 ∈ Word 𝑇 ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝑈 ‘ 𝑖 ) = ( ( pmTrsp ‘ 𝑁 ) ‘ dom ( ( 𝑊 ‘ 𝑖 ) ∖ I ) ) )
12 11 fveq1d ⊢ ( ( ( 𝑊 ∈ Word 𝑇 ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑈 ‘ 𝑖 ) ‘ 𝐾 ) = ( ( ( pmTrsp ‘ 𝑁 ) ‘ dom ( ( 𝑊 ‘ 𝑖 ) ∖ I ) ) ‘ 𝐾 ) )
13 wrdsymbcl ⊢ ( ( 𝑊 ∈ Word 𝑇 ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊 ‘ 𝑖 ) ∈ 𝑇 )
14 13 adantlr ⊢ ( ( ( 𝑊 ∈ Word 𝑇 ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊 ‘ 𝑖 ) ∈ 𝑇 )
15 simplr ⊢ ( ( ( 𝑊 ∈ Word 𝑇 ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → 𝐾 ∈ 𝑁 )
16 eqid ⊢ ( ( pmTrsp ‘ 𝑁 ) ‘ dom ( ( 𝑊 ‘ 𝑖 ) ∖ I ) ) = ( ( pmTrsp ‘ 𝑁 ) ‘ dom ( ( 𝑊 ‘ 𝑖 ) ∖ I ) )
17 1 2 16 pmtrdifellem4 ⊢ ( ( ( 𝑊 ‘ 𝑖 ) ∈ 𝑇 ∧ 𝐾 ∈ 𝑁 ) → ( ( ( pmTrsp ‘ 𝑁 ) ‘ dom ( ( 𝑊 ‘ 𝑖 ) ∖ I ) ) ‘ 𝐾 ) = 𝐾 )
18 14 15 17 syl2anc ⊢ ( ( ( 𝑊 ∈ Word 𝑇 ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( ( pmTrsp ‘ 𝑁 ) ‘ dom ( ( 𝑊 ‘ 𝑖 ) ∖ I ) ) ‘ 𝐾 ) = 𝐾 )
19 12 18 eqtrd ⊢ ( ( ( 𝑊 ∈ Word 𝑇 ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑈 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 )
20 19 ralrimiva ⊢ ( ( 𝑊 ∈ Word 𝑇 ∧ 𝐾 ∈ 𝑁 ) → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( 𝑈 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 )