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

Theorem 1wlksonproplem 40909
Description: Lemma for theorems for properties of walks between two vertices, e.g. trlsonprop 40912. (Contributed by AV, 16-Jan-2021.)
Hypotheses
Ref Expression
1wlksonproplem.v 𝑉 = (Vtx‘𝐺)
1wlksonproplem.b (((𝐺 ∈ V ∧ 𝐴𝑉𝐵𝑉) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → (𝐹(𝐴(𝑊𝐺)𝐵)𝑃 ↔ (𝐹(𝐴(𝑂𝐺)𝐵)𝑃𝐹(𝑄𝐺)𝑃)))
1wlksonproplem.d 𝑊 = (𝑔 ∈ V ↦ (𝑎 ∈ (Vtx‘𝑔), 𝑏 ∈ (Vtx‘𝑔) ↦ {⟨𝑓, 𝑝⟩ ∣ (𝑓(𝑎(𝑂𝑔)𝑏)𝑝𝑓(𝑄𝑔)𝑝)}))
1wlksonproplem.w (((𝐺 ∈ V ∧ 𝐴𝑉𝐵𝑉) ∧ 𝑓(𝑄𝐺)𝑝) → 𝑓(1Walks‘𝐺)𝑝)
Assertion
Ref Expression
1wlksonproplem (𝐹(𝐴(𝑊𝐺)𝐵)𝑃 → ((𝐺 ∈ V ∧ 𝐴𝑉𝐵𝑉) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐹(𝐴(𝑂𝐺)𝐵)𝑃𝐹(𝑄𝐺)𝑃)))
Distinct variable groups:   𝐴,𝑎,𝑏,𝑓,𝑔,𝑝   𝐵,𝑎,𝑏,𝑓,𝑔,𝑝   𝐺,𝑎,𝑏,𝑓,𝑔,𝑝   𝑂,𝑎,𝑏,𝑔   𝑄,𝑎,𝑏,𝑔   𝑉,𝑎,𝑏,𝑓,𝑔,𝑝
Allowed substitution hints:   𝑃(𝑓,𝑔,𝑝,𝑎,𝑏)   𝑄(𝑓,𝑝)   𝐹(𝑓,𝑔,𝑝,𝑎,𝑏)   𝑂(𝑓,𝑝)   𝑊(𝑓,𝑔,𝑝,𝑎,𝑏)

Proof of Theorem 1wlksonproplem
StepHypRef Expression
1 1wlksonproplem.v . . . . . 6 𝑉 = (Vtx‘𝐺)
2 fvex 6093 . . . . . 6 (Vtx‘𝐺) ∈ V
31, 2eqeltri 2678 . . . . 5 𝑉 ∈ V
4 1wlksonproplem.d . . . . . 6 𝑊 = (𝑔 ∈ V ↦ (𝑎 ∈ (Vtx‘𝑔), 𝑏 ∈ (Vtx‘𝑔) ↦ {⟨𝑓, 𝑝⟩ ∣ (𝑓(𝑎(𝑂𝑔)𝑏)𝑝𝑓(𝑄𝑔)𝑝)}))
5 simp1 1053 . . . . . . 7 ((𝐺 ∈ V ∧ 𝐴𝑉𝐵𝑉) → 𝐺 ∈ V)
6 simp2 1054 . . . . . . . 8 ((𝐺 ∈ V ∧ 𝐴𝑉𝐵𝑉) → 𝐴𝑉)
76, 1syl6eleq 2692 . . . . . . 7 ((𝐺 ∈ V ∧ 𝐴𝑉𝐵𝑉) → 𝐴 ∈ (Vtx‘𝐺))
8 simp3 1055 . . . . . . . 8 ((𝐺 ∈ V ∧ 𝐴𝑉𝐵𝑉) → 𝐵𝑉)
98, 1syl6eleq 2692 . . . . . . 7 ((𝐺 ∈ V ∧ 𝐴𝑉𝐵𝑉) → 𝐵 ∈ (Vtx‘𝐺))
10 1wlksv 40821 . . . . . . . 8 {⟨𝑓, 𝑝⟩ ∣ 𝑓(1Walks‘𝐺)𝑝} ∈ V
1110a1i 11 . . . . . . 7 ((𝐺 ∈ V ∧ 𝐴𝑉𝐵𝑉) → {⟨𝑓, 𝑝⟩ ∣ 𝑓(1Walks‘𝐺)𝑝} ∈ V)
12 1wlksonproplem.w . . . . . . 7 (((𝐺 ∈ V ∧ 𝐴𝑉𝐵𝑉) ∧ 𝑓(𝑄𝐺)𝑝) → 𝑓(1Walks‘𝐺)𝑝)
135, 7, 9, 11, 12, 4mptmpt2opabovd 40158 . . . . . 6 ((𝐺 ∈ V ∧ 𝐴𝑉𝐵𝑉) → (𝐴(𝑊𝐺)𝐵) = {⟨𝑓, 𝑝⟩ ∣ (𝑓(𝐴(𝑂𝐺)𝐵)𝑝𝑓(𝑄𝐺)𝑝)})
14 fveq2 6083 . . . . . . 7 (𝑔 = 𝐺 → (Vtx‘𝑔) = (Vtx‘𝐺))
1514, 1syl6eqr 2656 . . . . . 6 (𝑔 = 𝐺 → (Vtx‘𝑔) = 𝑉)
16 fveq2 6083 . . . . . . . . 9 (𝑔 = 𝐺 → (𝑂𝑔) = (𝑂𝐺))
1716oveqd 6539 . . . . . . . 8 (𝑔 = 𝐺 → (𝑎(𝑂𝑔)𝑏) = (𝑎(𝑂𝐺)𝑏))
1817breqd 4583 . . . . . . 7 (𝑔 = 𝐺 → (𝑓(𝑎(𝑂𝑔)𝑏)𝑝𝑓(𝑎(𝑂𝐺)𝑏)𝑝))
19 fveq2 6083 . . . . . . . 8 (𝑔 = 𝐺 → (𝑄𝑔) = (𝑄𝐺))
2019breqd 4583 . . . . . . 7 (𝑔 = 𝐺 → (𝑓(𝑄𝑔)𝑝𝑓(𝑄𝐺)𝑝))
2118, 20anbi12d 742 . . . . . 6 (𝑔 = 𝐺 → ((𝑓(𝑎(𝑂𝑔)𝑏)𝑝𝑓(𝑄𝑔)𝑝) ↔ (𝑓(𝑎(𝑂𝐺)𝑏)𝑝𝑓(𝑄𝐺)𝑝)))
224, 13, 15, 15, 21bropfvvvv 7116 . . . . 5 ((𝑉 ∈ V ∧ 𝑉 ∈ V) → (𝐹(𝐴(𝑊𝐺)𝐵)𝑃 → (𝐺 ∈ V ∧ (𝐴𝑉𝐵𝑉) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V))))
233, 3, 22mp2an 703 . . . 4 (𝐹(𝐴(𝑊𝐺)𝐵)𝑃 → (𝐺 ∈ V ∧ (𝐴𝑉𝐵𝑉) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)))
24 3anass 1034 . . . . . 6 ((𝐺 ∈ V ∧ 𝐴𝑉𝐵𝑉) ↔ (𝐺 ∈ V ∧ (𝐴𝑉𝐵𝑉)))
2524anbi1i 726 . . . . 5 (((𝐺 ∈ V ∧ 𝐴𝑉𝐵𝑉) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ↔ ((𝐺 ∈ V ∧ (𝐴𝑉𝐵𝑉)) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)))
26 df-3an 1032 . . . . 5 ((𝐺 ∈ V ∧ (𝐴𝑉𝐵𝑉) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ↔ ((𝐺 ∈ V ∧ (𝐴𝑉𝐵𝑉)) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)))
2725, 26bitr4i 265 . . . 4 (((𝐺 ∈ V ∧ 𝐴𝑉𝐵𝑉) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ↔ (𝐺 ∈ V ∧ (𝐴𝑉𝐵𝑉) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)))
2823, 27sylibr 222 . . 3 (𝐹(𝐴(𝑊𝐺)𝐵)𝑃 → ((𝐺 ∈ V ∧ 𝐴𝑉𝐵𝑉) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)))
29 1wlksonproplem.b . . . . 5 (((𝐺 ∈ V ∧ 𝐴𝑉𝐵𝑉) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → (𝐹(𝐴(𝑊𝐺)𝐵)𝑃 ↔ (𝐹(𝐴(𝑂𝐺)𝐵)𝑃𝐹(𝑄𝐺)𝑃)))
3029biimpd 217 . . . 4 (((𝐺 ∈ V ∧ 𝐴𝑉𝐵𝑉) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → (𝐹(𝐴(𝑊𝐺)𝐵)𝑃 → (𝐹(𝐴(𝑂𝐺)𝐵)𝑃𝐹(𝑄𝐺)𝑃)))
3130imdistani 721 . . 3 ((((𝐺 ∈ V ∧ 𝐴𝑉𝐵𝑉) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ 𝐹(𝐴(𝑊𝐺)𝐵)𝑃) → (((𝐺 ∈ V ∧ 𝐴𝑉𝐵𝑉) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ (𝐹(𝐴(𝑂𝐺)𝐵)𝑃𝐹(𝑄𝐺)𝑃)))
3228, 31mpancom 699 . 2 (𝐹(𝐴(𝑊𝐺)𝐵)𝑃 → (((𝐺 ∈ V ∧ 𝐴𝑉𝐵𝑉) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ (𝐹(𝐴(𝑂𝐺)𝐵)𝑃𝐹(𝑄𝐺)𝑃)))
33 df-3an 1032 . 2 (((𝐺 ∈ V ∧ 𝐴𝑉𝐵𝑉) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐹(𝐴(𝑂𝐺)𝐵)𝑃𝐹(𝑄𝐺)𝑃)) ↔ (((𝐺 ∈ V ∧ 𝐴𝑉𝐵𝑉) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ (𝐹(𝐴(𝑂𝐺)𝐵)𝑃𝐹(𝑄𝐺)𝑃)))
3432, 33sylibr 222 1 (𝐹(𝐴(𝑊𝐺)𝐵)𝑃 → ((𝐺 ∈ V ∧ 𝐴𝑉𝐵𝑉) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐹(𝐴(𝑂𝐺)𝐵)𝑃𝐹(𝑄𝐺)𝑃)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wa 382  w3a 1030   = wceq 1474  wcel 1975  Vcvv 3167   class class class wbr 4572  {copab 4631  cmpt 4632  cfv 5785  (class class class)co 6522  cmpt2 6524  Vtxcvtx 40226  1Walksc1wlks 40793
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-8 1977  ax-9 1984  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2227  ax-ext 2584  ax-rep 4688  ax-sep 4698  ax-nul 4707  ax-pow 4759  ax-pr 4823  ax-un 6819  ax-cnex 9843  ax-resscn 9844  ax-1cn 9845  ax-icn 9846  ax-addcl 9847  ax-addrcl 9848  ax-mulcl 9849  ax-mulrcl 9850  ax-mulcom 9851  ax-addass 9852  ax-mulass 9853  ax-distr 9854  ax-i2m1 9855  ax-1ne0 9856  ax-1rid 9857  ax-rnegex 9858  ax-rrecex 9859  ax-cnre 9860  ax-pre-lttri 9861  ax-pre-lttrn 9862  ax-pre-ltadd 9863  ax-pre-mulgt0 9864
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 1866  df-eu 2456  df-mo 2457  df-clab 2591  df-cleq 2597  df-clel 2600  df-nfc 2734  df-ne 2776  df-nel 2777  df-ral 2895  df-rex 2896  df-reu 2897  df-rab 2899  df-v 3169  df-sbc 3397  df-csb 3494  df-dif 3537  df-un 3539  df-in 3541  df-ss 3548  df-pss 3550  df-nul 3869  df-if 4031  df-pw 4104  df-sn 4120  df-pr 4122  df-tp 4124  df-op 4126  df-uni 4362  df-int 4400  df-iun 4446  df-br 4573  df-opab 4633  df-mpt 4634  df-tr 4670  df-eprel 4934  df-id 4938  df-po 4944  df-so 4945  df-fr 4982  df-we 4984  df-xp 5029  df-rel 5030  df-cnv 5031  df-co 5032  df-dm 5033  df-rn 5034  df-res 5035  df-ima 5036  df-pred 5578  df-ord 5624  df-on 5625  df-lim 5626  df-suc 5627  df-iota 5749  df-fun 5787  df-fn 5788  df-f 5789  df-f1 5790  df-fo 5791  df-f1o 5792  df-fv 5793  df-riota 6484  df-ov 6525  df-oprab 6526  df-mpt2 6527  df-om 6930  df-1st 7031  df-2nd 7032  df-wrecs 7266  df-recs 7327  df-rdg 7365  df-1o 7419  df-er 7601  df-map 7718  df-pm 7719  df-en 7814  df-dom 7815  df-sdom 7816  df-fin 7817  df-card 8620  df-pnf 9927  df-mnf 9928  df-xr 9929  df-ltxr 9930  df-le 9931  df-sub 10114  df-neg 10115  df-nn 10863  df-n0 11135  df-z 11206  df-uz 11515  df-fz 12148  df-fzo 12285  df-hash 12930  df-word 13095  df-1wlks 40797
This theorem is referenced by:  trlsonprop  40912  pthsonprop  40947  spthonprop  40948
  Copyright terms: Public domain W3C validator