upgrimpthslem2

	Ref	Expression
Hypotheses	upgrimwlk.i	$⊢ I = iEdg (G)$
	upgrimwlk.j	$⊢ J = iEdg (H)$
	upgrimwlk.g	$⊢ φ \to G \in USHGraph$
	upgrimwlk.h	$⊢ φ \to H \in USHGraph$
	upgrimwlk.n	$⊢ φ \to N \in (G GraphIso H)$
	upgrimwlk.e	$⊢ E = (x \in dom F ⟼ J^{-1} (N [I (F (x))]))$
	upgrimpths.p	$⊢ φ \to F Paths (G) P$
Assertion	upgrimpthslem2	$⊢ (φ \land X \in (1 ..^\|F\|)) \to (\neg (N \circ P) (X) = (N \circ P) (0) \land \neg (N \circ P) (X) = (N \circ P) (\|F\|))$

Proof

Step	Hyp	Ref	Expression
1		upgrimwlk.i	$⊢ I = iEdg (G)$
2		upgrimwlk.j	$⊢ J = iEdg (H)$
3		upgrimwlk.g	$⊢ φ \to G \in USHGraph$
4		upgrimwlk.h	$⊢ φ \to H \in USHGraph$
5		upgrimwlk.n	$⊢ φ \to N \in (G GraphIso H)$
6		upgrimwlk.e	$⊢ E = (x \in dom F ⟼ J^{-1} (N [I (F (x))]))$
7		upgrimpths.p	$⊢ φ \to F Paths (G) P$
8		eqid	$⊢ Vtx (G) = Vtx (G)$
9		eqid	$⊢ Vtx (H) = Vtx (H)$
10	8 9	grimf1o	$⊢ N \in (G GraphIso H) \to N : Vtx (G) \underset{1-1 onto}{⟶} Vtx (H)$
11		f1of1	$⊢ N : Vtx (G) \underset{1-1 onto}{⟶} Vtx (H) \to N : Vtx (G) \underset{1-1}{⟶} Vtx (H)$
12	5 10 11	3syl	$⊢ φ \to N : Vtx (G) \underset{1-1}{⟶} Vtx (H)$
13	12	adantr	$⊢ (φ \land X \in (1 ..^\|F\|)) \to N : Vtx (G) \underset{1-1}{⟶} Vtx (H)$
14		pthiswlk	$⊢ F Paths (G) P \to F Walks (G) P$
15	8	wlkp	$⊢ F Walks (G) P \to P : (0 \dots \|F\|) ⟶ Vtx (G)$
16	15	adantr	$⊢ (F Walks (G) P \land X \in (1 ..^\|F\|)) \to P : (0 \dots \|F\|) ⟶ Vtx (G)$
17		fzo0ss1	$⊢ (1 ..^\|F\|) \subseteq (0 ..^\|F\|)$
18		fzossfz	$⊢ (0 ..^\|F\|) \subseteq (0 \dots \|F\|)$
19	17 18	sstri	$⊢ (1 ..^\|F\|) \subseteq (0 \dots \|F\|)$
20	19	sseli	$⊢ X \in (1 ..^\|F\|) \to X \in (0 \dots \|F\|)$
21	20	adantl	$⊢ (F Walks (G) P \land X \in (1 ..^\|F\|)) \to X \in (0 \dots \|F\|)$
22	16 21	ffvelcdmd	$⊢ (F Walks (G) P \land X \in (1 ..^\|F\|)) \to P (X) \in Vtx (G)$
23	22	ex	$⊢ F Walks (G) P \to (X \in (1 ..^\|F\|) \to P (X) \in Vtx (G))$
24	7 14 23	3syl	$⊢ φ \to (X \in (1 ..^\|F\|) \to P (X) \in Vtx (G))$
25	24	imp	$⊢ (φ \land X \in (1 ..^\|F\|)) \to P (X) \in Vtx (G)$
26		wlkcl	$⊢ F Walks (G) P \to \|F\| \in ℕ_{0}$
27		0elfz	$⊢ \|F\| \in ℕ_{0} \to 0 \in (0 \dots \|F\|)$
28	26 27	syl	$⊢ F Walks (G) P \to 0 \in (0 \dots \|F\|)$
29	15 28	ffvelcdmd	$⊢ F Walks (G) P \to P (0) \in Vtx (G)$
30	7 14 29	3syl	$⊢ φ \to P (0) \in Vtx (G)$
31	30	adantr	$⊢ (φ \land X \in (1 ..^\|F\|)) \to P (0) \in Vtx (G)$
32	7	adantr	$⊢ (φ \land X \in (1 ..^\|F\|)) \to F Paths (G) P$
33		simpr	$⊢ (φ \land X \in (1 ..^\|F\|)) \to X \in (1 ..^\|F\|)$
34	7 14 26	3syl	$⊢ φ \to \|F\| \in ℕ_{0}$
35	34 27	syl	$⊢ φ \to 0 \in (0 \dots \|F\|)$
36	35	adantr	$⊢ (φ \land X \in (1 ..^\|F\|)) \to 0 \in (0 \dots \|F\|)$
37		elfzole1	$⊢ X \in (1 ..^\|F\|) \to 1 \leq X$
38		elfzoelz	$⊢ X \in (1 ..^\|F\|) \to X \in ℤ$
39		zgt0ge1	$⊢ X \in ℤ \to (0 < X \leftrightarrow 1 \leq X)$
40	38 39	syl	$⊢ X \in (1 ..^\|F\|) \to (0 < X \leftrightarrow 1 \leq X)$
41		simpr	$⊢ (X \in (1 ..^\|F\|) \land 0 < X) \to 0 < X$
42	41	gt0ne0d	$⊢ (X \in (1 ..^\|F\|) \land 0 < X) \to X \neq 0$
43	42	ex	$⊢ X \in (1 ..^\|F\|) \to (0 < X \to X \neq 0)$
44	40 43	sylbird	$⊢ X \in (1 ..^\|F\|) \to (1 \leq X \to X \neq 0)$
45	37 44	mpd	$⊢ X \in (1 ..^\|F\|) \to X \neq 0$
46	45	adantl	$⊢ (φ \land X \in (1 ..^\|F\|)) \to X \neq 0$
47		pthdivtx	$⊢ (F Paths (G) P \land (X \in (1 ..^\|F\|) \land 0 \in (0 \dots \|F\|) \land X \neq 0)) \to P (X) \neq P (0)$
48	32 33 36 46 47	syl13anc	$⊢ (φ \land X \in (1 ..^\|F\|)) \to P (X) \neq P (0)$
49		dff14i	$⊢ (N : Vtx (G) \underset{1-1}{⟶} Vtx (H) \land (P (X) \in Vtx (G) \land P (0) \in Vtx (G) \land P (X) \neq P (0))) \to N (P (X)) \neq N (P (0))$
50	13 25 31 48 49	syl13anc	$⊢ (φ \land X \in (1 ..^\|F\|)) \to N (P (X)) \neq N (P (0))$
51		nn0fz0	$⊢ \|F\| \in ℕ_{0} \leftrightarrow \|F\| \in (0 \dots \|F\|)$
52	26 51	sylib	$⊢ F Walks (G) P \to \|F\| \in (0 \dots \|F\|)$
53	15 52	ffvelcdmd	$⊢ F Walks (G) P \to P (\|F\|) \in Vtx (G)$
54	7 14 53	3syl	$⊢ φ \to P (\|F\|) \in Vtx (G)$
55	54	adantr	$⊢ (φ \land X \in (1 ..^\|F\|)) \to P (\|F\|) \in Vtx (G)$
56	34 51	sylib	$⊢ φ \to \|F\| \in (0 \dots \|F\|)$
57	56	adantr	$⊢ (φ \land X \in (1 ..^\|F\|)) \to \|F\| \in (0 \dots \|F\|)$
58	38	zred	$⊢ X \in (1 ..^\|F\|) \to X \in ℝ$
59		elfzolt2	$⊢ X \in (1 ..^\|F\|) \to X < \|F\|$
60	58 59	ltned	$⊢ X \in (1 ..^\|F\|) \to X \neq \|F\|$
61	60	adantl	$⊢ (φ \land X \in (1 ..^\|F\|)) \to X \neq \|F\|$
62		pthdivtx	$⊢ (F Paths (G) P \land (X \in (1 ..^\|F\|) \land \|F\| \in (0 \dots \|F\|) \land X \neq \|F\|)) \to P (X) \neq P (\|F\|)$
63	32 33 57 61 62	syl13anc	$⊢ (φ \land X \in (1 ..^\|F\|)) \to P (X) \neq P (\|F\|)$
64		dff14i	$⊢ (N : Vtx (G) \underset{1-1}{⟶} Vtx (H) \land (P (X) \in Vtx (G) \land P (\|F\|) \in Vtx (G) \land P (X) \neq P (\|F\|))) \to N (P (X)) \neq N (P (\|F\|))$
65	13 25 55 63 64	syl13anc	$⊢ (φ \land X \in (1 ..^\|F\|)) \to N (P (X)) \neq N (P (\|F\|))$
66	7 14 15	3syl	$⊢ φ \to P : (0 \dots \|F\|) ⟶ Vtx (G)$
67	66	adantr	$⊢ (φ \land X \in (1 ..^\|F\|)) \to P : (0 \dots \|F\|) ⟶ Vtx (G)$
68	20	adantl	$⊢ (φ \land X \in (1 ..^\|F\|)) \to X \in (0 \dots \|F\|)$
69	67 68	fvco3d	$⊢ (φ \land X \in (1 ..^\|F\|)) \to (N \circ P) (X) = N (P (X))$
70	67 36	fvco3d	$⊢ (φ \land X \in (1 ..^\|F\|)) \to (N \circ P) (0) = N (P (0))$
71	69 70	neeq12d	$⊢ (φ \land X \in (1 ..^\|F\|)) \to ((N \circ P) (X) \neq (N \circ P) (0) \leftrightarrow N (P (X)) \neq N (P (0)))$
72	67 57	fvco3d	$⊢ (φ \land X \in (1 ..^\|F\|)) \to (N \circ P) (\|F\|) = N (P (\|F\|))$
73	69 72	neeq12d	$⊢ (φ \land X \in (1 ..^\|F\|)) \to ((N \circ P) (X) \neq (N \circ P) (\|F\|) \leftrightarrow N (P (X)) \neq N (P (\|F\|)))$
74	71 73	anbi12d	$⊢ (φ \land X \in (1 ..^\|F\|)) \to (((N \circ P) (X) \neq (N \circ P) (0) \land (N \circ P) (X) \neq (N \circ P) (\|F\|)) \leftrightarrow (N (P (X)) \neq N (P (0)) \land N (P (X)) \neq N (P (\|F\|))))$
75	50 65 74	mpbir2and	$⊢ (φ \land X \in (1 ..^\|F\|)) \to ((N \circ P) (X) \neq (N \circ P) (0) \land (N \circ P) (X) \neq (N \circ P) (\|F\|))$
76		df-ne	$⊢ (N \circ P) (X) \neq (N \circ P) (0) \leftrightarrow \neg (N \circ P) (X) = (N \circ P) (0)$
77		df-ne	$⊢ (N \circ P) (X) \neq (N \circ P) (\|F\|) \leftrightarrow \neg (N \circ P) (X) = (N \circ P) (\|F\|)$
78	76 77	anbi12i	$⊢ ((N \circ P) (X) \neq (N \circ P) (0) \land (N \circ P) (X) \neq (N \circ P) (\|F\|)) \leftrightarrow (\neg (N \circ P) (X) = (N \circ P) (0) \land \neg (N \circ P) (X) = (N \circ P) (\|F\|))$
79	75 78	sylib	$⊢ (φ \land X \in (1 ..^\|F\|)) \to (\neg (N \circ P) (X) = (N \circ P) (0) \land \neg (N \circ P) (X) = (N \circ P) (\|F\|))$

Metamath Proof Explorer

Theorem upgrimpthslem2

Proof