Proof of Theorem spthonepeq-av
Step | Hyp | Ref
| Expression |
1 | | eqid 2610 |
. . 3
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
2 | 1 | spthonprop 40951 |
. 2
⊢ (𝐹(𝐴(SPathsOn‘𝐺)𝐵)𝑃 → ((𝐺 ∈ V ∧ 𝐴 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺)) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐹(𝐴(TrailsOn‘𝐺)𝐵)𝑃 ∧ 𝐹(SPathS‘𝐺)𝑃))) |
3 | 1 | istrlson 40914 |
. . . . . 6
⊢ (((𝐴 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺)) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → (𝐹(𝐴(TrailsOn‘𝐺)𝐵)𝑃 ↔ (𝐹(𝐴(WalksOn‘𝐺)𝐵)𝑃 ∧ 𝐹(TrailS‘𝐺)𝑃))) |
4 | 3 | 3adantl1 1210 |
. . . . 5
⊢ (((𝐺 ∈ V ∧ 𝐴 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺)) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → (𝐹(𝐴(TrailsOn‘𝐺)𝐵)𝑃 ↔ (𝐹(𝐴(WalksOn‘𝐺)𝐵)𝑃 ∧ 𝐹(TrailS‘𝐺)𝑃))) |
5 | | simp1 1054 |
. . . . . . . 8
⊢ ((𝐺 ∈ V ∧ 𝐴 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺)) → 𝐺 ∈ V) |
6 | 5 | anim1i 590 |
. . . . . . 7
⊢ (((𝐺 ∈ V ∧ 𝐴 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺)) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → (𝐺 ∈ V ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V))) |
7 | | 3anass 1035 |
. . . . . . 7
⊢ ((𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V) ↔ (𝐺 ∈ V ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V))) |
8 | 6, 7 | sylibr 223 |
. . . . . 6
⊢ (((𝐺 ∈ V ∧ 𝐴 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺)) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → (𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V)) |
9 | | issPth 40930 |
. . . . . 6
⊢ ((𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V) → (𝐹(SPathS‘𝐺)𝑃 ↔ (𝐹(TrailS‘𝐺)𝑃 ∧ Fun ◡𝑃))) |
10 | 8, 9 | syl 17 |
. . . . 5
⊢ (((𝐺 ∈ V ∧ 𝐴 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺)) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → (𝐹(SPathS‘𝐺)𝑃 ↔ (𝐹(TrailS‘𝐺)𝑃 ∧ Fun ◡𝑃))) |
11 | 4, 10 | anbi12d 743 |
. . . 4
⊢ (((𝐺 ∈ V ∧ 𝐴 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺)) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → ((𝐹(𝐴(TrailsOn‘𝐺)𝐵)𝑃 ∧ 𝐹(SPathS‘𝐺)𝑃) ↔ ((𝐹(𝐴(WalksOn‘𝐺)𝐵)𝑃 ∧ 𝐹(TrailS‘𝐺)𝑃) ∧ (𝐹(TrailS‘𝐺)𝑃 ∧ Fun ◡𝑃)))) |
12 | 1 | wlkOnprop 40866 |
. . . . . . . 8
⊢ (𝐹(𝐴(WalksOn‘𝐺)𝐵)𝑃 → ((𝐺 ∈ V ∧ 𝐴 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺)) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐹(1Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵))) |
13 | | 1wlkcl 40820 |
. . . . . . . . . . . . 13
⊢ (𝐹(1Walks‘𝐺)𝑃 → (#‘𝐹) ∈
ℕ0) |
14 | 1 | 1wlkp 40821 |
. . . . . . . . . . . . 13
⊢ (𝐹(1Walks‘𝐺)𝑃 → 𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺)) |
15 | | df-f1 5809 |
. . . . . . . . . . . . . . . 16
⊢ (𝑃:(0...(#‘𝐹))–1-1→(Vtx‘𝐺) ↔ (𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ∧ Fun ◡𝑃)) |
16 | | eqeq2 2621 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐴 = 𝐵 → ((𝑃‘0) = 𝐴 ↔ (𝑃‘0) = 𝐵)) |
17 | | eqtr3 2631 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑃‘(#‘𝐹)) = 𝐵 ∧ (𝑃‘0) = 𝐵) → (𝑃‘(#‘𝐹)) = (𝑃‘0)) |
18 | | elnn0uz 11601 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((#‘𝐹) ∈
ℕ0 ↔ (#‘𝐹) ∈
(ℤ≥‘0)) |
19 | | eluzfz2 12220 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((#‘𝐹) ∈
(ℤ≥‘0) → (#‘𝐹) ∈ (0...(#‘𝐹))) |
20 | 18, 19 | sylbi 206 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((#‘𝐹) ∈
ℕ0 → (#‘𝐹) ∈ (0...(#‘𝐹))) |
21 | | 0elfz 12305 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((#‘𝐹) ∈
ℕ0 → 0 ∈ (0...(#‘𝐹))) |
22 | 20, 21 | jca 553 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((#‘𝐹) ∈
ℕ0 → ((#‘𝐹) ∈ (0...(#‘𝐹)) ∧ 0 ∈ (0...(#‘𝐹)))) |
23 | | f1veqaeq 6418 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑃:(0...(#‘𝐹))–1-1→(Vtx‘𝐺) ∧ ((#‘𝐹) ∈ (0...(#‘𝐹)) ∧ 0 ∈ (0...(#‘𝐹)))) → ((𝑃‘(#‘𝐹)) = (𝑃‘0) → (#‘𝐹) = 0)) |
24 | 22, 23 | sylan2 490 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑃:(0...(#‘𝐹))–1-1→(Vtx‘𝐺) ∧ (#‘𝐹) ∈ ℕ0) → ((𝑃‘(#‘𝐹)) = (𝑃‘0) → (#‘𝐹) = 0)) |
25 | 24 | ex 449 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑃:(0...(#‘𝐹))–1-1→(Vtx‘𝐺) → ((#‘𝐹) ∈ ℕ0 → ((𝑃‘(#‘𝐹)) = (𝑃‘0) → (#‘𝐹) = 0))) |
26 | 25 | com13 86 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑃‘(#‘𝐹)) = (𝑃‘0) → ((#‘𝐹) ∈ ℕ0 → (𝑃:(0...(#‘𝐹))–1-1→(Vtx‘𝐺) → (#‘𝐹) = 0))) |
27 | 17, 26 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑃‘(#‘𝐹)) = 𝐵 ∧ (𝑃‘0) = 𝐵) → ((#‘𝐹) ∈ ℕ0 → (𝑃:(0...(#‘𝐹))–1-1→(Vtx‘𝐺) → (#‘𝐹) = 0))) |
28 | 27 | expcom 450 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑃‘0) = 𝐵 → ((𝑃‘(#‘𝐹)) = 𝐵 → ((#‘𝐹) ∈ ℕ0 → (𝑃:(0...(#‘𝐹))–1-1→(Vtx‘𝐺) → (#‘𝐹) = 0)))) |
29 | 16, 28 | syl6bi 242 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 = 𝐵 → ((𝑃‘0) = 𝐴 → ((𝑃‘(#‘𝐹)) = 𝐵 → ((#‘𝐹) ∈ ℕ0 → (𝑃:(0...(#‘𝐹))–1-1→(Vtx‘𝐺) → (#‘𝐹) = 0))))) |
30 | 29 | com15 99 |
. . . . . . . . . . . . . . . 16
⊢ (𝑃:(0...(#‘𝐹))–1-1→(Vtx‘𝐺) → ((𝑃‘0) = 𝐴 → ((𝑃‘(#‘𝐹)) = 𝐵 → ((#‘𝐹) ∈ ℕ0 → (𝐴 = 𝐵 → (#‘𝐹) = 0))))) |
31 | 15, 30 | sylbir 224 |
. . . . . . . . . . . . . . 15
⊢ ((𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ∧ Fun ◡𝑃) → ((𝑃‘0) = 𝐴 → ((𝑃‘(#‘𝐹)) = 𝐵 → ((#‘𝐹) ∈ ℕ0 → (𝐴 = 𝐵 → (#‘𝐹) = 0))))) |
32 | 31 | expcom 450 |
. . . . . . . . . . . . . 14
⊢ (Fun
◡𝑃 → (𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) → ((𝑃‘0) = 𝐴 → ((𝑃‘(#‘𝐹)) = 𝐵 → ((#‘𝐹) ∈ ℕ0 → (𝐴 = 𝐵 → (#‘𝐹) = 0)))))) |
33 | 32 | com15 99 |
. . . . . . . . . . . . 13
⊢
((#‘𝐹) ∈
ℕ0 → (𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) → ((𝑃‘0) = 𝐴 → ((𝑃‘(#‘𝐹)) = 𝐵 → (Fun ◡𝑃 → (𝐴 = 𝐵 → (#‘𝐹) = 0)))))) |
34 | 13, 14, 33 | sylc 63 |
. . . . . . . . . . . 12
⊢ (𝐹(1Walks‘𝐺)𝑃 → ((𝑃‘0) = 𝐴 → ((𝑃‘(#‘𝐹)) = 𝐵 → (Fun ◡𝑃 → (𝐴 = 𝐵 → (#‘𝐹) = 0))))) |
35 | 34 | 3imp1 1272 |
. . . . . . . . . . 11
⊢ (((𝐹(1Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵) ∧ Fun ◡𝑃) → (𝐴 = 𝐵 → (#‘𝐹) = 0)) |
36 | | fveq2 6103 |
. . . . . . . . . . . . . . . . 17
⊢
((#‘𝐹) = 0
→ (𝑃‘(#‘𝐹)) = (𝑃‘0)) |
37 | 36 | eqeq1d 2612 |
. . . . . . . . . . . . . . . 16
⊢
((#‘𝐹) = 0
→ ((𝑃‘(#‘𝐹)) = 𝐵 ↔ (𝑃‘0) = 𝐵)) |
38 | 37 | anbi2d 736 |
. . . . . . . . . . . . . . 15
⊢
((#‘𝐹) = 0
→ (((𝑃‘0) =
𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵) ↔ ((𝑃‘0) = 𝐴 ∧ (𝑃‘0) = 𝐵))) |
39 | | eqtr2 2630 |
. . . . . . . . . . . . . . 15
⊢ (((𝑃‘0) = 𝐴 ∧ (𝑃‘0) = 𝐵) → 𝐴 = 𝐵) |
40 | 38, 39 | syl6bi 242 |
. . . . . . . . . . . . . 14
⊢
((#‘𝐹) = 0
→ (((𝑃‘0) =
𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵) → 𝐴 = 𝐵)) |
41 | 40 | com12 32 |
. . . . . . . . . . . . 13
⊢ (((𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵) → ((#‘𝐹) = 0 → 𝐴 = 𝐵)) |
42 | 41 | 3adant1 1072 |
. . . . . . . . . . . 12
⊢ ((𝐹(1Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵) → ((#‘𝐹) = 0 → 𝐴 = 𝐵)) |
43 | 42 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝐹(1Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵) ∧ Fun ◡𝑃) → ((#‘𝐹) = 0 → 𝐴 = 𝐵)) |
44 | 35, 43 | impbid 201 |
. . . . . . . . . 10
⊢ (((𝐹(1Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵) ∧ Fun ◡𝑃) → (𝐴 = 𝐵 ↔ (#‘𝐹) = 0)) |
45 | 44 | ex 449 |
. . . . . . . . 9
⊢ ((𝐹(1Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵) → (Fun ◡𝑃 → (𝐴 = 𝐵 ↔ (#‘𝐹) = 0))) |
46 | 45 | 3ad2ant3 1077 |
. . . . . . . 8
⊢ (((𝐺 ∈ V ∧ 𝐴 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺)) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐹(1Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵)) → (Fun ◡𝑃 → (𝐴 = 𝐵 ↔ (#‘𝐹) = 0))) |
47 | 12, 46 | syl 17 |
. . . . . . 7
⊢ (𝐹(𝐴(WalksOn‘𝐺)𝐵)𝑃 → (Fun ◡𝑃 → (𝐴 = 𝐵 ↔ (#‘𝐹) = 0))) |
48 | 47 | adantld 482 |
. . . . . 6
⊢ (𝐹(𝐴(WalksOn‘𝐺)𝐵)𝑃 → ((𝐹(TrailS‘𝐺)𝑃 ∧ Fun ◡𝑃) → (𝐴 = 𝐵 ↔ (#‘𝐹) = 0))) |
49 | 48 | adantr 480 |
. . . . 5
⊢ ((𝐹(𝐴(WalksOn‘𝐺)𝐵)𝑃 ∧ 𝐹(TrailS‘𝐺)𝑃) → ((𝐹(TrailS‘𝐺)𝑃 ∧ Fun ◡𝑃) → (𝐴 = 𝐵 ↔ (#‘𝐹) = 0))) |
50 | 49 | imp 444 |
. . . 4
⊢ (((𝐹(𝐴(WalksOn‘𝐺)𝐵)𝑃 ∧ 𝐹(TrailS‘𝐺)𝑃) ∧ (𝐹(TrailS‘𝐺)𝑃 ∧ Fun ◡𝑃)) → (𝐴 = 𝐵 ↔ (#‘𝐹) = 0)) |
51 | 11, 50 | syl6bi 242 |
. . 3
⊢ (((𝐺 ∈ V ∧ 𝐴 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺)) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → ((𝐹(𝐴(TrailsOn‘𝐺)𝐵)𝑃 ∧ 𝐹(SPathS‘𝐺)𝑃) → (𝐴 = 𝐵 ↔ (#‘𝐹) = 0))) |
52 | 51 | 3impia 1253 |
. 2
⊢ (((𝐺 ∈ V ∧ 𝐴 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺)) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐹(𝐴(TrailsOn‘𝐺)𝐵)𝑃 ∧ 𝐹(SPathS‘𝐺)𝑃)) → (𝐴 = 𝐵 ↔ (#‘𝐹) = 0)) |
53 | 2, 52 | syl 17 |
1
⊢ (𝐹(𝐴(SPathsOn‘𝐺)𝐵)𝑃 → (𝐴 = 𝐵 ↔ (#‘𝐹) = 0)) |