![]() |
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 28871 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 35290 | . . . . . . 7 ⊢ (𝐾 ∈ OL → 𝐾 ∈ OP) | |
2 | 1 | adantr 474 | . . . . . 6 ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵) → 𝐾 ∈ OP) |
3 | eqid 2826 | . . . . . . 7 ⊢ (0.‘𝐾) = (0.‘𝐾) | |
4 | olm1.u | . . . . . . 7 ⊢ 1 = (1.‘𝐾) | |
5 | eqid 2826 | . . . . . . 7 ⊢ (oc‘𝐾) = (oc‘𝐾) | |
6 | 3, 4, 5 | opoc1 35278 | . . . . . 6 ⊢ (𝐾 ∈ OP → ((oc‘𝐾)‘ 1 ) = (0.‘𝐾)) |
7 | 2, 6 | syl 17 | . . . . 5 ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵) → ((oc‘𝐾)‘ 1 ) = (0.‘𝐾)) |
8 | 7 | oveq2d 6922 | . . . 4 ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵) → (((oc‘𝐾)‘𝑋)(join‘𝐾)((oc‘𝐾)‘ 1 )) = (((oc‘𝐾)‘𝑋)(join‘𝐾)(0.‘𝐾))) |
9 | olm1.b | . . . . . . 7 ⊢ 𝐵 = (Base‘𝐾) | |
10 | 9, 5 | opoccl 35270 | . . . . . 6 ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → ((oc‘𝐾)‘𝑋) ∈ 𝐵) |
11 | 1, 10 | sylan 577 | . . . . 5 ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵) → ((oc‘𝐾)‘𝑋) ∈ 𝐵) |
12 | eqid 2826 | . . . . . 6 ⊢ (join‘𝐾) = (join‘𝐾) | |
13 | 9, 12, 3 | olj01 35301 | . . . . 5 ⊢ ((𝐾 ∈ OL ∧ ((oc‘𝐾)‘𝑋) ∈ 𝐵) → (((oc‘𝐾)‘𝑋)(join‘𝐾)(0.‘𝐾)) = ((oc‘𝐾)‘𝑋)) |
14 | 11, 13 | syldan 587 | . . . 4 ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵) → (((oc‘𝐾)‘𝑋)(join‘𝐾)(0.‘𝐾)) = ((oc‘𝐾)‘𝑋)) |
15 | 8, 14 | eqtrd 2862 | . . 3 ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵) → (((oc‘𝐾)‘𝑋)(join‘𝐾)((oc‘𝐾)‘ 1 )) = ((oc‘𝐾)‘𝑋)) |
16 | 15 | fveq2d 6438 | . 2 ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵) → ((oc‘𝐾)‘(((oc‘𝐾)‘𝑋)(join‘𝐾)((oc‘𝐾)‘ 1 ))) = ((oc‘𝐾)‘((oc‘𝐾)‘𝑋))) |
17 | 9, 4 | op1cl 35261 | . . . 4 ⊢ (𝐾 ∈ OP → 1 ∈ 𝐵) |
18 | 2, 17 | syl 17 | . . 3 ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵) → 1 ∈ 𝐵) |
19 | olm1.m | . . . 4 ⊢ ∧ = (meet‘𝐾) | |
20 | 9, 12, 19, 5 | oldmj4 35300 | . . 3 ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 1 ∈ 𝐵) → ((oc‘𝐾)‘(((oc‘𝐾)‘𝑋)(join‘𝐾)((oc‘𝐾)‘ 1 ))) = (𝑋 ∧ 1 )) |
21 | 18, 20 | mpd3an3 1592 | . 2 ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵) → ((oc‘𝐾)‘(((oc‘𝐾)‘𝑋)(join‘𝐾)((oc‘𝐾)‘ 1 ))) = (𝑋 ∧ 1 )) |
22 | 9, 5 | opococ 35271 | . . 3 ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → ((oc‘𝐾)‘((oc‘𝐾)‘𝑋)) = 𝑋) |
23 | 1, 22 | sylan 577 | . 2 ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵) → ((oc‘𝐾)‘((oc‘𝐾)‘𝑋)) = 𝑋) |
24 | 16, 21, 23 | 3eqtr3d 2870 | 1 ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵) → (𝑋 ∧ 1 ) = 𝑋) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 386 = wceq 1658 ∈ wcel 2166 ‘cfv 6124 (class class class)co 6906 Basecbs 16223 occoc 16314 joincjn 17298 meetcmee 17299 0.cp0 17391 1.cp1 17392 OPcops 35248 OLcol 35250 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1896 ax-4 1910 ax-5 2011 ax-6 2077 ax-7 2114 ax-8 2168 ax-9 2175 ax-10 2194 ax-11 2209 ax-12 2222 ax-13 2391 ax-ext 2804 ax-rep 4995 ax-sep 5006 ax-nul 5014 ax-pow 5066 ax-pr 5128 ax-un 7210 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 881 df-3an 1115 df-tru 1662 df-ex 1881 df-nf 1885 df-sb 2070 df-mo 2606 df-eu 2641 df-clab 2813 df-cleq 2819 df-clel 2822 df-nfc 2959 df-ne 3001 df-ral 3123 df-rex 3124 df-reu 3125 df-rab 3127 df-v 3417 df-sbc 3664 df-csb 3759 df-dif 3802 df-un 3804 df-in 3806 df-ss 3813 df-nul 4146 df-if 4308 df-pw 4381 df-sn 4399 df-pr 4401 df-op 4405 df-uni 4660 df-iun 4743 df-br 4875 df-opab 4937 df-mpt 4954 df-id 5251 df-xp 5349 df-rel 5350 df-cnv 5351 df-co 5352 df-dm 5353 df-rn 5354 df-res 5355 df-ima 5356 df-iota 6087 df-fun 6126 df-fn 6127 df-f 6128 df-f1 6129 df-fo 6130 df-f1o 6131 df-fv 6132 df-riota 6867 df-ov 6909 df-oprab 6910 df-proset 17282 df-poset 17300 df-lub 17328 df-glb 17329 df-join 17330 df-meet 17331 df-p0 17393 df-p1 17394 df-lat 17400 df-oposet 35252 df-ol 35254 |
This theorem is referenced by: olm12 35304 lhpmcvr3 36101 trljat1 36242 trljat2 36243 cdlemc1 36267 cdlemc6 36272 cdleme0cp 36290 cdleme0cq 36291 cdleme1 36303 cdleme4 36314 cdleme5 36316 cdleme8 36326 cdleme9 36329 cdleme10 36330 cdleme20c 36387 cdleme20j 36394 cdleme22e 36420 cdleme22eALTN 36421 cdleme30a 36454 cdleme35b 36526 cdleme35e 36529 cdleme42a 36547 trlcoabs2N 36798 trlcolem 36802 cdlemi1 36894 cdlemk4 36910 dia2dimlem1 37140 cdlemn10 37282 dihglbcpreN 37376 |
Copyright terms: Public domain | W3C validator |