MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  uspgr2wlkeq Structured version   Visualization version   GIF version

Theorem uspgr2wlkeq 26424
Description: Conditions for two walks within the same simple pseudograph being the same. It is sufficient that the vertices (in the same order) are identical. (Contributed by AV, 3-Jul-2018.) (Revised by AV, 14-Apr-2021.)
Assertion
Ref Expression
uspgr2wlkeq ((𝐺 ∈ USPGraph ∧ (𝐴 ∈ (Walks‘𝐺) ∧ 𝐵 ∈ (Walks‘𝐺)) ∧ 𝑁 = (#‘(1st𝐴))) → (𝐴 = 𝐵 ↔ (𝑁 = (#‘(1st𝐵)) ∧ ∀𝑦 ∈ (0...𝑁)((2nd𝐴)‘𝑦) = ((2nd𝐵)‘𝑦))))
Distinct variable groups:   𝑦,𝐴   𝑦,𝐵   𝑦,𝐺   𝑦,𝑁

Proof of Theorem uspgr2wlkeq
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 3anan32 1048 . . 3 ((𝑁 = (#‘(1st𝐵)) ∧ ∀𝑦 ∈ (0..^𝑁)((1st𝐴)‘𝑦) = ((1st𝐵)‘𝑦) ∧ ∀𝑦 ∈ (0...𝑁)((2nd𝐴)‘𝑦) = ((2nd𝐵)‘𝑦)) ↔ ((𝑁 = (#‘(1st𝐵)) ∧ ∀𝑦 ∈ (0...𝑁)((2nd𝐴)‘𝑦) = ((2nd𝐵)‘𝑦)) ∧ ∀𝑦 ∈ (0..^𝑁)((1st𝐴)‘𝑦) = ((1st𝐵)‘𝑦)))
21a1i 11 . 2 ((𝐺 ∈ USPGraph ∧ (𝐴 ∈ (Walks‘𝐺) ∧ 𝐵 ∈ (Walks‘𝐺)) ∧ 𝑁 = (#‘(1st𝐴))) → ((𝑁 = (#‘(1st𝐵)) ∧ ∀𝑦 ∈ (0..^𝑁)((1st𝐴)‘𝑦) = ((1st𝐵)‘𝑦) ∧ ∀𝑦 ∈ (0...𝑁)((2nd𝐴)‘𝑦) = ((2nd𝐵)‘𝑦)) ↔ ((𝑁 = (#‘(1st𝐵)) ∧ ∀𝑦 ∈ (0...𝑁)((2nd𝐴)‘𝑦) = ((2nd𝐵)‘𝑦)) ∧ ∀𝑦 ∈ (0..^𝑁)((1st𝐴)‘𝑦) = ((1st𝐵)‘𝑦))))
3 wlkeq 26412 . . . 4 ((𝐴 ∈ (Walks‘𝐺) ∧ 𝐵 ∈ (Walks‘𝐺) ∧ 𝑁 = (#‘(1st𝐴))) → (𝐴 = 𝐵 ↔ (𝑁 = (#‘(1st𝐵)) ∧ ∀𝑦 ∈ (0..^𝑁)((1st𝐴)‘𝑦) = ((1st𝐵)‘𝑦) ∧ ∀𝑦 ∈ (0...𝑁)((2nd𝐴)‘𝑦) = ((2nd𝐵)‘𝑦))))
433expa 1262 . . 3 (((𝐴 ∈ (Walks‘𝐺) ∧ 𝐵 ∈ (Walks‘𝐺)) ∧ 𝑁 = (#‘(1st𝐴))) → (𝐴 = 𝐵 ↔ (𝑁 = (#‘(1st𝐵)) ∧ ∀𝑦 ∈ (0..^𝑁)((1st𝐴)‘𝑦) = ((1st𝐵)‘𝑦) ∧ ∀𝑦 ∈ (0...𝑁)((2nd𝐴)‘𝑦) = ((2nd𝐵)‘𝑦))))
543adant1 1077 . 2 ((𝐺 ∈ USPGraph ∧ (𝐴 ∈ (Walks‘𝐺) ∧ 𝐵 ∈ (Walks‘𝐺)) ∧ 𝑁 = (#‘(1st𝐴))) → (𝐴 = 𝐵 ↔ (𝑁 = (#‘(1st𝐵)) ∧ ∀𝑦 ∈ (0..^𝑁)((1st𝐴)‘𝑦) = ((1st𝐵)‘𝑦) ∧ ∀𝑦 ∈ (0...𝑁)((2nd𝐴)‘𝑦) = ((2nd𝐵)‘𝑦))))
6 fzofzp1 12513 . . . . . . . . . . . 12 (𝑥 ∈ (0..^𝑁) → (𝑥 + 1) ∈ (0...𝑁))
76adantl 482 . . . . . . . . . . 11 ((((𝐺 ∈ USPGraph ∧ (𝐴 ∈ (Walks‘𝐺) ∧ 𝐵 ∈ (Walks‘𝐺)) ∧ 𝑁 = (#‘(1st𝐴))) ∧ 𝑁 = (#‘(1st𝐵))) ∧ 𝑥 ∈ (0..^𝑁)) → (𝑥 + 1) ∈ (0...𝑁))
8 fveq2 6153 . . . . . . . . . . . . 13 (𝑦 = (𝑥 + 1) → ((2nd𝐴)‘𝑦) = ((2nd𝐴)‘(𝑥 + 1)))
9 fveq2 6153 . . . . . . . . . . . . 13 (𝑦 = (𝑥 + 1) → ((2nd𝐵)‘𝑦) = ((2nd𝐵)‘(𝑥 + 1)))
108, 9eqeq12d 2636 . . . . . . . . . . . 12 (𝑦 = (𝑥 + 1) → (((2nd𝐴)‘𝑦) = ((2nd𝐵)‘𝑦) ↔ ((2nd𝐴)‘(𝑥 + 1)) = ((2nd𝐵)‘(𝑥 + 1))))
1110adantl 482 . . . . . . . . . . 11 (((((𝐺 ∈ USPGraph ∧ (𝐴 ∈ (Walks‘𝐺) ∧ 𝐵 ∈ (Walks‘𝐺)) ∧ 𝑁 = (#‘(1st𝐴))) ∧ 𝑁 = (#‘(1st𝐵))) ∧ 𝑥 ∈ (0..^𝑁)) ∧ 𝑦 = (𝑥 + 1)) → (((2nd𝐴)‘𝑦) = ((2nd𝐵)‘𝑦) ↔ ((2nd𝐴)‘(𝑥 + 1)) = ((2nd𝐵)‘(𝑥 + 1))))
127, 11rspcdv 3301 . . . . . . . . . 10 ((((𝐺 ∈ USPGraph ∧ (𝐴 ∈ (Walks‘𝐺) ∧ 𝐵 ∈ (Walks‘𝐺)) ∧ 𝑁 = (#‘(1st𝐴))) ∧ 𝑁 = (#‘(1st𝐵))) ∧ 𝑥 ∈ (0..^𝑁)) → (∀𝑦 ∈ (0...𝑁)((2nd𝐴)‘𝑦) = ((2nd𝐵)‘𝑦) → ((2nd𝐴)‘(𝑥 + 1)) = ((2nd𝐵)‘(𝑥 + 1))))
1312impancom 456 . . . . . . . . 9 ((((𝐺 ∈ USPGraph ∧ (𝐴 ∈ (Walks‘𝐺) ∧ 𝐵 ∈ (Walks‘𝐺)) ∧ 𝑁 = (#‘(1st𝐴))) ∧ 𝑁 = (#‘(1st𝐵))) ∧ ∀𝑦 ∈ (0...𝑁)((2nd𝐴)‘𝑦) = ((2nd𝐵)‘𝑦)) → (𝑥 ∈ (0..^𝑁) → ((2nd𝐴)‘(𝑥 + 1)) = ((2nd𝐵)‘(𝑥 + 1))))
1413ralrimiv 2960 . . . . . . . 8 ((((𝐺 ∈ USPGraph ∧ (𝐴 ∈ (Walks‘𝐺) ∧ 𝐵 ∈ (Walks‘𝐺)) ∧ 𝑁 = (#‘(1st𝐴))) ∧ 𝑁 = (#‘(1st𝐵))) ∧ ∀𝑦 ∈ (0...𝑁)((2nd𝐴)‘𝑦) = ((2nd𝐵)‘𝑦)) → ∀𝑥 ∈ (0..^𝑁)((2nd𝐴)‘(𝑥 + 1)) = ((2nd𝐵)‘(𝑥 + 1)))
15 oveq1 6617 . . . . . . . . . . 11 (𝑦 = 𝑥 → (𝑦 + 1) = (𝑥 + 1))
1615fveq2d 6157 . . . . . . . . . 10 (𝑦 = 𝑥 → ((2nd𝐴)‘(𝑦 + 1)) = ((2nd𝐴)‘(𝑥 + 1)))
1715fveq2d 6157 . . . . . . . . . 10 (𝑦 = 𝑥 → ((2nd𝐵)‘(𝑦 + 1)) = ((2nd𝐵)‘(𝑥 + 1)))
1816, 17eqeq12d 2636 . . . . . . . . 9 (𝑦 = 𝑥 → (((2nd𝐴)‘(𝑦 + 1)) = ((2nd𝐵)‘(𝑦 + 1)) ↔ ((2nd𝐴)‘(𝑥 + 1)) = ((2nd𝐵)‘(𝑥 + 1))))
1918cbvralv 3162 . . . . . . . 8 (∀𝑦 ∈ (0..^𝑁)((2nd𝐴)‘(𝑦 + 1)) = ((2nd𝐵)‘(𝑦 + 1)) ↔ ∀𝑥 ∈ (0..^𝑁)((2nd𝐴)‘(𝑥 + 1)) = ((2nd𝐵)‘(𝑥 + 1)))
2014, 19sylibr 224 . . . . . . 7 ((((𝐺 ∈ USPGraph ∧ (𝐴 ∈ (Walks‘𝐺) ∧ 𝐵 ∈ (Walks‘𝐺)) ∧ 𝑁 = (#‘(1st𝐴))) ∧ 𝑁 = (#‘(1st𝐵))) ∧ ∀𝑦 ∈ (0...𝑁)((2nd𝐴)‘𝑦) = ((2nd𝐵)‘𝑦)) → ∀𝑦 ∈ (0..^𝑁)((2nd𝐴)‘(𝑦 + 1)) = ((2nd𝐵)‘(𝑦 + 1)))
21 fzossfz 12436 . . . . . . . . . 10 (0..^𝑁) ⊆ (0...𝑁)
22 ssralv 3650 . . . . . . . . . 10 ((0..^𝑁) ⊆ (0...𝑁) → (∀𝑦 ∈ (0...𝑁)((2nd𝐴)‘𝑦) = ((2nd𝐵)‘𝑦) → ∀𝑦 ∈ (0..^𝑁)((2nd𝐴)‘𝑦) = ((2nd𝐵)‘𝑦)))
2321, 22mp1i 13 . . . . . . . . 9 (((𝐺 ∈ USPGraph ∧ (𝐴 ∈ (Walks‘𝐺) ∧ 𝐵 ∈ (Walks‘𝐺)) ∧ 𝑁 = (#‘(1st𝐴))) ∧ 𝑁 = (#‘(1st𝐵))) → (∀𝑦 ∈ (0...𝑁)((2nd𝐴)‘𝑦) = ((2nd𝐵)‘𝑦) → ∀𝑦 ∈ (0..^𝑁)((2nd𝐴)‘𝑦) = ((2nd𝐵)‘𝑦)))
24 r19.26 3058 . . . . . . . . . . 11 (∀𝑦 ∈ (0..^𝑁)(((2nd𝐴)‘𝑦) = ((2nd𝐵)‘𝑦) ∧ ((2nd𝐴)‘(𝑦 + 1)) = ((2nd𝐵)‘(𝑦 + 1))) ↔ (∀𝑦 ∈ (0..^𝑁)((2nd𝐴)‘𝑦) = ((2nd𝐵)‘𝑦) ∧ ∀𝑦 ∈ (0..^𝑁)((2nd𝐴)‘(𝑦 + 1)) = ((2nd𝐵)‘(𝑦 + 1))))
25 preq12 4245 . . . . . . . . . . . . 13 ((((2nd𝐴)‘𝑦) = ((2nd𝐵)‘𝑦) ∧ ((2nd𝐴)‘(𝑦 + 1)) = ((2nd𝐵)‘(𝑦 + 1))) → {((2nd𝐴)‘𝑦), ((2nd𝐴)‘(𝑦 + 1))} = {((2nd𝐵)‘𝑦), ((2nd𝐵)‘(𝑦 + 1))})
2625a1i 11 . . . . . . . . . . . 12 (((𝐺 ∈ USPGraph ∧ (𝐴 ∈ (Walks‘𝐺) ∧ 𝐵 ∈ (Walks‘𝐺)) ∧ 𝑁 = (#‘(1st𝐴))) ∧ 𝑁 = (#‘(1st𝐵))) → ((((2nd𝐴)‘𝑦) = ((2nd𝐵)‘𝑦) ∧ ((2nd𝐴)‘(𝑦 + 1)) = ((2nd𝐵)‘(𝑦 + 1))) → {((2nd𝐴)‘𝑦), ((2nd𝐴)‘(𝑦 + 1))} = {((2nd𝐵)‘𝑦), ((2nd𝐵)‘(𝑦 + 1))}))
2726ralimdv 2958 . . . . . . . . . . 11 (((𝐺 ∈ USPGraph ∧ (𝐴 ∈ (Walks‘𝐺) ∧ 𝐵 ∈ (Walks‘𝐺)) ∧ 𝑁 = (#‘(1st𝐴))) ∧ 𝑁 = (#‘(1st𝐵))) → (∀𝑦 ∈ (0..^𝑁)(((2nd𝐴)‘𝑦) = ((2nd𝐵)‘𝑦) ∧ ((2nd𝐴)‘(𝑦 + 1)) = ((2nd𝐵)‘(𝑦 + 1))) → ∀𝑦 ∈ (0..^𝑁){((2nd𝐴)‘𝑦), ((2nd𝐴)‘(𝑦 + 1))} = {((2nd𝐵)‘𝑦), ((2nd𝐵)‘(𝑦 + 1))}))
2824, 27syl5bir 233 . . . . . . . . . 10 (((𝐺 ∈ USPGraph ∧ (𝐴 ∈ (Walks‘𝐺) ∧ 𝐵 ∈ (Walks‘𝐺)) ∧ 𝑁 = (#‘(1st𝐴))) ∧ 𝑁 = (#‘(1st𝐵))) → ((∀𝑦 ∈ (0..^𝑁)((2nd𝐴)‘𝑦) = ((2nd𝐵)‘𝑦) ∧ ∀𝑦 ∈ (0..^𝑁)((2nd𝐴)‘(𝑦 + 1)) = ((2nd𝐵)‘(𝑦 + 1))) → ∀𝑦 ∈ (0..^𝑁){((2nd𝐴)‘𝑦), ((2nd𝐴)‘(𝑦 + 1))} = {((2nd𝐵)‘𝑦), ((2nd𝐵)‘(𝑦 + 1))}))
2928expd 452 . . . . . . . . 9 (((𝐺 ∈ USPGraph ∧ (𝐴 ∈ (Walks‘𝐺) ∧ 𝐵 ∈ (Walks‘𝐺)) ∧ 𝑁 = (#‘(1st𝐴))) ∧ 𝑁 = (#‘(1st𝐵))) → (∀𝑦 ∈ (0..^𝑁)((2nd𝐴)‘𝑦) = ((2nd𝐵)‘𝑦) → (∀𝑦 ∈ (0..^𝑁)((2nd𝐴)‘(𝑦 + 1)) = ((2nd𝐵)‘(𝑦 + 1)) → ∀𝑦 ∈ (0..^𝑁){((2nd𝐴)‘𝑦), ((2nd𝐴)‘(𝑦 + 1))} = {((2nd𝐵)‘𝑦), ((2nd𝐵)‘(𝑦 + 1))})))
3023, 29syld 47 . . . . . . . 8 (((𝐺 ∈ USPGraph ∧ (𝐴 ∈ (Walks‘𝐺) ∧ 𝐵 ∈ (Walks‘𝐺)) ∧ 𝑁 = (#‘(1st𝐴))) ∧ 𝑁 = (#‘(1st𝐵))) → (∀𝑦 ∈ (0...𝑁)((2nd𝐴)‘𝑦) = ((2nd𝐵)‘𝑦) → (∀𝑦 ∈ (0..^𝑁)((2nd𝐴)‘(𝑦 + 1)) = ((2nd𝐵)‘(𝑦 + 1)) → ∀𝑦 ∈ (0..^𝑁){((2nd𝐴)‘𝑦), ((2nd𝐴)‘(𝑦 + 1))} = {((2nd𝐵)‘𝑦), ((2nd𝐵)‘(𝑦 + 1))})))
3130imp 445 . . . . . . 7 ((((𝐺 ∈ USPGraph ∧ (𝐴 ∈ (Walks‘𝐺) ∧ 𝐵 ∈ (Walks‘𝐺)) ∧ 𝑁 = (#‘(1st𝐴))) ∧ 𝑁 = (#‘(1st𝐵))) ∧ ∀𝑦 ∈ (0...𝑁)((2nd𝐴)‘𝑦) = ((2nd𝐵)‘𝑦)) → (∀𝑦 ∈ (0..^𝑁)((2nd𝐴)‘(𝑦 + 1)) = ((2nd𝐵)‘(𝑦 + 1)) → ∀𝑦 ∈ (0..^𝑁){((2nd𝐴)‘𝑦), ((2nd𝐴)‘(𝑦 + 1))} = {((2nd𝐵)‘𝑦), ((2nd𝐵)‘(𝑦 + 1))}))
3220, 31mpd 15 . . . . . 6 ((((𝐺 ∈ USPGraph ∧ (𝐴 ∈ (Walks‘𝐺) ∧ 𝐵 ∈ (Walks‘𝐺)) ∧ 𝑁 = (#‘(1st𝐴))) ∧ 𝑁 = (#‘(1st𝐵))) ∧ ∀𝑦 ∈ (0...𝑁)((2nd𝐴)‘𝑦) = ((2nd𝐵)‘𝑦)) → ∀𝑦 ∈ (0..^𝑁){((2nd𝐴)‘𝑦), ((2nd𝐴)‘(𝑦 + 1))} = {((2nd𝐵)‘𝑦), ((2nd𝐵)‘(𝑦 + 1))})
3332ex 450 . . . . 5 (((𝐺 ∈ USPGraph ∧ (𝐴 ∈ (Walks‘𝐺) ∧ 𝐵 ∈ (Walks‘𝐺)) ∧ 𝑁 = (#‘(1st𝐴))) ∧ 𝑁 = (#‘(1st𝐵))) → (∀𝑦 ∈ (0...𝑁)((2nd𝐴)‘𝑦) = ((2nd𝐵)‘𝑦) → ∀𝑦 ∈ (0..^𝑁){((2nd𝐴)‘𝑦), ((2nd𝐴)‘(𝑦 + 1))} = {((2nd𝐵)‘𝑦), ((2nd𝐵)‘(𝑦 + 1))}))
34 uspgrupgr 25977 . . . . . . . 8 (𝐺 ∈ USPGraph → 𝐺 ∈ UPGraph )
35 eqid 2621 . . . . . . . . . 10 (Vtx‘𝐺) = (Vtx‘𝐺)
36 eqid 2621 . . . . . . . . . 10 (iEdg‘𝐺) = (iEdg‘𝐺)
37 eqid 2621 . . . . . . . . . 10 (1st𝐴) = (1st𝐴)
38 eqid 2621 . . . . . . . . . 10 (2nd𝐴) = (2nd𝐴)
3935, 36, 37, 38upgrwlkcompim 26421 . . . . . . . . 9 ((𝐺 ∈ UPGraph ∧ 𝐴 ∈ (Walks‘𝐺)) → ((1st𝐴) ∈ Word dom (iEdg‘𝐺) ∧ (2nd𝐴):(0...(#‘(1st𝐴)))⟶(Vtx‘𝐺) ∧ ∀𝑦 ∈ (0..^(#‘(1st𝐴)))((iEdg‘𝐺)‘((1st𝐴)‘𝑦)) = {((2nd𝐴)‘𝑦), ((2nd𝐴)‘(𝑦 + 1))}))
4039ex 450 . . . . . . . 8 (𝐺 ∈ UPGraph → (𝐴 ∈ (Walks‘𝐺) → ((1st𝐴) ∈ Word dom (iEdg‘𝐺) ∧ (2nd𝐴):(0...(#‘(1st𝐴)))⟶(Vtx‘𝐺) ∧ ∀𝑦 ∈ (0..^(#‘(1st𝐴)))((iEdg‘𝐺)‘((1st𝐴)‘𝑦)) = {((2nd𝐴)‘𝑦), ((2nd𝐴)‘(𝑦 + 1))})))
4134, 40syl 17 . . . . . . 7 (𝐺 ∈ USPGraph → (𝐴 ∈ (Walks‘𝐺) → ((1st𝐴) ∈ Word dom (iEdg‘𝐺) ∧ (2nd𝐴):(0...(#‘(1st𝐴)))⟶(Vtx‘𝐺) ∧ ∀𝑦 ∈ (0..^(#‘(1st𝐴)))((iEdg‘𝐺)‘((1st𝐴)‘𝑦)) = {((2nd𝐴)‘𝑦), ((2nd𝐴)‘(𝑦 + 1))})))
42 eqid 2621 . . . . . . . . . 10 (1st𝐵) = (1st𝐵)
43 eqid 2621 . . . . . . . . . 10 (2nd𝐵) = (2nd𝐵)
4435, 36, 42, 43upgrwlkcompim 26421 . . . . . . . . 9 ((𝐺 ∈ UPGraph ∧ 𝐵 ∈ (Walks‘𝐺)) → ((1st𝐵) ∈ Word dom (iEdg‘𝐺) ∧ (2nd𝐵):(0...(#‘(1st𝐵)))⟶(Vtx‘𝐺) ∧ ∀𝑦 ∈ (0..^(#‘(1st𝐵)))((iEdg‘𝐺)‘((1st𝐵)‘𝑦)) = {((2nd𝐵)‘𝑦), ((2nd𝐵)‘(𝑦 + 1))}))
4544ex 450 . . . . . . . 8 (𝐺 ∈ UPGraph → (𝐵 ∈ (Walks‘𝐺) → ((1st𝐵) ∈ Word dom (iEdg‘𝐺) ∧ (2nd𝐵):(0...(#‘(1st𝐵)))⟶(Vtx‘𝐺) ∧ ∀𝑦 ∈ (0..^(#‘(1st𝐵)))((iEdg‘𝐺)‘((1st𝐵)‘𝑦)) = {((2nd𝐵)‘𝑦), ((2nd𝐵)‘(𝑦 + 1))})))
4634, 45syl 17 . . . . . . 7 (𝐺 ∈ USPGraph → (𝐵 ∈ (Walks‘𝐺) → ((1st𝐵) ∈ Word dom (iEdg‘𝐺) ∧ (2nd𝐵):(0...(#‘(1st𝐵)))⟶(Vtx‘𝐺) ∧ ∀𝑦 ∈ (0..^(#‘(1st𝐵)))((iEdg‘𝐺)‘((1st𝐵)‘𝑦)) = {((2nd𝐵)‘𝑦), ((2nd𝐵)‘(𝑦 + 1))})))
47 oveq2 6618 . . . . . . . . . . . . . . . . . . 19 ((#‘(1st𝐵)) = 𝑁 → (0..^(#‘(1st𝐵))) = (0..^𝑁))
4847eqcoms 2629 . . . . . . . . . . . . . . . . . 18 (𝑁 = (#‘(1st𝐵)) → (0..^(#‘(1st𝐵))) = (0..^𝑁))
4948raleqdv 3136 . . . . . . . . . . . . . . . . 17 (𝑁 = (#‘(1st𝐵)) → (∀𝑦 ∈ (0..^(#‘(1st𝐵)))((iEdg‘𝐺)‘((1st𝐵)‘𝑦)) = {((2nd𝐵)‘𝑦), ((2nd𝐵)‘(𝑦 + 1))} ↔ ∀𝑦 ∈ (0..^𝑁)((iEdg‘𝐺)‘((1st𝐵)‘𝑦)) = {((2nd𝐵)‘𝑦), ((2nd𝐵)‘(𝑦 + 1))}))
50 oveq2 6618 . . . . . . . . . . . . . . . . . . 19 ((#‘(1st𝐴)) = 𝑁 → (0..^(#‘(1st𝐴))) = (0..^𝑁))
5150eqcoms 2629 . . . . . . . . . . . . . . . . . 18 (𝑁 = (#‘(1st𝐴)) → (0..^(#‘(1st𝐴))) = (0..^𝑁))
5251raleqdv 3136 . . . . . . . . . . . . . . . . 17 (𝑁 = (#‘(1st𝐴)) → (∀𝑦 ∈ (0..^(#‘(1st𝐴)))((iEdg‘𝐺)‘((1st𝐴)‘𝑦)) = {((2nd𝐴)‘𝑦), ((2nd𝐴)‘(𝑦 + 1))} ↔ ∀𝑦 ∈ (0..^𝑁)((iEdg‘𝐺)‘((1st𝐴)‘𝑦)) = {((2nd𝐴)‘𝑦), ((2nd𝐴)‘(𝑦 + 1))}))
5349, 52bi2anan9r 917 . . . . . . . . . . . . . . . 16 ((𝑁 = (#‘(1st𝐴)) ∧ 𝑁 = (#‘(1st𝐵))) → ((∀𝑦 ∈ (0..^(#‘(1st𝐵)))((iEdg‘𝐺)‘((1st𝐵)‘𝑦)) = {((2nd𝐵)‘𝑦), ((2nd𝐵)‘(𝑦 + 1))} ∧ ∀𝑦 ∈ (0..^(#‘(1st𝐴)))((iEdg‘𝐺)‘((1st𝐴)‘𝑦)) = {((2nd𝐴)‘𝑦), ((2nd𝐴)‘(𝑦 + 1))}) ↔ (∀𝑦 ∈ (0..^𝑁)((iEdg‘𝐺)‘((1st𝐵)‘𝑦)) = {((2nd𝐵)‘𝑦), ((2nd𝐵)‘(𝑦 + 1))} ∧ ∀𝑦 ∈ (0..^𝑁)((iEdg‘𝐺)‘((1st𝐴)‘𝑦)) = {((2nd𝐴)‘𝑦), ((2nd𝐴)‘(𝑦 + 1))})))
54 r19.26 3058 . . . . . . . . . . . . . . . . 17 (∀𝑦 ∈ (0..^𝑁)(((iEdg‘𝐺)‘((1st𝐵)‘𝑦)) = {((2nd𝐵)‘𝑦), ((2nd𝐵)‘(𝑦 + 1))} ∧ ((iEdg‘𝐺)‘((1st𝐴)‘𝑦)) = {((2nd𝐴)‘𝑦), ((2nd𝐴)‘(𝑦 + 1))}) ↔ (∀𝑦 ∈ (0..^𝑁)((iEdg‘𝐺)‘((1st𝐵)‘𝑦)) = {((2nd𝐵)‘𝑦), ((2nd𝐵)‘(𝑦 + 1))} ∧ ∀𝑦 ∈ (0..^𝑁)((iEdg‘𝐺)‘((1st𝐴)‘𝑦)) = {((2nd𝐴)‘𝑦), ((2nd𝐴)‘(𝑦 + 1))}))
55 eqeq2 2632 . . . . . . . . . . . . . . . . . . . . 21 ({((2nd𝐴)‘𝑦), ((2nd𝐴)‘(𝑦 + 1))} = {((2nd𝐵)‘𝑦), ((2nd𝐵)‘(𝑦 + 1))} → (((iEdg‘𝐺)‘((1st𝐴)‘𝑦)) = {((2nd𝐴)‘𝑦), ((2nd𝐴)‘(𝑦 + 1))} ↔ ((iEdg‘𝐺)‘((1st𝐴)‘𝑦)) = {((2nd𝐵)‘𝑦), ((2nd𝐵)‘(𝑦 + 1))}))
56 eqeq2 2632 . . . . . . . . . . . . . . . . . . . . . . 23 ({((2nd𝐵)‘𝑦), ((2nd𝐵)‘(𝑦 + 1))} = ((iEdg‘𝐺)‘((1st𝐴)‘𝑦)) → (((iEdg‘𝐺)‘((1st𝐵)‘𝑦)) = {((2nd𝐵)‘𝑦), ((2nd𝐵)‘(𝑦 + 1))} ↔ ((iEdg‘𝐺)‘((1st𝐵)‘𝑦)) = ((iEdg‘𝐺)‘((1st𝐴)‘𝑦))))
5756eqcoms 2629 . . . . . . . . . . . . . . . . . . . . . 22 (((iEdg‘𝐺)‘((1st𝐴)‘𝑦)) = {((2nd𝐵)‘𝑦), ((2nd𝐵)‘(𝑦 + 1))} → (((iEdg‘𝐺)‘((1st𝐵)‘𝑦)) = {((2nd𝐵)‘𝑦), ((2nd𝐵)‘(𝑦 + 1))} ↔ ((iEdg‘𝐺)‘((1st𝐵)‘𝑦)) = ((iEdg‘𝐺)‘((1st𝐴)‘𝑦))))
5857biimpd 219 . . . . . . . . . . . . . . . . . . . . 21 (((iEdg‘𝐺)‘((1st𝐴)‘𝑦)) = {((2nd𝐵)‘𝑦), ((2nd𝐵)‘(𝑦 + 1))} → (((iEdg‘𝐺)‘((1st𝐵)‘𝑦)) = {((2nd𝐵)‘𝑦), ((2nd𝐵)‘(𝑦 + 1))} → ((iEdg‘𝐺)‘((1st𝐵)‘𝑦)) = ((iEdg‘𝐺)‘((1st𝐴)‘𝑦))))
5955, 58syl6bi 243 . . . . . . . . . . . . . . . . . . . 20 ({((2nd𝐴)‘𝑦), ((2nd𝐴)‘(𝑦 + 1))} = {((2nd𝐵)‘𝑦), ((2nd𝐵)‘(𝑦 + 1))} → (((iEdg‘𝐺)‘((1st𝐴)‘𝑦)) = {((2nd𝐴)‘𝑦), ((2nd𝐴)‘(𝑦 + 1))} → (((iEdg‘𝐺)‘((1st𝐵)‘𝑦)) = {((2nd𝐵)‘𝑦), ((2nd𝐵)‘(𝑦 + 1))} → ((iEdg‘𝐺)‘((1st𝐵)‘𝑦)) = ((iEdg‘𝐺)‘((1st𝐴)‘𝑦)))))
6059com13 88 . . . . . . . . . . . . . . . . . . 19 (((iEdg‘𝐺)‘((1st𝐵)‘𝑦)) = {((2nd𝐵)‘𝑦), ((2nd𝐵)‘(𝑦 + 1))} → (((iEdg‘𝐺)‘((1st𝐴)‘𝑦)) = {((2nd𝐴)‘𝑦), ((2nd𝐴)‘(𝑦 + 1))} → ({((2nd𝐴)‘𝑦), ((2nd𝐴)‘(𝑦 + 1))} = {((2nd𝐵)‘𝑦), ((2nd𝐵)‘(𝑦 + 1))} → ((iEdg‘𝐺)‘((1st𝐵)‘𝑦)) = ((iEdg‘𝐺)‘((1st𝐴)‘𝑦)))))
6160imp 445 . . . . . . . . . . . . . . . . . 18 ((((iEdg‘𝐺)‘((1st𝐵)‘𝑦)) = {((2nd𝐵)‘𝑦), ((2nd𝐵)‘(𝑦 + 1))} ∧ ((iEdg‘𝐺)‘((1st𝐴)‘𝑦)) = {((2nd𝐴)‘𝑦), ((2nd𝐴)‘(𝑦 + 1))}) → ({((2nd𝐴)‘𝑦), ((2nd𝐴)‘(𝑦 + 1))} = {((2nd𝐵)‘𝑦), ((2nd𝐵)‘(𝑦 + 1))} → ((iEdg‘𝐺)‘((1st𝐵)‘𝑦)) = ((iEdg‘𝐺)‘((1st𝐴)‘𝑦))))
6261ral2imi 2942 . . . . . . . . . . . . . . . . 17 (∀𝑦 ∈ (0..^𝑁)(((iEdg‘𝐺)‘((1st𝐵)‘𝑦)) = {((2nd𝐵)‘𝑦), ((2nd𝐵)‘(𝑦 + 1))} ∧ ((iEdg‘𝐺)‘((1st𝐴)‘𝑦)) = {((2nd𝐴)‘𝑦), ((2nd𝐴)‘(𝑦 + 1))}) → (∀𝑦 ∈ (0..^𝑁){((2nd𝐴)‘𝑦), ((2nd𝐴)‘(𝑦 + 1))} = {((2nd𝐵)‘𝑦), ((2nd𝐵)‘(𝑦 + 1))} → ∀𝑦 ∈ (0..^𝑁)((iEdg‘𝐺)‘((1st𝐵)‘𝑦)) = ((iEdg‘𝐺)‘((1st𝐴)‘𝑦))))
6354, 62sylbir 225 . . . . . . . . . . . . . . . 16 ((∀𝑦 ∈ (0..^𝑁)((iEdg‘𝐺)‘((1st𝐵)‘𝑦)) = {((2nd𝐵)‘𝑦), ((2nd𝐵)‘(𝑦 + 1))} ∧ ∀𝑦 ∈ (0..^𝑁)((iEdg‘𝐺)‘((1st𝐴)‘𝑦)) = {((2nd𝐴)‘𝑦), ((2nd𝐴)‘(𝑦 + 1))}) → (∀𝑦 ∈ (0..^𝑁){((2nd𝐴)‘𝑦), ((2nd𝐴)‘(𝑦 + 1))} = {((2nd𝐵)‘𝑦), ((2nd𝐵)‘(𝑦 + 1))} → ∀𝑦 ∈ (0..^𝑁)((iEdg‘𝐺)‘((1st𝐵)‘𝑦)) = ((iEdg‘𝐺)‘((1st𝐴)‘𝑦))))
6453, 63syl6bi 243 . . . . . . . . . . . . . . 15 ((𝑁 = (#‘(1st𝐴)) ∧ 𝑁 = (#‘(1st𝐵))) → ((∀𝑦 ∈ (0..^(#‘(1st𝐵)))((iEdg‘𝐺)‘((1st𝐵)‘𝑦)) = {((2nd𝐵)‘𝑦), ((2nd𝐵)‘(𝑦 + 1))} ∧ ∀𝑦 ∈ (0..^(#‘(1st𝐴)))((iEdg‘𝐺)‘((1st𝐴)‘𝑦)) = {((2nd𝐴)‘𝑦), ((2nd𝐴)‘(𝑦 + 1))}) → (∀𝑦 ∈ (0..^𝑁){((2nd𝐴)‘𝑦), ((2nd𝐴)‘(𝑦 + 1))} = {((2nd𝐵)‘𝑦), ((2nd𝐵)‘(𝑦 + 1))} → ∀𝑦 ∈ (0..^𝑁)((iEdg‘𝐺)‘((1st𝐵)‘𝑦)) = ((iEdg‘𝐺)‘((1st𝐴)‘𝑦)))))
6564com12 32 . . . . . . . . . . . . . 14 ((∀𝑦 ∈ (0..^(#‘(1st𝐵)))((iEdg‘𝐺)‘((1st𝐵)‘𝑦)) = {((2nd𝐵)‘𝑦), ((2nd𝐵)‘(𝑦 + 1))} ∧ ∀𝑦 ∈ (0..^(#‘(1st𝐴)))((iEdg‘𝐺)‘((1st𝐴)‘𝑦)) = {((2nd𝐴)‘𝑦), ((2nd𝐴)‘(𝑦 + 1))}) → ((𝑁 = (#‘(1st𝐴)) ∧ 𝑁 = (#‘(1st𝐵))) → (∀𝑦 ∈ (0..^𝑁){((2nd𝐴)‘𝑦), ((2nd𝐴)‘(𝑦 + 1))} = {((2nd𝐵)‘𝑦), ((2nd𝐵)‘(𝑦 + 1))} → ∀𝑦 ∈ (0..^𝑁)((iEdg‘𝐺)‘((1st𝐵)‘𝑦)) = ((iEdg‘𝐺)‘((1st𝐴)‘𝑦)))))
6665ex 450 . . . . . . . . . . . . 13 (∀𝑦 ∈ (0..^(#‘(1st𝐵)))((iEdg‘𝐺)‘((1st𝐵)‘𝑦)) = {((2nd𝐵)‘𝑦), ((2nd𝐵)‘(𝑦 + 1))} → (∀𝑦 ∈ (0..^(#‘(1st𝐴)))((iEdg‘𝐺)‘((1st𝐴)‘𝑦)) = {((2nd𝐴)‘𝑦), ((2nd𝐴)‘(𝑦 + 1))} → ((𝑁 = (#‘(1st𝐴)) ∧ 𝑁 = (#‘(1st𝐵))) → (∀𝑦 ∈ (0..^𝑁){((2nd𝐴)‘𝑦), ((2nd𝐴)‘(𝑦 + 1))} = {((2nd𝐵)‘𝑦), ((2nd𝐵)‘(𝑦 + 1))} → ∀𝑦 ∈ (0..^𝑁)((iEdg‘𝐺)‘((1st𝐵)‘𝑦)) = ((iEdg‘𝐺)‘((1st𝐴)‘𝑦))))))
67663ad2ant3 1082 . . . . . . . . . . . 12 (((1st𝐵) ∈ Word dom (iEdg‘𝐺) ∧ (2nd𝐵):(0...(#‘(1st𝐵)))⟶(Vtx‘𝐺) ∧ ∀𝑦 ∈ (0..^(#‘(1st𝐵)))((iEdg‘𝐺)‘((1st𝐵)‘𝑦)) = {((2nd𝐵)‘𝑦), ((2nd𝐵)‘(𝑦 + 1))}) → (∀𝑦 ∈ (0..^(#‘(1st𝐴)))((iEdg‘𝐺)‘((1st𝐴)‘𝑦)) = {((2nd𝐴)‘𝑦), ((2nd𝐴)‘(𝑦 + 1))} → ((𝑁 = (#‘(1st𝐴)) ∧ 𝑁 = (#‘(1st𝐵))) → (∀𝑦 ∈ (0..^𝑁){((2nd𝐴)‘𝑦), ((2nd𝐴)‘(𝑦 + 1))} = {((2nd𝐵)‘𝑦), ((2nd𝐵)‘(𝑦 + 1))} → ∀𝑦 ∈ (0..^𝑁)((iEdg‘𝐺)‘((1st𝐵)‘𝑦)) = ((iEdg‘𝐺)‘((1st𝐴)‘𝑦))))))
6867com12 32 . . . . . . . . . . 11 (∀𝑦 ∈ (0..^(#‘(1st𝐴)))((iEdg‘𝐺)‘((1st𝐴)‘𝑦)) = {((2nd𝐴)‘𝑦), ((2nd𝐴)‘(𝑦 + 1))} → (((1st𝐵) ∈ Word dom (iEdg‘𝐺) ∧ (2nd𝐵):(0...(#‘(1st𝐵)))⟶(Vtx‘𝐺) ∧ ∀𝑦 ∈ (0..^(#‘(1st𝐵)))((iEdg‘𝐺)‘((1st𝐵)‘𝑦)) = {((2nd𝐵)‘𝑦), ((2nd𝐵)‘(𝑦 + 1))}) → ((𝑁 = (#‘(1st𝐴)) ∧ 𝑁 = (#‘(1st𝐵))) → (∀𝑦 ∈ (0..^𝑁){((2nd𝐴)‘𝑦), ((2nd𝐴)‘(𝑦 + 1))} = {((2nd𝐵)‘𝑦), ((2nd𝐵)‘(𝑦 + 1))} → ∀𝑦 ∈ (0..^𝑁)((iEdg‘𝐺)‘((1st𝐵)‘𝑦)) = ((iEdg‘𝐺)‘((1st𝐴)‘𝑦))))))
69683ad2ant3 1082 . . . . . . . . . 10 (((1st𝐴) ∈ Word dom (iEdg‘𝐺) ∧ (2nd𝐴):(0...(#‘(1st𝐴)))⟶(Vtx‘𝐺) ∧ ∀𝑦 ∈ (0..^(#‘(1st𝐴)))((iEdg‘𝐺)‘((1st𝐴)‘𝑦)) = {((2nd𝐴)‘𝑦), ((2nd𝐴)‘(𝑦 + 1))}) → (((1st𝐵) ∈ Word dom (iEdg‘𝐺) ∧ (2nd𝐵):(0...(#‘(1st𝐵)))⟶(Vtx‘𝐺) ∧ ∀𝑦 ∈ (0..^(#‘(1st𝐵)))((iEdg‘𝐺)‘((1st𝐵)‘𝑦)) = {((2nd𝐵)‘𝑦), ((2nd𝐵)‘(𝑦 + 1))}) → ((𝑁 = (#‘(1st𝐴)) ∧ 𝑁 = (#‘(1st𝐵))) → (∀𝑦 ∈ (0..^𝑁){((2nd𝐴)‘𝑦), ((2nd𝐴)‘(𝑦 + 1))} = {((2nd𝐵)‘𝑦), ((2nd𝐵)‘(𝑦 + 1))} → ∀𝑦 ∈ (0..^𝑁)((iEdg‘𝐺)‘((1st𝐵)‘𝑦)) = ((iEdg‘𝐺)‘((1st𝐴)‘𝑦))))))
7069imp 445 . . . . . . . . 9 ((((1st𝐴) ∈ Word dom (iEdg‘𝐺) ∧ (2nd𝐴):(0...(#‘(1st𝐴)))⟶(Vtx‘𝐺) ∧ ∀𝑦 ∈ (0..^(#‘(1st𝐴)))((iEdg‘𝐺)‘((1st𝐴)‘𝑦)) = {((2nd𝐴)‘𝑦), ((2nd𝐴)‘(𝑦 + 1))}) ∧ ((1st𝐵) ∈ Word dom (iEdg‘𝐺) ∧ (2nd𝐵):(0...(#‘(1st𝐵)))⟶(Vtx‘𝐺) ∧ ∀𝑦 ∈ (0..^(#‘(1st𝐵)))((iEdg‘𝐺)‘((1st𝐵)‘𝑦)) = {((2nd𝐵)‘𝑦), ((2nd𝐵)‘(𝑦 + 1))})) → ((𝑁 = (#‘(1st𝐴)) ∧ 𝑁 = (#‘(1st𝐵))) → (∀𝑦 ∈ (0..^𝑁){((2nd𝐴)‘𝑦), ((2nd𝐴)‘(𝑦 + 1))} = {((2nd𝐵)‘𝑦), ((2nd𝐵)‘(𝑦 + 1))} → ∀𝑦 ∈ (0..^𝑁)((iEdg‘𝐺)‘((1st𝐵)‘𝑦)) = ((iEdg‘𝐺)‘((1st𝐴)‘𝑦)))))
7170expd 452 . . . . . . . 8 ((((1st𝐴) ∈ Word dom (iEdg‘𝐺) ∧ (2nd𝐴):(0...(#‘(1st𝐴)))⟶(Vtx‘𝐺) ∧ ∀𝑦 ∈ (0..^(#‘(1st𝐴)))((iEdg‘𝐺)‘((1st𝐴)‘𝑦)) = {((2nd𝐴)‘𝑦), ((2nd𝐴)‘(𝑦 + 1))}) ∧ ((1st𝐵) ∈ Word dom (iEdg‘𝐺) ∧ (2nd𝐵):(0...(#‘(1st𝐵)))⟶(Vtx‘𝐺) ∧ ∀𝑦 ∈ (0..^(#‘(1st𝐵)))((iEdg‘𝐺)‘((1st𝐵)‘𝑦)) = {((2nd𝐵)‘𝑦), ((2nd𝐵)‘(𝑦 + 1))})) → (𝑁 = (#‘(1st𝐴)) → (𝑁 = (#‘(1st𝐵)) → (∀𝑦 ∈ (0..^𝑁){((2nd𝐴)‘𝑦), ((2nd𝐴)‘(𝑦 + 1))} = {((2nd𝐵)‘𝑦), ((2nd𝐵)‘(𝑦 + 1))} → ∀𝑦 ∈ (0..^𝑁)((iEdg‘𝐺)‘((1st𝐵)‘𝑦)) = ((iEdg‘𝐺)‘((1st𝐴)‘𝑦))))))
7271a1i 11 . . . . . . 7 (𝐺 ∈ USPGraph → ((((1st𝐴) ∈ Word dom (iEdg‘𝐺) ∧ (2nd𝐴):(0...(#‘(1st𝐴)))⟶(Vtx‘𝐺) ∧ ∀𝑦 ∈ (0..^(#‘(1st𝐴)))((iEdg‘𝐺)‘((1st𝐴)‘𝑦)) = {((2nd𝐴)‘𝑦), ((2nd𝐴)‘(𝑦 + 1))}) ∧ ((1st𝐵) ∈ Word dom (iEdg‘𝐺) ∧ (2nd𝐵):(0...(#‘(1st𝐵)))⟶(Vtx‘𝐺) ∧ ∀𝑦 ∈ (0..^(#‘(1st𝐵)))((iEdg‘𝐺)‘((1st𝐵)‘𝑦)) = {((2nd𝐵)‘𝑦), ((2nd𝐵)‘(𝑦 + 1))})) → (𝑁 = (#‘(1st𝐴)) → (𝑁 = (#‘(1st𝐵)) → (∀𝑦 ∈ (0..^𝑁){((2nd𝐴)‘𝑦), ((2nd𝐴)‘(𝑦 + 1))} = {((2nd𝐵)‘𝑦), ((2nd𝐵)‘(𝑦 + 1))} → ∀𝑦 ∈ (0..^𝑁)((iEdg‘𝐺)‘((1st𝐵)‘𝑦)) = ((iEdg‘𝐺)‘((1st𝐴)‘𝑦)))))))
7341, 46, 72syl2and 500 . . . . . 6 (𝐺 ∈ USPGraph → ((𝐴 ∈ (Walks‘𝐺) ∧ 𝐵 ∈ (Walks‘𝐺)) → (𝑁 = (#‘(1st𝐴)) → (𝑁 = (#‘(1st𝐵)) → (∀𝑦 ∈ (0..^𝑁){((2nd𝐴)‘𝑦), ((2nd𝐴)‘(𝑦 + 1))} = {((2nd𝐵)‘𝑦), ((2nd𝐵)‘(𝑦 + 1))} → ∀𝑦 ∈ (0..^𝑁)((iEdg‘𝐺)‘((1st𝐵)‘𝑦)) = ((iEdg‘𝐺)‘((1st𝐴)‘𝑦)))))))
74733imp1 1277 . . . . 5 (((𝐺 ∈ USPGraph ∧ (𝐴 ∈ (Walks‘𝐺) ∧ 𝐵 ∈ (Walks‘𝐺)) ∧ 𝑁 = (#‘(1st𝐴))) ∧ 𝑁 = (#‘(1st𝐵))) → (∀𝑦 ∈ (0..^𝑁){((2nd𝐴)‘𝑦), ((2nd𝐴)‘(𝑦 + 1))} = {((2nd𝐵)‘𝑦), ((2nd𝐵)‘(𝑦 + 1))} → ∀𝑦 ∈ (0..^𝑁)((iEdg‘𝐺)‘((1st𝐵)‘𝑦)) = ((iEdg‘𝐺)‘((1st𝐴)‘𝑦))))
75 eqcom 2628 . . . . . . 7 (((iEdg‘𝐺)‘((1st𝐵)‘𝑦)) = ((iEdg‘𝐺)‘((1st𝐴)‘𝑦)) ↔ ((iEdg‘𝐺)‘((1st𝐴)‘𝑦)) = ((iEdg‘𝐺)‘((1st𝐵)‘𝑦)))
7636uspgrf1oedg 25974 . . . . . . . . . . . 12 (𝐺 ∈ USPGraph → (iEdg‘𝐺):dom (iEdg‘𝐺)–1-1-onto→(Edg‘𝐺))
77 f1of1 6098 . . . . . . . . . . . 12 ((iEdg‘𝐺):dom (iEdg‘𝐺)–1-1-onto→(Edg‘𝐺) → (iEdg‘𝐺):dom (iEdg‘𝐺)–1-1→(Edg‘𝐺))
7876, 77syl 17 . . . . . . . . . . 11 (𝐺 ∈ USPGraph → (iEdg‘𝐺):dom (iEdg‘𝐺)–1-1→(Edg‘𝐺))
79 eqidd 2622 . . . . . . . . . . . 12 (𝐺 ∈ USPGraph → (iEdg‘𝐺) = (iEdg‘𝐺))
80 eqidd 2622 . . . . . . . . . . . 12 (𝐺 ∈ USPGraph → dom (iEdg‘𝐺) = dom (iEdg‘𝐺))
81 edgval 25854 . . . . . . . . . . . . 13 (𝐺 ∈ USPGraph → (Edg‘𝐺) = ran (iEdg‘𝐺))
8281eqcomd 2627 . . . . . . . . . . . 12 (𝐺 ∈ USPGraph → ran (iEdg‘𝐺) = (Edg‘𝐺))
8379, 80, 82f1eq123d 6093 . . . . . . . . . . 11 (𝐺 ∈ USPGraph → ((iEdg‘𝐺):dom (iEdg‘𝐺)–1-1→ran (iEdg‘𝐺) ↔ (iEdg‘𝐺):dom (iEdg‘𝐺)–1-1→(Edg‘𝐺)))
8478, 83mpbird 247 . . . . . . . . . 10 (𝐺 ∈ USPGraph → (iEdg‘𝐺):dom (iEdg‘𝐺)–1-1→ran (iEdg‘𝐺))
85843ad2ant1 1080 . . . . . . . . 9 ((𝐺 ∈ USPGraph ∧ (𝐴 ∈ (Walks‘𝐺) ∧ 𝐵 ∈ (Walks‘𝐺)) ∧ 𝑁 = (#‘(1st𝐴))) → (iEdg‘𝐺):dom (iEdg‘𝐺)–1-1→ran (iEdg‘𝐺))
8685adantr 481 . . . . . . . 8 (((𝐺 ∈ USPGraph ∧ (𝐴 ∈ (Walks‘𝐺) ∧ 𝐵 ∈ (Walks‘𝐺)) ∧ 𝑁 = (#‘(1st𝐴))) ∧ 𝑁 = (#‘(1st𝐵))) → (iEdg‘𝐺):dom (iEdg‘𝐺)–1-1→ran (iEdg‘𝐺))
8735, 36, 37, 38wlkelwrd 26411 . . . . . . . . . . . . . . 15 (𝐴 ∈ (Walks‘𝐺) → ((1st𝐴) ∈ Word dom (iEdg‘𝐺) ∧ (2nd𝐴):(0...(#‘(1st𝐴)))⟶(Vtx‘𝐺)))
8835, 36, 42, 43wlkelwrd 26411 . . . . . . . . . . . . . . 15 (𝐵 ∈ (Walks‘𝐺) → ((1st𝐵) ∈ Word dom (iEdg‘𝐺) ∧ (2nd𝐵):(0...(#‘(1st𝐵)))⟶(Vtx‘𝐺)))
89 oveq2 6618 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑁 = (#‘(1st𝐴)) → (0..^𝑁) = (0..^(#‘(1st𝐴))))
9089eleq2d 2684 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑁 = (#‘(1st𝐴)) → (𝑦 ∈ (0..^𝑁) ↔ 𝑦 ∈ (0..^(#‘(1st𝐴)))))
91 wrdsymbcl 13264 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((1st𝐴) ∈ Word dom (iEdg‘𝐺) ∧ 𝑦 ∈ (0..^(#‘(1st𝐴)))) → ((1st𝐴)‘𝑦) ∈ dom (iEdg‘𝐺))
9291expcom 451 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 ∈ (0..^(#‘(1st𝐴))) → ((1st𝐴) ∈ Word dom (iEdg‘𝐺) → ((1st𝐴)‘𝑦) ∈ dom (iEdg‘𝐺)))
9390, 92syl6bi 243 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑁 = (#‘(1st𝐴)) → (𝑦 ∈ (0..^𝑁) → ((1st𝐴) ∈ Word dom (iEdg‘𝐺) → ((1st𝐴)‘𝑦) ∈ dom (iEdg‘𝐺))))
9493adantr 481 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑁 = (#‘(1st𝐴)) ∧ 𝑁 = (#‘(1st𝐵))) → (𝑦 ∈ (0..^𝑁) → ((1st𝐴) ∈ Word dom (iEdg‘𝐺) → ((1st𝐴)‘𝑦) ∈ dom (iEdg‘𝐺))))
9594imp 445 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑁 = (#‘(1st𝐴)) ∧ 𝑁 = (#‘(1st𝐵))) ∧ 𝑦 ∈ (0..^𝑁)) → ((1st𝐴) ∈ Word dom (iEdg‘𝐺) → ((1st𝐴)‘𝑦) ∈ dom (iEdg‘𝐺)))
9695com12 32 . . . . . . . . . . . . . . . . . . . . . 22 ((1st𝐴) ∈ Word dom (iEdg‘𝐺) → (((𝑁 = (#‘(1st𝐴)) ∧ 𝑁 = (#‘(1st𝐵))) ∧ 𝑦 ∈ (0..^𝑁)) → ((1st𝐴)‘𝑦) ∈ dom (iEdg‘𝐺)))
9796adantl 482 . . . . . . . . . . . . . . . . . . . . 21 (((1st𝐵) ∈ Word dom (iEdg‘𝐺) ∧ (1st𝐴) ∈ Word dom (iEdg‘𝐺)) → (((𝑁 = (#‘(1st𝐴)) ∧ 𝑁 = (#‘(1st𝐵))) ∧ 𝑦 ∈ (0..^𝑁)) → ((1st𝐴)‘𝑦) ∈ dom (iEdg‘𝐺)))
98 oveq2 6618 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑁 = (#‘(1st𝐵)) → (0..^𝑁) = (0..^(#‘(1st𝐵))))
9998eleq2d 2684 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑁 = (#‘(1st𝐵)) → (𝑦 ∈ (0..^𝑁) ↔ 𝑦 ∈ (0..^(#‘(1st𝐵)))))
100 wrdsymbcl 13264 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((1st𝐵) ∈ Word dom (iEdg‘𝐺) ∧ 𝑦 ∈ (0..^(#‘(1st𝐵)))) → ((1st𝐵)‘𝑦) ∈ dom (iEdg‘𝐺))
101100expcom 451 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 ∈ (0..^(#‘(1st𝐵))) → ((1st𝐵) ∈ Word dom (iEdg‘𝐺) → ((1st𝐵)‘𝑦) ∈ dom (iEdg‘𝐺)))
10299, 101syl6bi 243 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑁 = (#‘(1st𝐵)) → (𝑦 ∈ (0..^𝑁) → ((1st𝐵) ∈ Word dom (iEdg‘𝐺) → ((1st𝐵)‘𝑦) ∈ dom (iEdg‘𝐺))))
103102adantl 482 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑁 = (#‘(1st𝐴)) ∧ 𝑁 = (#‘(1st𝐵))) → (𝑦 ∈ (0..^𝑁) → ((1st𝐵) ∈ Word dom (iEdg‘𝐺) → ((1st𝐵)‘𝑦) ∈ dom (iEdg‘𝐺))))
104103imp 445 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑁 = (#‘(1st𝐴)) ∧ 𝑁 = (#‘(1st𝐵))) ∧ 𝑦 ∈ (0..^𝑁)) → ((1st𝐵) ∈ Word dom (iEdg‘𝐺) → ((1st𝐵)‘𝑦) ∈ dom (iEdg‘𝐺)))
105104com12 32 . . . . . . . . . . . . . . . . . . . . . 22 ((1st𝐵) ∈ Word dom (iEdg‘𝐺) → (((𝑁 = (#‘(1st𝐴)) ∧ 𝑁 = (#‘(1st𝐵))) ∧ 𝑦 ∈ (0..^𝑁)) → ((1st𝐵)‘𝑦) ∈ dom (iEdg‘𝐺)))
106105adantr 481 . . . . . . . . . . . . . . . . . . . . 21 (((1st𝐵) ∈ Word dom (iEdg‘𝐺) ∧ (1st𝐴) ∈ Word dom (iEdg‘𝐺)) → (((𝑁 = (#‘(1st𝐴)) ∧ 𝑁 = (#‘(1st𝐵))) ∧ 𝑦 ∈ (0..^𝑁)) → ((1st𝐵)‘𝑦) ∈ dom (iEdg‘𝐺)))
10797, 106jcad 555 . . . . . . . . . . . . . . . . . . . 20 (((1st𝐵) ∈ Word dom (iEdg‘𝐺) ∧ (1st𝐴) ∈ Word dom (iEdg‘𝐺)) → (((𝑁 = (#‘(1st𝐴)) ∧ 𝑁 = (#‘(1st𝐵))) ∧ 𝑦 ∈ (0..^𝑁)) → (((1st𝐴)‘𝑦) ∈ dom (iEdg‘𝐺) ∧ ((1st𝐵)‘𝑦) ∈ dom (iEdg‘𝐺))))
108107ex 450 . . . . . . . . . . . . . . . . . . 19 ((1st𝐵) ∈ Word dom (iEdg‘𝐺) → ((1st𝐴) ∈ Word dom (iEdg‘𝐺) → (((𝑁 = (#‘(1st𝐴)) ∧ 𝑁 = (#‘(1st𝐵))) ∧ 𝑦 ∈ (0..^𝑁)) → (((1st𝐴)‘𝑦) ∈ dom (iEdg‘𝐺) ∧ ((1st𝐵)‘𝑦) ∈ dom (iEdg‘𝐺)))))
109108adantr 481 . . . . . . . . . . . . . . . . . 18 (((1st𝐵) ∈ Word dom (iEdg‘𝐺) ∧ (2nd𝐵):(0...(#‘(1st𝐵)))⟶(Vtx‘𝐺)) → ((1st𝐴) ∈ Word dom (iEdg‘𝐺) → (((𝑁 = (#‘(1st𝐴)) ∧ 𝑁 = (#‘(1st𝐵))) ∧ 𝑦 ∈ (0..^𝑁)) → (((1st𝐴)‘𝑦) ∈ dom (iEdg‘𝐺) ∧ ((1st𝐵)‘𝑦) ∈ dom (iEdg‘𝐺)))))
110109com12 32 . . . . . . . . . . . . . . . . 17 ((1st𝐴) ∈ Word dom (iEdg‘𝐺) → (((1st𝐵) ∈ Word dom (iEdg‘𝐺) ∧ (2nd𝐵):(0...(#‘(1st𝐵)))⟶(Vtx‘𝐺)) → (((𝑁 = (#‘(1st𝐴)) ∧ 𝑁 = (#‘(1st𝐵))) ∧ 𝑦 ∈ (0..^𝑁)) → (((1st𝐴)‘𝑦) ∈ dom (iEdg‘𝐺) ∧ ((1st𝐵)‘𝑦) ∈ dom (iEdg‘𝐺)))))
111110adantr 481 . . . . . . . . . . . . . . . 16 (((1st𝐴) ∈ Word dom (iEdg‘𝐺) ∧ (2nd𝐴):(0...(#‘(1st𝐴)))⟶(Vtx‘𝐺)) → (((1st𝐵) ∈ Word dom (iEdg‘𝐺) ∧ (2nd𝐵):(0...(#‘(1st𝐵)))⟶(Vtx‘𝐺)) → (((𝑁 = (#‘(1st𝐴)) ∧ 𝑁 = (#‘(1st𝐵))) ∧ 𝑦 ∈ (0..^𝑁)) → (((1st𝐴)‘𝑦) ∈ dom (iEdg‘𝐺) ∧ ((1st𝐵)‘𝑦) ∈ dom (iEdg‘𝐺)))))
112111imp 445 . . . . . . . . . . . . . . 15 ((((1st𝐴) ∈ Word dom (iEdg‘𝐺) ∧ (2nd𝐴):(0...(#‘(1st𝐴)))⟶(Vtx‘𝐺)) ∧ ((1st𝐵) ∈ Word dom (iEdg‘𝐺) ∧ (2nd𝐵):(0...(#‘(1st𝐵)))⟶(Vtx‘𝐺))) → (((𝑁 = (#‘(1st𝐴)) ∧ 𝑁 = (#‘(1st𝐵))) ∧ 𝑦 ∈ (0..^𝑁)) → (((1st𝐴)‘𝑦) ∈ dom (iEdg‘𝐺) ∧ ((1st𝐵)‘𝑦) ∈ dom (iEdg‘𝐺))))
11387, 88, 112syl2an 494 . . . . . . . . . . . . . 14 ((𝐴 ∈ (Walks‘𝐺) ∧ 𝐵 ∈ (Walks‘𝐺)) → (((𝑁 = (#‘(1st𝐴)) ∧ 𝑁 = (#‘(1st𝐵))) ∧ 𝑦 ∈ (0..^𝑁)) → (((1st𝐴)‘𝑦) ∈ dom (iEdg‘𝐺) ∧ ((1st𝐵)‘𝑦) ∈ dom (iEdg‘𝐺))))
114113expd 452 . . . . . . . . . . . . 13 ((𝐴 ∈ (Walks‘𝐺) ∧ 𝐵 ∈ (Walks‘𝐺)) → ((𝑁 = (#‘(1st𝐴)) ∧ 𝑁 = (#‘(1st𝐵))) → (𝑦 ∈ (0..^𝑁) → (((1st𝐴)‘𝑦) ∈ dom (iEdg‘𝐺) ∧ ((1st𝐵)‘𝑦) ∈ dom (iEdg‘𝐺)))))
115114expd 452 . . . . . . . . . . . 12 ((𝐴 ∈ (Walks‘𝐺) ∧ 𝐵 ∈ (Walks‘𝐺)) → (𝑁 = (#‘(1st𝐴)) → (𝑁 = (#‘(1st𝐵)) → (𝑦 ∈ (0..^𝑁) → (((1st𝐴)‘𝑦) ∈ dom (iEdg‘𝐺) ∧ ((1st𝐵)‘𝑦) ∈ dom (iEdg‘𝐺))))))
116115imp 445 . . . . . . . . . . 11 (((𝐴 ∈ (Walks‘𝐺) ∧ 𝐵 ∈ (Walks‘𝐺)) ∧ 𝑁 = (#‘(1st𝐴))) → (𝑁 = (#‘(1st𝐵)) → (𝑦 ∈ (0..^𝑁) → (((1st𝐴)‘𝑦) ∈ dom (iEdg‘𝐺) ∧ ((1st𝐵)‘𝑦) ∈ dom (iEdg‘𝐺)))))
1171163adant1 1077 . . . . . . . . . 10 ((𝐺 ∈ USPGraph ∧ (𝐴 ∈ (Walks‘𝐺) ∧ 𝐵 ∈ (Walks‘𝐺)) ∧ 𝑁 = (#‘(1st𝐴))) → (𝑁 = (#‘(1st𝐵)) → (𝑦 ∈ (0..^𝑁) → (((1st𝐴)‘𝑦) ∈ dom (iEdg‘𝐺) ∧ ((1st𝐵)‘𝑦) ∈ dom (iEdg‘𝐺)))))
118117imp 445 . . . . . . . . 9 (((𝐺 ∈ USPGraph ∧ (𝐴 ∈ (Walks‘𝐺) ∧ 𝐵 ∈ (Walks‘𝐺)) ∧ 𝑁 = (#‘(1st𝐴))) ∧ 𝑁 = (#‘(1st𝐵))) → (𝑦 ∈ (0..^𝑁) → (((1st𝐴)‘𝑦) ∈ dom (iEdg‘𝐺) ∧ ((1st𝐵)‘𝑦) ∈ dom (iEdg‘𝐺))))
119118imp 445 . . . . . . . 8 ((((𝐺 ∈ USPGraph ∧ (𝐴 ∈ (Walks‘𝐺) ∧ 𝐵 ∈ (Walks‘𝐺)) ∧ 𝑁 = (#‘(1st𝐴))) ∧ 𝑁 = (#‘(1st𝐵))) ∧ 𝑦 ∈ (0..^𝑁)) → (((1st𝐴)‘𝑦) ∈ dom (iEdg‘𝐺) ∧ ((1st𝐵)‘𝑦) ∈ dom (iEdg‘𝐺)))
120 f1veqaeq 6474 . . . . . . . 8 (((iEdg‘𝐺):dom (iEdg‘𝐺)–1-1→ran (iEdg‘𝐺) ∧ (((1st𝐴)‘𝑦) ∈ dom (iEdg‘𝐺) ∧ ((1st𝐵)‘𝑦) ∈ dom (iEdg‘𝐺))) → (((iEdg‘𝐺)‘((1st𝐴)‘𝑦)) = ((iEdg‘𝐺)‘((1st𝐵)‘𝑦)) → ((1st𝐴)‘𝑦) = ((1st𝐵)‘𝑦)))
12186, 119, 120syl2an2r 875 . . . . . . 7 ((((𝐺 ∈ USPGraph ∧ (𝐴 ∈ (Walks‘𝐺) ∧ 𝐵 ∈ (Walks‘𝐺)) ∧ 𝑁 = (#‘(1st𝐴))) ∧ 𝑁 = (#‘(1st𝐵))) ∧ 𝑦 ∈ (0..^𝑁)) → (((iEdg‘𝐺)‘((1st𝐴)‘𝑦)) = ((iEdg‘𝐺)‘((1st𝐵)‘𝑦)) → ((1st𝐴)‘𝑦) = ((1st𝐵)‘𝑦)))
12275, 121syl5bi 232 . . . . . 6 ((((𝐺 ∈ USPGraph ∧ (𝐴 ∈ (Walks‘𝐺) ∧ 𝐵 ∈ (Walks‘𝐺)) ∧ 𝑁 = (#‘(1st𝐴))) ∧ 𝑁 = (#‘(1st𝐵))) ∧ 𝑦 ∈ (0..^𝑁)) → (((iEdg‘𝐺)‘((1st𝐵)‘𝑦)) = ((iEdg‘𝐺)‘((1st𝐴)‘𝑦)) → ((1st𝐴)‘𝑦) = ((1st𝐵)‘𝑦)))
123122ralimdva 2957 . . . . 5 (((𝐺 ∈ USPGraph ∧ (𝐴 ∈ (Walks‘𝐺) ∧ 𝐵 ∈ (Walks‘𝐺)) ∧ 𝑁 = (#‘(1st𝐴))) ∧ 𝑁 = (#‘(1st𝐵))) → (∀𝑦 ∈ (0..^𝑁)((iEdg‘𝐺)‘((1st𝐵)‘𝑦)) = ((iEdg‘𝐺)‘((1st𝐴)‘𝑦)) → ∀𝑦 ∈ (0..^𝑁)((1st𝐴)‘𝑦) = ((1st𝐵)‘𝑦)))
12433, 74, 1233syld 60 . . . 4 (((𝐺 ∈ USPGraph ∧ (𝐴 ∈ (Walks‘𝐺) ∧ 𝐵 ∈ (Walks‘𝐺)) ∧ 𝑁 = (#‘(1st𝐴))) ∧ 𝑁 = (#‘(1st𝐵))) → (∀𝑦 ∈ (0...𝑁)((2nd𝐴)‘𝑦) = ((2nd𝐵)‘𝑦) → ∀𝑦 ∈ (0..^𝑁)((1st𝐴)‘𝑦) = ((1st𝐵)‘𝑦)))
125124expimpd 628 . . 3 ((𝐺 ∈ USPGraph ∧ (𝐴 ∈ (Walks‘𝐺) ∧ 𝐵 ∈ (Walks‘𝐺)) ∧ 𝑁 = (#‘(1st𝐴))) → ((𝑁 = (#‘(1st𝐵)) ∧ ∀𝑦 ∈ (0...𝑁)((2nd𝐴)‘𝑦) = ((2nd𝐵)‘𝑦)) → ∀𝑦 ∈ (0..^𝑁)((1st𝐴)‘𝑦) = ((1st𝐵)‘𝑦)))
126125pm4.71d 665 . 2 ((𝐺 ∈ USPGraph ∧ (𝐴 ∈ (Walks‘𝐺) ∧ 𝐵 ∈ (Walks‘𝐺)) ∧ 𝑁 = (#‘(1st𝐴))) → ((𝑁 = (#‘(1st𝐵)) ∧ ∀𝑦 ∈ (0...𝑁)((2nd𝐴)‘𝑦) = ((2nd𝐵)‘𝑦)) ↔ ((𝑁 = (#‘(1st𝐵)) ∧ ∀𝑦 ∈ (0...𝑁)((2nd𝐴)‘𝑦) = ((2nd𝐵)‘𝑦)) ∧ ∀𝑦 ∈ (0..^𝑁)((1st𝐴)‘𝑦) = ((1st𝐵)‘𝑦))))
1272, 5, 1263bitr4d 300 1 ((𝐺 ∈ USPGraph ∧ (𝐴 ∈ (Walks‘𝐺) ∧ 𝐵 ∈ (Walks‘𝐺)) ∧ 𝑁 = (#‘(1st𝐴))) → (𝐴 = 𝐵 ↔ (𝑁 = (#‘(1st𝐵)) ∧ ∀𝑦 ∈ (0...𝑁)((2nd𝐴)‘𝑦) = ((2nd𝐵)‘𝑦))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384  w3a 1036   = wceq 1480  wcel 1987  wral 2907  wss 3559  {cpr 4155  dom cdm 5079  ran crn 5080  wf 5848  1-1wf1 5849  1-1-ontowf1o 5851  cfv 5852  (class class class)co 6610  1st c1st 7118  2nd c2nd 7119  0cc0 9887  1c1 9888   + caddc 9890  ...cfz 12275  ..^cfzo 12413  #chash 13064  Word cword 13237  Vtxcvtx 25787  iEdgciedg 25788  Edgcedg 25852   UPGraph cupgr 25884   USPGraph cuspgr 25949  Walkscwlks 26375
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4736  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6909  ax-cnex 9943  ax-resscn 9944  ax-1cn 9945  ax-icn 9946  ax-addcl 9947  ax-addrcl 9948  ax-mulcl 9949  ax-mulrcl 9950  ax-mulcom 9951  ax-addass 9952  ax-mulass 9953  ax-distr 9954  ax-i2m1 9955  ax-1ne0 9956  ax-1rid 9957  ax-rnegex 9958  ax-rrecex 9959  ax-cnre 9960  ax-pre-lttri 9961  ax-pre-lttrn 9962  ax-pre-ltadd 9963  ax-pre-mulgt0 9964
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-ifp 1012  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-rab 2916  df-v 3191  df-sbc 3422  df-csb 3519  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-pss 3575  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-tp 4158  df-op 4160  df-uni 4408  df-int 4446  df-iun 4492  df-br 4619  df-opab 4679  df-mpt 4680  df-tr 4718  df-eprel 4990  df-id 4994  df-po 5000  df-so 5001  df-fr 5038  df-we 5040  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-pred 5644  df-ord 5690  df-on 5691  df-lim 5692  df-suc 5693  df-iota 5815  df-fun 5854  df-fn 5855  df-f 5856  df-f1 5857  df-fo 5858  df-f1o 5859  df-fv 5860  df-riota 6571  df-ov 6613  df-oprab 6614  df-mpt2 6615  df-om 7020  df-1st 7120  df-2nd 7121  df-wrecs 7359  df-recs 7420  df-rdg 7458  df-1o 7512  df-2o 7513  df-oadd 7516  df-er 7694  df-map 7811  df-pm 7812  df-en 7907  df-dom 7908  df-sdom 7909  df-fin 7910  df-card 8716  df-cda 8941  df-pnf 10027  df-mnf 10028  df-xr 10029  df-ltxr 10030  df-le 10031  df-sub 10219  df-neg 10220  df-nn 10972  df-2 11030  df-n0 11244  df-xnn0 11315  df-z 11329  df-uz 11639  df-fz 12276  df-fzo 12414  df-hash 13065  df-word 13245  df-edg 25853  df-uhgr 25862  df-upgr 25886  df-uspgr 25951  df-wlks 26378
This theorem is referenced by:  uspgr2wlkeq2  26425  clwlksf1clwwlk  26848
  Copyright terms: Public domain W3C validator