| Step | Hyp | Ref
| Expression |
| 1 | | 3anan32 1097 |
. . 3
⊢ ((𝑁 =
(♯‘(1st ‘𝐵)) ∧ ∀𝑦 ∈ (0..^𝑁)((1st ‘𝐴)‘𝑦) = ((1st ‘𝐵)‘𝑦) ∧ ∀𝑦 ∈ (0...𝑁)((2nd ‘𝐴)‘𝑦) = ((2nd ‘𝐵)‘𝑦)) ↔ ((𝑁 = (♯‘(1st
‘𝐵)) ∧
∀𝑦 ∈ (0...𝑁)((2nd ‘𝐴)‘𝑦) = ((2nd ‘𝐵)‘𝑦)) ∧ ∀𝑦 ∈ (0..^𝑁)((1st ‘𝐴)‘𝑦) = ((1st ‘𝐵)‘𝑦))) |
| 2 | 1 | a1i 11 |
. 2
⊢ ((𝐺 ∈ USPGraph ∧ (𝐴 ∈ (Walks‘𝐺) ∧ 𝐵 ∈ (Walks‘𝐺)) ∧ 𝑁 = (♯‘(1st
‘𝐴))) → ((𝑁 =
(♯‘(1st ‘𝐵)) ∧ ∀𝑦 ∈ (0..^𝑁)((1st ‘𝐴)‘𝑦) = ((1st ‘𝐵)‘𝑦) ∧ ∀𝑦 ∈ (0...𝑁)((2nd ‘𝐴)‘𝑦) = ((2nd ‘𝐵)‘𝑦)) ↔ ((𝑁 = (♯‘(1st
‘𝐵)) ∧
∀𝑦 ∈ (0...𝑁)((2nd ‘𝐴)‘𝑦) = ((2nd ‘𝐵)‘𝑦)) ∧ ∀𝑦 ∈ (0..^𝑁)((1st ‘𝐴)‘𝑦) = ((1st ‘𝐵)‘𝑦)))) |
| 3 | | wlkeq 29652 |
. . . 4
⊢ ((𝐴 ∈ (Walks‘𝐺) ∧ 𝐵 ∈ (Walks‘𝐺) ∧ 𝑁 = (♯‘(1st
‘𝐴))) → (𝐴 = 𝐵 ↔ (𝑁 = (♯‘(1st
‘𝐵)) ∧
∀𝑦 ∈ (0..^𝑁)((1st ‘𝐴)‘𝑦) = ((1st ‘𝐵)‘𝑦) ∧ ∀𝑦 ∈ (0...𝑁)((2nd ‘𝐴)‘𝑦) = ((2nd ‘𝐵)‘𝑦)))) |
| 4 | 3 | 3expa 1119 |
. . 3
⊢ (((𝐴 ∈ (Walks‘𝐺) ∧ 𝐵 ∈ (Walks‘𝐺)) ∧ 𝑁 = (♯‘(1st
‘𝐴))) → (𝐴 = 𝐵 ↔ (𝑁 = (♯‘(1st
‘𝐵)) ∧
∀𝑦 ∈ (0..^𝑁)((1st ‘𝐴)‘𝑦) = ((1st ‘𝐵)‘𝑦) ∧ ∀𝑦 ∈ (0...𝑁)((2nd ‘𝐴)‘𝑦) = ((2nd ‘𝐵)‘𝑦)))) |
| 5 | 4 | 3adant1 1131 |
. 2
⊢ ((𝐺 ∈ USPGraph ∧ (𝐴 ∈ (Walks‘𝐺) ∧ 𝐵 ∈ (Walks‘𝐺)) ∧ 𝑁 = (♯‘(1st
‘𝐴))) → (𝐴 = 𝐵 ↔ (𝑁 = (♯‘(1st
‘𝐵)) ∧
∀𝑦 ∈ (0..^𝑁)((1st ‘𝐴)‘𝑦) = ((1st ‘𝐵)‘𝑦) ∧ ∀𝑦 ∈ (0...𝑁)((2nd ‘𝐴)‘𝑦) = ((2nd ‘𝐵)‘𝑦)))) |
| 6 | | fzofzp1 13803 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (0..^𝑁) → (𝑥 + 1) ∈ (0...𝑁)) |
| 7 | 6 | adantl 481 |
. . . . . . . . . . 11
⊢ ((((𝐺 ∈ USPGraph ∧ (𝐴 ∈ (Walks‘𝐺) ∧ 𝐵 ∈ (Walks‘𝐺)) ∧ 𝑁 = (♯‘(1st
‘𝐴))) ∧ 𝑁 =
(♯‘(1st ‘𝐵))) ∧ 𝑥 ∈ (0..^𝑁)) → (𝑥 + 1) ∈ (0...𝑁)) |
| 8 | | fveq2 6906 |
. . . . . . . . . . . . 13
⊢ (𝑦 = (𝑥 + 1) → ((2nd ‘𝐴)‘𝑦) = ((2nd ‘𝐴)‘(𝑥 + 1))) |
| 9 | | fveq2 6906 |
. . . . . . . . . . . . 13
⊢ (𝑦 = (𝑥 + 1) → ((2nd ‘𝐵)‘𝑦) = ((2nd ‘𝐵)‘(𝑥 + 1))) |
| 10 | 8, 9 | eqeq12d 2753 |
. . . . . . . . . . . 12
⊢ (𝑦 = (𝑥 + 1) → (((2nd ‘𝐴)‘𝑦) = ((2nd ‘𝐵)‘𝑦) ↔ ((2nd ‘𝐴)‘(𝑥 + 1)) = ((2nd ‘𝐵)‘(𝑥 + 1)))) |
| 11 | 10 | adantl 481 |
. . . . . . . . . . 11
⊢
(((((𝐺 ∈
USPGraph ∧ (𝐴 ∈
(Walks‘𝐺) ∧ 𝐵 ∈ (Walks‘𝐺)) ∧ 𝑁 = (♯‘(1st
‘𝐴))) ∧ 𝑁 =
(♯‘(1st ‘𝐵))) ∧ 𝑥 ∈ (0..^𝑁)) ∧ 𝑦 = (𝑥 + 1)) → (((2nd ‘𝐴)‘𝑦) = ((2nd ‘𝐵)‘𝑦) ↔ ((2nd ‘𝐴)‘(𝑥 + 1)) = ((2nd ‘𝐵)‘(𝑥 + 1)))) |
| 12 | 7, 11 | rspcdv 3614 |
. . . . . . . . . 10
⊢ ((((𝐺 ∈ USPGraph ∧ (𝐴 ∈ (Walks‘𝐺) ∧ 𝐵 ∈ (Walks‘𝐺)) ∧ 𝑁 = (♯‘(1st
‘𝐴))) ∧ 𝑁 =
(♯‘(1st ‘𝐵))) ∧ 𝑥 ∈ (0..^𝑁)) → (∀𝑦 ∈ (0...𝑁)((2nd ‘𝐴)‘𝑦) = ((2nd ‘𝐵)‘𝑦) → ((2nd ‘𝐴)‘(𝑥 + 1)) = ((2nd ‘𝐵)‘(𝑥 + 1)))) |
| 13 | 12 | impancom 451 |
. . . . . . . . 9
⊢ ((((𝐺 ∈ USPGraph ∧ (𝐴 ∈ (Walks‘𝐺) ∧ 𝐵 ∈ (Walks‘𝐺)) ∧ 𝑁 = (♯‘(1st
‘𝐴))) ∧ 𝑁 =
(♯‘(1st ‘𝐵))) ∧ ∀𝑦 ∈ (0...𝑁)((2nd ‘𝐴)‘𝑦) = ((2nd ‘𝐵)‘𝑦)) → (𝑥 ∈ (0..^𝑁) → ((2nd ‘𝐴)‘(𝑥 + 1)) = ((2nd ‘𝐵)‘(𝑥 + 1)))) |
| 14 | 13 | ralrimiv 3145 |
. . . . . . . 8
⊢ ((((𝐺 ∈ USPGraph ∧ (𝐴 ∈ (Walks‘𝐺) ∧ 𝐵 ∈ (Walks‘𝐺)) ∧ 𝑁 = (♯‘(1st
‘𝐴))) ∧ 𝑁 =
(♯‘(1st ‘𝐵))) ∧ ∀𝑦 ∈ (0...𝑁)((2nd ‘𝐴)‘𝑦) = ((2nd ‘𝐵)‘𝑦)) → ∀𝑥 ∈ (0..^𝑁)((2nd ‘𝐴)‘(𝑥 + 1)) = ((2nd ‘𝐵)‘(𝑥 + 1))) |
| 15 | | fvoveq1 7454 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑥 → ((2nd ‘𝐴)‘(𝑦 + 1)) = ((2nd ‘𝐴)‘(𝑥 + 1))) |
| 16 | | fvoveq1 7454 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑥 → ((2nd ‘𝐵)‘(𝑦 + 1)) = ((2nd ‘𝐵)‘(𝑥 + 1))) |
| 17 | 15, 16 | eqeq12d 2753 |
. . . . . . . . 9
⊢ (𝑦 = 𝑥 → (((2nd ‘𝐴)‘(𝑦 + 1)) = ((2nd ‘𝐵)‘(𝑦 + 1)) ↔ ((2nd ‘𝐴)‘(𝑥 + 1)) = ((2nd ‘𝐵)‘(𝑥 + 1)))) |
| 18 | 17 | cbvralvw 3237 |
. . . . . . . 8
⊢
(∀𝑦 ∈
(0..^𝑁)((2nd
‘𝐴)‘(𝑦 + 1)) = ((2nd
‘𝐵)‘(𝑦 + 1)) ↔ ∀𝑥 ∈ (0..^𝑁)((2nd ‘𝐴)‘(𝑥 + 1)) = ((2nd ‘𝐵)‘(𝑥 + 1))) |
| 19 | 14, 18 | sylibr 234 |
. . . . . . 7
⊢ ((((𝐺 ∈ USPGraph ∧ (𝐴 ∈ (Walks‘𝐺) ∧ 𝐵 ∈ (Walks‘𝐺)) ∧ 𝑁 = (♯‘(1st
‘𝐴))) ∧ 𝑁 =
(♯‘(1st ‘𝐵))) ∧ ∀𝑦 ∈ (0...𝑁)((2nd ‘𝐴)‘𝑦) = ((2nd ‘𝐵)‘𝑦)) → ∀𝑦 ∈ (0..^𝑁)((2nd ‘𝐴)‘(𝑦 + 1)) = ((2nd ‘𝐵)‘(𝑦 + 1))) |
| 20 | | fzossfz 13718 |
. . . . . . . . . 10
⊢
(0..^𝑁) ⊆
(0...𝑁) |
| 21 | | ssralv 4052 |
. . . . . . . . . 10
⊢
((0..^𝑁) ⊆
(0...𝑁) →
(∀𝑦 ∈
(0...𝑁)((2nd
‘𝐴)‘𝑦) = ((2nd
‘𝐵)‘𝑦) → ∀𝑦 ∈ (0..^𝑁)((2nd ‘𝐴)‘𝑦) = ((2nd ‘𝐵)‘𝑦))) |
| 22 | 20, 21 | mp1i 13 |
. . . . . . . . 9
⊢ (((𝐺 ∈ USPGraph ∧ (𝐴 ∈ (Walks‘𝐺) ∧ 𝐵 ∈ (Walks‘𝐺)) ∧ 𝑁 = (♯‘(1st
‘𝐴))) ∧ 𝑁 =
(♯‘(1st ‘𝐵))) → (∀𝑦 ∈ (0...𝑁)((2nd ‘𝐴)‘𝑦) = ((2nd ‘𝐵)‘𝑦) → ∀𝑦 ∈ (0..^𝑁)((2nd ‘𝐴)‘𝑦) = ((2nd ‘𝐵)‘𝑦))) |
| 23 | | r19.26 3111 |
. . . . . . . . . . 11
⊢
(∀𝑦 ∈
(0..^𝑁)(((2nd
‘𝐴)‘𝑦) = ((2nd
‘𝐵)‘𝑦) ∧ ((2nd
‘𝐴)‘(𝑦 + 1)) = ((2nd
‘𝐵)‘(𝑦 + 1))) ↔ (∀𝑦 ∈ (0..^𝑁)((2nd ‘𝐴)‘𝑦) = ((2nd ‘𝐵)‘𝑦) ∧ ∀𝑦 ∈ (0..^𝑁)((2nd ‘𝐴)‘(𝑦 + 1)) = ((2nd ‘𝐵)‘(𝑦 + 1)))) |
| 24 | | preq12 4735 |
. . . . . . . . . . . . 13
⊢
((((2nd ‘𝐴)‘𝑦) = ((2nd ‘𝐵)‘𝑦) ∧ ((2nd ‘𝐴)‘(𝑦 + 1)) = ((2nd ‘𝐵)‘(𝑦 + 1))) → {((2nd ‘𝐴)‘𝑦), ((2nd ‘𝐴)‘(𝑦 + 1))} = {((2nd ‘𝐵)‘𝑦), ((2nd ‘𝐵)‘(𝑦 + 1))}) |
| 25 | 24 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((𝐺 ∈ USPGraph ∧ (𝐴 ∈ (Walks‘𝐺) ∧ 𝐵 ∈ (Walks‘𝐺)) ∧ 𝑁 = (♯‘(1st
‘𝐴))) ∧ 𝑁 =
(♯‘(1st ‘𝐵))) → ((((2nd ‘𝐴)‘𝑦) = ((2nd ‘𝐵)‘𝑦) ∧ ((2nd ‘𝐴)‘(𝑦 + 1)) = ((2nd ‘𝐵)‘(𝑦 + 1))) → {((2nd ‘𝐴)‘𝑦), ((2nd ‘𝐴)‘(𝑦 + 1))} = {((2nd ‘𝐵)‘𝑦), ((2nd ‘𝐵)‘(𝑦 + 1))})) |
| 26 | 25 | ralimdv 3169 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ USPGraph ∧ (𝐴 ∈ (Walks‘𝐺) ∧ 𝐵 ∈ (Walks‘𝐺)) ∧ 𝑁 = (♯‘(1st
‘𝐴))) ∧ 𝑁 =
(♯‘(1st ‘𝐵))) → (∀𝑦 ∈ (0..^𝑁)(((2nd ‘𝐴)‘𝑦) = ((2nd ‘𝐵)‘𝑦) ∧ ((2nd ‘𝐴)‘(𝑦 + 1)) = ((2nd ‘𝐵)‘(𝑦 + 1))) → ∀𝑦 ∈ (0..^𝑁){((2nd ‘𝐴)‘𝑦), ((2nd ‘𝐴)‘(𝑦 + 1))} = {((2nd ‘𝐵)‘𝑦), ((2nd ‘𝐵)‘(𝑦 + 1))})) |
| 27 | 23, 26 | biimtrrid 243 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ USPGraph ∧ (𝐴 ∈ (Walks‘𝐺) ∧ 𝐵 ∈ (Walks‘𝐺)) ∧ 𝑁 = (♯‘(1st
‘𝐴))) ∧ 𝑁 =
(♯‘(1st ‘𝐵))) → ((∀𝑦 ∈ (0..^𝑁)((2nd ‘𝐴)‘𝑦) = ((2nd ‘𝐵)‘𝑦) ∧ ∀𝑦 ∈ (0..^𝑁)((2nd ‘𝐴)‘(𝑦 + 1)) = ((2nd ‘𝐵)‘(𝑦 + 1))) → ∀𝑦 ∈ (0..^𝑁){((2nd ‘𝐴)‘𝑦), ((2nd ‘𝐴)‘(𝑦 + 1))} = {((2nd ‘𝐵)‘𝑦), ((2nd ‘𝐵)‘(𝑦 + 1))})) |
| 28 | 27 | expd 415 |
. . . . . . . . 9
⊢ (((𝐺 ∈ USPGraph ∧ (𝐴 ∈ (Walks‘𝐺) ∧ 𝐵 ∈ (Walks‘𝐺)) ∧ 𝑁 = (♯‘(1st
‘𝐴))) ∧ 𝑁 =
(♯‘(1st ‘𝐵))) → (∀𝑦 ∈ (0..^𝑁)((2nd ‘𝐴)‘𝑦) = ((2nd ‘𝐵)‘𝑦) → (∀𝑦 ∈ (0..^𝑁)((2nd ‘𝐴)‘(𝑦 + 1)) = ((2nd ‘𝐵)‘(𝑦 + 1)) → ∀𝑦 ∈ (0..^𝑁){((2nd ‘𝐴)‘𝑦), ((2nd ‘𝐴)‘(𝑦 + 1))} = {((2nd ‘𝐵)‘𝑦), ((2nd ‘𝐵)‘(𝑦 + 1))}))) |
| 29 | 22, 28 | syld 47 |
. . . . . . . 8
⊢ (((𝐺 ∈ USPGraph ∧ (𝐴 ∈ (Walks‘𝐺) ∧ 𝐵 ∈ (Walks‘𝐺)) ∧ 𝑁 = (♯‘(1st
‘𝐴))) ∧ 𝑁 =
(♯‘(1st ‘𝐵))) → (∀𝑦 ∈ (0...𝑁)((2nd ‘𝐴)‘𝑦) = ((2nd ‘𝐵)‘𝑦) → (∀𝑦 ∈ (0..^𝑁)((2nd ‘𝐴)‘(𝑦 + 1)) = ((2nd ‘𝐵)‘(𝑦 + 1)) → ∀𝑦 ∈ (0..^𝑁){((2nd ‘𝐴)‘𝑦), ((2nd ‘𝐴)‘(𝑦 + 1))} = {((2nd ‘𝐵)‘𝑦), ((2nd ‘𝐵)‘(𝑦 + 1))}))) |
| 30 | 29 | imp 406 |
. . . . . . 7
⊢ ((((𝐺 ∈ USPGraph ∧ (𝐴 ∈ (Walks‘𝐺) ∧ 𝐵 ∈ (Walks‘𝐺)) ∧ 𝑁 = (♯‘(1st
‘𝐴))) ∧ 𝑁 =
(♯‘(1st ‘𝐵))) ∧ ∀𝑦 ∈ (0...𝑁)((2nd ‘𝐴)‘𝑦) = ((2nd ‘𝐵)‘𝑦)) → (∀𝑦 ∈ (0..^𝑁)((2nd ‘𝐴)‘(𝑦 + 1)) = ((2nd ‘𝐵)‘(𝑦 + 1)) → ∀𝑦 ∈ (0..^𝑁){((2nd ‘𝐴)‘𝑦), ((2nd ‘𝐴)‘(𝑦 + 1))} = {((2nd ‘𝐵)‘𝑦), ((2nd ‘𝐵)‘(𝑦 + 1))})) |
| 31 | 19, 30 | mpd 15 |
. . . . . 6
⊢ ((((𝐺 ∈ USPGraph ∧ (𝐴 ∈ (Walks‘𝐺) ∧ 𝐵 ∈ (Walks‘𝐺)) ∧ 𝑁 = (♯‘(1st
‘𝐴))) ∧ 𝑁 =
(♯‘(1st ‘𝐵))) ∧ ∀𝑦 ∈ (0...𝑁)((2nd ‘𝐴)‘𝑦) = ((2nd ‘𝐵)‘𝑦)) → ∀𝑦 ∈ (0..^𝑁){((2nd ‘𝐴)‘𝑦), ((2nd ‘𝐴)‘(𝑦 + 1))} = {((2nd ‘𝐵)‘𝑦), ((2nd ‘𝐵)‘(𝑦 + 1))}) |
| 32 | 31 | ex 412 |
. . . . 5
⊢ (((𝐺 ∈ USPGraph ∧ (𝐴 ∈ (Walks‘𝐺) ∧ 𝐵 ∈ (Walks‘𝐺)) ∧ 𝑁 = (♯‘(1st
‘𝐴))) ∧ 𝑁 =
(♯‘(1st ‘𝐵))) → (∀𝑦 ∈ (0...𝑁)((2nd ‘𝐴)‘𝑦) = ((2nd ‘𝐵)‘𝑦) → ∀𝑦 ∈ (0..^𝑁){((2nd ‘𝐴)‘𝑦), ((2nd ‘𝐴)‘(𝑦 + 1))} = {((2nd ‘𝐵)‘𝑦), ((2nd ‘𝐵)‘(𝑦 + 1))})) |
| 33 | | uspgrupgr 29195 |
. . . . . . . 8
⊢ (𝐺 ∈ USPGraph → 𝐺 ∈
UPGraph) |
| 34 | | eqid 2737 |
. . . . . . . . . 10
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
| 35 | | eqid 2737 |
. . . . . . . . . 10
⊢
(iEdg‘𝐺) =
(iEdg‘𝐺) |
| 36 | | eqid 2737 |
. . . . . . . . . 10
⊢
(1st ‘𝐴) = (1st ‘𝐴) |
| 37 | | eqid 2737 |
. . . . . . . . . 10
⊢
(2nd ‘𝐴) = (2nd ‘𝐴) |
| 38 | 34, 35, 36, 37 | upgrwlkcompim 29661 |
. . . . . . . . 9
⊢ ((𝐺 ∈ UPGraph ∧ 𝐴 ∈ (Walks‘𝐺)) → ((1st
‘𝐴) ∈ Word dom
(iEdg‘𝐺) ∧
(2nd ‘𝐴):(0...(♯‘(1st
‘𝐴)))⟶(Vtx‘𝐺) ∧ ∀𝑦 ∈ (0..^(♯‘(1st
‘𝐴)))((iEdg‘𝐺)‘((1st ‘𝐴)‘𝑦)) = {((2nd ‘𝐴)‘𝑦), ((2nd ‘𝐴)‘(𝑦 + 1))})) |
| 39 | 38 | ex 412 |
. . . . . . . 8
⊢ (𝐺 ∈ UPGraph → (𝐴 ∈ (Walks‘𝐺) → ((1st
‘𝐴) ∈ Word dom
(iEdg‘𝐺) ∧
(2nd ‘𝐴):(0...(♯‘(1st
‘𝐴)))⟶(Vtx‘𝐺) ∧ ∀𝑦 ∈ (0..^(♯‘(1st
‘𝐴)))((iEdg‘𝐺)‘((1st ‘𝐴)‘𝑦)) = {((2nd ‘𝐴)‘𝑦), ((2nd ‘𝐴)‘(𝑦 + 1))}))) |
| 40 | 33, 39 | syl 17 |
. . . . . . 7
⊢ (𝐺 ∈ USPGraph → (𝐴 ∈ (Walks‘𝐺) → ((1st
‘𝐴) ∈ Word dom
(iEdg‘𝐺) ∧
(2nd ‘𝐴):(0...(♯‘(1st
‘𝐴)))⟶(Vtx‘𝐺) ∧ ∀𝑦 ∈ (0..^(♯‘(1st
‘𝐴)))((iEdg‘𝐺)‘((1st ‘𝐴)‘𝑦)) = {((2nd ‘𝐴)‘𝑦), ((2nd ‘𝐴)‘(𝑦 + 1))}))) |
| 41 | | eqid 2737 |
. . . . . . . . . 10
⊢
(1st ‘𝐵) = (1st ‘𝐵) |
| 42 | | eqid 2737 |
. . . . . . . . . 10
⊢
(2nd ‘𝐵) = (2nd ‘𝐵) |
| 43 | 34, 35, 41, 42 | upgrwlkcompim 29661 |
. . . . . . . . 9
⊢ ((𝐺 ∈ UPGraph ∧ 𝐵 ∈ (Walks‘𝐺)) → ((1st
‘𝐵) ∈ Word dom
(iEdg‘𝐺) ∧
(2nd ‘𝐵):(0...(♯‘(1st
‘𝐵)))⟶(Vtx‘𝐺) ∧ ∀𝑦 ∈ (0..^(♯‘(1st
‘𝐵)))((iEdg‘𝐺)‘((1st ‘𝐵)‘𝑦)) = {((2nd ‘𝐵)‘𝑦), ((2nd ‘𝐵)‘(𝑦 + 1))})) |
| 44 | 43 | ex 412 |
. . . . . . . 8
⊢ (𝐺 ∈ UPGraph → (𝐵 ∈ (Walks‘𝐺) → ((1st
‘𝐵) ∈ Word dom
(iEdg‘𝐺) ∧
(2nd ‘𝐵):(0...(♯‘(1st
‘𝐵)))⟶(Vtx‘𝐺) ∧ ∀𝑦 ∈ (0..^(♯‘(1st
‘𝐵)))((iEdg‘𝐺)‘((1st ‘𝐵)‘𝑦)) = {((2nd ‘𝐵)‘𝑦), ((2nd ‘𝐵)‘(𝑦 + 1))}))) |
| 45 | 33, 44 | syl 17 |
. . . . . . 7
⊢ (𝐺 ∈ USPGraph → (𝐵 ∈ (Walks‘𝐺) → ((1st
‘𝐵) ∈ Word dom
(iEdg‘𝐺) ∧
(2nd ‘𝐵):(0...(♯‘(1st
‘𝐵)))⟶(Vtx‘𝐺) ∧ ∀𝑦 ∈ (0..^(♯‘(1st
‘𝐵)))((iEdg‘𝐺)‘((1st ‘𝐵)‘𝑦)) = {((2nd ‘𝐵)‘𝑦), ((2nd ‘𝐵)‘(𝑦 + 1))}))) |
| 46 | | oveq2 7439 |
. . . . . . . . . . . . . . . . . . 19
⊢
((♯‘(1st ‘𝐵)) = 𝑁 → (0..^(♯‘(1st
‘𝐵))) = (0..^𝑁)) |
| 47 | 46 | eqcoms 2745 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 =
(♯‘(1st ‘𝐵)) →
(0..^(♯‘(1st ‘𝐵))) = (0..^𝑁)) |
| 48 | 47 | raleqdv 3326 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 =
(♯‘(1st ‘𝐵)) → (∀𝑦 ∈ (0..^(♯‘(1st
‘𝐵)))((iEdg‘𝐺)‘((1st ‘𝐵)‘𝑦)) = {((2nd ‘𝐵)‘𝑦), ((2nd ‘𝐵)‘(𝑦 + 1))} ↔ ∀𝑦 ∈ (0..^𝑁)((iEdg‘𝐺)‘((1st ‘𝐵)‘𝑦)) = {((2nd ‘𝐵)‘𝑦), ((2nd ‘𝐵)‘(𝑦 + 1))})) |
| 49 | | oveq2 7439 |
. . . . . . . . . . . . . . . . . . 19
⊢
((♯‘(1st ‘𝐴)) = 𝑁 → (0..^(♯‘(1st
‘𝐴))) = (0..^𝑁)) |
| 50 | 49 | eqcoms 2745 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 =
(♯‘(1st ‘𝐴)) →
(0..^(♯‘(1st ‘𝐴))) = (0..^𝑁)) |
| 51 | 50 | raleqdv 3326 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 =
(♯‘(1st ‘𝐴)) → (∀𝑦 ∈ (0..^(♯‘(1st
‘𝐴)))((iEdg‘𝐺)‘((1st ‘𝐴)‘𝑦)) = {((2nd ‘𝐴)‘𝑦), ((2nd ‘𝐴)‘(𝑦 + 1))} ↔ ∀𝑦 ∈ (0..^𝑁)((iEdg‘𝐺)‘((1st ‘𝐴)‘𝑦)) = {((2nd ‘𝐴)‘𝑦), ((2nd ‘𝐴)‘(𝑦 + 1))})) |
| 52 | 48, 51 | bi2anan9r 639 |
. . . . . . . . . . . . . . . 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))}))) |
| 53 | | r19.26 3111 |
. . . . . . . . . . . . . . . . 17
⊢
(∀𝑦 ∈
(0..^𝑁)(((iEdg‘𝐺)‘((1st
‘𝐵)‘𝑦)) = {((2nd
‘𝐵)‘𝑦), ((2nd ‘𝐵)‘(𝑦 + 1))} ∧ ((iEdg‘𝐺)‘((1st ‘𝐴)‘𝑦)) = {((2nd ‘𝐴)‘𝑦), ((2nd ‘𝐴)‘(𝑦 + 1))}) ↔ (∀𝑦 ∈ (0..^𝑁)((iEdg‘𝐺)‘((1st ‘𝐵)‘𝑦)) = {((2nd ‘𝐵)‘𝑦), ((2nd ‘𝐵)‘(𝑦 + 1))} ∧ ∀𝑦 ∈ (0..^𝑁)((iEdg‘𝐺)‘((1st ‘𝐴)‘𝑦)) = {((2nd ‘𝐴)‘𝑦), ((2nd ‘𝐴)‘(𝑦 + 1))})) |
| 54 | | eqeq2 2749 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
({((2nd ‘𝐴)‘𝑦), ((2nd ‘𝐴)‘(𝑦 + 1))} = {((2nd ‘𝐵)‘𝑦), ((2nd ‘𝐵)‘(𝑦 + 1))} → (((iEdg‘𝐺)‘((1st
‘𝐴)‘𝑦)) = {((2nd
‘𝐴)‘𝑦), ((2nd ‘𝐴)‘(𝑦 + 1))} ↔ ((iEdg‘𝐺)‘((1st ‘𝐴)‘𝑦)) = {((2nd ‘𝐵)‘𝑦), ((2nd ‘𝐵)‘(𝑦 + 1))})) |
| 55 | | eqeq2 2749 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
({((2nd ‘𝐵)‘𝑦), ((2nd ‘𝐵)‘(𝑦 + 1))} = ((iEdg‘𝐺)‘((1st ‘𝐴)‘𝑦)) → (((iEdg‘𝐺)‘((1st ‘𝐵)‘𝑦)) = {((2nd ‘𝐵)‘𝑦), ((2nd ‘𝐵)‘(𝑦 + 1))} ↔ ((iEdg‘𝐺)‘((1st ‘𝐵)‘𝑦)) = ((iEdg‘𝐺)‘((1st ‘𝐴)‘𝑦)))) |
| 56 | 55 | eqcoms 2745 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((iEdg‘𝐺)‘((1st ‘𝐴)‘𝑦)) = {((2nd ‘𝐵)‘𝑦), ((2nd ‘𝐵)‘(𝑦 + 1))} → (((iEdg‘𝐺)‘((1st
‘𝐵)‘𝑦)) = {((2nd
‘𝐵)‘𝑦), ((2nd ‘𝐵)‘(𝑦 + 1))} ↔ ((iEdg‘𝐺)‘((1st ‘𝐵)‘𝑦)) = ((iEdg‘𝐺)‘((1st ‘𝐴)‘𝑦)))) |
| 57 | 56 | biimpd 229 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((iEdg‘𝐺)‘((1st ‘𝐴)‘𝑦)) = {((2nd ‘𝐵)‘𝑦), ((2nd ‘𝐵)‘(𝑦 + 1))} → (((iEdg‘𝐺)‘((1st
‘𝐵)‘𝑦)) = {((2nd
‘𝐵)‘𝑦), ((2nd ‘𝐵)‘(𝑦 + 1))} → ((iEdg‘𝐺)‘((1st ‘𝐵)‘𝑦)) = ((iEdg‘𝐺)‘((1st ‘𝐴)‘𝑦)))) |
| 58 | 54, 57 | biimtrdi 253 |
. . . . . . . . . . . . . . . . . . . 20
⊢
({((2nd ‘𝐴)‘𝑦), ((2nd ‘𝐴)‘(𝑦 + 1))} = {((2nd ‘𝐵)‘𝑦), ((2nd ‘𝐵)‘(𝑦 + 1))} → (((iEdg‘𝐺)‘((1st
‘𝐴)‘𝑦)) = {((2nd
‘𝐴)‘𝑦), ((2nd ‘𝐴)‘(𝑦 + 1))} → (((iEdg‘𝐺)‘((1st
‘𝐵)‘𝑦)) = {((2nd
‘𝐵)‘𝑦), ((2nd ‘𝐵)‘(𝑦 + 1))} → ((iEdg‘𝐺)‘((1st ‘𝐵)‘𝑦)) = ((iEdg‘𝐺)‘((1st ‘𝐴)‘𝑦))))) |
| 59 | 58 | com13 88 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((iEdg‘𝐺)‘((1st ‘𝐵)‘𝑦)) = {((2nd ‘𝐵)‘𝑦), ((2nd ‘𝐵)‘(𝑦 + 1))} → (((iEdg‘𝐺)‘((1st
‘𝐴)‘𝑦)) = {((2nd
‘𝐴)‘𝑦), ((2nd ‘𝐴)‘(𝑦 + 1))} → ({((2nd
‘𝐴)‘𝑦), ((2nd ‘𝐴)‘(𝑦 + 1))} = {((2nd ‘𝐵)‘𝑦), ((2nd ‘𝐵)‘(𝑦 + 1))} → ((iEdg‘𝐺)‘((1st ‘𝐵)‘𝑦)) = ((iEdg‘𝐺)‘((1st ‘𝐴)‘𝑦))))) |
| 60 | 59 | imp 406 |
. . . . . . . . . . . . . . . . . 18
⊢
((((iEdg‘𝐺)‘((1st ‘𝐵)‘𝑦)) = {((2nd ‘𝐵)‘𝑦), ((2nd ‘𝐵)‘(𝑦 + 1))} ∧ ((iEdg‘𝐺)‘((1st ‘𝐴)‘𝑦)) = {((2nd ‘𝐴)‘𝑦), ((2nd ‘𝐴)‘(𝑦 + 1))}) → ({((2nd
‘𝐴)‘𝑦), ((2nd ‘𝐴)‘(𝑦 + 1))} = {((2nd ‘𝐵)‘𝑦), ((2nd ‘𝐵)‘(𝑦 + 1))} → ((iEdg‘𝐺)‘((1st ‘𝐵)‘𝑦)) = ((iEdg‘𝐺)‘((1st ‘𝐴)‘𝑦)))) |
| 61 | 60 | ral2imi 3085 |
. . . . . . . . . . . . . . . . 17
⊢
(∀𝑦 ∈
(0..^𝑁)(((iEdg‘𝐺)‘((1st
‘𝐵)‘𝑦)) = {((2nd
‘𝐵)‘𝑦), ((2nd ‘𝐵)‘(𝑦 + 1))} ∧ ((iEdg‘𝐺)‘((1st ‘𝐴)‘𝑦)) = {((2nd ‘𝐴)‘𝑦), ((2nd ‘𝐴)‘(𝑦 + 1))}) → (∀𝑦 ∈ (0..^𝑁){((2nd ‘𝐴)‘𝑦), ((2nd ‘𝐴)‘(𝑦 + 1))} = {((2nd ‘𝐵)‘𝑦), ((2nd ‘𝐵)‘(𝑦 + 1))} → ∀𝑦 ∈ (0..^𝑁)((iEdg‘𝐺)‘((1st ‘𝐵)‘𝑦)) = ((iEdg‘𝐺)‘((1st ‘𝐴)‘𝑦)))) |
| 62 | 53, 61 | sylbir 235 |
. . . . . . . . . . . . . . . 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 ‘𝐴)‘𝑦)))) |
| 63 | 52, 62 | biimtrdi 253 |
. . . . . . . . . . . . . . 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 ‘𝐴)‘𝑦))))) |
| 64 | 63 | com12 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 ‘𝐴)‘𝑦))))) |
| 65 | 64 | ex 412 |
. . . . . . . . . . . . 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 ‘𝐴)‘𝑦)))))) |
| 66 | 65 | 3ad2ant3 1136 |
. . . . . . . . . . . 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 ‘𝐴)‘𝑦)))))) |
| 67 | 66 | com12 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 ‘𝐴)‘𝑦)))))) |
| 68 | 67 | 3ad2ant3 1136 |
. . . . . . . . . 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 ‘𝐴)‘𝑦)))))) |
| 69 | 68 | imp 406 |
. . . . . . . . 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 ‘𝐴)‘𝑦))))) |
| 70 | 69 | expd 415 |
. . . . . . . 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 ‘𝐴)‘𝑦)))))) |
| 71 | 70 | a1i 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 ‘𝐴)‘𝑦))))))) |
| 72 | 40, 45, 71 | syl2and 608 |
. . . . . 6
⊢ (𝐺 ∈ USPGraph → ((𝐴 ∈ (Walks‘𝐺) ∧ 𝐵 ∈ (Walks‘𝐺)) → (𝑁 = (♯‘(1st
‘𝐴)) → (𝑁 =
(♯‘(1st ‘𝐵)) → (∀𝑦 ∈ (0..^𝑁){((2nd ‘𝐴)‘𝑦), ((2nd ‘𝐴)‘(𝑦 + 1))} = {((2nd ‘𝐵)‘𝑦), ((2nd ‘𝐵)‘(𝑦 + 1))} → ∀𝑦 ∈ (0..^𝑁)((iEdg‘𝐺)‘((1st ‘𝐵)‘𝑦)) = ((iEdg‘𝐺)‘((1st ‘𝐴)‘𝑦))))))) |
| 73 | 72 | 3imp1 1348 |
. . . . 5
⊢ (((𝐺 ∈ USPGraph ∧ (𝐴 ∈ (Walks‘𝐺) ∧ 𝐵 ∈ (Walks‘𝐺)) ∧ 𝑁 = (♯‘(1st
‘𝐴))) ∧ 𝑁 =
(♯‘(1st ‘𝐵))) → (∀𝑦 ∈ (0..^𝑁){((2nd ‘𝐴)‘𝑦), ((2nd ‘𝐴)‘(𝑦 + 1))} = {((2nd ‘𝐵)‘𝑦), ((2nd ‘𝐵)‘(𝑦 + 1))} → ∀𝑦 ∈ (0..^𝑁)((iEdg‘𝐺)‘((1st ‘𝐵)‘𝑦)) = ((iEdg‘𝐺)‘((1st ‘𝐴)‘𝑦)))) |
| 74 | | eqcom 2744 |
. . . . . . 7
⊢
(((iEdg‘𝐺)‘((1st ‘𝐵)‘𝑦)) = ((iEdg‘𝐺)‘((1st ‘𝐴)‘𝑦)) ↔ ((iEdg‘𝐺)‘((1st ‘𝐴)‘𝑦)) = ((iEdg‘𝐺)‘((1st ‘𝐵)‘𝑦))) |
| 75 | 35 | uspgrf1oedg 29190 |
. . . . . . . . . . . 12
⊢ (𝐺 ∈ USPGraph →
(iEdg‘𝐺):dom
(iEdg‘𝐺)–1-1-onto→(Edg‘𝐺)) |
| 76 | | f1of1 6847 |
. . . . . . . . . . . 12
⊢
((iEdg‘𝐺):dom
(iEdg‘𝐺)–1-1-onto→(Edg‘𝐺) → (iEdg‘𝐺):dom (iEdg‘𝐺)–1-1→(Edg‘𝐺)) |
| 77 | 75, 76 | syl 17 |
. . . . . . . . . . 11
⊢ (𝐺 ∈ USPGraph →
(iEdg‘𝐺):dom
(iEdg‘𝐺)–1-1→(Edg‘𝐺)) |
| 78 | | eqidd 2738 |
. . . . . . . . . . . 12
⊢ (𝐺 ∈ USPGraph →
(iEdg‘𝐺) =
(iEdg‘𝐺)) |
| 79 | | eqidd 2738 |
. . . . . . . . . . . 12
⊢ (𝐺 ∈ USPGraph → dom
(iEdg‘𝐺) = dom
(iEdg‘𝐺)) |
| 80 | | edgval 29066 |
. . . . . . . . . . . . . 14
⊢
(Edg‘𝐺) = ran
(iEdg‘𝐺) |
| 81 | 80 | eqcomi 2746 |
. . . . . . . . . . . . 13
⊢ ran
(iEdg‘𝐺) =
(Edg‘𝐺) |
| 82 | 81 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝐺 ∈ USPGraph → ran
(iEdg‘𝐺) =
(Edg‘𝐺)) |
| 83 | 78, 79, 82 | f1eq123d 6840 |
. . . . . . . . . . 11
⊢ (𝐺 ∈ USPGraph →
((iEdg‘𝐺):dom
(iEdg‘𝐺)–1-1→ran (iEdg‘𝐺) ↔ (iEdg‘𝐺):dom (iEdg‘𝐺)–1-1→(Edg‘𝐺))) |
| 84 | 77, 83 | mpbird 257 |
. . . . . . . . . 10
⊢ (𝐺 ∈ USPGraph →
(iEdg‘𝐺):dom
(iEdg‘𝐺)–1-1→ran (iEdg‘𝐺)) |
| 85 | 84 | 3ad2ant1 1134 |
. . . . . . . . 9
⊢ ((𝐺 ∈ USPGraph ∧ (𝐴 ∈ (Walks‘𝐺) ∧ 𝐵 ∈ (Walks‘𝐺)) ∧ 𝑁 = (♯‘(1st
‘𝐴))) →
(iEdg‘𝐺):dom
(iEdg‘𝐺)–1-1→ran (iEdg‘𝐺)) |
| 86 | 85 | adantr 480 |
. . . . . . . 8
⊢ (((𝐺 ∈ USPGraph ∧ (𝐴 ∈ (Walks‘𝐺) ∧ 𝐵 ∈ (Walks‘𝐺)) ∧ 𝑁 = (♯‘(1st
‘𝐴))) ∧ 𝑁 =
(♯‘(1st ‘𝐵))) → (iEdg‘𝐺):dom (iEdg‘𝐺)–1-1→ran (iEdg‘𝐺)) |
| 87 | 34, 35, 36, 37 | wlkelwrd 29651 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ (Walks‘𝐺) → ((1st
‘𝐴) ∈ Word dom
(iEdg‘𝐺) ∧
(2nd ‘𝐴):(0...(♯‘(1st
‘𝐴)))⟶(Vtx‘𝐺))) |
| 88 | 34, 35, 41, 42 | wlkelwrd 29651 |
. . . . . . . . . . . . . . 15
⊢ (𝐵 ∈ (Walks‘𝐺) → ((1st
‘𝐵) ∈ Word dom
(iEdg‘𝐺) ∧
(2nd ‘𝐵):(0...(♯‘(1st
‘𝐵)))⟶(Vtx‘𝐺))) |
| 89 | | oveq2 7439 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑁 =
(♯‘(1st ‘𝐴)) → (0..^𝑁) = (0..^(♯‘(1st
‘𝐴)))) |
| 90 | 89 | eleq2d 2827 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑁 =
(♯‘(1st ‘𝐴)) → (𝑦 ∈ (0..^𝑁) ↔ 𝑦 ∈ (0..^(♯‘(1st
‘𝐴))))) |
| 91 | | wrdsymbcl 14565 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((1st ‘𝐴) ∈ Word dom (iEdg‘𝐺) ∧ 𝑦 ∈ (0..^(♯‘(1st
‘𝐴)))) →
((1st ‘𝐴)‘𝑦) ∈ dom (iEdg‘𝐺)) |
| 92 | 91 | expcom 413 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑦 ∈
(0..^(♯‘(1st ‘𝐴))) → ((1st ‘𝐴) ∈ Word dom
(iEdg‘𝐺) →
((1st ‘𝐴)‘𝑦) ∈ dom (iEdg‘𝐺))) |
| 93 | 90, 92 | biimtrdi 253 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑁 =
(♯‘(1st ‘𝐴)) → (𝑦 ∈ (0..^𝑁) → ((1st ‘𝐴) ∈ Word dom
(iEdg‘𝐺) →
((1st ‘𝐴)‘𝑦) ∈ dom (iEdg‘𝐺)))) |
| 94 | 93 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑁 =
(♯‘(1st ‘𝐴)) ∧ 𝑁 = (♯‘(1st
‘𝐵))) → (𝑦 ∈ (0..^𝑁) → ((1st ‘𝐴) ∈ Word dom
(iEdg‘𝐺) →
((1st ‘𝐴)‘𝑦) ∈ dom (iEdg‘𝐺)))) |
| 95 | 94 | imp 406 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑁 =
(♯‘(1st ‘𝐴)) ∧ 𝑁 = (♯‘(1st
‘𝐵))) ∧ 𝑦 ∈ (0..^𝑁)) → ((1st ‘𝐴) ∈ Word dom
(iEdg‘𝐺) →
((1st ‘𝐴)‘𝑦) ∈ dom (iEdg‘𝐺))) |
| 96 | 95 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((1st ‘𝐴) ∈ Word dom (iEdg‘𝐺) → (((𝑁 = (♯‘(1st
‘𝐴)) ∧ 𝑁 =
(♯‘(1st ‘𝐵))) ∧ 𝑦 ∈ (0..^𝑁)) → ((1st ‘𝐴)‘𝑦) ∈ dom (iEdg‘𝐺))) |
| 97 | 96 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((1st ‘𝐵) ∈ Word dom (iEdg‘𝐺) ∧ (1st
‘𝐴) ∈ Word dom
(iEdg‘𝐺)) →
(((𝑁 =
(♯‘(1st ‘𝐴)) ∧ 𝑁 = (♯‘(1st
‘𝐵))) ∧ 𝑦 ∈ (0..^𝑁)) → ((1st ‘𝐴)‘𝑦) ∈ dom (iEdg‘𝐺))) |
| 98 | | oveq2 7439 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑁 =
(♯‘(1st ‘𝐵)) → (0..^𝑁) = (0..^(♯‘(1st
‘𝐵)))) |
| 99 | 98 | eleq2d 2827 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑁 =
(♯‘(1st ‘𝐵)) → (𝑦 ∈ (0..^𝑁) ↔ 𝑦 ∈ (0..^(♯‘(1st
‘𝐵))))) |
| 100 | | wrdsymbcl 14565 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((1st ‘𝐵) ∈ Word dom (iEdg‘𝐺) ∧ 𝑦 ∈ (0..^(♯‘(1st
‘𝐵)))) →
((1st ‘𝐵)‘𝑦) ∈ dom (iEdg‘𝐺)) |
| 101 | 100 | expcom 413 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑦 ∈
(0..^(♯‘(1st ‘𝐵))) → ((1st ‘𝐵) ∈ Word dom
(iEdg‘𝐺) →
((1st ‘𝐵)‘𝑦) ∈ dom (iEdg‘𝐺))) |
| 102 | 99, 101 | biimtrdi 253 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑁 =
(♯‘(1st ‘𝐵)) → (𝑦 ∈ (0..^𝑁) → ((1st ‘𝐵) ∈ Word dom
(iEdg‘𝐺) →
((1st ‘𝐵)‘𝑦) ∈ dom (iEdg‘𝐺)))) |
| 103 | 102 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑁 =
(♯‘(1st ‘𝐴)) ∧ 𝑁 = (♯‘(1st
‘𝐵))) → (𝑦 ∈ (0..^𝑁) → ((1st ‘𝐵) ∈ Word dom
(iEdg‘𝐺) →
((1st ‘𝐵)‘𝑦) ∈ dom (iEdg‘𝐺)))) |
| 104 | 103 | imp 406 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑁 =
(♯‘(1st ‘𝐴)) ∧ 𝑁 = (♯‘(1st
‘𝐵))) ∧ 𝑦 ∈ (0..^𝑁)) → ((1st ‘𝐵) ∈ Word dom
(iEdg‘𝐺) →
((1st ‘𝐵)‘𝑦) ∈ dom (iEdg‘𝐺))) |
| 105 | 104 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((1st ‘𝐵) ∈ Word dom (iEdg‘𝐺) → (((𝑁 = (♯‘(1st
‘𝐴)) ∧ 𝑁 =
(♯‘(1st ‘𝐵))) ∧ 𝑦 ∈ (0..^𝑁)) → ((1st ‘𝐵)‘𝑦) ∈ dom (iEdg‘𝐺))) |
| 106 | 105 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((1st ‘𝐵) ∈ Word dom (iEdg‘𝐺) ∧ (1st
‘𝐴) ∈ Word dom
(iEdg‘𝐺)) →
(((𝑁 =
(♯‘(1st ‘𝐴)) ∧ 𝑁 = (♯‘(1st
‘𝐵))) ∧ 𝑦 ∈ (0..^𝑁)) → ((1st ‘𝐵)‘𝑦) ∈ dom (iEdg‘𝐺))) |
| 107 | 97, 106 | jcad 512 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((1st ‘𝐵) ∈ Word dom (iEdg‘𝐺) ∧ (1st
‘𝐴) ∈ Word dom
(iEdg‘𝐺)) →
(((𝑁 =
(♯‘(1st ‘𝐴)) ∧ 𝑁 = (♯‘(1st
‘𝐵))) ∧ 𝑦 ∈ (0..^𝑁)) → (((1st ‘𝐴)‘𝑦) ∈ dom (iEdg‘𝐺) ∧ ((1st ‘𝐵)‘𝑦) ∈ dom (iEdg‘𝐺)))) |
| 108 | 107 | ex 412 |
. . . . . . . . . . . . . . . . . . 19
⊢
((1st ‘𝐵) ∈ Word dom (iEdg‘𝐺) → ((1st
‘𝐴) ∈ Word dom
(iEdg‘𝐺) →
(((𝑁 =
(♯‘(1st ‘𝐴)) ∧ 𝑁 = (♯‘(1st
‘𝐵))) ∧ 𝑦 ∈ (0..^𝑁)) → (((1st ‘𝐴)‘𝑦) ∈ dom (iEdg‘𝐺) ∧ ((1st ‘𝐵)‘𝑦) ∈ dom (iEdg‘𝐺))))) |
| 109 | 108 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢
(((1st ‘𝐵) ∈ Word dom (iEdg‘𝐺) ∧ (2nd
‘𝐵):(0...(♯‘(1st
‘𝐵)))⟶(Vtx‘𝐺)) → ((1st ‘𝐴) ∈ Word dom
(iEdg‘𝐺) →
(((𝑁 =
(♯‘(1st ‘𝐴)) ∧ 𝑁 = (♯‘(1st
‘𝐵))) ∧ 𝑦 ∈ (0..^𝑁)) → (((1st ‘𝐴)‘𝑦) ∈ dom (iEdg‘𝐺) ∧ ((1st ‘𝐵)‘𝑦) ∈ dom (iEdg‘𝐺))))) |
| 110 | 109 | com12 32 |
. . . . . . . . . . . . . . . . 17
⊢
((1st ‘𝐴) ∈ Word dom (iEdg‘𝐺) → (((1st
‘𝐵) ∈ Word dom
(iEdg‘𝐺) ∧
(2nd ‘𝐵):(0...(♯‘(1st
‘𝐵)))⟶(Vtx‘𝐺)) → (((𝑁 = (♯‘(1st
‘𝐴)) ∧ 𝑁 =
(♯‘(1st ‘𝐵))) ∧ 𝑦 ∈ (0..^𝑁)) → (((1st ‘𝐴)‘𝑦) ∈ dom (iEdg‘𝐺) ∧ ((1st ‘𝐵)‘𝑦) ∈ dom (iEdg‘𝐺))))) |
| 111 | 110 | adantr 480 |
. . . . . . . . . . . . . . . 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‘𝐺))))) |
| 112 | 111 | imp 406 |
. . . . . . . . . . . . . . 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‘𝐺)))) |
| 113 | 87, 88, 112 | syl2an 596 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ (Walks‘𝐺) ∧ 𝐵 ∈ (Walks‘𝐺)) → (((𝑁 = (♯‘(1st
‘𝐴)) ∧ 𝑁 =
(♯‘(1st ‘𝐵))) ∧ 𝑦 ∈ (0..^𝑁)) → (((1st ‘𝐴)‘𝑦) ∈ dom (iEdg‘𝐺) ∧ ((1st ‘𝐵)‘𝑦) ∈ dom (iEdg‘𝐺)))) |
| 114 | 113 | expd 415 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ (Walks‘𝐺) ∧ 𝐵 ∈ (Walks‘𝐺)) → ((𝑁 = (♯‘(1st
‘𝐴)) ∧ 𝑁 =
(♯‘(1st ‘𝐵))) → (𝑦 ∈ (0..^𝑁) → (((1st ‘𝐴)‘𝑦) ∈ dom (iEdg‘𝐺) ∧ ((1st ‘𝐵)‘𝑦) ∈ dom (iEdg‘𝐺))))) |
| 115 | 114 | expd 415 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ (Walks‘𝐺) ∧ 𝐵 ∈ (Walks‘𝐺)) → (𝑁 = (♯‘(1st
‘𝐴)) → (𝑁 =
(♯‘(1st ‘𝐵)) → (𝑦 ∈ (0..^𝑁) → (((1st ‘𝐴)‘𝑦) ∈ dom (iEdg‘𝐺) ∧ ((1st ‘𝐵)‘𝑦) ∈ dom (iEdg‘𝐺)))))) |
| 116 | 115 | imp 406 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ (Walks‘𝐺) ∧ 𝐵 ∈ (Walks‘𝐺)) ∧ 𝑁 = (♯‘(1st
‘𝐴))) → (𝑁 =
(♯‘(1st ‘𝐵)) → (𝑦 ∈ (0..^𝑁) → (((1st ‘𝐴)‘𝑦) ∈ dom (iEdg‘𝐺) ∧ ((1st ‘𝐵)‘𝑦) ∈ dom (iEdg‘𝐺))))) |
| 117 | 116 | 3adant1 1131 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ USPGraph ∧ (𝐴 ∈ (Walks‘𝐺) ∧ 𝐵 ∈ (Walks‘𝐺)) ∧ 𝑁 = (♯‘(1st
‘𝐴))) → (𝑁 =
(♯‘(1st ‘𝐵)) → (𝑦 ∈ (0..^𝑁) → (((1st ‘𝐴)‘𝑦) ∈ dom (iEdg‘𝐺) ∧ ((1st ‘𝐵)‘𝑦) ∈ dom (iEdg‘𝐺))))) |
| 118 | 117 | imp 406 |
. . . . . . . . 9
⊢ (((𝐺 ∈ USPGraph ∧ (𝐴 ∈ (Walks‘𝐺) ∧ 𝐵 ∈ (Walks‘𝐺)) ∧ 𝑁 = (♯‘(1st
‘𝐴))) ∧ 𝑁 =
(♯‘(1st ‘𝐵))) → (𝑦 ∈ (0..^𝑁) → (((1st ‘𝐴)‘𝑦) ∈ dom (iEdg‘𝐺) ∧ ((1st ‘𝐵)‘𝑦) ∈ dom (iEdg‘𝐺)))) |
| 119 | 118 | imp 406 |
. . . . . . . 8
⊢ ((((𝐺 ∈ USPGraph ∧ (𝐴 ∈ (Walks‘𝐺) ∧ 𝐵 ∈ (Walks‘𝐺)) ∧ 𝑁 = (♯‘(1st
‘𝐴))) ∧ 𝑁 =
(♯‘(1st ‘𝐵))) ∧ 𝑦 ∈ (0..^𝑁)) → (((1st ‘𝐴)‘𝑦) ∈ dom (iEdg‘𝐺) ∧ ((1st ‘𝐵)‘𝑦) ∈ dom (iEdg‘𝐺))) |
| 120 | | f1veqaeq 7277 |
. . . . . . . 8
⊢
(((iEdg‘𝐺):dom
(iEdg‘𝐺)–1-1→ran (iEdg‘𝐺) ∧ (((1st ‘𝐴)‘𝑦) ∈ dom (iEdg‘𝐺) ∧ ((1st ‘𝐵)‘𝑦) ∈ dom (iEdg‘𝐺))) → (((iEdg‘𝐺)‘((1st ‘𝐴)‘𝑦)) = ((iEdg‘𝐺)‘((1st ‘𝐵)‘𝑦)) → ((1st ‘𝐴)‘𝑦) = ((1st ‘𝐵)‘𝑦))) |
| 121 | 86, 119, 120 | syl2an2r 685 |
. . . . . . 7
⊢ ((((𝐺 ∈ USPGraph ∧ (𝐴 ∈ (Walks‘𝐺) ∧ 𝐵 ∈ (Walks‘𝐺)) ∧ 𝑁 = (♯‘(1st
‘𝐴))) ∧ 𝑁 =
(♯‘(1st ‘𝐵))) ∧ 𝑦 ∈ (0..^𝑁)) → (((iEdg‘𝐺)‘((1st ‘𝐴)‘𝑦)) = ((iEdg‘𝐺)‘((1st ‘𝐵)‘𝑦)) → ((1st ‘𝐴)‘𝑦) = ((1st ‘𝐵)‘𝑦))) |
| 122 | 74, 121 | biimtrid 242 |
. . . . . 6
⊢ ((((𝐺 ∈ USPGraph ∧ (𝐴 ∈ (Walks‘𝐺) ∧ 𝐵 ∈ (Walks‘𝐺)) ∧ 𝑁 = (♯‘(1st
‘𝐴))) ∧ 𝑁 =
(♯‘(1st ‘𝐵))) ∧ 𝑦 ∈ (0..^𝑁)) → (((iEdg‘𝐺)‘((1st ‘𝐵)‘𝑦)) = ((iEdg‘𝐺)‘((1st ‘𝐴)‘𝑦)) → ((1st ‘𝐴)‘𝑦) = ((1st ‘𝐵)‘𝑦))) |
| 123 | 122 | ralimdva 3167 |
. . . . 5
⊢ (((𝐺 ∈ USPGraph ∧ (𝐴 ∈ (Walks‘𝐺) ∧ 𝐵 ∈ (Walks‘𝐺)) ∧ 𝑁 = (♯‘(1st
‘𝐴))) ∧ 𝑁 =
(♯‘(1st ‘𝐵))) → (∀𝑦 ∈ (0..^𝑁)((iEdg‘𝐺)‘((1st ‘𝐵)‘𝑦)) = ((iEdg‘𝐺)‘((1st ‘𝐴)‘𝑦)) → ∀𝑦 ∈ (0..^𝑁)((1st ‘𝐴)‘𝑦) = ((1st ‘𝐵)‘𝑦))) |
| 124 | 32, 73, 123 | 3syld 60 |
. . . 4
⊢ (((𝐺 ∈ USPGraph ∧ (𝐴 ∈ (Walks‘𝐺) ∧ 𝐵 ∈ (Walks‘𝐺)) ∧ 𝑁 = (♯‘(1st
‘𝐴))) ∧ 𝑁 =
(♯‘(1st ‘𝐵))) → (∀𝑦 ∈ (0...𝑁)((2nd ‘𝐴)‘𝑦) = ((2nd ‘𝐵)‘𝑦) → ∀𝑦 ∈ (0..^𝑁)((1st ‘𝐴)‘𝑦) = ((1st ‘𝐵)‘𝑦))) |
| 125 | 124 | expimpd 453 |
. . 3
⊢ ((𝐺 ∈ USPGraph ∧ (𝐴 ∈ (Walks‘𝐺) ∧ 𝐵 ∈ (Walks‘𝐺)) ∧ 𝑁 = (♯‘(1st
‘𝐴))) → ((𝑁 =
(♯‘(1st ‘𝐵)) ∧ ∀𝑦 ∈ (0...𝑁)((2nd ‘𝐴)‘𝑦) = ((2nd ‘𝐵)‘𝑦)) → ∀𝑦 ∈ (0..^𝑁)((1st ‘𝐴)‘𝑦) = ((1st ‘𝐵)‘𝑦))) |
| 126 | 125 | pm4.71d 561 |
. 2
⊢ ((𝐺 ∈ USPGraph ∧ (𝐴 ∈ (Walks‘𝐺) ∧ 𝐵 ∈ (Walks‘𝐺)) ∧ 𝑁 = (♯‘(1st
‘𝐴))) → ((𝑁 =
(♯‘(1st ‘𝐵)) ∧ ∀𝑦 ∈ (0...𝑁)((2nd ‘𝐴)‘𝑦) = ((2nd ‘𝐵)‘𝑦)) ↔ ((𝑁 = (♯‘(1st
‘𝐵)) ∧
∀𝑦 ∈ (0...𝑁)((2nd ‘𝐴)‘𝑦) = ((2nd ‘𝐵)‘𝑦)) ∧ ∀𝑦 ∈ (0..^𝑁)((1st ‘𝐴)‘𝑦) = ((1st ‘𝐵)‘𝑦)))) |
| 127 | 2, 5, 126 | 3bitr4d 311 |
1
⊢ ((𝐺 ∈ USPGraph ∧ (𝐴 ∈ (Walks‘𝐺) ∧ 𝐵 ∈ (Walks‘𝐺)) ∧ 𝑁 = (♯‘(1st
‘𝐴))) → (𝐴 = 𝐵 ↔ (𝑁 = (♯‘(1st
‘𝐵)) ∧
∀𝑦 ∈ (0...𝑁)((2nd ‘𝐴)‘𝑦) = ((2nd ‘𝐵)‘𝑦)))) |