Metamath Proof Explorer

Theorem wlkp1lem6

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

Ref Expression
Hypotheses wlkp1.v ⊢ V = Vtx ⁡ G
wlkp1.i ⊢ I = iEdg ⁡ G
wlkp1.f ⊢ φ → Fun ⁡ I
wlkp1.a ⊢ φ → I ∈ Fin
wlkp1.b ⊢ φ → B ∈ W
wlkp1.c ⊢ φ → C ∈ V
wlkp1.d ⊢ φ → ¬ B ∈ dom ⁡ I
wlkp1.w ⊢ φ → F Walks ⁡ G P
wlkp1.n ⊢ N = F
wlkp1.e ⊢ φ → E ∈ Edg ⁡ G
wlkp1.x ⊢ φ → P ⁡ N C ⊆ E
wlkp1.u ⊢ φ → iEdg ⁡ S = I ∪ B E
wlkp1.h ⊢ H = F ∪ N B
wlkp1.q ⊢ Q = P ∪ N + 1 C
wlkp1.s ⊢ φ → Vtx ⁡ S = V
Assertion wlkp1lem6 ⊢ φ → ∀ k ∈ 0 ..^ N Q ⁡ k = P ⁡ k ∧ Q ⁡ k + 1 = P ⁡ k + 1 ∧ iEdg ⁡ S ⁡ H ⁡ k = I ⁡ F ⁡ k

Proof

Step Hyp Ref Expression
1 wlkp1.v ⊢ V = Vtx ⁡ G
2 wlkp1.i ⊢ I = iEdg ⁡ G
3 wlkp1.f ⊢ φ → Fun ⁡ I
4 wlkp1.a ⊢ φ → I ∈ Fin
5 wlkp1.b ⊢ φ → B ∈ W
6 wlkp1.c ⊢ φ → C ∈ V
7 wlkp1.d ⊢ φ → ¬ B ∈ dom ⁡ I
8 wlkp1.w ⊢ φ → F Walks ⁡ G P
9 wlkp1.n ⊢ N = F
10 wlkp1.e ⊢ φ → E ∈ Edg ⁡ G
11 wlkp1.x ⊢ φ → P ⁡ N C ⊆ E
12 wlkp1.u ⊢ φ → iEdg ⁡ S = I ∪ B E
13 wlkp1.h ⊢ H = F ∪ N B
14 wlkp1.q ⊢ Q = P ∪ N + 1 C
15 wlkp1.s ⊢ φ → Vtx ⁡ S = V
16 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 wlkp1lem5 ⊢ φ → ∀ x ∈ 0 … N Q ⁡ x = P ⁡ x
17 elfzofz ⊢ k ∈ 0 ..^ N → k ∈ 0 … N
18 17 adantl ⊢ φ ∧ k ∈ 0 ..^ N → k ∈ 0 … N
19 fveq2 ⊢ x = k → Q ⁡ x = Q ⁡ k
20 fveq2 ⊢ x = k → P ⁡ x = P ⁡ k
21 19 20 eqeq12d ⊢ x = k → Q ⁡ x = P ⁡ x ↔ Q ⁡ k = P ⁡ k
22 21 rspcv ⊢ k ∈ 0 … N → ∀ x ∈ 0 … N Q ⁡ x = P ⁡ x → Q ⁡ k = P ⁡ k
23 18 22 syl ⊢ φ ∧ k ∈ 0 ..^ N → ∀ x ∈ 0 … N Q ⁡ x = P ⁡ x → Q ⁡ k = P ⁡ k
24 23 imp ⊢ φ ∧ k ∈ 0 ..^ N ∧ ∀ x ∈ 0 … N Q ⁡ x = P ⁡ x → Q ⁡ k = P ⁡ k
25 fzofzp1 ⊢ k ∈ 0 ..^ N → k + 1 ∈ 0 … N
26 25 adantl ⊢ φ ∧ k ∈ 0 ..^ N → k + 1 ∈ 0 … N
27 fveq2 ⊢ x = k + 1 → Q ⁡ x = Q ⁡ k + 1
28 fveq2 ⊢ x = k + 1 → P ⁡ x = P ⁡ k + 1
29 27 28 eqeq12d ⊢ x = k + 1 → Q ⁡ x = P ⁡ x ↔ Q ⁡ k + 1 = P ⁡ k + 1
30 29 rspcv ⊢ k + 1 ∈ 0 … N → ∀ x ∈ 0 … N Q ⁡ x = P ⁡ x → Q ⁡ k + 1 = P ⁡ k + 1
31 26 30 syl ⊢ φ ∧ k ∈ 0 ..^ N → ∀ x ∈ 0 … N Q ⁡ x = P ⁡ x → Q ⁡ k + 1 = P ⁡ k + 1
32 31 imp ⊢ φ ∧ k ∈ 0 ..^ N ∧ ∀ x ∈ 0 … N Q ⁡ x = P ⁡ x → Q ⁡ k + 1 = P ⁡ k + 1
33 12 adantr ⊢ φ ∧ k ∈ 0 ..^ N → iEdg ⁡ S = I ∪ B E
34 13 fveq1i ⊢ H ⁡ k = F ∪ N B ⁡ k
35 fzonel ⊢ ¬ N ∈ 0 ..^ N
36 eleq1 ⊢ N = k → N ∈ 0 ..^ N ↔ k ∈ 0 ..^ N
37 35 36 mtbii ⊢ N = k → ¬ k ∈ 0 ..^ N
38 37 a1i ⊢ φ → N = k → ¬ k ∈ 0 ..^ N
39 38 con2d ⊢ φ → k ∈ 0 ..^ N → ¬ N = k
40 39 imp ⊢ φ ∧ k ∈ 0 ..^ N → ¬ N = k
41 40 neqned ⊢ φ ∧ k ∈ 0 ..^ N → N ≠ k
42 fvunsn ⊢ N ≠ k → F ∪ N B ⁡ k = F ⁡ k
43 41 42 syl ⊢ φ ∧ k ∈ 0 ..^ N → F ∪ N B ⁡ k = F ⁡ k
44 34 43 eqtrid ⊢ φ ∧ k ∈ 0 ..^ N → H ⁡ k = F ⁡ k
45 33 44 fveq12d ⊢ φ ∧ k ∈ 0 ..^ N → iEdg ⁡ S ⁡ H ⁡ k = I ∪ B E ⁡ F ⁡ k
46 9 oveq2i ⊢ 0 ..^ N = 0 ..^ F
47 46 eleq2i ⊢ k ∈ 0 ..^ N ↔ k ∈ 0 ..^ F
48 2 wlkf ⊢ F Walks ⁡ G P → F ∈ Word dom ⁡ I
49 8 48 syl ⊢ φ → F ∈ Word dom ⁡ I
50 wrdsymbcl ⊢ F ∈ Word dom ⁡ I ∧ k ∈ 0 ..^ F → F ⁡ k ∈ dom ⁡ I
51 50 ex ⊢ F ∈ Word dom ⁡ I → k ∈ 0 ..^ F → F ⁡ k ∈ dom ⁡ I
52 49 51 syl ⊢ φ → k ∈ 0 ..^ F → F ⁡ k ∈ dom ⁡ I
53 47 52 syl5bi ⊢ φ → k ∈ 0 ..^ N → F ⁡ k ∈ dom ⁡ I
54 53 imp ⊢ φ ∧ k ∈ 0 ..^ N → F ⁡ k ∈ dom ⁡ I
55 eleq1 ⊢ B = F ⁡ k → B ∈ dom ⁡ I ↔ F ⁡ k ∈ dom ⁡ I
56 54 55 syl5ibrcom ⊢ φ ∧ k ∈ 0 ..^ N → B = F ⁡ k → B ∈ dom ⁡ I
57 56 con3d ⊢ φ ∧ k ∈ 0 ..^ N → ¬ B ∈ dom ⁡ I → ¬ B = F ⁡ k
58 57 ex ⊢ φ → k ∈ 0 ..^ N → ¬ B ∈ dom ⁡ I → ¬ B = F ⁡ k
59 7 58 mpid ⊢ φ → k ∈ 0 ..^ N → ¬ B = F ⁡ k
60 59 imp ⊢ φ ∧ k ∈ 0 ..^ N → ¬ B = F ⁡ k
61 60 neqned ⊢ φ ∧ k ∈ 0 ..^ N → B ≠ F ⁡ k
62 fvunsn ⊢ B ≠ F ⁡ k → I ∪ B E ⁡ F ⁡ k = I ⁡ F ⁡ k
63 61 62 syl ⊢ φ ∧ k ∈ 0 ..^ N → I ∪ B E ⁡ F ⁡ k = I ⁡ F ⁡ k
64 45 63 eqtrd ⊢ φ ∧ k ∈ 0 ..^ N → iEdg ⁡ S ⁡ H ⁡ k = I ⁡ F ⁡ k
65 64 adantr ⊢ φ ∧ k ∈ 0 ..^ N ∧ ∀ x ∈ 0 … N Q ⁡ x = P ⁡ x → iEdg ⁡ S ⁡ H ⁡ k = I ⁡ F ⁡ k
66 24 32 65 3jca ⊢ φ ∧ k ∈ 0 ..^ N ∧ ∀ x ∈ 0 … N Q ⁡ x = P ⁡ x → Q ⁡ k = P ⁡ k ∧ Q ⁡ k + 1 = P ⁡ k + 1 ∧ iEdg ⁡ S ⁡ H ⁡ k = I ⁡ F ⁡ k
67 16 66 mpidan ⊢ φ ∧ k ∈ 0 ..^ N → Q ⁡ k = P ⁡ k ∧ Q ⁡ k + 1 = P ⁡ k + 1 ∧ iEdg ⁡ S ⁡ H ⁡ k = I ⁡ F ⁡ k
68 67 ralrimiva ⊢ φ → ∀ k ∈ 0 ..^ N Q ⁡ k = P ⁡ k ∧ Q ⁡ k + 1 = P ⁡ k + 1 ∧ iEdg ⁡ S ⁡ H ⁡ k = I ⁡ F ⁡ k