upgrewlkle2

Description: In a pseudograph, there is no s-walk of edges of length greater than 1 with s>2. (Contributed by AV, 4-Jan-2021)

		Ref	Expression
	Assertion	upgrewlkle2	$⊢ (G \in UPGraph \land F \in (G EdgWalks S) \land 1 < \|F\|) \to S \leq 2$

Proof

Step	Hyp	Ref	Expression
1		eqid	$⊢ iEdg (G) = iEdg (G)$
2	1	ewlkprop	$⊢ F \in (G EdgWalks S) \to ((G \in V \land S \in ℕ_{0}^{*}) \land F \in Word dom iEdg (G) \land \forall k \in (1 ..^\|F\|) S \leq \|iEdg (G) (F (k - 1)) \cap iEdg (G) (F (k))\|)$
3		fvex	$⊢ iEdg (G) (F (k - 1)) \in V$
4		hashin	$⊢ iEdg (G) (F (k - 1)) \in V \to \|iEdg (G) (F (k - 1)) \cap iEdg (G) (F (k))\| \leq \|iEdg (G) (F (k - 1))\|$
5	3 4	ax-mp	$⊢ \|iEdg (G) (F (k - 1)) \cap iEdg (G) (F (k))\| \leq \|iEdg (G) (F (k - 1))\|$
6		simpl3	$⊢ (((G \in V \land S \in ℕ_{0}^{*}) \land F \in Word dom iEdg (G) \land G \in UPGraph) \land k \in (1 ..^\|F\|)) \to G \in UPGraph$
7		upgruhgr	$⊢ G \in UPGraph \to G \in UHGraph$
8	1	uhgrfun	$⊢ G \in UHGraph \to Fun iEdg (G)$
9	7 8	syl	$⊢ G \in UPGraph \to Fun iEdg (G)$
10	9	funfnd	$⊢ G \in UPGraph \to iEdg (G) Fn dom iEdg (G)$
11	10	3ad2ant3	$⊢ ((G \in V \land S \in ℕ_{0}^{*}) \land F \in Word dom iEdg (G) \land G \in UPGraph) \to iEdg (G) Fn dom iEdg (G)$
12	11	adantr	$⊢ (((G \in V \land S \in ℕ_{0}^{*}) \land F \in Word dom iEdg (G) \land G \in UPGraph) \land k \in (1 ..^\|F\|)) \to iEdg (G) Fn dom iEdg (G)$
13		elfzofz	$⊢ k \in (1 ..^\|F\|) \to k \in (1 \dots \|F\|)$
14		fz1fzo0m1	$⊢ k \in (1 \dots \|F\|) \to k - 1 \in (0 ..^\|F\|)$
15	13 14	syl	$⊢ k \in (1 ..^\|F\|) \to k - 1 \in (0 ..^\|F\|)$
16		wrdsymbcl	$⊢ (F \in Word dom iEdg (G) \land k - 1 \in (0 ..^\|F\|)) \to F (k - 1) \in dom iEdg (G)$
17	15 16	sylan2	$⊢ (F \in Word dom iEdg (G) \land k \in (1 ..^\|F\|)) \to F (k - 1) \in dom iEdg (G)$
18	17	3ad2antl2	$⊢ (((G \in V \land S \in ℕ_{0}^{*}) \land F \in Word dom iEdg (G) \land G \in UPGraph) \land k \in (1 ..^\|F\|)) \to F (k - 1) \in dom iEdg (G)$
19		eqid	$⊢ Vtx (G) = Vtx (G)$
20	19 1	upgrle	$⊢ (G \in UPGraph \land iEdg (G) Fn dom iEdg (G) \land F (k - 1) \in dom iEdg (G)) \to \|iEdg (G) (F (k - 1))\| \leq 2$
21	6 12 18 20	syl3anc	$⊢ (((G \in V \land S \in ℕ_{0}^{*}) \land F \in Word dom iEdg (G) \land G \in UPGraph) \land k \in (1 ..^\|F\|)) \to \|iEdg (G) (F (k - 1))\| \leq 2$
22	3	inex1	$⊢ iEdg (G) (F (k - 1)) \cap iEdg (G) (F (k)) \in V$
23		hashxrcl	$⊢ iEdg (G) (F (k - 1)) \cap iEdg (G) (F (k)) \in V \to \|iEdg (G) (F (k - 1)) \cap iEdg (G) (F (k))\| \in ℝ^{*}$
24	22 23	ax-mp	$⊢ \|iEdg (G) (F (k - 1)) \cap iEdg (G) (F (k))\| \in ℝ^{*}$
25		hashxrcl	$⊢ iEdg (G) (F (k - 1)) \in V \to \|iEdg (G) (F (k - 1))\| \in ℝ^{*}$
26	3 25	ax-mp	$⊢ \|iEdg (G) (F (k - 1))\| \in ℝ^{*}$
27		2re	$⊢ 2 \in ℝ$
28	27	rexri	$⊢ 2 \in ℝ^{*}$
29	24 26 28	3pm3.2i	$⊢ (\|iEdg (G) (F (k - 1)) \cap iEdg (G) (F (k))\| \in ℝ^{} \land \|iEdg (G) (F (k - 1))\| \in ℝ^{} \land 2 \in ℝ^{*})$
30	29	a1i	$⊢ (((G \in V \land S \in ℕ_{0}^{}) \land F \in Word dom iEdg (G) \land G \in UPGraph) \land k \in (1 ..^\|F\|)) \to (\|iEdg (G) (F (k - 1)) \cap iEdg (G) (F (k))\| \in ℝ^{} \land \|iEdg (G) (F (k - 1))\| \in ℝ^{} \land 2 \in ℝ^{})$
31		xrletr	$⊢ (\|iEdg (G) (F (k - 1)) \cap iEdg (G) (F (k))\| \in ℝ^{} \land \|iEdg (G) (F (k - 1))\| \in ℝ^{} \land 2 \in ℝ^{*}) \to ((\|iEdg (G) (F (k - 1)) \cap iEdg (G) (F (k))\| \leq \|iEdg (G) (F (k - 1))\| \land \|iEdg (G) (F (k - 1))\| \leq 2) \to \|iEdg (G) (F (k - 1)) \cap iEdg (G) (F (k))\| \leq 2)$
32	30 31	syl	$⊢ (((G \in V \land S \in ℕ_{0}^{*}) \land F \in Word dom iEdg (G) \land G \in UPGraph) \land k \in (1 ..^\|F\|)) \to ((\|iEdg (G) (F (k - 1)) \cap iEdg (G) (F (k))\| \leq \|iEdg (G) (F (k - 1))\| \land \|iEdg (G) (F (k - 1))\| \leq 2) \to \|iEdg (G) (F (k - 1)) \cap iEdg (G) (F (k))\| \leq 2)$
33	21 32	mpan2d	$⊢ (((G \in V \land S \in ℕ_{0}^{*}) \land F \in Word dom iEdg (G) \land G \in UPGraph) \land k \in (1 ..^\|F\|)) \to (\|iEdg (G) (F (k - 1)) \cap iEdg (G) (F (k))\| \leq \|iEdg (G) (F (k - 1))\| \to \|iEdg (G) (F (k - 1)) \cap iEdg (G) (F (k))\| \leq 2)$
34	5 33	mpi	$⊢ (((G \in V \land S \in ℕ_{0}^{*}) \land F \in Word dom iEdg (G) \land G \in UPGraph) \land k \in (1 ..^\|F\|)) \to \|iEdg (G) (F (k - 1)) \cap iEdg (G) (F (k))\| \leq 2$
35		xnn0xr	$⊢ S \in ℕ_{0}^{} \to S \in ℝ^{}$
36	24	a1i	$⊢ S \in ℕ_{0}^{} \to \|iEdg (G) (F (k - 1)) \cap iEdg (G) (F (k))\| \in ℝ^{}$
37	28	a1i	$⊢ S \in ℕ_{0}^{} \to 2 \in ℝ^{}$
38		xrletr	$⊢ (S \in ℝ^{} \land \|iEdg (G) (F (k - 1)) \cap iEdg (G) (F (k))\| \in ℝ^{} \land 2 \in ℝ^{*}) \to ((S \leq \|iEdg (G) (F (k - 1)) \cap iEdg (G) (F (k))\| \land \|iEdg (G) (F (k - 1)) \cap iEdg (G) (F (k))\| \leq 2) \to S \leq 2)$
39	35 36 37 38	syl3anc	$⊢ S \in ℕ_{0}^{*} \to ((S \leq \|iEdg (G) (F (k - 1)) \cap iEdg (G) (F (k))\| \land \|iEdg (G) (F (k - 1)) \cap iEdg (G) (F (k))\| \leq 2) \to S \leq 2)$
40	39	expcomd	$⊢ S \in ℕ_{0}^{*} \to (\|iEdg (G) (F (k - 1)) \cap iEdg (G) (F (k))\| \leq 2 \to (S \leq \|iEdg (G) (F (k - 1)) \cap iEdg (G) (F (k))\| \to S \leq 2))$
41	40	adantl	$⊢ (G \in V \land S \in ℕ_{0}^{*}) \to (\|iEdg (G) (F (k - 1)) \cap iEdg (G) (F (k))\| \leq 2 \to (S \leq \|iEdg (G) (F (k - 1)) \cap iEdg (G) (F (k))\| \to S \leq 2))$
42	41	3ad2ant1	$⊢ ((G \in V \land S \in ℕ_{0}^{*}) \land F \in Word dom iEdg (G) \land G \in UPGraph) \to (\|iEdg (G) (F (k - 1)) \cap iEdg (G) (F (k))\| \leq 2 \to (S \leq \|iEdg (G) (F (k - 1)) \cap iEdg (G) (F (k))\| \to S \leq 2))$
43	42	adantr	$⊢ (((G \in V \land S \in ℕ_{0}^{*}) \land F \in Word dom iEdg (G) \land G \in UPGraph) \land k \in (1 ..^\|F\|)) \to (\|iEdg (G) (F (k - 1)) \cap iEdg (G) (F (k))\| \leq 2 \to (S \leq \|iEdg (G) (F (k - 1)) \cap iEdg (G) (F (k))\| \to S \leq 2))$
44	34 43	mpd	$⊢ (((G \in V \land S \in ℕ_{0}^{*}) \land F \in Word dom iEdg (G) \land G \in UPGraph) \land k \in (1 ..^\|F\|)) \to (S \leq \|iEdg (G) (F (k - 1)) \cap iEdg (G) (F (k))\| \to S \leq 2)$
45	44	ralimdva	$⊢ ((G \in V \land S \in ℕ_{0}^{*}) \land F \in Word dom iEdg (G) \land G \in UPGraph) \to (\forall k \in (1 ..^\|F\|) S \leq \|iEdg (G) (F (k - 1)) \cap iEdg (G) (F (k))\| \to \forall k \in (1 ..^\|F\|) S \leq 2)$
46	45	3exp	$⊢ (G \in V \land S \in ℕ_{0}^{*}) \to (F \in Word dom iEdg (G) \to (G \in UPGraph \to (\forall k \in (1 ..^\|F\|) S \leq \|iEdg (G) (F (k - 1)) \cap iEdg (G) (F (k))\| \to \forall k \in (1 ..^\|F\|) S \leq 2)))$
47	46	com34	$⊢ (G \in V \land S \in ℕ_{0}^{*}) \to (F \in Word dom iEdg (G) \to (\forall k \in (1 ..^\|F\|) S \leq \|iEdg (G) (F (k - 1)) \cap iEdg (G) (F (k))\| \to (G \in UPGraph \to \forall k \in (1 ..^\|F\|) S \leq 2)))$
48	47	3imp	$⊢ ((G \in V \land S \in ℕ_{0}^{*}) \land F \in Word dom iEdg (G) \land \forall k \in (1 ..^\|F\|) S \leq \|iEdg (G) (F (k - 1)) \cap iEdg (G) (F (k))\|) \to (G \in UPGraph \to \forall k \in (1 ..^\|F\|) S \leq 2)$
49		lencl	$⊢ F \in Word dom iEdg (G) \to \|F\| \in ℕ_{0}$
50		1zzd	$⊢ \|F\| \in ℕ_{0} \to 1 \in ℤ$
51		nn0z	$⊢ \|F\| \in ℕ_{0} \to \|F\| \in ℤ$
52		fzon	$⊢ (1 \in ℤ \land \|F\| \in ℤ) \to (\|F\| \leq 1 \leftrightarrow (1 ..^\|F\|) = \emptyset)$
53	50 51 52	syl2anc	$⊢ \|F\| \in ℕ_{0} \to (\|F\| \leq 1 \leftrightarrow (1 ..^\|F\|) = \emptyset)$
54		nn0re	$⊢ \|F\| \in ℕ_{0} \to \|F\| \in ℝ$
55		1red	$⊢ \|F\| \in ℕ_{0} \to 1 \in ℝ$
56	54 55	lenltd	$⊢ \|F\| \in ℕ_{0} \to (\|F\| \leq 1 \leftrightarrow \neg 1 < \|F\|)$
57	53 56	bitr3d	$⊢ \|F\| \in ℕ_{0} \to ((1 ..^\|F\|) = \emptyset \leftrightarrow \neg 1 < \|F\|)$
58	57	biimpd	$⊢ \|F\| \in ℕ_{0} \to ((1 ..^\|F\|) = \emptyset \to \neg 1 < \|F\|)$
59	58	necon2ad	$⊢ \|F\| \in ℕ_{0} \to (1 < \|F\| \to (1 ..^\|F\|) \neq \emptyset)$
60		rspn0	$⊢ (1 ..^\|F\|) \neq \emptyset \to (\forall k \in (1 ..^\|F\|) S \leq 2 \to S \leq 2)$
61	59 60	syl6com	$⊢ 1 < \|F\| \to (\|F\| \in ℕ_{0} \to (\forall k \in (1 ..^\|F\|) S \leq 2 \to S \leq 2))$
62	61	com3l	$⊢ \|F\| \in ℕ_{0} \to (\forall k \in (1 ..^\|F\|) S \leq 2 \to (1 < \|F\| \to S \leq 2))$
63	49 62	syl	$⊢ F \in Word dom iEdg (G) \to (\forall k \in (1 ..^\|F\|) S \leq 2 \to (1 < \|F\| \to S \leq 2))$
64	63	3ad2ant2	$⊢ ((G \in V \land S \in ℕ_{0}^{*}) \land F \in Word dom iEdg (G) \land \forall k \in (1 ..^\|F\|) S \leq \|iEdg (G) (F (k - 1)) \cap iEdg (G) (F (k))\|) \to (\forall k \in (1 ..^\|F\|) S \leq 2 \to (1 < \|F\| \to S \leq 2))$
65	48 64	syld	$⊢ ((G \in V \land S \in ℕ_{0}^{*}) \land F \in Word dom iEdg (G) \land \forall k \in (1 ..^\|F\|) S \leq \|iEdg (G) (F (k - 1)) \cap iEdg (G) (F (k))\|) \to (G \in UPGraph \to (1 < \|F\| \to S \leq 2))$
66	2 65	syl	$⊢ F \in (G EdgWalks S) \to (G \in UPGraph \to (1 < \|F\| \to S \leq 2))$
67	66	3imp21	$⊢ (G \in UPGraph \land F \in (G EdgWalks S) \land 1 < \|F\|) \to S \leq 2$

Metamath Proof Explorer

Theorem upgrewlkle2

Proof