Metamath Proof Explorer

Theorem pthdlem2lem

Description: Lemma for pthdlem2 . (Contributed by AV, 10-Feb-2021)

Ref Expression
Hypotheses pthd.p ⊢ ( 𝜑 → 𝑃 ∈ Word V )
pthd.r ⊢ 𝑅 = ( ( ♯ ‘ 𝑃 ) − 1 )
pthd.s ⊢ ( 𝜑 → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑃 ) ) ∀ 𝑗 ∈ ( 1 ..^ 𝑅 ) ( 𝑖 ≠ 𝑗 → ( 𝑃 ‘ 𝑖 ) ≠ ( 𝑃 ‘ 𝑗 ) ) )
Assertion pthdlem2lem ( ( 𝜑 ∧ ( ♯ ‘ 𝑃 ) ∈ ℕ ∧ ( 𝐼 = 0 ∨ 𝐼 = 𝑅 ) ) → ( 𝑃 ‘ 𝐼 ) ∉ ( 𝑃 “ ( 1 ..^ 𝑅 ) ) )

Proof

Step Hyp Ref Expression
1 pthd.p ⊢ ( 𝜑 → 𝑃 ∈ Word V )
2 pthd.r ⊢ 𝑅 = ( ( ♯ ‘ 𝑃 ) − 1 )
3 pthd.s ⊢ ( 𝜑 → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑃 ) ) ∀ 𝑗 ∈ ( 1 ..^ 𝑅 ) ( 𝑖 ≠ 𝑗 → ( 𝑃 ‘ 𝑖 ) ≠ ( 𝑃 ‘ 𝑗 ) ) )
4 3 3ad2ant1 ⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝑃 ) ∈ ℕ ∧ ( 𝐼 = 0 ∨ 𝐼 = 𝑅 ) ) → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑃 ) ) ∀ 𝑗 ∈ ( 1 ..^ 𝑅 ) ( 𝑖 ≠ 𝑗 → ( 𝑃 ‘ 𝑖 ) ≠ ( 𝑃 ‘ 𝑗 ) ) )
5 ralcom ⊢ ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑃 ) ) ∀ 𝑗 ∈ ( 1 ..^ 𝑅 ) ( 𝑖 ≠ 𝑗 → ( 𝑃 ‘ 𝑖 ) ≠ ( 𝑃 ‘ 𝑗 ) ) ↔ ∀ 𝑗 ∈ ( 1 ..^ 𝑅 ) ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑃 ) ) ( 𝑖 ≠ 𝑗 → ( 𝑃 ‘ 𝑖 ) ≠ ( 𝑃 ‘ 𝑗 ) ) )
6 elfzo1 ⊢ ( 𝑗 ∈ ( 1 ..^ 𝑅 ) ↔ ( 𝑗 ∈ ℕ ∧ 𝑅 ∈ ℕ ∧ 𝑗 < 𝑅 ) )
7 nnne0 ⊢ ( 𝑗 ∈ ℕ → 𝑗 ≠ 0 )
8 7 necomd ⊢ ( 𝑗 ∈ ℕ → 0 ≠ 𝑗 )
9 8 3ad2ant1 ⊢ ( ( 𝑗 ∈ ℕ ∧ 𝑅 ∈ ℕ ∧ 𝑗 < 𝑅 ) → 0 ≠ 𝑗 )
10 6 9 sylbi ⊢ ( 𝑗 ∈ ( 1 ..^ 𝑅 ) → 0 ≠ 𝑗 )
11 10 adantl ⊢ ( ( ( ♯ ‘ 𝑃 ) ∈ ℕ ∧ 𝑗 ∈ ( 1 ..^ 𝑅 ) ) → 0 ≠ 𝑗 )
12 neeq1 ⊢ ( 𝐼 = 0 → ( 𝐼 ≠ 𝑗 ↔ 0 ≠ 𝑗 ) )
13 11 12 syl5ibr ⊢ ( 𝐼 = 0 → ( ( ( ♯ ‘ 𝑃 ) ∈ ℕ ∧ 𝑗 ∈ ( 1 ..^ 𝑅 ) ) → 𝐼 ≠ 𝑗 ) )
14 13 expd ⊢ ( 𝐼 = 0 → ( ( ♯ ‘ 𝑃 ) ∈ ℕ → ( 𝑗 ∈ ( 1 ..^ 𝑅 ) → 𝐼 ≠ 𝑗 ) ) )
15 nnre ⊢ ( 𝑗 ∈ ℕ → 𝑗 ∈ ℝ )
16 15 adantr ⊢ ( ( 𝑗 ∈ ℕ ∧ 𝑅 ∈ ℕ ) → 𝑗 ∈ ℝ )
17 nnre ⊢ ( 𝑅 ∈ ℕ → 𝑅 ∈ ℝ )
18 17 adantl ⊢ ( ( 𝑗 ∈ ℕ ∧ 𝑅 ∈ ℕ ) → 𝑅 ∈ ℝ )
19 16 18 ltlend ⊢ ( ( 𝑗 ∈ ℕ ∧ 𝑅 ∈ ℕ ) → ( 𝑗 < 𝑅 ↔ ( 𝑗 ≤ 𝑅 ∧ 𝑅 ≠ 𝑗 ) ) )
20 simpr ⊢ ( ( 𝑗 ≤ 𝑅 ∧ 𝑅 ≠ 𝑗 ) → 𝑅 ≠ 𝑗 )
21 19 20 syl6bi ⊢ ( ( 𝑗 ∈ ℕ ∧ 𝑅 ∈ ℕ ) → ( 𝑗 < 𝑅 → 𝑅 ≠ 𝑗 ) )
22 21 3impia ⊢ ( ( 𝑗 ∈ ℕ ∧ 𝑅 ∈ ℕ ∧ 𝑗 < 𝑅 ) → 𝑅 ≠ 𝑗 )
23 6 22 sylbi ⊢ ( 𝑗 ∈ ( 1 ..^ 𝑅 ) → 𝑅 ≠ 𝑗 )
24 23 adantl ⊢ ( ( ( ♯ ‘ 𝑃 ) ∈ ℕ ∧ 𝑗 ∈ ( 1 ..^ 𝑅 ) ) → 𝑅 ≠ 𝑗 )
25 neeq1 ⊢ ( 𝐼 = 𝑅 → ( 𝐼 ≠ 𝑗 ↔ 𝑅 ≠ 𝑗 ) )
26 24 25 syl5ibr ⊢ ( 𝐼 = 𝑅 → ( ( ( ♯ ‘ 𝑃 ) ∈ ℕ ∧ 𝑗 ∈ ( 1 ..^ 𝑅 ) ) → 𝐼 ≠ 𝑗 ) )
27 26 expd ⊢ ( 𝐼 = 𝑅 → ( ( ♯ ‘ 𝑃 ) ∈ ℕ → ( 𝑗 ∈ ( 1 ..^ 𝑅 ) → 𝐼 ≠ 𝑗 ) ) )
28 14 27 jaoi ⊢ ( ( 𝐼 = 0 ∨ 𝐼 = 𝑅 ) → ( ( ♯ ‘ 𝑃 ) ∈ ℕ → ( 𝑗 ∈ ( 1 ..^ 𝑅 ) → 𝐼 ≠ 𝑗 ) ) )
29 28 impcom ⊢ ( ( ( ♯ ‘ 𝑃 ) ∈ ℕ ∧ ( 𝐼 = 0 ∨ 𝐼 = 𝑅 ) ) → ( 𝑗 ∈ ( 1 ..^ 𝑅 ) → 𝐼 ≠ 𝑗 ) )
30 29 3adant1 ⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝑃 ) ∈ ℕ ∧ ( 𝐼 = 0 ∨ 𝐼 = 𝑅 ) ) → ( 𝑗 ∈ ( 1 ..^ 𝑅 ) → 𝐼 ≠ 𝑗 ) )
31 30 imp ⊢ ( ( ( 𝜑 ∧ ( ♯ ‘ 𝑃 ) ∈ ℕ ∧ ( 𝐼 = 0 ∨ 𝐼 = 𝑅 ) ) ∧ 𝑗 ∈ ( 1 ..^ 𝑅 ) ) → 𝐼 ≠ 𝑗 )
32 lbfzo0 ⊢ ( 0 ∈ ( 0 ..^ ( ♯ ‘ 𝑃 ) ) ↔ ( ♯ ‘ 𝑃 ) ∈ ℕ )
33 32 biimpri ⊢ ( ( ♯ ‘ 𝑃 ) ∈ ℕ → 0 ∈ ( 0 ..^ ( ♯ ‘ 𝑃 ) ) )
34 eleq1 ⊢ ( 𝐼 = 0 → ( 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑃 ) ) ↔ 0 ∈ ( 0 ..^ ( ♯ ‘ 𝑃 ) ) ) )
35 33 34 syl5ibr ⊢ ( 𝐼 = 0 → ( ( ♯ ‘ 𝑃 ) ∈ ℕ → 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑃 ) ) ) )
36 fzo0end ⊢ ( ( ♯ ‘ 𝑃 ) ∈ ℕ → ( ( ♯ ‘ 𝑃 ) − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑃 ) ) )
37 2 36 eqeltrid ⊢ ( ( ♯ ‘ 𝑃 ) ∈ ℕ → 𝑅 ∈ ( 0 ..^ ( ♯ ‘ 𝑃 ) ) )
38 eleq1 ⊢ ( 𝐼 = 𝑅 → ( 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑃 ) ) ↔ 𝑅 ∈ ( 0 ..^ ( ♯ ‘ 𝑃 ) ) ) )
39 37 38 syl5ibr ⊢ ( 𝐼 = 𝑅 → ( ( ♯ ‘ 𝑃 ) ∈ ℕ → 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑃 ) ) ) )
40 35 39 jaoi ⊢ ( ( 𝐼 = 0 ∨ 𝐼 = 𝑅 ) → ( ( ♯ ‘ 𝑃 ) ∈ ℕ → 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑃 ) ) ) )
41 40 impcom ⊢ ( ( ( ♯ ‘ 𝑃 ) ∈ ℕ ∧ ( 𝐼 = 0 ∨ 𝐼 = 𝑅 ) ) → 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑃 ) ) )
42 41 3adant1 ⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝑃 ) ∈ ℕ ∧ ( 𝐼 = 0 ∨ 𝐼 = 𝑅 ) ) → 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑃 ) ) )
43 42 adantr ⊢ ( ( ( 𝜑 ∧ ( ♯ ‘ 𝑃 ) ∈ ℕ ∧ ( 𝐼 = 0 ∨ 𝐼 = 𝑅 ) ) ∧ 𝑗 ∈ ( 1 ..^ 𝑅 ) ) → 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑃 ) ) )
44 neeq1 ⊢ ( 𝑖 = 𝐼 → ( 𝑖 ≠ 𝑗 ↔ 𝐼 ≠ 𝑗 ) )
45 fveq2 ⊢ ( 𝑖 = 𝐼 → ( 𝑃 ‘ 𝑖 ) = ( 𝑃 ‘ 𝐼 ) )
46 45 neeq1d ⊢ ( 𝑖 = 𝐼 → ( ( 𝑃 ‘ 𝑖 ) ≠ ( 𝑃 ‘ 𝑗 ) ↔ ( 𝑃 ‘ 𝐼 ) ≠ ( 𝑃 ‘ 𝑗 ) ) )
47 44 46 imbi12d ⊢ ( 𝑖 = 𝐼 → ( ( 𝑖 ≠ 𝑗 → ( 𝑃 ‘ 𝑖 ) ≠ ( 𝑃 ‘ 𝑗 ) ) ↔ ( 𝐼 ≠ 𝑗 → ( 𝑃 ‘ 𝐼 ) ≠ ( 𝑃 ‘ 𝑗 ) ) ) )
48 47 rspcv ⊢ ( 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑃 ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑃 ) ) ( 𝑖 ≠ 𝑗 → ( 𝑃 ‘ 𝑖 ) ≠ ( 𝑃 ‘ 𝑗 ) ) → ( 𝐼 ≠ 𝑗 → ( 𝑃 ‘ 𝐼 ) ≠ ( 𝑃 ‘ 𝑗 ) ) ) )
49 43 48 syl ⊢ ( ( ( 𝜑 ∧ ( ♯ ‘ 𝑃 ) ∈ ℕ ∧ ( 𝐼 = 0 ∨ 𝐼 = 𝑅 ) ) ∧ 𝑗 ∈ ( 1 ..^ 𝑅 ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑃 ) ) ( 𝑖 ≠ 𝑗 → ( 𝑃 ‘ 𝑖 ) ≠ ( 𝑃 ‘ 𝑗 ) ) → ( 𝐼 ≠ 𝑗 → ( 𝑃 ‘ 𝐼 ) ≠ ( 𝑃 ‘ 𝑗 ) ) ) )
50 31 49 mpid ⊢ ( ( ( 𝜑 ∧ ( ♯ ‘ 𝑃 ) ∈ ℕ ∧ ( 𝐼 = 0 ∨ 𝐼 = 𝑅 ) ) ∧ 𝑗 ∈ ( 1 ..^ 𝑅 ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑃 ) ) ( 𝑖 ≠ 𝑗 → ( 𝑃 ‘ 𝑖 ) ≠ ( 𝑃 ‘ 𝑗 ) ) → ( 𝑃 ‘ 𝐼 ) ≠ ( 𝑃 ‘ 𝑗 ) ) )
51 nesym ⊢ ( ( 𝑃 ‘ 𝐼 ) ≠ ( 𝑃 ‘ 𝑗 ) ↔ ¬ ( 𝑃 ‘ 𝑗 ) = ( 𝑃 ‘ 𝐼 ) )
52 50 51 syl6ib ⊢ ( ( ( 𝜑 ∧ ( ♯ ‘ 𝑃 ) ∈ ℕ ∧ ( 𝐼 = 0 ∨ 𝐼 = 𝑅 ) ) ∧ 𝑗 ∈ ( 1 ..^ 𝑅 ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑃 ) ) ( 𝑖 ≠ 𝑗 → ( 𝑃 ‘ 𝑖 ) ≠ ( 𝑃 ‘ 𝑗 ) ) → ¬ ( 𝑃 ‘ 𝑗 ) = ( 𝑃 ‘ 𝐼 ) ) )
53 52 ralimdva ⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝑃 ) ∈ ℕ ∧ ( 𝐼 = 0 ∨ 𝐼 = 𝑅 ) ) → ( ∀ 𝑗 ∈ ( 1 ..^ 𝑅 ) ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑃 ) ) ( 𝑖 ≠ 𝑗 → ( 𝑃 ‘ 𝑖 ) ≠ ( 𝑃 ‘ 𝑗 ) ) → ∀ 𝑗 ∈ ( 1 ..^ 𝑅 ) ¬ ( 𝑃 ‘ 𝑗 ) = ( 𝑃 ‘ 𝐼 ) ) )
54 5 53 syl5bi ⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝑃 ) ∈ ℕ ∧ ( 𝐼 = 0 ∨ 𝐼 = 𝑅 ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑃 ) ) ∀ 𝑗 ∈ ( 1 ..^ 𝑅 ) ( 𝑖 ≠ 𝑗 → ( 𝑃 ‘ 𝑖 ) ≠ ( 𝑃 ‘ 𝑗 ) ) → ∀ 𝑗 ∈ ( 1 ..^ 𝑅 ) ¬ ( 𝑃 ‘ 𝑗 ) = ( 𝑃 ‘ 𝐼 ) ) )
55 4 54 mpd ⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝑃 ) ∈ ℕ ∧ ( 𝐼 = 0 ∨ 𝐼 = 𝑅 ) ) → ∀ 𝑗 ∈ ( 1 ..^ 𝑅 ) ¬ ( 𝑃 ‘ 𝑗 ) = ( 𝑃 ‘ 𝐼 ) )
56 ralnex ⊢ ( ∀ 𝑗 ∈ ( 1 ..^ 𝑅 ) ¬ ( 𝑃 ‘ 𝑗 ) = ( 𝑃 ‘ 𝐼 ) ↔ ¬ ∃ 𝑗 ∈ ( 1 ..^ 𝑅 ) ( 𝑃 ‘ 𝑗 ) = ( 𝑃 ‘ 𝐼 ) )
57 55 56 sylib ⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝑃 ) ∈ ℕ ∧ ( 𝐼 = 0 ∨ 𝐼 = 𝑅 ) ) → ¬ ∃ 𝑗 ∈ ( 1 ..^ 𝑅 ) ( 𝑃 ‘ 𝑗 ) = ( 𝑃 ‘ 𝐼 ) )
58 wrdf ⊢ ( 𝑃 ∈ Word V → 𝑃 : ( 0 ..^ ( ♯ ‘ 𝑃 ) ) ⟶ V )
59 ffun ⊢ ( 𝑃 : ( 0 ..^ ( ♯ ‘ 𝑃 ) ) ⟶ V → Fun 𝑃 )
60 1 58 59 3syl ⊢ ( 𝜑 → Fun 𝑃 )
61 60 3ad2ant1 ⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝑃 ) ∈ ℕ ∧ ( 𝐼 = 0 ∨ 𝐼 = 𝑅 ) ) → Fun 𝑃 )
62 fvelima ⊢ ( ( Fun 𝑃 ∧ ( 𝑃 ‘ 𝐼 ) ∈ ( 𝑃 “ ( 1 ..^ 𝑅 ) ) ) → ∃ 𝑗 ∈ ( 1 ..^ 𝑅 ) ( 𝑃 ‘ 𝑗 ) = ( 𝑃 ‘ 𝐼 ) )
63 62 ex ⊢ ( Fun 𝑃 → ( ( 𝑃 ‘ 𝐼 ) ∈ ( 𝑃 “ ( 1 ..^ 𝑅 ) ) → ∃ 𝑗 ∈ ( 1 ..^ 𝑅 ) ( 𝑃 ‘ 𝑗 ) = ( 𝑃 ‘ 𝐼 ) ) )
64 61 63 syl ⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝑃 ) ∈ ℕ ∧ ( 𝐼 = 0 ∨ 𝐼 = 𝑅 ) ) → ( ( 𝑃 ‘ 𝐼 ) ∈ ( 𝑃 “ ( 1 ..^ 𝑅 ) ) → ∃ 𝑗 ∈ ( 1 ..^ 𝑅 ) ( 𝑃 ‘ 𝑗 ) = ( 𝑃 ‘ 𝐼 ) ) )
65 57 64 mtod ⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝑃 ) ∈ ℕ ∧ ( 𝐼 = 0 ∨ 𝐼 = 𝑅 ) ) → ¬ ( 𝑃 ‘ 𝐼 ) ∈ ( 𝑃 “ ( 1 ..^ 𝑅 ) ) )
66 df-nel ⊢ ( ( 𝑃 ‘ 𝐼 ) ∉ ( 𝑃 “ ( 1 ..^ 𝑅 ) ) ↔ ¬ ( 𝑃 ‘ 𝐼 ) ∈ ( 𝑃 “ ( 1 ..^ 𝑅 ) ) )
67 65 66 sylibr ⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝑃 ) ∈ ℕ ∧ ( 𝐼 = 0 ∨ 𝐼 = 𝑅 ) ) → ( 𝑃 ‘ 𝐼 ) ∉ ( 𝑃 “ ( 1 ..^ 𝑅 ) ) )