This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem upgrtrls

Description: The set of trails in a pseudograph, definition of walks expanded. (Contributed by Alexander van der Vekens, 20-Oct-2017) (Revised by AV, 7-Jan-2021)

Ref Expression
Hypotheses upgrtrls.v ⊢ V = Vtx ⁡ G
upgrtrls.i ⊢ I = iEdg ⁡ G
Assertion upgrtrls ⊢ G ∈ UPGraph → Trails ⁡ G = f p | f ∈ Word dom ⁡ I ∧ Fun ⁡ f -1 ∧ p : 0 … f ⟶ V ∧ ∀ k ∈ 0 ..^ f I ⁡ f ⁡ k = p ⁡ k p ⁡ k + 1

Proof

Step Hyp Ref Expression
1 upgrtrls.v ⊢ V = Vtx ⁡ G
2 upgrtrls.i ⊢ I = iEdg ⁡ G
3 trlsfval ⊢ Trails ⁡ G = f p | f Walks ⁡ G p ∧ Fun ⁡ f -1
4 1 2 upgriswlk ⊢ G ∈ UPGraph → f Walks ⁡ G p ↔ f ∈ Word dom ⁡ I ∧ p : 0 … f ⟶ V ∧ ∀ k ∈ 0 ..^ f I ⁡ f ⁡ k = p ⁡ k p ⁡ k + 1
5 4 anbi1d ⊢ G ∈ UPGraph → f Walks ⁡ G p ∧ Fun ⁡ f -1 ↔ f ∈ Word dom ⁡ I ∧ p : 0 … f ⟶ V ∧ ∀ k ∈ 0 ..^ f I ⁡ f ⁡ k = p ⁡ k p ⁡ k + 1 ∧ Fun ⁡ f -1
6 an32 ⊢ f ∈ Word dom ⁡ I ∧ p : 0 … f ⟶ V ∧ ∀ k ∈ 0 ..^ f I ⁡ f ⁡ k = p ⁡ k p ⁡ k + 1 ∧ Fun ⁡ f -1 ↔ f ∈ Word dom ⁡ I ∧ Fun ⁡ f -1 ∧ p : 0 … f ⟶ V ∧ ∀ k ∈ 0 ..^ f I ⁡ f ⁡ k = p ⁡ k p ⁡ k + 1
7 3anass ⊢ f ∈ Word dom ⁡ I ∧ p : 0 … f ⟶ V ∧ ∀ k ∈ 0 ..^ f I ⁡ f ⁡ k = p ⁡ k p ⁡ k + 1 ↔ f ∈ Word dom ⁡ I ∧ p : 0 … f ⟶ V ∧ ∀ k ∈ 0 ..^ f I ⁡ f ⁡ k = p ⁡ k p ⁡ k + 1
8 7 anbi1i ⊢ f ∈ Word dom ⁡ I ∧ p : 0 … f ⟶ V ∧ ∀ k ∈ 0 ..^ f I ⁡ f ⁡ k = p ⁡ k p ⁡ k + 1 ∧ Fun ⁡ f -1 ↔ f ∈ Word dom ⁡ I ∧ p : 0 … f ⟶ V ∧ ∀ k ∈ 0 ..^ f I ⁡ f ⁡ k = p ⁡ k p ⁡ k + 1 ∧ Fun ⁡ f -1
9 3anass ⊢ f ∈ Word dom ⁡ I ∧ Fun ⁡ f -1 ∧ p : 0 … f ⟶ V ∧ ∀ k ∈ 0 ..^ f I ⁡ f ⁡ k = p ⁡ k p ⁡ k + 1 ↔ f ∈ Word dom ⁡ I ∧ Fun ⁡ f -1 ∧ p : 0 … f ⟶ V ∧ ∀ k ∈ 0 ..^ f I ⁡ f ⁡ k = p ⁡ k p ⁡ k + 1
10 6 8 9 3bitr4i ⊢ f ∈ Word dom ⁡ I ∧ p : 0 … f ⟶ V ∧ ∀ k ∈ 0 ..^ f I ⁡ f ⁡ k = p ⁡ k p ⁡ k + 1 ∧ Fun ⁡ f -1 ↔ f ∈ Word dom ⁡ I ∧ Fun ⁡ f -1 ∧ p : 0 … f ⟶ V ∧ ∀ k ∈ 0 ..^ f I ⁡ f ⁡ k = p ⁡ k p ⁡ k + 1
11 5 10 bitrdi ⊢ G ∈ UPGraph → f Walks ⁡ G p ∧ Fun ⁡ f -1 ↔ f ∈ Word dom ⁡ I ∧ Fun ⁡ f -1 ∧ p : 0 … f ⟶ V ∧ ∀ k ∈ 0 ..^ f I ⁡ f ⁡ k = p ⁡ k p ⁡ k + 1
12 11 opabbidv ⊢ G ∈ UPGraph → f p | f Walks ⁡ G p ∧ Fun ⁡ f -1 = f p | f ∈ Word dom ⁡ I ∧ Fun ⁡ f -1 ∧ p : 0 … f ⟶ V ∧ ∀ k ∈ 0 ..^ f I ⁡ f ⁡ k = p ⁡ k p ⁡ k + 1
13 3 12 eqtrid ⊢ G ∈ UPGraph → Trails ⁡ G = f p | f ∈ Word dom ⁡ I ∧ Fun ⁡ f -1 ∧ p : 0 … f ⟶ V ∧ ∀ k ∈ 0 ..^ f I ⁡ f ⁡ k = p ⁡ k p ⁡ k + 1