| 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 31713 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 39845 | . . . . . . 7 ⊢ (𝐾 ∈ OL → 𝐾 ∈ OP) | |
| 2 | 1 | adantr 485 | . . . . . 6 ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵) → 𝐾 ∈ OP) |
| 3 | eqid 2765 | . . . . . . 7 ⊢ (0.‘𝐾) = (0.‘𝐾) | |
| 4 | olm1.u | . . . . . . 7 ⊢ 1 = (1.‘𝐾) | |
| 5 | eqid 2765 | . . . . . . 7 ⊢ (oc‘𝐾) = (oc‘𝐾) | |
| 6 | 3, 4, 5 | opoc1 39833 | . . . . . 6 ⊢ (𝐾 ∈ OP → ((oc‘𝐾)‘ 1 ) = (0.‘𝐾)) |
| 7 | 2, 6 | syl 18 | . . . . 5 ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵) → ((oc‘𝐾)‘ 1 ) = (0.‘𝐾)) |
| 8 | 7 | oveq2d 7416 | . . . 4 ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵) → (((oc‘𝐾)‘𝑋)(join‘𝐾)((oc‘𝐾)‘ 1 )) = (((oc‘𝐾)‘𝑋)(join‘𝐾)(0.‘𝐾))) |
| 9 | olm1.b | . . . . . . 7 ⊢ 𝐵 = (Base‘𝐾) | |
| 10 | 9, 5 | opoccl 39825 | . . . . . 6 ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → ((oc‘𝐾)‘𝑋) ∈ 𝐵) |
| 11 | 1, 10 | sylan 591 | . . . . 5 ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵) → ((oc‘𝐾)‘𝑋) ∈ 𝐵) |
| 12 | eqid 2765 | . . . . . 6 ⊢ (join‘𝐾) = (join‘𝐾) | |
| 13 | 9, 12, 3 | olj01 39856 | . . . . 5 ⊢ ((𝐾 ∈ OL ∧ ((oc‘𝐾)‘𝑋) ∈ 𝐵) → (((oc‘𝐾)‘𝑋)(join‘𝐾)(0.‘𝐾)) = ((oc‘𝐾)‘𝑋)) |
| 14 | 11, 13 | syldan 602 | . . . 4 ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵) → (((oc‘𝐾)‘𝑋)(join‘𝐾)(0.‘𝐾)) = ((oc‘𝐾)‘𝑋)) |
| 15 | 8, 14 | eqtrd 2800 | . . 3 ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵) → (((oc‘𝐾)‘𝑋)(join‘𝐾)((oc‘𝐾)‘ 1 )) = ((oc‘𝐾)‘𝑋)) |
| 16 | 15 | fveq2d 6875 | . 2 ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵) → ((oc‘𝐾)‘(((oc‘𝐾)‘𝑋)(join‘𝐾)((oc‘𝐾)‘ 1 ))) = ((oc‘𝐾)‘((oc‘𝐾)‘𝑋))) |
| 17 | 9, 4 | op1cl 39816 | . . . 4 ⊢ (𝐾 ∈ OP → 1 ∈ 𝐵) |
| 18 | 2, 17 | syl 18 | . . 3 ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵) → 1 ∈ 𝐵) |
| 19 | olm1.m | . . . 4 ⊢ ∧ = (meet‘𝐾) | |
| 20 | 9, 12, 19, 5 | oldmj4 39855 | . . 3 ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 1 ∈ 𝐵) → ((oc‘𝐾)‘(((oc‘𝐾)‘𝑋)(join‘𝐾)((oc‘𝐾)‘ 1 ))) = (𝑋 ∧ 1 )) |
| 21 | 18, 20 | mpd3an3 1486 | . 2 ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵) → ((oc‘𝐾)‘(((oc‘𝐾)‘𝑋)(join‘𝐾)((oc‘𝐾)‘ 1 ))) = (𝑋 ∧ 1 )) |
| 22 | 9, 5 | opococ 39826 | . . 3 ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → ((oc‘𝐾)‘((oc‘𝐾)‘𝑋)) = 𝑋) |
| 23 | 1, 22 | sylan 591 | . 2 ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵) → ((oc‘𝐾)‘((oc‘𝐾)‘𝑋)) = 𝑋) |
| 24 | 16, 21, 23 | 3eqtr3d 2808 | 1 ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵) → (𝑋 ∧ 1 ) = 𝑋) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 400 = wceq 1563 ∈ wcel 2145 ‘cfv 6525 (class class class)co 7400 Basecbs 17257 occoc 17306 joincjn 18355 meetcmee 18356 0.cp0 18465 1.cp1 18466 OPcops 39803 OLcol 39805 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1818 ax-4 1832 ax-5 1933 ax-6 1990 ax-7 2031 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2215 ax-ext 2737 ax-rep 5231 ax-sep 5250 ax-nul 5260 ax-pow 5326 ax-pr 5394 ax-un 7722 |
| This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3an 1103 df-tru 1566 df-fal 1576 df-ex 1803 df-nf 1807 df-sb 2094 df-mo 2569 df-eu 2599 df-clab 2744 df-cleq 2757 df-clel 2840 df-nfc 2914 df-ne 2961 df-ral 3080 df-rex 3090 df-rmo 3370 df-reu 3371 df-rab 3418 df-v 3459 df-sbc 3748 df-csb 3856 df-dif 3910 df-un 3912 df-in 3914 df-ss 3924 df-nul 4289 df-if 4484 df-pw 4560 df-sn 4586 df-pr 4588 df-op 4592 df-uni 4868 df-iun 4953 df-br 5105 df-opab 5167 df-mpt 5186 df-id 5546 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 df-iota 6481 df-fun 6527 df-fn 6528 df-f 6529 df-f1 6530 df-fo 6531 df-f1o 6532 df-fv 6533 df-riota 7357 df-ov 7403 df-oprab 7404 df-proset 18338 df-poset 18357 df-lub 18388 df-glb 18389 df-join 18390 df-meet 18391 df-p0 18467 df-p1 18468 df-lat 18476 df-oposet 39807 df-ol 39809 |
| This theorem is referenced by: olm12 39859 lhpmcvr3 40656 trljat1 40797 trljat2 40798 cdlemc1 40822 cdlemc6 40827 cdleme0cp 40845 cdleme0cq 40846 cdleme1 40858 cdleme4 40869 cdleme5 40871 cdleme8 40881 cdleme9 40884 cdleme10 40885 cdleme20c 40942 cdleme20j 40949 cdleme22e 40975 cdleme22eALTN 40976 cdleme30a 41009 cdleme35b 41081 cdleme35e 41084 cdleme42a 41102 trlcoabs2N 41353 trlcolem 41357 cdlemi1 41449 cdlemk4 41465 dia2dimlem1 41695 cdlemn10 41837 dihglbcpreN 41931 |
| Copyright terms: Public domain | W3C validator |