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 ∈ Word T ∧ K ∈ N → ∀ i ∈ 0 ..^ W U ⁡ 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 ∈ Word T ∧ 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 ∈ Word T ∧ K ∈ N ∧ i ∈ 0 ..^ W → U ⁡ i = pmTrsp ⁡ N ⁡ dom ⁡ W ⁡ i ∖ I
12 11 fveq1d ⊢ W ∈ Word T ∧ K ∈ N ∧ i ∈ 0 ..^ W → U ⁡ i ⁡ K = pmTrsp ⁡ N ⁡ dom ⁡ W ⁡ i ∖ I ⁡ K
13 wrdsymbcl ⊢ W ∈ Word T ∧ i ∈ 0 ..^ W → W ⁡ i ∈ T
14 13 adantlr ⊢ W ∈ Word T ∧ K ∈ N ∧ i ∈ 0 ..^ W → W ⁡ i ∈ T
15 simplr ⊢ W ∈ Word T ∧ 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 ∈ Word T ∧ K ∈ N ∧ i ∈ 0 ..^ W → pmTrsp ⁡ N ⁡ dom ⁡ W ⁡ i ∖ I ⁡ K = K
19 12 18 eqtrd ⊢ W ∈ Word T ∧ K ∈ N ∧ i ∈ 0 ..^ W → U ⁡ i ⁡ K = K
20 19 ralrimiva ⊢ W ∈ Word T ∧ K ∈ N → ∀ i ∈ 0 ..^ W U ⁡ i ⁡ K = K