![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > efgcpbllema | Structured version Visualization version GIF version |
Description: Lemma for efgrelex 19619. 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 7417 | . . . . 5 β’ (π = π β (π΄ ++ π) = (π΄ ++ π)) | |
2 | 1 | oveq1d 7424 | . . . 4 β’ (π = π β ((π΄ ++ π) ++ π΅) = ((π΄ ++ π) ++ π΅)) |
3 | oveq2 7417 | . . . . 5 β’ (π = π β (π΄ ++ π) = (π΄ ++ π)) | |
4 | 3 | oveq1d 7424 | . . . 4 β’ (π = π β ((π΄ ++ π) ++ π΅) = ((π΄ ++ π) ++ π΅)) |
5 | 2, 4 | breqan12d 5165 | . . 3 β’ ((π = π β§ π = π) β (((π΄ ++ π) ++ π΅) βΌ ((π΄ ++ π) ++ π΅) β ((π΄ ++ π) ++ π΅) βΌ ((π΄ ++ π) ++ π΅))) |
6 | efgcpbllem.1 | . . . 4 β’ πΏ = {β¨π, πβ© β£ ({π, π} β π β§ ((π΄ ++ π) ++ π΅) βΌ ((π΄ ++ π) ++ π΅))} | |
7 | vex 3479 | . . . . . . 7 β’ π β V | |
8 | vex 3479 | . . . . . . 7 β’ π β V | |
9 | 7, 8 | prss 4824 | . . . . . 6 β’ ((π β π β§ π β π) β {π, π} β π) |
10 | 9 | anbi1i 625 | . . . . 5 β’ (((π β π β§ π β π) β§ ((π΄ ++ π) ++ π΅) βΌ ((π΄ ++ π) ++ π΅)) β ({π, π} β π β§ ((π΄ ++ π) ++ π΅) βΌ ((π΄ ++ π) ++ π΅))) |
11 | 10 | opabbii 5216 | . . . 4 β’ {β¨π, πβ© β£ ((π β π β§ π β π) β§ ((π΄ ++ π) ++ π΅) βΌ ((π΄ ++ π) ++ π΅))} = {β¨π, πβ© β£ ({π, π} β π β§ ((π΄ ++ π) ++ π΅) βΌ ((π΄ ++ π) ++ π΅))} |
12 | 6, 11 | eqtr4i 2764 | . . 3 β’ πΏ = {β¨π, πβ© β£ ((π β π β§ π β π) β§ ((π΄ ++ π) ++ π΅) βΌ ((π΄ ++ π) ++ π΅))} |
13 | 5, 12 | brab2a 5770 | . 2 β’ (ππΏπ β ((π β π β§ π β π) β§ ((π΄ ++ π) ++ π΅) βΌ ((π΄ ++ π) ++ π΅))) |
14 | df-3an 1090 | . 2 β’ ((π β π β§ π β π β§ ((π΄ ++ π) ++ π΅) βΌ ((π΄ ++ π) ++ π΅)) β ((π β π β§ π β π) β§ ((π΄ ++ π) ++ π΅) βΌ ((π΄ ++ π) ++ π΅))) | |
15 | 13, 14 | bitr4i 278 | 1 β’ (ππΏπ β (π β π β§ π β π β§ ((π΄ ++ π) ++ π΅) βΌ ((π΄ ++ π) ++ π΅))) |
Colors of variables: wff setvar class |
Syntax hints: β wb 205 β§ wa 397 β§ w3a 1088 = wceq 1542 β wcel 2107 βwral 3062 {crab 3433 β cdif 3946 β wss 3949 β c0 4323 {csn 4629 {cpr 4631 β¨cop 4635 β¨cotp 4637 βͺ ciun 4998 class class class wbr 5149 {copab 5211 β¦ cmpt 5232 I cid 5574 Γ cxp 5675 ran crn 5678 βcfv 6544 (class class class)co 7409 β cmpo 7411 1oc1o 8459 2oc2o 8460 0cc0 11110 1c1 11111 β cmin 11444 ...cfz 13484 ..^cfzo 13627 β―chash 14290 Word cword 14464 ++ cconcat 14520 splice csplice 14699 β¨βcs2 14792 ~FG cefg 19574 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2704 ax-sep 5300 ax-nul 5307 ax-pr 5428 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-ral 3063 df-rex 3072 df-rab 3434 df-v 3477 df-dif 3952 df-un 3954 df-in 3956 df-ss 3966 df-nul 4324 df-if 4530 df-sn 4630 df-pr 4632 df-op 4636 df-uni 4910 df-br 5150 df-opab 5212 df-xp 5683 df-iota 6496 df-fv 6552 df-ov 7412 |
This theorem is referenced by: efgcpbllemb 19623 efgcpbl 19624 |
Copyright terms: Public domain | W3C validator |