upgrimtrls

Description: Graph isomorphisms between simple pseudographs map trails onto trails. (Contributed by AV, 29-Oct-2025)

	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))]))$
	upgrimtrls.t	$⊢ φ \to F Trails (G) P$
Assertion	upgrimtrls	$⊢ φ \to E Trails (H) (N \circ P)$

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		upgrimtrls.t	$⊢ φ \to F Trails (G) P$
8		trliswlk	$⊢ F Trails (G) P \to F Walks (G) P$
9	7 8	syl	$⊢ φ \to F Walks (G) P$
10	1 2 3 4 5 6 9	upgrimwlk	$⊢ φ \to E Walks (H) (N \circ P)$
11	4	adantr	$⊢ (φ \land x \in dom F) \to H \in USHGraph$
12	2	uspgrf1oedg	$⊢ H \in USHGraph \to J : dom J \underset{1-1 onto}{⟶} Edg (H)$
13	11 12	syl	$⊢ (φ \land x \in dom F) \to J : dom J \underset{1-1 onto}{⟶} Edg (H)$
14	1 2 3 4 5 6 7	upgrimtrlslem1	$⊢ (φ \land x \in dom F) \to N [I (F (x))] \in Edg (H)$
15		f1ocnvdm	$⊢ (J : dom J \underset{1-1 onto}{⟶} Edg (H) \land N [I (F (x))] \in Edg (H)) \to J^{-1} (N [I (F (x))]) \in dom J$
16	13 14 15	syl2anc	$⊢ (φ \land x \in dom F) \to J^{-1} (N [I (F (x))]) \in dom J$
17	16	ralrimiva	$⊢ φ \to \forall x \in dom F J^{-1} (N [I (F (x))]) \in dom J$
18	1 2 3 4 5 6 7	upgrimtrlslem2	$⊢ (φ \land (x \in dom F \land y \in dom F)) \to (J^{-1} (N [I (F (x))]) = J^{-1} (N [I (F (y))]) \to x = y)$
19	18	ralrimivva	$⊢ φ \to \forall x \in dom F \forall y \in dom F (J^{-1} (N [I (F (x))]) = J^{-1} (N [I (F (y))]) \to x = y)$
20		2fveq3	$⊢ x = y \to I (F (x)) = I (F (y))$
21	20	imaeq2d	$⊢ x = y \to N [I (F (x))] = N [I (F (y))]$
22	21	fveq2d	$⊢ x = y \to J^{-1} (N [I (F (x))]) = J^{-1} (N [I (F (y))])$
23	6 22	f1mpt	$⊢ E : dom F \underset{1-1}{⟶} dom J \leftrightarrow (\forall x \in dom F J^{-1} (N [I (F (x))]) \in dom J \land \forall x \in dom F \forall y \in dom F (J^{-1} (N [I (F (x))]) = J^{-1} (N [I (F (y))]) \to x = y))$
24	17 19 23	sylanbrc	$⊢ φ \to E : dom F \underset{1-1}{⟶} dom J$
25		eqidd	$⊢ φ \to E = E$
26	1	wlkf	$⊢ F Walks (G) P \to F \in Word dom I$
27	7 8 26	3syl	$⊢ φ \to F \in Word dom I$
28	1 2 3 4 5 6 27	upgrimwlklem1	$⊢ φ \to \|E\| = \|F\|$
29	28	oveq2d	$⊢ φ \to (0 ..^\|E\|) = (0 ..^\|F\|)$
30		wrddm	$⊢ F \in Word dom I \to dom F = (0 ..^\|F\|)$
31	8 26 30	3syl	$⊢ F Trails (G) P \to dom F = (0 ..^\|F\|)$
32	7 31	syl	$⊢ φ \to dom F = (0 ..^\|F\|)$
33	29 32	eqtr4d	$⊢ φ \to (0 ..^\|E\|) = dom F$
34		eqidd	$⊢ φ \to dom J = dom J$
35	25 33 34	f1eq123d	$⊢ φ \to (E : (0 ..^\|E\|) \underset{1-1}{⟶} dom J \leftrightarrow E : dom F \underset{1-1}{⟶} dom J)$
36	24 35	mpbird	$⊢ φ \to E : (0 ..^\|E\|) \underset{1-1}{⟶} dom J$
37		df-f1	$⊢ E : (0 ..^\|E\|) \underset{1-1}{⟶} dom J \leftrightarrow (E : (0 ..^\|E\|) ⟶ dom J \land Fun E^{-1})$
38	37	simprbi	$⊢ E : (0 ..^\|E\|) \underset{1-1}{⟶} dom J \to Fun E^{-1}$
39	36 38	syl	$⊢ φ \to Fun E^{-1}$
40		istrl	$⊢ E Trails (H) (N \circ P) \leftrightarrow (E Walks (H) (N \circ P) \land Fun E^{-1})$
41	10 39 40	sylanbrc	$⊢ φ \to E Trails (H) (N \circ P)$

Metamath Proof Explorer

Theorem upgrimtrls

Proof