upgrimpthslem1

	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	upgrimpthslem1	$⊢ φ \to Fun {({(N \circ P) ↾}_{(1 ..^\|F\|)})}^{-1}$

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		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)$
9	8	simp2bi	$⊢ F Paths (G) P \to Fun {({P ↾}_{(1 ..^\|F\|)})}^{-1}$
10	7 9	syl	$⊢ φ \to Fun {({P ↾}_{(1 ..^\|F\|)})}^{-1}$
11		eqid	$⊢ Vtx (G) = Vtx (G)$
12		eqid	$⊢ Vtx (H) = Vtx (H)$
13	11 12	grimf1o	$⊢ N \in (G GraphIso H) \to N : Vtx (G) \underset{1-1 onto}{⟶} Vtx (H)$
14		dff1o3	$⊢ N : Vtx (G) \underset{1-1 onto}{⟶} Vtx (H) \leftrightarrow (N : Vtx (G) \underset{onto}{⟶} Vtx (H) \land Fun N^{-1})$
15	14	simprbi	$⊢ N : Vtx (G) \underset{1-1 onto}{⟶} Vtx (H) \to Fun N^{-1}$
16	5 13 15	3syl	$⊢ φ \to Fun N^{-1}$
17		funco	$⊢ (Fun {({P ↾}_{(1 ..^\|F\|)})}^{-1} \land Fun N^{-1}) \to Fun ({({P ↾}_{(1 ..^\|F\|)})}^{-1} \circ N^{-1})$
18	10 16 17	syl2anc	$⊢ φ \to Fun ({({P ↾}_{(1 ..^\|F\|)})}^{-1} \circ N^{-1})$
19		resco	$⊢ {(N \circ P) ↾}_{(1 ..^\|F\|)} = N \circ ({P ↾}_{(1 ..^\|F\|)})$
20	19	cnveqi	$⊢ {({(N \circ P) ↾}_{(1 ..^\|F\|)})}^{-1} = {(N \circ ({P ↾}_{(1 ..^\|F\|)}))}^{-1}$
21		cnvco	$⊢ {(N \circ ({P ↾}_{(1 ..^\|F\|)}))}^{-1} = {({P ↾}_{(1 ..^\|F\|)})}^{-1} \circ N^{-1}$
22	20 21	eqtri	$⊢ {({(N \circ P) ↾}_{(1 ..^\|F\|)})}^{-1} = {({P ↾}_{(1 ..^\|F\|)})}^{-1} \circ N^{-1}$
23	22	funeqi	$⊢ Fun {({(N \circ P) ↾}_{(1 ..^\|F\|)})}^{-1} \leftrightarrow Fun ({({P ↾}_{(1 ..^\|F\|)})}^{-1} \circ N^{-1})$
24	18 23	sylibr	$⊢ φ \to Fun {({(N \circ P) ↾}_{(1 ..^\|F\|)})}^{-1}$

Metamath Proof Explorer

Theorem upgrimpthslem1

Proof