Metamath Proof Explorer

Theorem pmtrdifwrdel2lem1

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

Ref Expression
Hypotheses pmtrdifel.t ⊢T=ran⁡pmTrsp⁡N∖K
pmtrdifel.r ⊢R=ran⁡pmTrsp⁡N
pmtrdifwrdel.0 ⊢U=x∈0..^W⟼pmTrsp⁡N⁡dom⁡W⁡x∖I
Assertion pmtrdifwrdel2lem1 ⊢W∈WordT∧K∈N→∀i∈0..^WU⁡i⁡K=K

Proof

Step Hyp Ref Expression
1 pmtrdifel.t ⊢T=ran⁡pmTrsp⁡N∖K
2 pmtrdifel.r ⊢R=ran⁡pmTrsp⁡N
3 pmtrdifwrdel.0 ⊢U=x∈0..^W⟼pmTrsp⁡N⁡dom⁡W⁡x∖I
4 simpr ⊢W∈WordT∧K∈N∧i∈0..^W→i∈0..^W
5 fvex ⊢pmTrsp⁡N⁡dom⁡W⁡i∖I∈V
6 fveq2 ⊢x=i→W⁡x=W⁡i
7 6 difeq1d ⊢x=i→W⁡x∖I=W⁡i∖I
8 7 dmeqd ⊢x=i→dom⁡W⁡x∖I=dom⁡W⁡i∖I
9 8 fveq2d ⊢x=i→pmTrsp⁡N⁡dom⁡W⁡x∖I=pmTrsp⁡N⁡dom⁡W⁡i∖I
10 9 3 fvmptg ⊢i∈0..^W∧pmTrsp⁡N⁡dom⁡W⁡i∖I∈V→U⁡i=pmTrsp⁡N⁡dom⁡W⁡i∖I
11 4 5 10 sylancl ⊢W∈WordT∧K∈N∧i∈0..^W→U⁡i=pmTrsp⁡N⁡dom⁡W⁡i∖I
12 11 fveq1d ⊢W∈WordT∧K∈N∧i∈0..^W→U⁡i⁡K=pmTrsp⁡N⁡dom⁡W⁡i∖I⁡K
13 wrdsymbcl ⊢W∈WordT∧i∈0..^W→W⁡i∈T
14 13 adantlr ⊢W∈WordT∧K∈N∧i∈0..^W→W⁡i∈T
15 simplr ⊢W∈WordT∧K∈N∧i∈0..^W→K∈N
16 eqid ⊢pmTrsp⁡N⁡dom⁡W⁡i∖I=pmTrsp⁡N⁡dom⁡W⁡i∖I
17 1 2 16 pmtrdifellem4 ⊢W⁡i∈T∧K∈N→pmTrsp⁡N⁡dom⁡W⁡i∖I⁡K=K
18 14 15 17 syl2anc ⊢W∈WordT∧K∈N∧i∈0..^W→pmTrsp⁡N⁡dom⁡W⁡i∖I⁡K=K
19 12 18 eqtrd ⊢W∈WordT∧K∈N∧i∈0..^W→U⁡i⁡K=K
20 19 ralrimiva ⊢W∈WordT∧K∈N→∀i∈0..^WU⁡i⁡K=K