![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > efgcpbllema | Structured version Visualization version GIF version |
Description: Lemma for efgrelex 19621. 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.) |
Ref | Expression |
---|---|
efgval.w | β’ π = ( I βWord (πΌ Γ 2o)) |
efgval.r | β’ βΌ = ( ~FG βπΌ) |
efgval2.m | β’ π = (π¦ β πΌ, π§ β 2o β¦ β¨π¦, (1o β π§)β©) |
efgval2.t | β’ π = (π£ β π β¦ (π β (0...(β―βπ£)), π€ β (πΌ Γ 2o) β¦ (π£ splice β¨π, π, β¨βπ€(πβπ€)ββ©β©))) |
efgred.d | β’ π· = (π β βͺ π₯ β π ran (πβπ₯)) |
efgred.s | β’ π = (π β {π‘ β (Word π β {β }) β£ ((π‘β0) β π· β§ βπ β (1..^(β―βπ‘))(π‘βπ) β ran (πβ(π‘β(π β 1))))} β¦ (πβ((β―βπ) β 1))) |
efgcpbllem.1 | β’ πΏ = {β¨π, πβ© β£ ({π, π} β π β§ ((π΄ ++ π) ++ π΅) βΌ ((π΄ ++ π) ++ π΅))} |
Ref | Expression |
---|---|
efgcpbllema | β’ (ππΏπ β (π β π β§ π β π β§ ((π΄ ++ π) ++ π΅) βΌ ((π΄ ++ π) ++ π΅))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | oveq2 7419 | . . . . 5 β’ (π = π β (π΄ ++ π) = (π΄ ++ π)) | |
2 | 1 | oveq1d 7426 | . . . 4 β’ (π = π β ((π΄ ++ π) ++ π΅) = ((π΄ ++ π) ++ π΅)) |
3 | oveq2 7419 | . . . . 5 β’ (π = π β (π΄ ++ π) = (π΄ ++ π)) | |
4 | 3 | oveq1d 7426 | . . . 4 β’ (π = π β ((π΄ ++ π) ++ π΅) = ((π΄ ++ π) ++ π΅)) |
5 | 2, 4 | breqan12d 5164 | . . 3 β’ ((π = π β§ π = π) β (((π΄ ++ π) ++ π΅) βΌ ((π΄ ++ π) ++ π΅) β ((π΄ ++ π) ++ π΅) βΌ ((π΄ ++ π) ++ π΅))) |
6 | efgcpbllem.1 | . . . 4 β’ πΏ = {β¨π, πβ© β£ ({π, π} β π β§ ((π΄ ++ π) ++ π΅) βΌ ((π΄ ++ π) ++ π΅))} | |
7 | vex 3478 | . . . . . . 7 β’ π β V | |
8 | vex 3478 | . . . . . . 7 β’ π β V | |
9 | 7, 8 | prss 4823 | . . . . . 6 β’ ((π β π β§ π β π) β {π, π} β π) |
10 | 9 | anbi1i 624 | . . . . 5 β’ (((π β π β§ π β π) β§ ((π΄ ++ π) ++ π΅) βΌ ((π΄ ++ π) ++ π΅)) β ({π, π} β π β§ ((π΄ ++ π) ++ π΅) βΌ ((π΄ ++ π) ++ π΅))) |
11 | 10 | opabbii 5215 | . . . 4 β’ {β¨π, πβ© β£ ((π β π β§ π β π) β§ ((π΄ ++ π) ++ π΅) βΌ ((π΄ ++ π) ++ π΅))} = {β¨π, πβ© β£ ({π, π} β π β§ ((π΄ ++ π) ++ π΅) βΌ ((π΄ ++ π) ++ π΅))} |
12 | 6, 11 | eqtr4i 2763 | . . 3 β’ πΏ = {β¨π, πβ© β£ ((π β π β§ π β π) β§ ((π΄ ++ π) ++ π΅) βΌ ((π΄ ++ π) ++ π΅))} |
13 | 5, 12 | brab2a 5769 | . 2 β’ (ππΏπ β ((π β π β§ π β π) β§ ((π΄ ++ π) ++ π΅) βΌ ((π΄ ++ π) ++ π΅))) |
14 | df-3an 1089 | . 2 β’ ((π β π β§ π β π β§ ((π΄ ++ π) ++ π΅) βΌ ((π΄ ++ π) ++ π΅)) β ((π β π β§ π β π) β§ ((π΄ ++ π) ++ π΅) βΌ ((π΄ ++ π) ++ π΅))) | |
15 | 13, 14 | bitr4i 277 | 1 β’ (ππΏπ β (π β π β§ π β π β§ ((π΄ ++ π) ++ π΅) βΌ ((π΄ ++ π) ++ π΅))) |
Colors of variables: wff setvar class |
Syntax hints: β wb 205 β§ wa 396 β§ w3a 1087 = wceq 1541 β wcel 2106 βwral 3061 {crab 3432 β cdif 3945 β wss 3948 β c0 4322 {csn 4628 {cpr 4630 β¨cop 4634 β¨cotp 4636 βͺ ciun 4997 class class class wbr 5148 {copab 5210 β¦ cmpt 5231 I cid 5573 Γ cxp 5674 ran crn 5677 βcfv 6543 (class class class)co 7411 β cmpo 7413 1oc1o 8461 2oc2o 8462 0cc0 11112 1c1 11113 β cmin 11446 ...cfz 13486 ..^cfzo 13629 β―chash 14292 Word cword 14466 ++ cconcat 14522 splice csplice 14701 β¨βcs2 14794 ~FG cefg 19576 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2703 ax-sep 5299 ax-nul 5306 ax-pr 5427 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-sb 2068 df-clab 2710 df-cleq 2724 df-clel 2810 df-ral 3062 df-rex 3071 df-rab 3433 df-v 3476 df-dif 3951 df-un 3953 df-in 3955 df-ss 3965 df-nul 4323 df-if 4529 df-sn 4629 df-pr 4631 df-op 4635 df-uni 4909 df-br 5149 df-opab 5211 df-xp 5682 df-iota 6495 df-fv 6551 df-ov 7414 |
This theorem is referenced by: efgcpbllemb 19625 efgcpbl 19626 |
Copyright terms: Public domain | W3C validator |