Nearby theorems
|
|
Mathbox for Norm Megill |
< Previous
Next >
Nearby theorems |
|
| Mirrors > Home > MPE Home > Th. List > Mathboxes > olm11 | Structured version Visualization version GIF version | ||
| Description: The meet of an ortholattice element with one equals itself. (chm1i 31279 analog.) (Contributed by NM, 22-May-2012.) |
| Ref | Expression |
|---|---|
| olm1.b | β’ π΅ = (BaseβπΎ) |
| olm1.m | β’ β§ = (meetβπΎ) |
| olm1.u | β’ 1 = (1.βπΎ) |
| Ref | Expression |
|---|---|
| olm11 | β’ ((πΎ β OL β§ π β π΅) β (π β§ 1 ) = π) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | olop 38686 | . . . . . . 7 β’ (πΎ β OL β πΎ β OP) | |
| 2 | 1 | adantr 480 | . . . . . 6 β’ ((πΎ β OL β§ π β π΅) β πΎ β OP) |
| 3 | eqid 2728 | . . . . . . 7 β’ (0.βπΎ) = (0.βπΎ) | |
| 4 | olm1.u | . . . . . . 7 β’ 1 = (1.βπΎ) | |
| 5 | eqid 2728 | . . . . . . 7 β’ (ocβπΎ) = (ocβπΎ) | |
| 6 | 3, 4, 5 | opoc1 38674 | . . . . . 6 β’ (πΎ β OP β ((ocβπΎ)β 1 ) = (0.βπΎ)) |
| 7 | 2, 6 | syl 17 | . . . . 5 β’ ((πΎ β OL β§ π β π΅) β ((ocβπΎ)β 1 ) = (0.βπΎ)) |
| 8 | 7 | oveq2d 7436 | . . . 4 β’ ((πΎ β OL β§ π β π΅) β (((ocβπΎ)βπ)(joinβπΎ)((ocβπΎ)β 1 )) = (((ocβπΎ)βπ)(joinβπΎ)(0.βπΎ))) |
| 9 | olm1.b | . . . . . . 7 β’ π΅ = (BaseβπΎ) | |
| 10 | 9, 5 | opoccl 38666 | . . . . . 6 β’ ((πΎ β OP β§ π β π΅) β ((ocβπΎ)βπ) β π΅) |
| 11 | 1, 10 | sylan 579 | . . . . 5 β’ ((πΎ β OL β§ π β π΅) β ((ocβπΎ)βπ) β π΅) |
| 12 | eqid 2728 | . . . . . 6 β’ (joinβπΎ) = (joinβπΎ) | |
| 13 | 9, 12, 3 | olj01 38697 | . . . . 5 β’ ((πΎ β OL β§ ((ocβπΎ)βπ) β π΅) β (((ocβπΎ)βπ)(joinβπΎ)(0.βπΎ)) = ((ocβπΎ)βπ)) |
| 14 | 11, 13 | syldan 590 | . . . 4 β’ ((πΎ β OL β§ π β π΅) β (((ocβπΎ)βπ)(joinβπΎ)(0.βπΎ)) = ((ocβπΎ)βπ)) |
| 15 | 8, 14 | eqtrd 2768 | . . 3 β’ ((πΎ β OL β§ π β π΅) β (((ocβπΎ)βπ)(joinβπΎ)((ocβπΎ)β 1 )) = ((ocβπΎ)βπ)) |
| 16 | 15 | fveq2d 6901 | . 2 β’ ((πΎ β OL β§ π β π΅) β ((ocβπΎ)β(((ocβπΎ)βπ)(joinβπΎ)((ocβπΎ)β 1 ))) = ((ocβπΎ)β((ocβπΎ)βπ))) |
| 17 | 9, 4 | op1cl 38657 | . . . 4 β’ (πΎ β OP β 1 β π΅) |
| 18 | 2, 17 | syl 17 | . . 3 β’ ((πΎ β OL β§ π β π΅) β 1 β π΅) |
| 19 | olm1.m | . . . 4 β’ β§ = (meetβπΎ) | |
| 20 | 9, 12, 19, 5 | oldmj4 38696 | . . 3 β’ ((πΎ β OL β§ π β π΅ β§ 1 β π΅) β ((ocβπΎ)β(((ocβπΎ)βπ)(joinβπΎ)((ocβπΎ)β 1 ))) = (π β§ 1 )) |
| 21 | 18, 20 | mpd3an3 1459 | . 2 β’ ((πΎ β OL β§ π β π΅) β ((ocβπΎ)β(((ocβπΎ)βπ)(joinβπΎ)((ocβπΎ)β 1 ))) = (π β§ 1 )) |
| 22 | 9, 5 | opococ 38667 | . . 3 β’ ((πΎ β OP β§ π β π΅) β ((ocβπΎ)β((ocβπΎ)βπ)) = π) |
| 23 | 1, 22 | sylan 579 | . 2 β’ ((πΎ β OL β§ π β π΅) β ((ocβπΎ)β((ocβπΎ)βπ)) = π) |
| 24 | 16, 21, 23 | 3eqtr3d 2776 | 1 β’ ((πΎ β OL β§ π β π΅) β (π β§ 1 ) = π) |
| Colors of variables: wff setvar class |
| Syntax hints: β wi 4 β§ wa 395 = wceq 1534 β wcel 2099 βcfv 6548 (class class class)co 7420 Basecbs 17180 occoc 17241 joincjn 18303 meetcmee 18304 0.cp0 18415 1.cp1 18416 OPcops 38644 OLcol 38646 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-10 2130 ax-11 2147 ax-12 2167 ax-ext 2699 ax-rep 5285 ax-sep 5299 ax-nul 5306 ax-pow 5365 ax-pr 5429 ax-un 7740 |
| This theorem depends on definitions: df-bi 206 df-an 396 df-or 847 df-3an 1087 df-tru 1537 df-fal 1547 df-ex 1775 df-nf 1779 df-sb 2061 df-mo 2530 df-eu 2559 df-clab 2706 df-cleq 2720 df-clel 2806 df-nfc 2881 df-ne 2938 df-ral 3059 df-rex 3068 df-rmo 3373 df-reu 3374 df-rab 3430 df-v 3473 df-sbc 3777 df-csb 3893 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-nul 4324 df-if 4530 df-pw 4605 df-sn 4630 df-pr 4632 df-op 4636 df-uni 4909 df-iun 4998 df-br 5149 df-opab 5211 df-mpt 5232 df-id 5576 df-xp 5684 df-rel 5685 df-cnv 5686 df-co 5687 df-dm 5688 df-rn 5689 df-res 5690 df-ima 5691 df-iota 6500 df-fun 6550 df-fn 6551 df-f 6552 df-f1 6553 df-fo 6554 df-f1o 6555 df-fv 6556 df-riota 7376 df-ov 7423 df-oprab 7424 df-proset 18287 df-poset 18305 df-lub 18338 df-glb 18339 df-join 18340 df-meet 18341 df-p0 18417 df-p1 18418 df-lat 18424 df-oposet 38648 df-ol 38650 |
| This theorem is referenced by: olm12 38700 lhpmcvr3 39498 trljat1 39639 trljat2 39640 cdlemc1 39664 cdlemc6 39669 cdleme0cp 39687 cdleme0cq 39688 cdleme1 39700 cdleme4 39711 cdleme5 39713 cdleme8 39723 cdleme9 39726 cdleme10 39727 cdleme20c 39784 cdleme20j 39791 cdleme22e 39817 cdleme22eALTN 39818 cdleme30a 39851 cdleme35b 39923 cdleme35e 39926 cdleme42a 39944 trlcoabs2N 40195 trlcolem 40199 cdlemi1 40291 cdlemk4 40307 dia2dimlem1 40537 cdlemn10 40679 dihglbcpreN 40773 |
| Copyright terms: Public domain | W3C validator |