Proof of Theorem 1wlkeq
Step | Hyp | Ref
| Expression |
1 | | 1wlkop 40832 |
. . . . 5
⊢ (𝐴 ∈ (1Walks‘𝐺) → 𝐴 = 〈(1st ‘𝐴), (2nd ‘𝐴)〉) |
2 | | 1st2ndb 7097 |
. . . . 5
⊢ (𝐴 ∈ (V × V) ↔
𝐴 = 〈(1st
‘𝐴), (2nd
‘𝐴)〉) |
3 | 1, 2 | sylibr 223 |
. . . 4
⊢ (𝐴 ∈ (1Walks‘𝐺) → 𝐴 ∈ (V × V)) |
4 | | 1wlkop 40832 |
. . . . 5
⊢ (𝐵 ∈ (1Walks‘𝐺) → 𝐵 = 〈(1st ‘𝐵), (2nd ‘𝐵)〉) |
5 | | 1st2ndb 7097 |
. . . . 5
⊢ (𝐵 ∈ (V × V) ↔
𝐵 = 〈(1st
‘𝐵), (2nd
‘𝐵)〉) |
6 | 4, 5 | sylibr 223 |
. . . 4
⊢ (𝐵 ∈ (1Walks‘𝐺) → 𝐵 ∈ (V × V)) |
7 | | xpopth 7098 |
. . . . 5
⊢ ((𝐴 ∈ (V × V) ∧
𝐵 ∈ (V × V))
→ (((1st ‘𝐴) = (1st ‘𝐵) ∧ (2nd ‘𝐴) = (2nd ‘𝐵)) ↔ 𝐴 = 𝐵)) |
8 | 7 | bicomd 212 |
. . . 4
⊢ ((𝐴 ∈ (V × V) ∧
𝐵 ∈ (V × V))
→ (𝐴 = 𝐵 ↔ ((1st
‘𝐴) = (1st
‘𝐵) ∧
(2nd ‘𝐴) =
(2nd ‘𝐵)))) |
9 | 3, 6, 8 | syl2an 493 |
. . 3
⊢ ((𝐴 ∈ (1Walks‘𝐺) ∧ 𝐵 ∈ (1Walks‘𝐺)) → (𝐴 = 𝐵 ↔ ((1st ‘𝐴) = (1st ‘𝐵) ∧ (2nd
‘𝐴) = (2nd
‘𝐵)))) |
10 | 9 | 3adant3 1074 |
. 2
⊢ ((𝐴 ∈ (1Walks‘𝐺) ∧ 𝐵 ∈ (1Walks‘𝐺) ∧ 𝑁 = (#‘(1st ‘𝐴))) → (𝐴 = 𝐵 ↔ ((1st ‘𝐴) = (1st ‘𝐵) ∧ (2nd
‘𝐴) = (2nd
‘𝐵)))) |
11 | | eqid 2610 |
. . . . . . 7
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
12 | | eqid 2610 |
. . . . . . 7
⊢
(iEdg‘𝐺) =
(iEdg‘𝐺) |
13 | | eqid 2610 |
. . . . . . 7
⊢
(1st ‘𝐴) = (1st ‘𝐴) |
14 | | eqid 2610 |
. . . . . . 7
⊢
(2nd ‘𝐴) = (2nd ‘𝐴) |
15 | 11, 12, 13, 14 | 1wlkelwrd 40837 |
. . . . . 6
⊢ (𝐴 ∈ (1Walks‘𝐺) → ((1st
‘𝐴) ∈ Word dom
(iEdg‘𝐺) ∧
(2nd ‘𝐴):(0...(#‘(1st ‘𝐴)))⟶(Vtx‘𝐺))) |
16 | | eqid 2610 |
. . . . . . 7
⊢
(1st ‘𝐵) = (1st ‘𝐵) |
17 | | eqid 2610 |
. . . . . . 7
⊢
(2nd ‘𝐵) = (2nd ‘𝐵) |
18 | 11, 12, 16, 17 | 1wlkelwrd 40837 |
. . . . . 6
⊢ (𝐵 ∈ (1Walks‘𝐺) → ((1st
‘𝐵) ∈ Word dom
(iEdg‘𝐺) ∧
(2nd ‘𝐵):(0...(#‘(1st ‘𝐵)))⟶(Vtx‘𝐺))) |
19 | 15, 18 | anim12i 588 |
. . . . 5
⊢ ((𝐴 ∈ (1Walks‘𝐺) ∧ 𝐵 ∈ (1Walks‘𝐺)) → (((1st ‘𝐴) ∈ Word dom
(iEdg‘𝐺) ∧
(2nd ‘𝐴):(0...(#‘(1st ‘𝐴)))⟶(Vtx‘𝐺)) ∧ ((1st
‘𝐵) ∈ Word dom
(iEdg‘𝐺) ∧
(2nd ‘𝐵):(0...(#‘(1st ‘𝐵)))⟶(Vtx‘𝐺)))) |
20 | | eleq1 2676 |
. . . . . . . 8
⊢ (𝐴 = 〈(1st
‘𝐴), (2nd
‘𝐴)〉 →
(𝐴 ∈
(1Walks‘𝐺) ↔
〈(1st ‘𝐴), (2nd ‘𝐴)〉 ∈ (1Walks‘𝐺))) |
21 | | df-br 4584 |
. . . . . . . . 9
⊢
((1st ‘𝐴)(1Walks‘𝐺)(2nd ‘𝐴) ↔ 〈(1st ‘𝐴), (2nd ‘𝐴)〉 ∈
(1Walks‘𝐺)) |
22 | | 1wlklenvm1 40826 |
. . . . . . . . 9
⊢
((1st ‘𝐴)(1Walks‘𝐺)(2nd ‘𝐴) → (#‘(1st
‘𝐴)) =
((#‘(2nd ‘𝐴)) − 1)) |
23 | 21, 22 | sylbir 224 |
. . . . . . . 8
⊢
(〈(1st ‘𝐴), (2nd ‘𝐴)〉 ∈ (1Walks‘𝐺) →
(#‘(1st ‘𝐴)) = ((#‘(2nd ‘𝐴)) − 1)) |
24 | 20, 23 | syl6bi 242 |
. . . . . . 7
⊢ (𝐴 = 〈(1st
‘𝐴), (2nd
‘𝐴)〉 →
(𝐴 ∈
(1Walks‘𝐺) →
(#‘(1st ‘𝐴)) = ((#‘(2nd ‘𝐴)) − 1))) |
25 | 1, 24 | mpcom 37 |
. . . . . 6
⊢ (𝐴 ∈ (1Walks‘𝐺) →
(#‘(1st ‘𝐴)) = ((#‘(2nd ‘𝐴)) − 1)) |
26 | | eleq1 2676 |
. . . . . . . 8
⊢ (𝐵 = 〈(1st
‘𝐵), (2nd
‘𝐵)〉 →
(𝐵 ∈
(1Walks‘𝐺) ↔
〈(1st ‘𝐵), (2nd ‘𝐵)〉 ∈ (1Walks‘𝐺))) |
27 | | df-br 4584 |
. . . . . . . . 9
⊢
((1st ‘𝐵)(1Walks‘𝐺)(2nd ‘𝐵) ↔ 〈(1st ‘𝐵), (2nd ‘𝐵)〉 ∈
(1Walks‘𝐺)) |
28 | | 1wlklenvm1 40826 |
. . . . . . . . 9
⊢
((1st ‘𝐵)(1Walks‘𝐺)(2nd ‘𝐵) → (#‘(1st
‘𝐵)) =
((#‘(2nd ‘𝐵)) − 1)) |
29 | 27, 28 | sylbir 224 |
. . . . . . . 8
⊢
(〈(1st ‘𝐵), (2nd ‘𝐵)〉 ∈ (1Walks‘𝐺) →
(#‘(1st ‘𝐵)) = ((#‘(2nd ‘𝐵)) − 1)) |
30 | 26, 29 | syl6bi 242 |
. . . . . . 7
⊢ (𝐵 = 〈(1st
‘𝐵), (2nd
‘𝐵)〉 →
(𝐵 ∈
(1Walks‘𝐺) →
(#‘(1st ‘𝐵)) = ((#‘(2nd ‘𝐵)) − 1))) |
31 | 4, 30 | mpcom 37 |
. . . . . 6
⊢ (𝐵 ∈ (1Walks‘𝐺) →
(#‘(1st ‘𝐵)) = ((#‘(2nd ‘𝐵)) − 1)) |
32 | 25, 31 | anim12i 588 |
. . . . 5
⊢ ((𝐴 ∈ (1Walks‘𝐺) ∧ 𝐵 ∈ (1Walks‘𝐺)) → ((#‘(1st
‘𝐴)) =
((#‘(2nd ‘𝐴)) − 1) ∧ (#‘(1st
‘𝐵)) =
((#‘(2nd ‘𝐵)) − 1))) |
33 | | eqwrd 13201 |
. . . . . . . 8
⊢
(((1st ‘𝐴) ∈ Word dom (iEdg‘𝐺) ∧ (1st
‘𝐵) ∈ Word dom
(iEdg‘𝐺)) →
((1st ‘𝐴)
= (1st ‘𝐵)
↔ ((#‘(1st ‘𝐴)) = (#‘(1st ‘𝐵)) ∧ ∀𝑥 ∈
(0..^(#‘(1st ‘𝐴)))((1st ‘𝐴)‘𝑥) = ((1st ‘𝐵)‘𝑥)))) |
34 | 33 | ad2ant2r 779 |
. . . . . . 7
⊢
((((1st ‘𝐴) ∈ Word dom (iEdg‘𝐺) ∧ (2nd
‘𝐴):(0...(#‘(1st ‘𝐴)))⟶(Vtx‘𝐺)) ∧ ((1st
‘𝐵) ∈ Word dom
(iEdg‘𝐺) ∧
(2nd ‘𝐵):(0...(#‘(1st ‘𝐵)))⟶(Vtx‘𝐺))) → ((1st
‘𝐴) = (1st
‘𝐵) ↔
((#‘(1st ‘𝐴)) = (#‘(1st ‘𝐵)) ∧ ∀𝑥 ∈
(0..^(#‘(1st ‘𝐴)))((1st ‘𝐴)‘𝑥) = ((1st ‘𝐵)‘𝑥)))) |
35 | 34 | adantr 480 |
. . . . . 6
⊢
(((((1st ‘𝐴) ∈ Word dom (iEdg‘𝐺) ∧ (2nd
‘𝐴):(0...(#‘(1st ‘𝐴)))⟶(Vtx‘𝐺)) ∧ ((1st
‘𝐵) ∈ Word dom
(iEdg‘𝐺) ∧
(2nd ‘𝐵):(0...(#‘(1st ‘𝐵)))⟶(Vtx‘𝐺))) ∧
((#‘(1st ‘𝐴)) = ((#‘(2nd ‘𝐴)) − 1) ∧
(#‘(1st ‘𝐵)) = ((#‘(2nd ‘𝐵)) − 1))) →
((1st ‘𝐴)
= (1st ‘𝐵)
↔ ((#‘(1st ‘𝐴)) = (#‘(1st ‘𝐵)) ∧ ∀𝑥 ∈
(0..^(#‘(1st ‘𝐴)))((1st ‘𝐴)‘𝑥) = ((1st ‘𝐵)‘𝑥)))) |
36 | | lencl 13179 |
. . . . . . . . . . 11
⊢
((1st ‘𝐴) ∈ Word dom (iEdg‘𝐺) →
(#‘(1st ‘𝐴)) ∈
ℕ0) |
37 | 36 | adantr 480 |
. . . . . . . . . 10
⊢
(((1st ‘𝐴) ∈ Word dom (iEdg‘𝐺) ∧ (2nd
‘𝐴):(0...(#‘(1st ‘𝐴)))⟶(Vtx‘𝐺)) →
(#‘(1st ‘𝐴)) ∈
ℕ0) |
38 | 37 | adantr 480 |
. . . . . . . . 9
⊢
((((1st ‘𝐴) ∈ Word dom (iEdg‘𝐺) ∧ (2nd
‘𝐴):(0...(#‘(1st ‘𝐴)))⟶(Vtx‘𝐺)) ∧ ((1st
‘𝐵) ∈ Word dom
(iEdg‘𝐺) ∧
(2nd ‘𝐵):(0...(#‘(1st ‘𝐵)))⟶(Vtx‘𝐺))) →
(#‘(1st ‘𝐴)) ∈
ℕ0) |
39 | | simplr 788 |
. . . . . . . . 9
⊢
((((1st ‘𝐴) ∈ Word dom (iEdg‘𝐺) ∧ (2nd
‘𝐴):(0...(#‘(1st ‘𝐴)))⟶(Vtx‘𝐺)) ∧ ((1st
‘𝐵) ∈ Word dom
(iEdg‘𝐺) ∧
(2nd ‘𝐵):(0...(#‘(1st ‘𝐵)))⟶(Vtx‘𝐺))) → (2nd
‘𝐴):(0...(#‘(1st ‘𝐴)))⟶(Vtx‘𝐺)) |
40 | | simprr 792 |
. . . . . . . . 9
⊢
((((1st ‘𝐴) ∈ Word dom (iEdg‘𝐺) ∧ (2nd
‘𝐴):(0...(#‘(1st ‘𝐴)))⟶(Vtx‘𝐺)) ∧ ((1st
‘𝐵) ∈ Word dom
(iEdg‘𝐺) ∧
(2nd ‘𝐵):(0...(#‘(1st ‘𝐵)))⟶(Vtx‘𝐺))) → (2nd
‘𝐵):(0...(#‘(1st ‘𝐵)))⟶(Vtx‘𝐺)) |
41 | 38, 39, 40 | 3jca 1235 |
. . . . . . . 8
⊢
((((1st ‘𝐴) ∈ Word dom (iEdg‘𝐺) ∧ (2nd
‘𝐴):(0...(#‘(1st ‘𝐴)))⟶(Vtx‘𝐺)) ∧ ((1st
‘𝐵) ∈ Word dom
(iEdg‘𝐺) ∧
(2nd ‘𝐵):(0...(#‘(1st ‘𝐵)))⟶(Vtx‘𝐺))) →
((#‘(1st ‘𝐴)) ∈ ℕ0 ∧
(2nd ‘𝐴):(0...(#‘(1st ‘𝐴)))⟶(Vtx‘𝐺) ∧ (2nd
‘𝐵):(0...(#‘(1st ‘𝐵)))⟶(Vtx‘𝐺))) |
42 | 41 | adantr 480 |
. . . . . . 7
⊢
(((((1st ‘𝐴) ∈ Word dom (iEdg‘𝐺) ∧ (2nd
‘𝐴):(0...(#‘(1st ‘𝐴)))⟶(Vtx‘𝐺)) ∧ ((1st
‘𝐵) ∈ Word dom
(iEdg‘𝐺) ∧
(2nd ‘𝐵):(0...(#‘(1st ‘𝐵)))⟶(Vtx‘𝐺))) ∧
((#‘(1st ‘𝐴)) = ((#‘(2nd ‘𝐴)) − 1) ∧
(#‘(1st ‘𝐵)) = ((#‘(2nd ‘𝐵)) − 1))) →
((#‘(1st ‘𝐴)) ∈ ℕ0 ∧
(2nd ‘𝐴):(0...(#‘(1st ‘𝐴)))⟶(Vtx‘𝐺) ∧ (2nd
‘𝐵):(0...(#‘(1st ‘𝐵)))⟶(Vtx‘𝐺))) |
43 | | 2ffzeq 12329 |
. . . . . . 7
⊢
(((#‘(1st ‘𝐴)) ∈ ℕ0 ∧
(2nd ‘𝐴):(0...(#‘(1st ‘𝐴)))⟶(Vtx‘𝐺) ∧ (2nd
‘𝐵):(0...(#‘(1st ‘𝐵)))⟶(Vtx‘𝐺)) → ((2nd
‘𝐴) = (2nd
‘𝐵) ↔
((#‘(1st ‘𝐴)) = (#‘(1st ‘𝐵)) ∧ ∀𝑥 ∈
(0...(#‘(1st ‘𝐴)))((2nd ‘𝐴)‘𝑥) = ((2nd ‘𝐵)‘𝑥)))) |
44 | 42, 43 | syl 17 |
. . . . . 6
⊢
(((((1st ‘𝐴) ∈ Word dom (iEdg‘𝐺) ∧ (2nd
‘𝐴):(0...(#‘(1st ‘𝐴)))⟶(Vtx‘𝐺)) ∧ ((1st
‘𝐵) ∈ Word dom
(iEdg‘𝐺) ∧
(2nd ‘𝐵):(0...(#‘(1st ‘𝐵)))⟶(Vtx‘𝐺))) ∧
((#‘(1st ‘𝐴)) = ((#‘(2nd ‘𝐴)) − 1) ∧
(#‘(1st ‘𝐵)) = ((#‘(2nd ‘𝐵)) − 1))) →
((2nd ‘𝐴)
= (2nd ‘𝐵)
↔ ((#‘(1st ‘𝐴)) = (#‘(1st ‘𝐵)) ∧ ∀𝑥 ∈
(0...(#‘(1st ‘𝐴)))((2nd ‘𝐴)‘𝑥) = ((2nd ‘𝐵)‘𝑥)))) |
45 | 35, 44 | anbi12d 743 |
. . . . 5
⊢
(((((1st ‘𝐴) ∈ Word dom (iEdg‘𝐺) ∧ (2nd
‘𝐴):(0...(#‘(1st ‘𝐴)))⟶(Vtx‘𝐺)) ∧ ((1st
‘𝐵) ∈ Word dom
(iEdg‘𝐺) ∧
(2nd ‘𝐵):(0...(#‘(1st ‘𝐵)))⟶(Vtx‘𝐺))) ∧
((#‘(1st ‘𝐴)) = ((#‘(2nd ‘𝐴)) − 1) ∧
(#‘(1st ‘𝐵)) = ((#‘(2nd ‘𝐵)) − 1))) →
(((1st ‘𝐴)
= (1st ‘𝐵)
∧ (2nd ‘𝐴) = (2nd ‘𝐵)) ↔ (((#‘(1st
‘𝐴)) =
(#‘(1st ‘𝐵)) ∧ ∀𝑥 ∈ (0..^(#‘(1st
‘𝐴)))((1st
‘𝐴)‘𝑥) = ((1st
‘𝐵)‘𝑥)) ∧
((#‘(1st ‘𝐴)) = (#‘(1st ‘𝐵)) ∧ ∀𝑥 ∈
(0...(#‘(1st ‘𝐴)))((2nd ‘𝐴)‘𝑥) = ((2nd ‘𝐵)‘𝑥))))) |
46 | 19, 32, 45 | syl2anc 691 |
. . . 4
⊢ ((𝐴 ∈ (1Walks‘𝐺) ∧ 𝐵 ∈ (1Walks‘𝐺)) → (((1st ‘𝐴) = (1st ‘𝐵) ∧ (2nd
‘𝐴) = (2nd
‘𝐵)) ↔
(((#‘(1st ‘𝐴)) = (#‘(1st ‘𝐵)) ∧ ∀𝑥 ∈
(0..^(#‘(1st ‘𝐴)))((1st ‘𝐴)‘𝑥) = ((1st ‘𝐵)‘𝑥)) ∧ ((#‘(1st
‘𝐴)) =
(#‘(1st ‘𝐵)) ∧ ∀𝑥 ∈ (0...(#‘(1st
‘𝐴)))((2nd
‘𝐴)‘𝑥) = ((2nd
‘𝐵)‘𝑥))))) |
47 | 46 | 3adant3 1074 |
. . 3
⊢ ((𝐴 ∈ (1Walks‘𝐺) ∧ 𝐵 ∈ (1Walks‘𝐺) ∧ 𝑁 = (#‘(1st ‘𝐴))) → (((1st
‘𝐴) = (1st
‘𝐵) ∧
(2nd ‘𝐴) =
(2nd ‘𝐵))
↔ (((#‘(1st ‘𝐴)) = (#‘(1st ‘𝐵)) ∧ ∀𝑥 ∈
(0..^(#‘(1st ‘𝐴)))((1st ‘𝐴)‘𝑥) = ((1st ‘𝐵)‘𝑥)) ∧ ((#‘(1st
‘𝐴)) =
(#‘(1st ‘𝐵)) ∧ ∀𝑥 ∈ (0...(#‘(1st
‘𝐴)))((2nd
‘𝐴)‘𝑥) = ((2nd
‘𝐵)‘𝑥))))) |
48 | | eqeq1 2614 |
. . . . . . 7
⊢ (𝑁 = (#‘(1st
‘𝐴)) → (𝑁 = (#‘(1st
‘𝐵)) ↔
(#‘(1st ‘𝐴)) = (#‘(1st ‘𝐵)))) |
49 | | oveq2 6557 |
. . . . . . . 8
⊢ (𝑁 = (#‘(1st
‘𝐴)) →
(0..^𝑁) =
(0..^(#‘(1st ‘𝐴)))) |
50 | 49 | raleqdv 3121 |
. . . . . . 7
⊢ (𝑁 = (#‘(1st
‘𝐴)) →
(∀𝑥 ∈
(0..^𝑁)((1st
‘𝐴)‘𝑥) = ((1st
‘𝐵)‘𝑥) ↔ ∀𝑥 ∈
(0..^(#‘(1st ‘𝐴)))((1st ‘𝐴)‘𝑥) = ((1st ‘𝐵)‘𝑥))) |
51 | 48, 50 | anbi12d 743 |
. . . . . 6
⊢ (𝑁 = (#‘(1st
‘𝐴)) → ((𝑁 = (#‘(1st
‘𝐵)) ∧
∀𝑥 ∈ (0..^𝑁)((1st ‘𝐴)‘𝑥) = ((1st ‘𝐵)‘𝑥)) ↔ ((#‘(1st
‘𝐴)) =
(#‘(1st ‘𝐵)) ∧ ∀𝑥 ∈ (0..^(#‘(1st
‘𝐴)))((1st
‘𝐴)‘𝑥) = ((1st
‘𝐵)‘𝑥)))) |
52 | | oveq2 6557 |
. . . . . . . 8
⊢ (𝑁 = (#‘(1st
‘𝐴)) →
(0...𝑁) =
(0...(#‘(1st ‘𝐴)))) |
53 | 52 | raleqdv 3121 |
. . . . . . 7
⊢ (𝑁 = (#‘(1st
‘𝐴)) →
(∀𝑥 ∈
(0...𝑁)((2nd
‘𝐴)‘𝑥) = ((2nd
‘𝐵)‘𝑥) ↔ ∀𝑥 ∈
(0...(#‘(1st ‘𝐴)))((2nd ‘𝐴)‘𝑥) = ((2nd ‘𝐵)‘𝑥))) |
54 | 48, 53 | anbi12d 743 |
. . . . . 6
⊢ (𝑁 = (#‘(1st
‘𝐴)) → ((𝑁 = (#‘(1st
‘𝐵)) ∧
∀𝑥 ∈ (0...𝑁)((2nd ‘𝐴)‘𝑥) = ((2nd ‘𝐵)‘𝑥)) ↔ ((#‘(1st
‘𝐴)) =
(#‘(1st ‘𝐵)) ∧ ∀𝑥 ∈ (0...(#‘(1st
‘𝐴)))((2nd
‘𝐴)‘𝑥) = ((2nd
‘𝐵)‘𝑥)))) |
55 | 51, 54 | anbi12d 743 |
. . . . 5
⊢ (𝑁 = (#‘(1st
‘𝐴)) → (((𝑁 = (#‘(1st
‘𝐵)) ∧
∀𝑥 ∈ (0..^𝑁)((1st ‘𝐴)‘𝑥) = ((1st ‘𝐵)‘𝑥)) ∧ (𝑁 = (#‘(1st ‘𝐵)) ∧ ∀𝑥 ∈ (0...𝑁)((2nd ‘𝐴)‘𝑥) = ((2nd ‘𝐵)‘𝑥))) ↔ (((#‘(1st
‘𝐴)) =
(#‘(1st ‘𝐵)) ∧ ∀𝑥 ∈ (0..^(#‘(1st
‘𝐴)))((1st
‘𝐴)‘𝑥) = ((1st
‘𝐵)‘𝑥)) ∧
((#‘(1st ‘𝐴)) = (#‘(1st ‘𝐵)) ∧ ∀𝑥 ∈
(0...(#‘(1st ‘𝐴)))((2nd ‘𝐴)‘𝑥) = ((2nd ‘𝐵)‘𝑥))))) |
56 | 55 | bibi2d 331 |
. . . 4
⊢ (𝑁 = (#‘(1st
‘𝐴)) →
((((1st ‘𝐴) = (1st ‘𝐵) ∧ (2nd ‘𝐴) = (2nd ‘𝐵)) ↔ ((𝑁 = (#‘(1st ‘𝐵)) ∧ ∀𝑥 ∈ (0..^𝑁)((1st ‘𝐴)‘𝑥) = ((1st ‘𝐵)‘𝑥)) ∧ (𝑁 = (#‘(1st ‘𝐵)) ∧ ∀𝑥 ∈ (0...𝑁)((2nd ‘𝐴)‘𝑥) = ((2nd ‘𝐵)‘𝑥)))) ↔ (((1st ‘𝐴) = (1st ‘𝐵) ∧ (2nd
‘𝐴) = (2nd
‘𝐵)) ↔
(((#‘(1st ‘𝐴)) = (#‘(1st ‘𝐵)) ∧ ∀𝑥 ∈
(0..^(#‘(1st ‘𝐴)))((1st ‘𝐴)‘𝑥) = ((1st ‘𝐵)‘𝑥)) ∧ ((#‘(1st
‘𝐴)) =
(#‘(1st ‘𝐵)) ∧ ∀𝑥 ∈ (0...(#‘(1st
‘𝐴)))((2nd
‘𝐴)‘𝑥) = ((2nd
‘𝐵)‘𝑥)))))) |
57 | 56 | 3ad2ant3 1077 |
. . 3
⊢ ((𝐴 ∈ (1Walks‘𝐺) ∧ 𝐵 ∈ (1Walks‘𝐺) ∧ 𝑁 = (#‘(1st ‘𝐴))) → ((((1st
‘𝐴) = (1st
‘𝐵) ∧
(2nd ‘𝐴) =
(2nd ‘𝐵))
↔ ((𝑁 =
(#‘(1st ‘𝐵)) ∧ ∀𝑥 ∈ (0..^𝑁)((1st ‘𝐴)‘𝑥) = ((1st ‘𝐵)‘𝑥)) ∧ (𝑁 = (#‘(1st ‘𝐵)) ∧ ∀𝑥 ∈ (0...𝑁)((2nd ‘𝐴)‘𝑥) = ((2nd ‘𝐵)‘𝑥)))) ↔ (((1st ‘𝐴) = (1st ‘𝐵) ∧ (2nd
‘𝐴) = (2nd
‘𝐵)) ↔
(((#‘(1st ‘𝐴)) = (#‘(1st ‘𝐵)) ∧ ∀𝑥 ∈
(0..^(#‘(1st ‘𝐴)))((1st ‘𝐴)‘𝑥) = ((1st ‘𝐵)‘𝑥)) ∧ ((#‘(1st
‘𝐴)) =
(#‘(1st ‘𝐵)) ∧ ∀𝑥 ∈ (0...(#‘(1st
‘𝐴)))((2nd
‘𝐴)‘𝑥) = ((2nd
‘𝐵)‘𝑥)))))) |
58 | 47, 57 | mpbird 246 |
. 2
⊢ ((𝐴 ∈ (1Walks‘𝐺) ∧ 𝐵 ∈ (1Walks‘𝐺) ∧ 𝑁 = (#‘(1st ‘𝐴))) → (((1st
‘𝐴) = (1st
‘𝐵) ∧
(2nd ‘𝐴) =
(2nd ‘𝐵))
↔ ((𝑁 =
(#‘(1st ‘𝐵)) ∧ ∀𝑥 ∈ (0..^𝑁)((1st ‘𝐴)‘𝑥) = ((1st ‘𝐵)‘𝑥)) ∧ (𝑁 = (#‘(1st ‘𝐵)) ∧ ∀𝑥 ∈ (0...𝑁)((2nd ‘𝐴)‘𝑥) = ((2nd ‘𝐵)‘𝑥))))) |
59 | | 3anass 1035 |
. . . 4
⊢ ((𝑁 = (#‘(1st
‘𝐵)) ∧
∀𝑥 ∈ (0..^𝑁)((1st ‘𝐴)‘𝑥) = ((1st ‘𝐵)‘𝑥) ∧ ∀𝑥 ∈ (0...𝑁)((2nd ‘𝐴)‘𝑥) = ((2nd ‘𝐵)‘𝑥)) ↔ (𝑁 = (#‘(1st ‘𝐵)) ∧ (∀𝑥 ∈ (0..^𝑁)((1st ‘𝐴)‘𝑥) = ((1st ‘𝐵)‘𝑥) ∧ ∀𝑥 ∈ (0...𝑁)((2nd ‘𝐴)‘𝑥) = ((2nd ‘𝐵)‘𝑥)))) |
60 | | anandi 867 |
. . . 4
⊢ ((𝑁 = (#‘(1st
‘𝐵)) ∧
(∀𝑥 ∈
(0..^𝑁)((1st
‘𝐴)‘𝑥) = ((1st
‘𝐵)‘𝑥) ∧ ∀𝑥 ∈ (0...𝑁)((2nd ‘𝐴)‘𝑥) = ((2nd ‘𝐵)‘𝑥))) ↔ ((𝑁 = (#‘(1st ‘𝐵)) ∧ ∀𝑥 ∈ (0..^𝑁)((1st ‘𝐴)‘𝑥) = ((1st ‘𝐵)‘𝑥)) ∧ (𝑁 = (#‘(1st ‘𝐵)) ∧ ∀𝑥 ∈ (0...𝑁)((2nd ‘𝐴)‘𝑥) = ((2nd ‘𝐵)‘𝑥)))) |
61 | 59, 60 | bitr2i 264 |
. . 3
⊢ (((𝑁 = (#‘(1st
‘𝐵)) ∧
∀𝑥 ∈ (0..^𝑁)((1st ‘𝐴)‘𝑥) = ((1st ‘𝐵)‘𝑥)) ∧ (𝑁 = (#‘(1st ‘𝐵)) ∧ ∀𝑥 ∈ (0...𝑁)((2nd ‘𝐴)‘𝑥) = ((2nd ‘𝐵)‘𝑥))) ↔ (𝑁 = (#‘(1st ‘𝐵)) ∧ ∀𝑥 ∈ (0..^𝑁)((1st ‘𝐴)‘𝑥) = ((1st ‘𝐵)‘𝑥) ∧ ∀𝑥 ∈ (0...𝑁)((2nd ‘𝐴)‘𝑥) = ((2nd ‘𝐵)‘𝑥))) |
62 | 61 | a1i 11 |
. 2
⊢ ((𝐴 ∈ (1Walks‘𝐺) ∧ 𝐵 ∈ (1Walks‘𝐺) ∧ 𝑁 = (#‘(1st ‘𝐴))) → (((𝑁 = (#‘(1st ‘𝐵)) ∧ ∀𝑥 ∈ (0..^𝑁)((1st ‘𝐴)‘𝑥) = ((1st ‘𝐵)‘𝑥)) ∧ (𝑁 = (#‘(1st ‘𝐵)) ∧ ∀𝑥 ∈ (0...𝑁)((2nd ‘𝐴)‘𝑥) = ((2nd ‘𝐵)‘𝑥))) ↔ (𝑁 = (#‘(1st ‘𝐵)) ∧ ∀𝑥 ∈ (0..^𝑁)((1st ‘𝐴)‘𝑥) = ((1st ‘𝐵)‘𝑥) ∧ ∀𝑥 ∈ (0...𝑁)((2nd ‘𝐴)‘𝑥) = ((2nd ‘𝐵)‘𝑥)))) |
63 | 10, 58, 62 | 3bitrd 293 |
1
⊢ ((𝐴 ∈ (1Walks‘𝐺) ∧ 𝐵 ∈ (1Walks‘𝐺) ∧ 𝑁 = (#‘(1st ‘𝐴))) → (𝐴 = 𝐵 ↔ (𝑁 = (#‘(1st ‘𝐵)) ∧ ∀𝑥 ∈ (0..^𝑁)((1st ‘𝐴)‘𝑥) = ((1st ‘𝐵)‘𝑥) ∧ ∀𝑥 ∈ (0...𝑁)((2nd ‘𝐴)‘𝑥) = ((2nd ‘𝐵)‘𝑥)))) |