Metamath Proof Explorer

Theorem pmtrdifwrdellem3

Description: Lemma 3 for pmtrdifwrdel . (Contributed by AV, 15-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 pmtrdifwrdellem3 ⊢ W ∈ Word T → ∀ i ∈ 0 ..^ W ∀ n ∈ N ∖ K W ⁡ i ⁡ n = U ⁡ i ⁡ n

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 wrdsymbcl ⊢ W ∈ Word T ∧ i ∈ 0 ..^ W → W ⁡ i ∈ T
5 eqid ⊢ pmTrsp ⁡ N ⁡ dom ⁡ W ⁡ i ∖ I = pmTrsp ⁡ N ⁡ dom ⁡ W ⁡ i ∖ I
6 1 2 5 pmtrdifellem3 ⊢ W ⁡ i ∈ T → ∀ n ∈ N ∖ K W ⁡ i ⁡ n = pmTrsp ⁡ N ⁡ dom ⁡ W ⁡ i ∖ I ⁡ n
7 4 6 syl ⊢ W ∈ Word T ∧ i ∈ 0 ..^ W → ∀ n ∈ N ∖ K W ⁡ i ⁡ n = pmTrsp ⁡ N ⁡ dom ⁡ W ⁡ i ∖ I ⁡ n
8 fveq2 ⊢ x = i → W ⁡ x = W ⁡ i
9 8 difeq1d ⊢ x = i → W ⁡ x ∖ I = W ⁡ i ∖ I
10 9 dmeqd ⊢ x = i → dom ⁡ W ⁡ x ∖ I = dom ⁡ W ⁡ i ∖ I
11 10 fveq2d ⊢ x = i → pmTrsp ⁡ N ⁡ dom ⁡ W ⁡ x ∖ I = pmTrsp ⁡ N ⁡ dom ⁡ W ⁡ i ∖ I
12 simpr ⊢ W ∈ Word T ∧ i ∈ 0 ..^ W → i ∈ 0 ..^ W
13 fvexd ⊢ W ∈ Word T ∧ i ∈ 0 ..^ W → pmTrsp ⁡ N ⁡ dom ⁡ W ⁡ i ∖ I ∈ V
14 3 11 12 13 fvmptd3 ⊢ W ∈ Word T ∧ i ∈ 0 ..^ W → U ⁡ i = pmTrsp ⁡ N ⁡ dom ⁡ W ⁡ i ∖ I
15 14 fveq1d ⊢ W ∈ Word T ∧ i ∈ 0 ..^ W → U ⁡ i ⁡ n = pmTrsp ⁡ N ⁡ dom ⁡ W ⁡ i ∖ I ⁡ n
16 15 eqeq2d ⊢ W ∈ Word T ∧ i ∈ 0 ..^ W → W ⁡ i ⁡ n = U ⁡ i ⁡ n ↔ W ⁡ i ⁡ n = pmTrsp ⁡ N ⁡ dom ⁡ W ⁡ i ∖ I ⁡ n
17 16 ralbidv ⊢ W ∈ Word T ∧ i ∈ 0 ..^ W → ∀ n ∈ N ∖ K W ⁡ i ⁡ n = U ⁡ i ⁡ n ↔ ∀ n ∈ N ∖ K W ⁡ i ⁡ n = pmTrsp ⁡ N ⁡ dom ⁡ W ⁡ i ∖ I ⁡ n
18 7 17 mpbird ⊢ W ∈ Word T ∧ i ∈ 0 ..^ W → ∀ n ∈ N ∖ K W ⁡ i ⁡ n = U ⁡ i ⁡ n
19 18 ralrimiva ⊢ W ∈ Word T → ∀ i ∈ 0 ..^ W ∀ n ∈ N ∖ K W ⁡ i ⁡ n = U ⁡ i ⁡ n