Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  efgcpbllema Structured version   Visualization version   GIF version

Theorem efgcpbllema 17990
 Description: Lemma for efgrelex 17987. Define an auxiliary equivalence relation 𝐿 such that 𝐴𝐿𝐵 if there are sequences from 𝐴 to 𝐵 passing through the same reduced word. (Contributed by Mario Carneiro, 1-Oct-2015.)
Hypotheses
Ref Expression
efgval.w 𝑊 = ( I ‘Word (𝐼 × 2𝑜))
efgval.r = ( ~FG𝐼)
efgval2.m 𝑀 = (𝑦𝐼, 𝑧 ∈ 2𝑜 ↦ ⟨𝑦, (1𝑜𝑧)⟩)
efgval2.t 𝑇 = (𝑣𝑊 ↦ (𝑛 ∈ (0...(#‘𝑣)), 𝑤 ∈ (𝐼 × 2𝑜) ↦ (𝑣 splice ⟨𝑛, 𝑛, ⟨“𝑤(𝑀𝑤)”⟩⟩)))
efgred.d 𝐷 = (𝑊 𝑥𝑊 ran (𝑇𝑥))
efgred.s 𝑆 = (𝑚 ∈ {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(#‘𝑡))(𝑡𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))} ↦ (𝑚‘((#‘𝑚) − 1)))
efgcpbllem.1 𝐿 = {⟨𝑖, 𝑗⟩ ∣ ({𝑖, 𝑗} ⊆ 𝑊 ∧ ((𝐴 ++ 𝑖) ++ 𝐵) ((𝐴 ++ 𝑗) ++ 𝐵))}
Assertion
Ref Expression
efgcpbllema (𝑋𝐿𝑌 ↔ (𝑋𝑊𝑌𝑊 ∧ ((𝐴 ++ 𝑋) ++ 𝐵) ((𝐴 ++ 𝑌) ++ 𝐵)))
Distinct variable groups:   𝑖,𝑗,𝐴   𝑦,𝑧   𝑡,𝑛,𝑣,𝑤,𝑦,𝑧   𝑖,𝑚,𝑛,𝑡,𝑣,𝑤,𝑥,𝑀,𝑗   𝑖,𝑘,𝑇,𝑗,𝑚,𝑡,𝑥   𝑖,𝑋,𝑗   𝑦,𝑖,𝑧,𝑊,𝑗   𝑘,𝑛,𝑣,𝑤,𝑦,𝑧,𝑊,𝑚,𝑡,𝑥   ,𝑖,𝑗,𝑚,𝑡,𝑥,𝑦,𝑧   𝐵,𝑖,𝑗   𝑆,𝑖,𝑗   𝑖,𝑌,𝑗   𝑖,𝐼,𝑗,𝑚,𝑛,𝑡,𝑣,𝑤,𝑥,𝑦,𝑧   𝐷,𝑖,𝑗,𝑚,𝑡
Allowed substitution hints:   𝐴(𝑥,𝑦,𝑧,𝑤,𝑣,𝑡,𝑘,𝑚,𝑛)   𝐵(𝑥,𝑦,𝑧,𝑤,𝑣,𝑡,𝑘,𝑚,𝑛)   𝐷(𝑥,𝑦,𝑧,𝑤,𝑣,𝑘,𝑛)   (𝑤,𝑣,𝑘,𝑛)   𝑆(𝑥,𝑦,𝑧,𝑤,𝑣,𝑡,𝑘,𝑚,𝑛)   𝑇(𝑦,𝑧,𝑤,𝑣,𝑛)   𝐼(𝑘)   𝐿(𝑥,𝑦,𝑧,𝑤,𝑣,𝑡,𝑖,𝑗,𝑘,𝑚,𝑛)   𝑀(𝑦,𝑧,𝑘)   𝑋(𝑥,𝑦,𝑧,𝑤,𝑣,𝑡,𝑘,𝑚,𝑛)   𝑌(𝑥,𝑦,𝑧,𝑤,𝑣,𝑡,𝑘,𝑚,𝑛)

Proof of Theorem efgcpbllema
StepHypRef Expression
1 oveq2 6557 . . . . 5 (𝑖 = 𝑋 → (𝐴 ++ 𝑖) = (𝐴 ++ 𝑋))
21oveq1d 6564 . . . 4 (𝑖 = 𝑋 → ((𝐴 ++ 𝑖) ++ 𝐵) = ((𝐴 ++ 𝑋) ++ 𝐵))
3 oveq2 6557 . . . . 5 (𝑗 = 𝑌 → (𝐴 ++ 𝑗) = (𝐴 ++ 𝑌))
43oveq1d 6564 . . . 4 (𝑗 = 𝑌 → ((𝐴 ++ 𝑗) ++ 𝐵) = ((𝐴 ++ 𝑌) ++ 𝐵))
52, 4breqan12d 4599 . . 3 ((𝑖 = 𝑋𝑗 = 𝑌) → (((𝐴 ++ 𝑖) ++ 𝐵) ((𝐴 ++ 𝑗) ++ 𝐵) ↔ ((𝐴 ++ 𝑋) ++ 𝐵) ((𝐴 ++ 𝑌) ++ 𝐵)))
6 efgcpbllem.1 . . . 4 𝐿 = {⟨𝑖, 𝑗⟩ ∣ ({𝑖, 𝑗} ⊆ 𝑊 ∧ ((𝐴 ++ 𝑖) ++ 𝐵) ((𝐴 ++ 𝑗) ++ 𝐵))}
7 vex 3176 . . . . . . 7 𝑖 ∈ V
8 vex 3176 . . . . . . 7 𝑗 ∈ V
97, 8prss 4291 . . . . . 6 ((𝑖𝑊𝑗𝑊) ↔ {𝑖, 𝑗} ⊆ 𝑊)
109anbi1i 727 . . . . 5 (((𝑖𝑊𝑗𝑊) ∧ ((𝐴 ++ 𝑖) ++ 𝐵) ((𝐴 ++ 𝑗) ++ 𝐵)) ↔ ({𝑖, 𝑗} ⊆ 𝑊 ∧ ((𝐴 ++ 𝑖) ++ 𝐵) ((𝐴 ++ 𝑗) ++ 𝐵)))
1110opabbii 4649 . . . 4 {⟨𝑖, 𝑗⟩ ∣ ((𝑖𝑊𝑗𝑊) ∧ ((𝐴 ++ 𝑖) ++ 𝐵) ((𝐴 ++ 𝑗) ++ 𝐵))} = {⟨𝑖, 𝑗⟩ ∣ ({𝑖, 𝑗} ⊆ 𝑊 ∧ ((𝐴 ++ 𝑖) ++ 𝐵) ((𝐴 ++ 𝑗) ++ 𝐵))}
126, 11eqtr4i 2635 . . 3 𝐿 = {⟨𝑖, 𝑗⟩ ∣ ((𝑖𝑊𝑗𝑊) ∧ ((𝐴 ++ 𝑖) ++ 𝐵) ((𝐴 ++ 𝑗) ++ 𝐵))}
135, 12brab2ga 5117 . 2 (𝑋𝐿𝑌 ↔ ((𝑋𝑊𝑌𝑊) ∧ ((𝐴 ++ 𝑋) ++ 𝐵) ((𝐴 ++ 𝑌) ++ 𝐵)))
14 df-3an 1033 . 2 ((𝑋𝑊𝑌𝑊 ∧ ((𝐴 ++ 𝑋) ++ 𝐵) ((𝐴 ++ 𝑌) ++ 𝐵)) ↔ ((𝑋𝑊𝑌𝑊) ∧ ((𝐴 ++ 𝑋) ++ 𝐵) ((𝐴 ++ 𝑌) ++ 𝐵)))
1513, 14bitr4i 266 1 (𝑋𝐿𝑌 ↔ (𝑋𝑊𝑌𝑊 ∧ ((𝐴 ++ 𝑋) ++ 𝐵) ((𝐴 ++ 𝑌) ++ 𝐵)))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 195   ∧ wa 383   ∧ w3a 1031   = wceq 1475   ∈ wcel 1977  ∀wral 2896  {crab 2900   ∖ cdif 3537   ⊆ wss 3540  ∅c0 3874  {csn 4125  {cpr 4127  ⟨cop 4131  ⟨cotp 4133  ∪ ciun 4455   class class class wbr 4583  {copab 4642   ↦ cmpt 4643   I cid 4948   × cxp 5036  ran crn 5039  ‘cfv 5804  (class class class)co 6549   ↦ cmpt2 6551  1𝑜c1o 7440  2𝑜c2o 7441  0cc0 9815  1c1 9816   − cmin 10145  ...cfz 12197  ..^cfzo 12334  #chash 12979  Word cword 13146   ++ cconcat 13148   splice csplice 13151  ⟨“cs2 13437   ~FG cefg 17942 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pr 4833 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-opab 4644  df-xp 5044  df-iota 5768  df-fv 5812  df-ov 6552 This theorem is referenced by:  efgcpbllemb  17991  efgcpbl  17992
 Copyright terms: Public domain W3C validator