Metamath Proof Explorer

Theorem wlkp1lem6

Description: Lemma for wlkp1 . (Contributed by AV, 6-Mar-2021)

Ref Expression
Hypotheses wlkp1.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
wlkp1.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
wlkp1.f ⊢ ( 𝜑 → Fun 𝐼 )
wlkp1.a ⊢ ( 𝜑 → 𝐼 ∈ Fin )
wlkp1.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
wlkp1.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
wlkp1.d ⊢ ( 𝜑 → ¬ 𝐵 ∈ dom 𝐼 )
wlkp1.w ⊢ ( 𝜑 → 𝐹 ( Walks ‘ 𝐺 ) 𝑃 )
wlkp1.n ⊢ 𝑁 = ( ♯ ‘ 𝐹 )
wlkp1.e ⊢ ( 𝜑 → 𝐸 ∈ ( Edg ‘ 𝐺 ) )
wlkp1.x ⊢ ( 𝜑 → { ( 𝑃 ‘ 𝑁 ) , 𝐶 } ⊆ 𝐸 )
wlkp1.u ⊢ ( 𝜑 → ( iEdg ‘ 𝑆 ) = ( 𝐼 ∪ { ⟨ 𝐵 , 𝐸 ⟩ } ) )
wlkp1.h ⊢ 𝐻 = ( 𝐹 ∪ { ⟨ 𝑁 , 𝐵 ⟩ } )
wlkp1.q ⊢ 𝑄 = ( 𝑃 ∪ { ⟨ ( 𝑁 + 1 ) , 𝐶 ⟩ } )
wlkp1.s ⊢ ( 𝜑 → ( Vtx ‘ 𝑆 ) = 𝑉 )
Assertion wlkp1lem6 ( 𝜑 → ∀ 𝑘 ∈ ( 0 ..^ 𝑁 ) ( ( 𝑄 ‘ 𝑘 ) = ( 𝑃 ‘ 𝑘 ) ∧ ( 𝑄 ‘ ( 𝑘 + 1 ) ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∧ ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑘 ) ) = ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) )

Proof

Step Hyp Ref Expression
1 wlkp1.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 wlkp1.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
3 wlkp1.f ⊢ ( 𝜑 → Fun 𝐼 )
4 wlkp1.a ⊢ ( 𝜑 → 𝐼 ∈ Fin )
5 wlkp1.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
6 wlkp1.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
7 wlkp1.d ⊢ ( 𝜑 → ¬ 𝐵 ∈ dom 𝐼 )
8 wlkp1.w ⊢ ( 𝜑 → 𝐹 ( Walks ‘ 𝐺 ) 𝑃 )
9 wlkp1.n ⊢ 𝑁 = ( ♯ ‘ 𝐹 )
10 wlkp1.e ⊢ ( 𝜑 → 𝐸 ∈ ( Edg ‘ 𝐺 ) )
11 wlkp1.x ⊢ ( 𝜑 → { ( 𝑃 ‘ 𝑁 ) , 𝐶 } ⊆ 𝐸 )
12 wlkp1.u ⊢ ( 𝜑 → ( iEdg ‘ 𝑆 ) = ( 𝐼 ∪ { ⟨ 𝐵 , 𝐸 ⟩ } ) )
13 wlkp1.h ⊢ 𝐻 = ( 𝐹 ∪ { ⟨ 𝑁 , 𝐵 ⟩ } )
14 wlkp1.q ⊢ 𝑄 = ( 𝑃 ∪ { ⟨ ( 𝑁 + 1 ) , 𝐶 ⟩ } )
15 wlkp1.s ⊢ ( 𝜑 → ( Vtx ‘ 𝑆 ) = 𝑉 )
16 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 wlkp1lem5 ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( 0 ... 𝑁 ) ( 𝑄 ‘ 𝑥 ) = ( 𝑃 ‘ 𝑥 ) )
17 elfzofz ⊢ ( 𝑘 ∈ ( 0 ..^ 𝑁 ) → 𝑘 ∈ ( 0 ... 𝑁 ) )
18 17 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → 𝑘 ∈ ( 0 ... 𝑁 ) )
19 fveq2 ⊢ ( 𝑥 = 𝑘 → ( 𝑄 ‘ 𝑥 ) = ( 𝑄 ‘ 𝑘 ) )
20 fveq2 ⊢ ( 𝑥 = 𝑘 → ( 𝑃 ‘ 𝑥 ) = ( 𝑃 ‘ 𝑘 ) )
21 19 20 eqeq12d ⊢ ( 𝑥 = 𝑘 → ( ( 𝑄 ‘ 𝑥 ) = ( 𝑃 ‘ 𝑥 ) ↔ ( 𝑄 ‘ 𝑘 ) = ( 𝑃 ‘ 𝑘 ) ) )
22 21 rspcv ⊢ ( 𝑘 ∈ ( 0 ... 𝑁 ) → ( ∀ 𝑥 ∈ ( 0 ... 𝑁 ) ( 𝑄 ‘ 𝑥 ) = ( 𝑃 ‘ 𝑥 ) → ( 𝑄 ‘ 𝑘 ) = ( 𝑃 ‘ 𝑘 ) ) )
23 18 22 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → ( ∀ 𝑥 ∈ ( 0 ... 𝑁 ) ( 𝑄 ‘ 𝑥 ) = ( 𝑃 ‘ 𝑥 ) → ( 𝑄 ‘ 𝑘 ) = ( 𝑃 ‘ 𝑘 ) ) )
24 23 imp ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) ∧ ∀ 𝑥 ∈ ( 0 ... 𝑁 ) ( 𝑄 ‘ 𝑥 ) = ( 𝑃 ‘ 𝑥 ) ) → ( 𝑄 ‘ 𝑘 ) = ( 𝑃 ‘ 𝑘 ) )
25 fzofzp1 ⊢ ( 𝑘 ∈ ( 0 ..^ 𝑁 ) → ( 𝑘 + 1 ) ∈ ( 0 ... 𝑁 ) )
26 25 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑘 + 1 ) ∈ ( 0 ... 𝑁 ) )
27 fveq2 ⊢ ( 𝑥 = ( 𝑘 + 1 ) → ( 𝑄 ‘ 𝑥 ) = ( 𝑄 ‘ ( 𝑘 + 1 ) ) )
28 fveq2 ⊢ ( 𝑥 = ( 𝑘 + 1 ) → ( 𝑃 ‘ 𝑥 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) )
29 27 28 eqeq12d ⊢ ( 𝑥 = ( 𝑘 + 1 ) → ( ( 𝑄 ‘ 𝑥 ) = ( 𝑃 ‘ 𝑥 ) ↔ ( 𝑄 ‘ ( 𝑘 + 1 ) ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) )
30 29 rspcv ⊢ ( ( 𝑘 + 1 ) ∈ ( 0 ... 𝑁 ) → ( ∀ 𝑥 ∈ ( 0 ... 𝑁 ) ( 𝑄 ‘ 𝑥 ) = ( 𝑃 ‘ 𝑥 ) → ( 𝑄 ‘ ( 𝑘 + 1 ) ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) )
31 26 30 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → ( ∀ 𝑥 ∈ ( 0 ... 𝑁 ) ( 𝑄 ‘ 𝑥 ) = ( 𝑃 ‘ 𝑥 ) → ( 𝑄 ‘ ( 𝑘 + 1 ) ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) )
32 31 imp ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) ∧ ∀ 𝑥 ∈ ( 0 ... 𝑁 ) ( 𝑄 ‘ 𝑥 ) = ( 𝑃 ‘ 𝑥 ) ) → ( 𝑄 ‘ ( 𝑘 + 1 ) ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) )
33 12 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → ( iEdg ‘ 𝑆 ) = ( 𝐼 ∪ { ⟨ 𝐵 , 𝐸 ⟩ } ) )
34 13 fveq1i ⊢ ( 𝐻 ‘ 𝑘 ) = ( ( 𝐹 ∪ { ⟨ 𝑁 , 𝐵 ⟩ } ) ‘ 𝑘 )
35 fzonel ⊢ ¬ 𝑁 ∈ ( 0 ..^ 𝑁 )
36 eleq1 ⊢ ( 𝑁 = 𝑘 → ( 𝑁 ∈ ( 0 ..^ 𝑁 ) ↔ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) )
37 35 36 mtbii ⊢ ( 𝑁 = 𝑘 → ¬ 𝑘 ∈ ( 0 ..^ 𝑁 ) )
38 37 a1i ⊢ ( 𝜑 → ( 𝑁 = 𝑘 → ¬ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) )
39 38 con2d ⊢ ( 𝜑 → ( 𝑘 ∈ ( 0 ..^ 𝑁 ) → ¬ 𝑁 = 𝑘 ) )
40 39 imp ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → ¬ 𝑁 = 𝑘 )
41 40 neqned ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → 𝑁 ≠ 𝑘 )
42 fvunsn ⊢ ( 𝑁 ≠ 𝑘 → ( ( 𝐹 ∪ { ⟨ 𝑁 , 𝐵 ⟩ } ) ‘ 𝑘 ) = ( 𝐹 ‘ 𝑘 ) )
43 41 42 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝐹 ∪ { ⟨ 𝑁 , 𝐵 ⟩ } ) ‘ 𝑘 ) = ( 𝐹 ‘ 𝑘 ) )
44 34 43 eqtrid ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐻 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑘 ) )
45 33 44 fveq12d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑘 ) ) = ( ( 𝐼 ∪ { ⟨ 𝐵 , 𝐸 ⟩ } ) ‘ ( 𝐹 ‘ 𝑘 ) ) )
46 9 oveq2i ⊢ ( 0 ..^ 𝑁 ) = ( 0 ..^ ( ♯ ‘ 𝐹 ) )
47 46 eleq2i ⊢ ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↔ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
48 2 wlkf ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → 𝐹 ∈ Word dom 𝐼 )
49 8 48 syl ⊢ ( 𝜑 → 𝐹 ∈ Word dom 𝐼 )
50 wrdsymbcl ⊢ ( ( 𝐹 ∈ Word dom 𝐼 ∧ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( 𝐹 ‘ 𝑘 ) ∈ dom 𝐼 )
51 50 ex ⊢ ( 𝐹 ∈ Word dom 𝐼 → ( 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ dom 𝐼 ) )
52 49 51 syl ⊢ ( 𝜑 → ( 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ dom 𝐼 ) )
53 47 52 biimtrid ⊢ ( 𝜑 → ( 𝑘 ∈ ( 0 ..^ 𝑁 ) → ( 𝐹 ‘ 𝑘 ) ∈ dom 𝐼 ) )
54 53 imp ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ dom 𝐼 )
55 eleq1 ⊢ ( 𝐵 = ( 𝐹 ‘ 𝑘 ) → ( 𝐵 ∈ dom 𝐼 ↔ ( 𝐹 ‘ 𝑘 ) ∈ dom 𝐼 ) )
56 54 55 syl5ibrcom ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐵 = ( 𝐹 ‘ 𝑘 ) → 𝐵 ∈ dom 𝐼 ) )
57 56 con3d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → ( ¬ 𝐵 ∈ dom 𝐼 → ¬ 𝐵 = ( 𝐹 ‘ 𝑘 ) ) )
58 57 ex ⊢ ( 𝜑 → ( 𝑘 ∈ ( 0 ..^ 𝑁 ) → ( ¬ 𝐵 ∈ dom 𝐼 → ¬ 𝐵 = ( 𝐹 ‘ 𝑘 ) ) ) )
59 7 58 mpid ⊢ ( 𝜑 → ( 𝑘 ∈ ( 0 ..^ 𝑁 ) → ¬ 𝐵 = ( 𝐹 ‘ 𝑘 ) ) )
60 59 imp ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → ¬ 𝐵 = ( 𝐹 ‘ 𝑘 ) )
61 60 neqned ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → 𝐵 ≠ ( 𝐹 ‘ 𝑘 ) )
62 fvunsn ⊢ ( 𝐵 ≠ ( 𝐹 ‘ 𝑘 ) → ( ( 𝐼 ∪ { ⟨ 𝐵 , 𝐸 ⟩ } ) ‘ ( 𝐹 ‘ 𝑘 ) ) = ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) )
63 61 62 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝐼 ∪ { ⟨ 𝐵 , 𝐸 ⟩ } ) ‘ ( 𝐹 ‘ 𝑘 ) ) = ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) )
64 45 63 eqtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑘 ) ) = ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) )
65 64 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) ∧ ∀ 𝑥 ∈ ( 0 ... 𝑁 ) ( 𝑄 ‘ 𝑥 ) = ( 𝑃 ‘ 𝑥 ) ) → ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑘 ) ) = ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) )
66 24 32 65 3jca ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) ∧ ∀ 𝑥 ∈ ( 0 ... 𝑁 ) ( 𝑄 ‘ 𝑥 ) = ( 𝑃 ‘ 𝑥 ) ) → ( ( 𝑄 ‘ 𝑘 ) = ( 𝑃 ‘ 𝑘 ) ∧ ( 𝑄 ‘ ( 𝑘 + 1 ) ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∧ ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑘 ) ) = ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) )
67 16 66 mpidan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑄 ‘ 𝑘 ) = ( 𝑃 ‘ 𝑘 ) ∧ ( 𝑄 ‘ ( 𝑘 + 1 ) ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∧ ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑘 ) ) = ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) )
68 67 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 0 ..^ 𝑁 ) ( ( 𝑄 ‘ 𝑘 ) = ( 𝑃 ‘ 𝑘 ) ∧ ( 𝑄 ‘ ( 𝑘 + 1 ) ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∧ ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑘 ) ) = ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) )