spthispth

Description: A simple path is a path (in an undirected graph). (Contributed by Alexander van der Vekens, 21-Oct-2017) (Revised by AV, 9-Jan-2021) (Proof shortened by AV, 30-Oct-2021)

		Ref	Expression
	Assertion	spthispth	$⊢ F SPaths (G) P \to F Paths (G) P$

Proof

Step	Hyp	Ref	Expression
1		simpl	$⊢ (F Trails (G) P \land Fun P^{-1}) \to F Trails (G) P$
2		funres11	$⊢ Fun P^{-1} \to Fun {({P ↾}_{(1 ..^\|F\|)})}^{-1}$
3	2	adantl	$⊢ (F Trails (G) P \land Fun P^{-1}) \to Fun {({P ↾}_{(1 ..^\|F\|)})}^{-1}$
4		1e0p1	$⊢ 1 = 0 + 1$
5	4	oveq1i	$⊢ (1 ..^\|F\|) = (0 + 1 ..^\|F\|)$
6	5	ineq2i	$⊢ \{0, \|F\|\} \cap (1 ..^\|F\|) = \{0, \|F\|\} \cap (0 + 1 ..^\|F\|)$
7		0z	$⊢ 0 \in ℤ$
8		prinfzo0	$⊢ 0 \in ℤ \to \{0, \|F\|\} \cap (0 + 1 ..^\|F\|) = \emptyset$
9	7 8	ax-mp	$⊢ \{0, \|F\|\} \cap (0 + 1 ..^\|F\|) = \emptyset$
10	6 9	eqtri	$⊢ \{0, \|F\|\} \cap (1 ..^\|F\|) = \emptyset$
11	10	imaeq2i	$⊢ P [\{0, \|F\|\} \cap (1 ..^\|F\|)] = P [\emptyset]$
12		ima0	$⊢ P [\emptyset] = \emptyset$
13	11 12	eqtri	$⊢ P [\{0, \|F\|\} \cap (1 ..^\|F\|)] = \emptyset$
14		imain	$⊢ Fun P^{-1} \to P [\{0, \|F\|\} \cap (1 ..^\|F\|)] = P [\{0, \|F\|\}] \cap P [(1 ..^\|F\|)]$
15	13 14	syl5reqr	$⊢ Fun P^{-1} \to P [\{0, \|F\|\}] \cap P [(1 ..^\|F\|)] = \emptyset$
16	15	adantl	$⊢ (F Trails (G) P \land Fun P^{-1}) \to P [\{0, \|F\|\}] \cap P [(1 ..^\|F\|)] = \emptyset$
17	1 3 16	3jca	$⊢ (F Trails (G) P \land Fun P^{-1}) \to (F Trails (G) P \land Fun {({P ↾}_{(1 ..^\|F\|)})}^{-1} \land P [\{0, \|F\|\}] \cap P [(1 ..^\|F\|)] = \emptyset)$
18		isspth	$⊢ F SPaths (G) P \leftrightarrow (F Trails (G) P \land Fun P^{-1})$
19		ispth	$⊢ F Paths (G) P \leftrightarrow (F Trails (G) P \land Fun {({P ↾}_{(1 ..^\|F\|)})}^{-1} \land P [\{0, \|F\|\}] \cap P [(1 ..^\|F\|)] = \emptyset)$
20	17 18 19	3imtr4i	$⊢ F SPaths (G) P \to F Paths (G) P$

Metamath Proof Explorer

Theorem spthispth

Proof