Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  1wlkp1lem6 Structured version   Visualization version   GIF version

Theorem 1wlkp1lem6 40882
Description: Lemma for 1wlkp1 40885. (Contributed by AV, 6-Mar-2021.)
Hypotheses
Ref Expression
1wlkp1.v 𝑉 = (Vtx‘𝐺)
1wlkp1.i 𝐼 = (iEdg‘𝐺)
1wlkp1.f (𝜑 → Fun 𝐼)
1wlkp1.a (𝜑𝐼 ∈ Fin)
1wlkp1.b (𝜑𝐵 ∈ V)
1wlkp1.c (𝜑𝐶𝑉)
1wlkp1.d (𝜑 → ¬ 𝐵 ∈ dom 𝐼)
1wlkp1.w (𝜑𝐹(1Walks‘𝐺)𝑃)
1wlkp1.n 𝑁 = (#‘𝐹)
1wlkp1.e (𝜑𝐸 ∈ (Edg‘𝐺))
1wlkp1.x (𝜑 → {(𝑃𝑁), 𝐶} ⊆ 𝐸)
1wlkp1.u (𝜑 → (iEdg‘𝑆) = (𝐼 ∪ {⟨𝐵, 𝐸⟩}))
1wlkp1.h 𝐻 = (𝐹 ∪ {⟨𝑁, 𝐵⟩})
1wlkp1.q 𝑄 = (𝑃 ∪ {⟨(𝑁 + 1), 𝐶⟩})
1wlkp1.s (𝜑 → (Vtx‘𝑆) = 𝑉)
Assertion
Ref Expression
1wlkp1lem6 (𝜑 → ∀𝑘 ∈ (0..^𝑁)((𝑄𝑘) = (𝑃𝑘) ∧ (𝑄‘(𝑘 + 1)) = (𝑃‘(𝑘 + 1)) ∧ ((iEdg‘𝑆)‘(𝐻𝑘)) = (𝐼‘(𝐹𝑘))))
Distinct variable group:   𝜑,𝑘
Allowed substitution hints:   𝐵(𝑘)   𝐶(𝑘)   𝑃(𝑘)   𝑄(𝑘)   𝑆(𝑘)   𝐸(𝑘)   𝐹(𝑘)   𝐺(𝑘)   𝐻(𝑘)   𝐼(𝑘)   𝑁(𝑘)   𝑉(𝑘)

Proof of Theorem 1wlkp1lem6
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 1wlkp1.v . . . 4 𝑉 = (Vtx‘𝐺)
2 1wlkp1.i . . . 4 𝐼 = (iEdg‘𝐺)
3 1wlkp1.f . . . 4 (𝜑 → Fun 𝐼)
4 1wlkp1.a . . . 4 (𝜑𝐼 ∈ Fin)
5 1wlkp1.b . . . 4 (𝜑𝐵 ∈ V)
6 1wlkp1.c . . . 4 (𝜑𝐶𝑉)
7 1wlkp1.d . . . 4 (𝜑 → ¬ 𝐵 ∈ dom 𝐼)
8 1wlkp1.w . . . 4 (𝜑𝐹(1Walks‘𝐺)𝑃)
9 1wlkp1.n . . . 4 𝑁 = (#‘𝐹)
10 1wlkp1.e . . . 4 (𝜑𝐸 ∈ (Edg‘𝐺))
11 1wlkp1.x . . . 4 (𝜑 → {(𝑃𝑁), 𝐶} ⊆ 𝐸)
12 1wlkp1.u . . . 4 (𝜑 → (iEdg‘𝑆) = (𝐼 ∪ {⟨𝐵, 𝐸⟩}))
13 1wlkp1.h . . . 4 𝐻 = (𝐹 ∪ {⟨𝑁, 𝐵⟩})
14 1wlkp1.q . . . 4 𝑄 = (𝑃 ∪ {⟨(𝑁 + 1), 𝐶⟩})
15 1wlkp1.s . . . 4 (𝜑 → (Vtx‘𝑆) = 𝑉)
161, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 151wlkp1lem5 40881 . . 3 (𝜑 → ∀𝑥 ∈ (0...𝑁)(𝑄𝑥) = (𝑃𝑥))
17 elfzofz 12309 . . . . . . 7 (𝑘 ∈ (0..^𝑁) → 𝑘 ∈ (0...𝑁))
1817adantl 480 . . . . . 6 ((𝜑𝑘 ∈ (0..^𝑁)) → 𝑘 ∈ (0...𝑁))
19 fveq2 6088 . . . . . . . 8 (𝑥 = 𝑘 → (𝑄𝑥) = (𝑄𝑘))
20 fveq2 6088 . . . . . . . 8 (𝑥 = 𝑘 → (𝑃𝑥) = (𝑃𝑘))
2119, 20eqeq12d 2624 . . . . . . 7 (𝑥 = 𝑘 → ((𝑄𝑥) = (𝑃𝑥) ↔ (𝑄𝑘) = (𝑃𝑘)))
2221rspcv 3277 . . . . . 6 (𝑘 ∈ (0...𝑁) → (∀𝑥 ∈ (0...𝑁)(𝑄𝑥) = (𝑃𝑥) → (𝑄𝑘) = (𝑃𝑘)))
2318, 22syl 17 . . . . 5 ((𝜑𝑘 ∈ (0..^𝑁)) → (∀𝑥 ∈ (0...𝑁)(𝑄𝑥) = (𝑃𝑥) → (𝑄𝑘) = (𝑃𝑘)))
2423imp 443 . . . 4 (((𝜑𝑘 ∈ (0..^𝑁)) ∧ ∀𝑥 ∈ (0...𝑁)(𝑄𝑥) = (𝑃𝑥)) → (𝑄𝑘) = (𝑃𝑘))
25 fzofzp1 12386 . . . . . . 7 (𝑘 ∈ (0..^𝑁) → (𝑘 + 1) ∈ (0...𝑁))
2625adantl 480 . . . . . 6 ((𝜑𝑘 ∈ (0..^𝑁)) → (𝑘 + 1) ∈ (0...𝑁))
27 fveq2 6088 . . . . . . . 8 (𝑥 = (𝑘 + 1) → (𝑄𝑥) = (𝑄‘(𝑘 + 1)))
28 fveq2 6088 . . . . . . . 8 (𝑥 = (𝑘 + 1) → (𝑃𝑥) = (𝑃‘(𝑘 + 1)))
2927, 28eqeq12d 2624 . . . . . . 7 (𝑥 = (𝑘 + 1) → ((𝑄𝑥) = (𝑃𝑥) ↔ (𝑄‘(𝑘 + 1)) = (𝑃‘(𝑘 + 1))))
3029rspcv 3277 . . . . . 6 ((𝑘 + 1) ∈ (0...𝑁) → (∀𝑥 ∈ (0...𝑁)(𝑄𝑥) = (𝑃𝑥) → (𝑄‘(𝑘 + 1)) = (𝑃‘(𝑘 + 1))))
3126, 30syl 17 . . . . 5 ((𝜑𝑘 ∈ (0..^𝑁)) → (∀𝑥 ∈ (0...𝑁)(𝑄𝑥) = (𝑃𝑥) → (𝑄‘(𝑘 + 1)) = (𝑃‘(𝑘 + 1))))
3231imp 443 . . . 4 (((𝜑𝑘 ∈ (0..^𝑁)) ∧ ∀𝑥 ∈ (0...𝑁)(𝑄𝑥) = (𝑃𝑥)) → (𝑄‘(𝑘 + 1)) = (𝑃‘(𝑘 + 1)))
3312adantr 479 . . . . . . 7 ((𝜑𝑘 ∈ (0..^𝑁)) → (iEdg‘𝑆) = (𝐼 ∪ {⟨𝐵, 𝐸⟩}))
3413fveq1i 6089 . . . . . . . 8 (𝐻𝑘) = ((𝐹 ∪ {⟨𝑁, 𝐵⟩})‘𝑘)
35 fzonel 12307 . . . . . . . . . . . . . 14 ¬ 𝑁 ∈ (0..^𝑁)
36 eleq1 2675 . . . . . . . . . . . . . 14 (𝑁 = 𝑘 → (𝑁 ∈ (0..^𝑁) ↔ 𝑘 ∈ (0..^𝑁)))
3735, 36mtbii 314 . . . . . . . . . . . . 13 (𝑁 = 𝑘 → ¬ 𝑘 ∈ (0..^𝑁))
3837a1i 11 . . . . . . . . . . . 12 (𝜑 → (𝑁 = 𝑘 → ¬ 𝑘 ∈ (0..^𝑁)))
3938con2d 127 . . . . . . . . . . 11 (𝜑 → (𝑘 ∈ (0..^𝑁) → ¬ 𝑁 = 𝑘))
4039imp 443 . . . . . . . . . 10 ((𝜑𝑘 ∈ (0..^𝑁)) → ¬ 𝑁 = 𝑘)
4140neqned 2788 . . . . . . . . 9 ((𝜑𝑘 ∈ (0..^𝑁)) → 𝑁𝑘)
42 fvunsn 6328 . . . . . . . . 9 (𝑁𝑘 → ((𝐹 ∪ {⟨𝑁, 𝐵⟩})‘𝑘) = (𝐹𝑘))
4341, 42syl 17 . . . . . . . 8 ((𝜑𝑘 ∈ (0..^𝑁)) → ((𝐹 ∪ {⟨𝑁, 𝐵⟩})‘𝑘) = (𝐹𝑘))
4434, 43syl5eq 2655 . . . . . . 7 ((𝜑𝑘 ∈ (0..^𝑁)) → (𝐻𝑘) = (𝐹𝑘))
4533, 44fveq12d 6094 . . . . . 6 ((𝜑𝑘 ∈ (0..^𝑁)) → ((iEdg‘𝑆)‘(𝐻𝑘)) = ((𝐼 ∪ {⟨𝐵, 𝐸⟩})‘(𝐹𝑘)))
469oveq2i 6538 . . . . . . . . . . . . . . . 16 (0..^𝑁) = (0..^(#‘𝐹))
4746eleq2i 2679 . . . . . . . . . . . . . . 15 (𝑘 ∈ (0..^𝑁) ↔ 𝑘 ∈ (0..^(#‘𝐹)))
4821wlkf 40814 . . . . . . . . . . . . . . . . 17 (𝐹(1Walks‘𝐺)𝑃𝐹 ∈ Word dom 𝐼)
498, 48syl 17 . . . . . . . . . . . . . . . 16 (𝜑𝐹 ∈ Word dom 𝐼)
50 wrdsymbcl 13119 . . . . . . . . . . . . . . . . 17 ((𝐹 ∈ Word dom 𝐼𝑘 ∈ (0..^(#‘𝐹))) → (𝐹𝑘) ∈ dom 𝐼)
5150ex 448 . . . . . . . . . . . . . . . 16 (𝐹 ∈ Word dom 𝐼 → (𝑘 ∈ (0..^(#‘𝐹)) → (𝐹𝑘) ∈ dom 𝐼))
5249, 51syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (𝑘 ∈ (0..^(#‘𝐹)) → (𝐹𝑘) ∈ dom 𝐼))
5347, 52syl5bi 230 . . . . . . . . . . . . . 14 (𝜑 → (𝑘 ∈ (0..^𝑁) → (𝐹𝑘) ∈ dom 𝐼))
5453imp 443 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ (0..^𝑁)) → (𝐹𝑘) ∈ dom 𝐼)
55 eleq1 2675 . . . . . . . . . . . . 13 (𝐵 = (𝐹𝑘) → (𝐵 ∈ dom 𝐼 ↔ (𝐹𝑘) ∈ dom 𝐼))
5654, 55syl5ibrcom 235 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ (0..^𝑁)) → (𝐵 = (𝐹𝑘) → 𝐵 ∈ dom 𝐼))
5756con3d 146 . . . . . . . . . . 11 ((𝜑𝑘 ∈ (0..^𝑁)) → (¬ 𝐵 ∈ dom 𝐼 → ¬ 𝐵 = (𝐹𝑘)))
5857ex 448 . . . . . . . . . 10 (𝜑 → (𝑘 ∈ (0..^𝑁) → (¬ 𝐵 ∈ dom 𝐼 → ¬ 𝐵 = (𝐹𝑘))))
597, 58mpid 42 . . . . . . . . 9 (𝜑 → (𝑘 ∈ (0..^𝑁) → ¬ 𝐵 = (𝐹𝑘)))
6059imp 443 . . . . . . . 8 ((𝜑𝑘 ∈ (0..^𝑁)) → ¬ 𝐵 = (𝐹𝑘))
6160neqned 2788 . . . . . . 7 ((𝜑𝑘 ∈ (0..^𝑁)) → 𝐵 ≠ (𝐹𝑘))
62 fvunsn 6328 . . . . . . 7 (𝐵 ≠ (𝐹𝑘) → ((𝐼 ∪ {⟨𝐵, 𝐸⟩})‘(𝐹𝑘)) = (𝐼‘(𝐹𝑘)))
6361, 62syl 17 . . . . . 6 ((𝜑𝑘 ∈ (0..^𝑁)) → ((𝐼 ∪ {⟨𝐵, 𝐸⟩})‘(𝐹𝑘)) = (𝐼‘(𝐹𝑘)))
6445, 63eqtrd 2643 . . . . 5 ((𝜑𝑘 ∈ (0..^𝑁)) → ((iEdg‘𝑆)‘(𝐻𝑘)) = (𝐼‘(𝐹𝑘)))
6564adantr 479 . . . 4 (((𝜑𝑘 ∈ (0..^𝑁)) ∧ ∀𝑥 ∈ (0...𝑁)(𝑄𝑥) = (𝑃𝑥)) → ((iEdg‘𝑆)‘(𝐻𝑘)) = (𝐼‘(𝐹𝑘)))
6624, 32, 653jca 1234 . . 3 (((𝜑𝑘 ∈ (0..^𝑁)) ∧ ∀𝑥 ∈ (0...𝑁)(𝑄𝑥) = (𝑃𝑥)) → ((𝑄𝑘) = (𝑃𝑘) ∧ (𝑄‘(𝑘 + 1)) = (𝑃‘(𝑘 + 1)) ∧ ((iEdg‘𝑆)‘(𝐻𝑘)) = (𝐼‘(𝐹𝑘))))
6716, 66mpidan 700 . 2 ((𝜑𝑘 ∈ (0..^𝑁)) → ((𝑄𝑘) = (𝑃𝑘) ∧ (𝑄‘(𝑘 + 1)) = (𝑃‘(𝑘 + 1)) ∧ ((iEdg‘𝑆)‘(𝐻𝑘)) = (𝐼‘(𝐹𝑘))))
6867ralrimiva 2948 1 (𝜑 → ∀𝑘 ∈ (0..^𝑁)((𝑄𝑘) = (𝑃𝑘) ∧ (𝑄‘(𝑘 + 1)) = (𝑃‘(𝑘 + 1)) ∧ ((iEdg‘𝑆)‘(𝐻𝑘)) = (𝐼‘(𝐹𝑘))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 382  w3a 1030   = wceq 1474  wcel 1976  wne 2779  wral 2895  Vcvv 3172  cun 3537  wss 3539  {csn 4124  {cpr 4126  cop 4130   class class class wbr 4577  dom cdm 5028  Fun wfun 5784  cfv 5790  (class class class)co 6527  Fincfn 7818  0cc0 9792  1c1 9793   + caddc 9795  ...cfz 12152  ..^cfzo 12289  #chash 12934  Word cword 13092  Vtxcvtx 40224  iEdgciedg 40225  Edgcedga 40346  1Walksc1wlks 40791
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-rep 4693  ax-sep 4703  ax-nul 4712  ax-pow 4764  ax-pr 4828  ax-un 6824  ax-cnex 9848  ax-resscn 9849  ax-1cn 9850  ax-icn 9851  ax-addcl 9852  ax-addrcl 9853  ax-mulcl 9854  ax-mulrcl 9855  ax-mulcom 9856  ax-addass 9857  ax-mulass 9858  ax-distr 9859  ax-i2m1 9860  ax-1ne0 9861  ax-1rid 9862  ax-rnegex 9863  ax-rrecex 9864  ax-cnre 9865  ax-pre-lttri 9866  ax-pre-lttrn 9867  ax-pre-ltadd 9868  ax-pre-mulgt0 9869
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-ifp 1006  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-nel 2782  df-ral 2900  df-rex 2901  df-reu 2902  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-pss 3555  df-nul 3874  df-if 4036  df-pw 4109  df-sn 4125  df-pr 4127  df-tp 4129  df-op 4131  df-uni 4367  df-int 4405  df-iun 4451  df-br 4578  df-opab 4638  df-mpt 4639  df-tr 4675  df-eprel 4939  df-id 4943  df-po 4949  df-so 4950  df-fr 4987  df-we 4989  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-pred 5583  df-ord 5629  df-on 5630  df-lim 5631  df-suc 5632  df-iota 5754  df-fun 5792  df-fn 5793  df-f 5794  df-f1 5795  df-fo 5796  df-f1o 5797  df-fv 5798  df-riota 6489  df-ov 6530  df-oprab 6531  df-mpt2 6532  df-om 6935  df-1st 7036  df-2nd 7037  df-wrecs 7271  df-recs 7332  df-rdg 7370  df-1o 7424  df-er 7606  df-map 7723  df-pm 7724  df-en 7819  df-dom 7820  df-sdom 7821  df-fin 7822  df-card 8625  df-pnf 9932  df-mnf 9933  df-xr 9934  df-ltxr 9935  df-le 9936  df-sub 10119  df-neg 10120  df-nn 10868  df-n0 11140  df-z 11211  df-uz 11520  df-fz 12153  df-fzo 12290  df-hash 12935  df-word 13100  df-1wlks 40795
This theorem is referenced by:  1wlkp1lem8  40884
  Copyright terms: Public domain W3C validator