subgrwlk

Description: If a walk exists in a subgraph of a graph G , then that walk also exists in G . (Contributed by BTernaryTau, 22-Oct-2023)

		Ref	Expression
	Assertion	subgrwlk	$⊢ S SubGraph G \to (F Walks (S) P \to F Walks (G) P)$

Proof

Step	Hyp	Ref	Expression
1		subgrv	$⊢ S SubGraph G \to (S \in V \land G \in V)$
2	1	simpld	$⊢ S SubGraph G \to S \in V$
3		eqid	$⊢ Vtx (S) = Vtx (S)$
4		eqid	$⊢ iEdg (S) = iEdg (S)$
5	3 4	iswlkg	$⊢ S \in V \to (F Walks (S) P \leftrightarrow (F \in Word dom iEdg (S) \land P : (0 \dots \|F\|) ⟶ Vtx (S) \land \forall k \in (0 ..^\|F\|) if- (P (k) = P (k + 1), iEdg (S) (F (k)) = \{P (k)\}, \{P (k), P (k + 1)\} \subseteq iEdg (S) (F (k)))))$
6	2 5	syl	$⊢ S SubGraph G \to (F Walks (S) P \leftrightarrow (F \in Word dom iEdg (S) \land P : (0 \dots \|F\|) ⟶ Vtx (S) \land \forall k \in (0 ..^\|F\|) if- (P (k) = P (k + 1), iEdg (S) (F (k)) = \{P (k)\}, \{P (k), P (k + 1)\} \subseteq iEdg (S) (F (k)))))$
7		3simpa	$⊢ (F \in Word dom iEdg (S) \land P : (0 \dots \|F\|) ⟶ Vtx (S) \land \forall k \in (0 ..^\|F\|) if- (P (k) = P (k + 1), iEdg (S) (F (k)) = \{P (k)\}, \{P (k), P (k + 1)\} \subseteq iEdg (S) (F (k)))) \to (F \in Word dom iEdg (S) \land P : (0 \dots \|F\|) ⟶ Vtx (S))$
8		eqid	$⊢ Vtx (G) = Vtx (G)$
9		eqid	$⊢ iEdg (G) = iEdg (G)$
10		eqid	$⊢ Edg (S) = Edg (S)$
11	3 8 4 9 10	subgrprop2	$⊢ S SubGraph G \to (Vtx (S) \subseteq Vtx (G) \land iEdg (S) \subseteq iEdg (G) \land Edg (S) \subseteq 𝒫 Vtx (S))$
12	11	simp2d	$⊢ S SubGraph G \to iEdg (S) \subseteq iEdg (G)$
13		dmss	$⊢ iEdg (S) \subseteq iEdg (G) \to dom iEdg (S) \subseteq dom iEdg (G)$
14		sswrd	$⊢ dom iEdg (S) \subseteq dom iEdg (G) \to Word dom iEdg (S) \subseteq Word dom iEdg (G)$
15	12 13 14	3syl	$⊢ S SubGraph G \to Word dom iEdg (S) \subseteq Word dom iEdg (G)$
16	15	sseld	$⊢ S SubGraph G \to (F \in Word dom iEdg (S) \to F \in Word dom iEdg (G))$
17	11	simp1d	$⊢ S SubGraph G \to Vtx (S) \subseteq Vtx (G)$
18		fss	$⊢ (P : (0 \dots \|F\|) ⟶ Vtx (S) \land Vtx (S) \subseteq Vtx (G)) \to P : (0 \dots \|F\|) ⟶ Vtx (G)$
19	18	expcom	$⊢ Vtx (S) \subseteq Vtx (G) \to (P : (0 \dots \|F\|) ⟶ Vtx (S) \to P : (0 \dots \|F\|) ⟶ Vtx (G))$
20	17 19	syl	$⊢ S SubGraph G \to (P : (0 \dots \|F\|) ⟶ Vtx (S) \to P : (0 \dots \|F\|) ⟶ Vtx (G))$
21	16 20	anim12d	$⊢ S SubGraph G \to ((F \in Word dom iEdg (S) \land P : (0 \dots \|F\|) ⟶ Vtx (S)) \to (F \in Word dom iEdg (G) \land P : (0 \dots \|F\|) ⟶ Vtx (G)))$
22	7 21	syl5	$⊢ S SubGraph G \to ((F \in Word dom iEdg (S) \land P : (0 \dots \|F\|) ⟶ Vtx (S) \land \forall k \in (0 ..^\|F\|) if- (P (k) = P (k + 1), iEdg (S) (F (k)) = \{P (k)\}, \{P (k), P (k + 1)\} \subseteq iEdg (S) (F (k)))) \to (F \in Word dom iEdg (G) \land P : (0 \dots \|F\|) ⟶ Vtx (G)))$
23		3simpb	$⊢ (F \in Word dom iEdg (S) \land P : (0 \dots \|F\|) ⟶ Vtx (S) \land \forall k \in (0 ..^\|F\|) if- (P (k) = P (k + 1), iEdg (S) (F (k)) = \{P (k)\}, \{P (k), P (k + 1)\} \subseteq iEdg (S) (F (k)))) \to (F \in Word dom iEdg (S) \land \forall k \in (0 ..^\|F\|) if- (P (k) = P (k + 1), iEdg (S) (F (k)) = \{P (k)\}, \{P (k), P (k + 1)\} \subseteq iEdg (S) (F (k))))$
24	3 8 4 9 10	subgrprop	$⊢ S SubGraph G \to (Vtx (S) \subseteq Vtx (G) \land iEdg (S) = {iEdg (G) ↾}_{dom iEdg (S)} \land Edg (S) \subseteq 𝒫 Vtx (S))$
25	24	simp2d	$⊢ S SubGraph G \to iEdg (S) = {iEdg (G) ↾}_{dom iEdg (S)}$
26	25	fveq1d	$⊢ S SubGraph G \to iEdg (S) (F (k)) = ({iEdg (G) ↾}_{dom iEdg (S)}) (F (k))$
27	26	3ad2ant1	$⊢ (S SubGraph G \land F \in Word dom iEdg (S) \land k \in (0 ..^\|F\|)) \to iEdg (S) (F (k)) = ({iEdg (G) ↾}_{dom iEdg (S)}) (F (k))$
28		wrdsymbcl	$⊢ (F \in Word dom iEdg (S) \land k \in (0 ..^\|F\|)) \to F (k) \in dom iEdg (S)$
29	28	fvresd	$⊢ (F \in Word dom iEdg (S) \land k \in (0 ..^\|F\|)) \to ({iEdg (G) ↾}_{dom iEdg (S)}) (F (k)) = iEdg (G) (F (k))$
30	29	3adant1	$⊢ (S SubGraph G \land F \in Word dom iEdg (S) \land k \in (0 ..^\|F\|)) \to ({iEdg (G) ↾}_{dom iEdg (S)}) (F (k)) = iEdg (G) (F (k))$
31	27 30	eqtrd	$⊢ (S SubGraph G \land F \in Word dom iEdg (S) \land k \in (0 ..^\|F\|)) \to iEdg (S) (F (k)) = iEdg (G) (F (k))$
32	31	eqeq1d	$⊢ (S SubGraph G \land F \in Word dom iEdg (S) \land k \in (0 ..^\|F\|)) \to (iEdg (S) (F (k)) = \{P (k)\} \leftrightarrow iEdg (G) (F (k)) = \{P (k)\})$
33	31	sseq2d	$⊢ (S SubGraph G \land F \in Word dom iEdg (S) \land k \in (0 ..^\|F\|)) \to (\{P (k), P (k + 1)\} \subseteq iEdg (S) (F (k)) \leftrightarrow \{P (k), P (k + 1)\} \subseteq iEdg (G) (F (k)))$
34	32 33	ifpbi23d	$⊢ (S SubGraph G \land F \in Word dom iEdg (S) \land k \in (0 ..^\|F\|)) \to (if- (P (k) = P (k + 1), iEdg (S) (F (k)) = \{P (k)\}, \{P (k), P (k + 1)\} \subseteq iEdg (S) (F (k))) \leftrightarrow if- (P (k) = P (k + 1), iEdg (G) (F (k)) = \{P (k)\}, \{P (k), P (k + 1)\} \subseteq iEdg (G) (F (k))))$
35	34	biimpd	$⊢ (S SubGraph G \land F \in Word dom iEdg (S) \land k \in (0 ..^\|F\|)) \to (if- (P (k) = P (k + 1), iEdg (S) (F (k)) = \{P (k)\}, \{P (k), P (k + 1)\} \subseteq iEdg (S) (F (k))) \to if- (P (k) = P (k + 1), iEdg (G) (F (k)) = \{P (k)\}, \{P (k), P (k + 1)\} \subseteq iEdg (G) (F (k))))$
36	35	3expia	$⊢ (S SubGraph G \land F \in Word dom iEdg (S)) \to (k \in (0 ..^\|F\|) \to (if- (P (k) = P (k + 1), iEdg (S) (F (k)) = \{P (k)\}, \{P (k), P (k + 1)\} \subseteq iEdg (S) (F (k))) \to if- (P (k) = P (k + 1), iEdg (G) (F (k)) = \{P (k)\}, \{P (k), P (k + 1)\} \subseteq iEdg (G) (F (k)))))$
37	36	ralrimiv	$⊢ (S SubGraph G \land F \in Word dom iEdg (S)) \to \forall k \in (0 ..^\|F\|) (if- (P (k) = P (k + 1), iEdg (S) (F (k)) = \{P (k)\}, \{P (k), P (k + 1)\} \subseteq iEdg (S) (F (k))) \to if- (P (k) = P (k + 1), iEdg (G) (F (k)) = \{P (k)\}, \{P (k), P (k + 1)\} \subseteq iEdg (G) (F (k))))$
38		ralim	$⊢ \forall k \in (0 ..^\|F\|) (if- (P (k) = P (k + 1), iEdg (S) (F (k)) = \{P (k)\}, \{P (k), P (k + 1)\} \subseteq iEdg (S) (F (k))) \to if- (P (k) = P (k + 1), iEdg (G) (F (k)) = \{P (k)\}, \{P (k), P (k + 1)\} \subseteq iEdg (G) (F (k)))) \to (\forall k \in (0 ..^\|F\|) if- (P (k) = P (k + 1), iEdg (S) (F (k)) = \{P (k)\}, \{P (k), P (k + 1)\} \subseteq iEdg (S) (F (k))) \to \forall k \in (0 ..^\|F\|) if- (P (k) = P (k + 1), iEdg (G) (F (k)) = \{P (k)\}, \{P (k), P (k + 1)\} \subseteq iEdg (G) (F (k))))$
39	37 38	syl	$⊢ (S SubGraph G \land F \in Word dom iEdg (S)) \to (\forall k \in (0 ..^\|F\|) if- (P (k) = P (k + 1), iEdg (S) (F (k)) = \{P (k)\}, \{P (k), P (k + 1)\} \subseteq iEdg (S) (F (k))) \to \forall k \in (0 ..^\|F\|) if- (P (k) = P (k + 1), iEdg (G) (F (k)) = \{P (k)\}, \{P (k), P (k + 1)\} \subseteq iEdg (G) (F (k))))$
40	39	expimpd	$⊢ S SubGraph G \to ((F \in Word dom iEdg (S) \land \forall k \in (0 ..^\|F\|) if- (P (k) = P (k + 1), iEdg (S) (F (k)) = \{P (k)\}, \{P (k), P (k + 1)\} \subseteq iEdg (S) (F (k)))) \to \forall k \in (0 ..^\|F\|) if- (P (k) = P (k + 1), iEdg (G) (F (k)) = \{P (k)\}, \{P (k), P (k + 1)\} \subseteq iEdg (G) (F (k))))$
41	23 40	syl5	$⊢ S SubGraph G \to ((F \in Word dom iEdg (S) \land P : (0 \dots \|F\|) ⟶ Vtx (S) \land \forall k \in (0 ..^\|F\|) if- (P (k) = P (k + 1), iEdg (S) (F (k)) = \{P (k)\}, \{P (k), P (k + 1)\} \subseteq iEdg (S) (F (k)))) \to \forall k \in (0 ..^\|F\|) if- (P (k) = P (k + 1), iEdg (G) (F (k)) = \{P (k)\}, \{P (k), P (k + 1)\} \subseteq iEdg (G) (F (k))))$
42	22 41	jcad	$⊢ S SubGraph G \to ((F \in Word dom iEdg (S) \land P : (0 \dots \|F\|) ⟶ Vtx (S) \land \forall k \in (0 ..^\|F\|) if- (P (k) = P (k + 1), iEdg (S) (F (k)) = \{P (k)\}, \{P (k), P (k + 1)\} \subseteq iEdg (S) (F (k)))) \to ((F \in Word dom iEdg (G) \land P : (0 \dots \|F\|) ⟶ Vtx (G)) \land \forall k \in (0 ..^\|F\|) if- (P (k) = P (k + 1), iEdg (G) (F (k)) = \{P (k)\}, \{P (k), P (k + 1)\} \subseteq iEdg (G) (F (k)))))$
43	6 42	sylbid	$⊢ S SubGraph G \to (F Walks (S) P \to ((F \in Word dom iEdg (G) \land P : (0 \dots \|F\|) ⟶ Vtx (G)) \land \forall k \in (0 ..^\|F\|) if- (P (k) = P (k + 1), iEdg (G) (F (k)) = \{P (k)\}, \{P (k), P (k + 1)\} \subseteq iEdg (G) (F (k)))))$
44		df-3an	$⊢ (F \in Word dom iEdg (G) \land P : (0 \dots \|F\|) ⟶ Vtx (G) \land \forall k \in (0 ..^\|F\|) if- (P (k) = P (k + 1), iEdg (G) (F (k)) = \{P (k)\}, \{P (k), P (k + 1)\} \subseteq iEdg (G) (F (k)))) \leftrightarrow ((F \in Word dom iEdg (G) \land P : (0 \dots \|F\|) ⟶ Vtx (G)) \land \forall k \in (0 ..^\|F\|) if- (P (k) = P (k + 1), iEdg (G) (F (k)) = \{P (k)\}, \{P (k), P (k + 1)\} \subseteq iEdg (G) (F (k))))$
45	43 44	syl6ibr	$⊢ S SubGraph G \to (F Walks (S) P \to (F \in Word dom iEdg (G) \land P : (0 \dots \|F\|) ⟶ Vtx (G) \land \forall k \in (0 ..^\|F\|) if- (P (k) = P (k + 1), iEdg (G) (F (k)) = \{P (k)\}, \{P (k), P (k + 1)\} \subseteq iEdg (G) (F (k)))))$
46	8 9	iswlkg	$⊢ G \in V \to (F Walks (G) P \leftrightarrow (F \in Word dom iEdg (G) \land P : (0 \dots \|F\|) ⟶ Vtx (G) \land \forall k \in (0 ..^\|F\|) if- (P (k) = P (k + 1), iEdg (G) (F (k)) = \{P (k)\}, \{P (k), P (k + 1)\} \subseteq iEdg (G) (F (k)))))$
47	1 46	simpl2im	$⊢ S SubGraph G \to (F Walks (G) P \leftrightarrow (F \in Word dom iEdg (G) \land P : (0 \dots \|F\|) ⟶ Vtx (G) \land \forall k \in (0 ..^\|F\|) if- (P (k) = P (k + 1), iEdg (G) (F (k)) = \{P (k)\}, \{P (k), P (k + 1)\} \subseteq iEdg (G) (F (k)))))$
48	45 47	sylibrd	$⊢ S SubGraph G \to (F Walks (S) P \to F Walks (G) P)$

Metamath Proof Explorer

Theorem subgrwlk

Proof