Metamath Proof Explorer

Theorem uhgrwkspthlem2

Description: Lemma 2 for uhgrwkspth . (Contributed by AV, 25-Jan-2021)

Ref Expression
Assertion uhgrwkspthlem2 ⊢ F Walks ⁡ G P ∧ F = 1 ∧ A ≠ B ∧ P ⁡ 0 = A ∧ P ⁡ F = B → Fun ⁡ P -1

Proof

Step Hyp Ref Expression
1 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
2 1 wlkp ⊢ F Walks ⁡ G P → P : 0 … F ⟶ Vtx ⁡ G
3 oveq2 ⊢ F = 1 → 0 … F = 0 … 1
4 fz01pr ⊢ 0 … 1 = 0 1
5 3 4 eqtrdi ⊢ F = 1 → 0 … F = 0 1
6 5 feq2d ⊢ F = 1 → P : 0 … F ⟶ Vtx ⁡ G ↔ P : 0 1 ⟶ Vtx ⁡ G
7 6 adantr ⊢ F = 1 ∧ P ⁡ 0 = A ∧ P ⁡ F = B → P : 0 … F ⟶ Vtx ⁡ G ↔ P : 0 1 ⟶ Vtx ⁡ G
8 simpl ⊢ P ⁡ 0 = A ∧ P ⁡ F = B → P ⁡ 0 = A
9 simpr ⊢ P ⁡ 0 = A ∧ P ⁡ F = B → P ⁡ F = B
10 8 9 neeq12d ⊢ P ⁡ 0 = A ∧ P ⁡ F = B → P ⁡ 0 ≠ P ⁡ F ↔ A ≠ B
11 10 bicomd ⊢ P ⁡ 0 = A ∧ P ⁡ F = B → A ≠ B ↔ P ⁡ 0 ≠ P ⁡ F
12 fveq2 ⊢ F = 1 → P ⁡ F = P ⁡ 1
13 12 neeq2d ⊢ F = 1 → P ⁡ 0 ≠ P ⁡ F ↔ P ⁡ 0 ≠ P ⁡ 1
14 11 13 sylan9bbr ⊢ F = 1 ∧ P ⁡ 0 = A ∧ P ⁡ F = B → A ≠ B ↔ P ⁡ 0 ≠ P ⁡ 1
15 7 14 anbi12d ⊢ F = 1 ∧ P ⁡ 0 = A ∧ P ⁡ F = B → P : 0 … F ⟶ Vtx ⁡ G ∧ A ≠ B ↔ P : 0 1 ⟶ Vtx ⁡ G ∧ P ⁡ 0 ≠ P ⁡ 1
16 0z ⊢ 0 ∈ ℤ
17 1z ⊢ 1 ∈ ℤ
18 fpr2g ⊢ 0 ∈ ℤ ∧ 1 ∈ ℤ → P : 0 1 ⟶ Vtx ⁡ G ↔ P ⁡ 0 ∈ Vtx ⁡ G ∧ P ⁡ 1 ∈ Vtx ⁡ G ∧ P = 0 P ⁡ 0 1 P ⁡ 1
19 16 17 18 mp2an ⊢ P : 0 1 ⟶ Vtx ⁡ G ↔ P ⁡ 0 ∈ Vtx ⁡ G ∧ P ⁡ 1 ∈ Vtx ⁡ G ∧ P = 0 P ⁡ 0 1 P ⁡ 1
20 funcnvs2 ⊢ P ⁡ 0 ∈ Vtx ⁡ G ∧ P ⁡ 1 ∈ Vtx ⁡ G ∧ P ⁡ 0 ≠ P ⁡ 1 → Fun ⁡ ⟨“ P ⁡ 0 P ⁡ 1 ”⟩ -1
21 20 3expa ⊢ P ⁡ 0 ∈ Vtx ⁡ G ∧ P ⁡ 1 ∈ Vtx ⁡ G ∧ P ⁡ 0 ≠ P ⁡ 1 → Fun ⁡ ⟨“ P ⁡ 0 P ⁡ 1 ”⟩ -1
22 21 adantl ⊢ P = 0 P ⁡ 0 1 P ⁡ 1 ∧ P ⁡ 0 ∈ Vtx ⁡ G ∧ P ⁡ 1 ∈ Vtx ⁡ G ∧ P ⁡ 0 ≠ P ⁡ 1 → Fun ⁡ ⟨“ P ⁡ 0 P ⁡ 1 ”⟩ -1
23 simpl ⊢ P = 0 P ⁡ 0 1 P ⁡ 1 ∧ P ⁡ 0 ∈ Vtx ⁡ G ∧ P ⁡ 1 ∈ Vtx ⁡ G ∧ P ⁡ 0 ≠ P ⁡ 1 → P = 0 P ⁡ 0 1 P ⁡ 1
24 s2prop ⊢ P ⁡ 0 ∈ Vtx ⁡ G ∧ P ⁡ 1 ∈ Vtx ⁡ G → ⟨“ P ⁡ 0 P ⁡ 1 ”⟩ = 0 P ⁡ 0 1 P ⁡ 1
25 24 eqcomd ⊢ P ⁡ 0 ∈ Vtx ⁡ G ∧ P ⁡ 1 ∈ Vtx ⁡ G → 0 P ⁡ 0 1 P ⁡ 1 = ⟨“ P ⁡ 0 P ⁡ 1 ”⟩
26 25 adantr ⊢ P ⁡ 0 ∈ Vtx ⁡ G ∧ P ⁡ 1 ∈ Vtx ⁡ G ∧ P ⁡ 0 ≠ P ⁡ 1 → 0 P ⁡ 0 1 P ⁡ 1 = ⟨“ P ⁡ 0 P ⁡ 1 ”⟩
27 26 adantl ⊢ P = 0 P ⁡ 0 1 P ⁡ 1 ∧ P ⁡ 0 ∈ Vtx ⁡ G ∧ P ⁡ 1 ∈ Vtx ⁡ G ∧ P ⁡ 0 ≠ P ⁡ 1 → 0 P ⁡ 0 1 P ⁡ 1 = ⟨“ P ⁡ 0 P ⁡ 1 ”⟩
28 23 27 eqtrd ⊢ P = 0 P ⁡ 0 1 P ⁡ 1 ∧ P ⁡ 0 ∈ Vtx ⁡ G ∧ P ⁡ 1 ∈ Vtx ⁡ G ∧ P ⁡ 0 ≠ P ⁡ 1 → P = ⟨“ P ⁡ 0 P ⁡ 1 ”⟩
29 28 cnveqd ⊢ P = 0 P ⁡ 0 1 P ⁡ 1 ∧ P ⁡ 0 ∈ Vtx ⁡ G ∧ P ⁡ 1 ∈ Vtx ⁡ G ∧ P ⁡ 0 ≠ P ⁡ 1 → P -1 = ⟨“ P ⁡ 0 P ⁡ 1 ”⟩ -1
30 29 funeqd ⊢ P = 0 P ⁡ 0 1 P ⁡ 1 ∧ P ⁡ 0 ∈ Vtx ⁡ G ∧ P ⁡ 1 ∈ Vtx ⁡ G ∧ P ⁡ 0 ≠ P ⁡ 1 → Fun ⁡ P -1 ↔ Fun ⁡ ⟨“ P ⁡ 0 P ⁡ 1 ”⟩ -1
31 22 30 mpbird ⊢ P = 0 P ⁡ 0 1 P ⁡ 1 ∧ P ⁡ 0 ∈ Vtx ⁡ G ∧ P ⁡ 1 ∈ Vtx ⁡ G ∧ P ⁡ 0 ≠ P ⁡ 1 → Fun ⁡ P -1
32 31 exp32 ⊢ P = 0 P ⁡ 0 1 P ⁡ 1 → P ⁡ 0 ∈ Vtx ⁡ G ∧ P ⁡ 1 ∈ Vtx ⁡ G → P ⁡ 0 ≠ P ⁡ 1 → Fun ⁡ P -1
33 32 impcom ⊢ P ⁡ 0 ∈ Vtx ⁡ G ∧ P ⁡ 1 ∈ Vtx ⁡ G ∧ P = 0 P ⁡ 0 1 P ⁡ 1 → P ⁡ 0 ≠ P ⁡ 1 → Fun ⁡ P -1
34 33 3impa ⊢ P ⁡ 0 ∈ Vtx ⁡ G ∧ P ⁡ 1 ∈ Vtx ⁡ G ∧ P = 0 P ⁡ 0 1 P ⁡ 1 → P ⁡ 0 ≠ P ⁡ 1 → Fun ⁡ P -1
35 19 34 sylbi ⊢ P : 0 1 ⟶ Vtx ⁡ G → P ⁡ 0 ≠ P ⁡ 1 → Fun ⁡ P -1
36 35 imp ⊢ P : 0 1 ⟶ Vtx ⁡ G ∧ P ⁡ 0 ≠ P ⁡ 1 → Fun ⁡ P -1
37 15 36 biimtrdi ⊢ F = 1 ∧ P ⁡ 0 = A ∧ P ⁡ F = B → P : 0 … F ⟶ Vtx ⁡ G ∧ A ≠ B → Fun ⁡ P -1
38 37 expd ⊢ F = 1 ∧ P ⁡ 0 = A ∧ P ⁡ F = B → P : 0 … F ⟶ Vtx ⁡ G → A ≠ B → Fun ⁡ P -1
39 38 com12 ⊢ P : 0 … F ⟶ Vtx ⁡ G → F = 1 ∧ P ⁡ 0 = A ∧ P ⁡ F = B → A ≠ B → Fun ⁡ P -1
40 39 expd ⊢ P : 0 … F ⟶ Vtx ⁡ G → F = 1 → P ⁡ 0 = A ∧ P ⁡ F = B → A ≠ B → Fun ⁡ P -1
41 40 com34 ⊢ P : 0 … F ⟶ Vtx ⁡ G → F = 1 → A ≠ B → P ⁡ 0 = A ∧ P ⁡ F = B → Fun ⁡ P -1
42 41 impd ⊢ P : 0 … F ⟶ Vtx ⁡ G → F = 1 ∧ A ≠ B → P ⁡ 0 = A ∧ P ⁡ F = B → Fun ⁡ P -1
43 2 42 syl ⊢ F Walks ⁡ G P → F = 1 ∧ A ≠ B → P ⁡ 0 = A ∧ P ⁡ F = B → Fun ⁡ P -1
44 43 3imp ⊢ F Walks ⁡ G P ∧ F = 1 ∧ A ≠ B ∧ P ⁡ 0 = A ∧ P ⁡ F = B → Fun ⁡ P -1