wlkp1lem6

	Ref	Expression
Hypotheses	wlkp1.v	$⊢ V = Vtx (G)$
	wlkp1.i	$⊢ I = iEdg (G)$
	wlkp1.f	$⊢ φ \to Fun I$
	wlkp1.a	$⊢ φ \to I \in Fin$
	wlkp1.b	$⊢ φ \to B \in W$
	wlkp1.c	$⊢ φ \to C \in V$
	wlkp1.d	$⊢ φ \to \neg B \in dom I$
	wlkp1.w	$⊢ φ \to F Walks (G) P$
	wlkp1.n	$⊢ N = \|F\|$
	wlkp1.e	$⊢ φ \to E \in Edg (G)$
	wlkp1.x	$⊢ φ \to \{P (N), C\} \subseteq E$
	wlkp1.u	$⊢ φ \to iEdg (S) = I \cup \{⟨B, E⟩\}$
	wlkp1.h	$⊢ H = F \cup \{⟨N, B⟩\}$
	wlkp1.q	$⊢ Q = P \cup \{⟨N + 1, C⟩\}$
	wlkp1.s	$⊢ φ \to Vtx (S) = V$
Assertion	wlkp1lem6	$⊢ φ \to \forall k \in (0 ..^N) (Q (k) = P (k) \land Q (k + 1) = P (k + 1) \land 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	$⊢ φ \to Fun I$
4		wlkp1.a	$⊢ φ \to I \in Fin$
5		wlkp1.b	$⊢ φ \to B \in W$
6		wlkp1.c	$⊢ φ \to C \in V$
7		wlkp1.d	$⊢ φ \to \neg B \in dom I$
8		wlkp1.w	$⊢ φ \to F Walks (G) P$
9		wlkp1.n	$⊢ N = \|F\|$
10		wlkp1.e	$⊢ φ \to E \in Edg (G)$
11		wlkp1.x	$⊢ φ \to \{P (N), C\} \subseteq E$
12		wlkp1.u	$⊢ φ \to iEdg (S) = I \cup \{⟨B, E⟩\}$
13		wlkp1.h	$⊢ H = F \cup \{⟨N, B⟩\}$
14		wlkp1.q	$⊢ Q = P \cup \{⟨N + 1, C⟩\}$
15		wlkp1.s	$⊢ φ \to Vtx (S) = V$
16	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15	wlkp1lem5	$⊢ φ \to \forall x \in (0 \dots N) Q (x) = P (x)$
17		elfzofz	$⊢ k \in (0 ..^N) \to k \in (0 \dots N)$
18	17	adantl	$⊢ (φ \land k \in (0 ..^N)) \to k \in (0 \dots N)$
19		fveq2	$⊢ x = k \to Q (x) = Q (k)$
20		fveq2	$⊢ x = k \to P (x) = P (k)$
21	19 20	eqeq12d	$⊢ x = k \to (Q (x) = P (x) \leftrightarrow Q (k) = P (k))$
22	21	rspcv	$⊢ k \in (0 \dots N) \to (\forall x \in (0 \dots N) Q (x) = P (x) \to Q (k) = P (k))$
23	18 22	syl	$⊢ (φ \land k \in (0 ..^N)) \to (\forall x \in (0 \dots N) Q (x) = P (x) \to Q (k) = P (k))$
24	23	imp	$⊢ ((φ \land k \in (0 ..^N)) \land \forall x \in (0 \dots N) Q (x) = P (x)) \to Q (k) = P (k)$
25		fzofzp1	$⊢ k \in (0 ..^N) \to k + 1 \in (0 \dots N)$
26	25	adantl	$⊢ (φ \land k \in (0 ..^N)) \to k + 1 \in (0 \dots N)$
27		fveq2	$⊢ x = k + 1 \to Q (x) = Q (k + 1)$
28		fveq2	$⊢ x = k + 1 \to P (x) = P (k + 1)$
29	27 28	eqeq12d	$⊢ x = k + 1 \to (Q (x) = P (x) \leftrightarrow Q (k + 1) = P (k + 1))$
30	29	rspcv	$⊢ k + 1 \in (0 \dots N) \to (\forall x \in (0 \dots N) Q (x) = P (x) \to Q (k + 1) = P (k + 1))$
31	26 30	syl	$⊢ (φ \land k \in (0 ..^N)) \to (\forall x \in (0 \dots N) Q (x) = P (x) \to Q (k + 1) = P (k + 1))$
32	31	imp	$⊢ ((φ \land k \in (0 ..^N)) \land \forall x \in (0 \dots N) Q (x) = P (x)) \to Q (k + 1) = P (k + 1)$
33	12	adantr	$⊢ (φ \land k \in (0 ..^N)) \to iEdg (S) = I \cup \{⟨B, E⟩\}$
34	13	fveq1i	$⊢ H (k) = (F \cup \{⟨N, B⟩\}) (k)$
35		fzonel	$⊢ \neg N \in (0 ..^N)$
36		eleq1	$⊢ N = k \to (N \in (0 ..^N) \leftrightarrow k \in (0 ..^N))$
37	35 36	mtbii	$⊢ N = k \to \neg k \in (0 ..^N)$
38	37	a1i	$⊢ φ \to (N = k \to \neg k \in (0 ..^N))$
39	38	con2d	$⊢ φ \to (k \in (0 ..^N) \to \neg N = k)$
40	39	imp	$⊢ (φ \land k \in (0 ..^N)) \to \neg N = k$
41	40	neqned	$⊢ (φ \land k \in (0 ..^N)) \to N \neq k$
42		fvunsn	$⊢ N \neq k \to (F \cup \{⟨N, B⟩\}) (k) = F (k)$
43	41 42	syl	$⊢ (φ \land k \in (0 ..^N)) \to (F \cup \{⟨N, B⟩\}) (k) = F (k)$
44	34 43	eqtrid	$⊢ (φ \land k \in (0 ..^N)) \to H (k) = F (k)$
45	33 44	fveq12d	$⊢ (φ \land k \in (0 ..^N)) \to iEdg (S) (H (k)) = (I \cup \{⟨B, E⟩\}) (F (k))$
46	9	oveq2i	$⊢ (0 ..^N) = (0 ..^\|F\|)$
47	46	eleq2i	$⊢ k \in (0 ..^N) \leftrightarrow k \in (0 ..^\|F\|)$
48	2	wlkf	$⊢ F Walks (G) P \to F \in Word dom I$
49	8 48	syl	$⊢ φ \to F \in Word dom I$
50		wrdsymbcl	$⊢ (F \in Word dom I \land k \in (0 ..^\|F\|)) \to F (k) \in dom I$
51	50	ex	$⊢ F \in Word dom I \to (k \in (0 ..^\|F\|) \to F (k) \in dom I)$
52	49 51	syl	$⊢ φ \to (k \in (0 ..^\|F\|) \to F (k) \in dom I)$
53	47 52	biimtrid	$⊢ φ \to (k \in (0 ..^N) \to F (k) \in dom I)$
54	53	imp	$⊢ (φ \land k \in (0 ..^N)) \to F (k) \in dom I$
55		eleq1	$⊢ B = F (k) \to (B \in dom I \leftrightarrow F (k) \in dom I)$
56	54 55	syl5ibrcom	$⊢ (φ \land k \in (0 ..^N)) \to (B = F (k) \to B \in dom I)$
57	56	con3d	$⊢ (φ \land k \in (0 ..^N)) \to (\neg B \in dom I \to \neg B = F (k))$
58	57	ex	$⊢ φ \to (k \in (0 ..^N) \to (\neg B \in dom I \to \neg B = F (k)))$
59	7 58	mpid	$⊢ φ \to (k \in (0 ..^N) \to \neg B = F (k))$
60	59	imp	$⊢ (φ \land k \in (0 ..^N)) \to \neg B = F (k)$
61	60	neqned	$⊢ (φ \land k \in (0 ..^N)) \to B \neq F (k)$
62		fvunsn	$⊢ B \neq F (k) \to (I \cup \{⟨B, E⟩\}) (F (k)) = I (F (k))$
63	61 62	syl	$⊢ (φ \land k \in (0 ..^N)) \to (I \cup \{⟨B, E⟩\}) (F (k)) = I (F (k))$
64	45 63	eqtrd	$⊢ (φ \land k \in (0 ..^N)) \to iEdg (S) (H (k)) = I (F (k))$
65	64	adantr	$⊢ ((φ \land k \in (0 ..^N)) \land \forall x \in (0 \dots N) Q (x) = P (x)) \to iEdg (S) (H (k)) = I (F (k))$
66	24 32 65	3jca	$⊢ ((φ \land k \in (0 ..^N)) \land \forall x \in (0 \dots N) Q (x) = P (x)) \to (Q (k) = P (k) \land Q (k + 1) = P (k + 1) \land iEdg (S) (H (k)) = I (F (k)))$
67	16 66	mpidan	$⊢ (φ \land k \in (0 ..^N)) \to (Q (k) = P (k) \land Q (k + 1) = P (k + 1) \land iEdg (S) (H (k)) = I (F (k)))$
68	67	ralrimiva	$⊢ φ \to \forall k \in (0 ..^N) (Q (k) = P (k) \land Q (k + 1) = P (k + 1) \land iEdg (S) (H (k)) = I (F (k)))$

Metamath Proof Explorer

Theorem wlkp1lem6

Proof