![]() |
Mathbox for Norm Megill |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > hlatjidm | Structured version Visualization version GIF version |
Description: Idempotence of join operation. Frequently-used special case of latjcom 17374 for atoms. (Contributed by NM, 15-Jul-2012.) |
Ref | Expression |
---|---|
hlatjcom.j | ⊢ ∨ = (join‘𝐾) |
hlatjcom.a | ⊢ 𝐴 = (Atoms‘𝐾) |
Ref | Expression |
---|---|
hlatjidm | ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐴) → (𝑋 ∨ 𝑋) = 𝑋) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hllat 35384 | . 2 ⊢ (𝐾 ∈ HL → 𝐾 ∈ Lat) | |
2 | eqid 2799 | . . 3 ⊢ (Base‘𝐾) = (Base‘𝐾) | |
3 | hlatjcom.a | . . 3 ⊢ 𝐴 = (Atoms‘𝐾) | |
4 | 2, 3 | atbase 35310 | . 2 ⊢ (𝑋 ∈ 𝐴 → 𝑋 ∈ (Base‘𝐾)) |
5 | hlatjcom.j | . . 3 ⊢ ∨ = (join‘𝐾) | |
6 | 2, 5 | latjidm 17389 | . 2 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ (Base‘𝐾)) → (𝑋 ∨ 𝑋) = 𝑋) |
7 | 1, 4, 6 | syl2an 590 | 1 ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐴) → (𝑋 ∨ 𝑋) = 𝑋) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 385 = wceq 1653 ∈ wcel 2157 ‘cfv 6101 (class class class)co 6878 Basecbs 16184 joincjn 17259 Latclat 17360 Atomscatm 35284 HLchlt 35371 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1891 ax-4 1905 ax-5 2006 ax-6 2072 ax-7 2107 ax-8 2159 ax-9 2166 ax-10 2185 ax-11 2200 ax-12 2213 ax-13 2377 ax-ext 2777 ax-rep 4964 ax-sep 4975 ax-nul 4983 ax-pow 5035 ax-pr 5097 ax-un 7183 |
This theorem depends on definitions: df-bi 199 df-an 386 df-or 875 df-3an 1110 df-tru 1657 df-ex 1876 df-nf 1880 df-sb 2065 df-mo 2591 df-eu 2609 df-clab 2786 df-cleq 2792 df-clel 2795 df-nfc 2930 df-ne 2972 df-ral 3094 df-rex 3095 df-reu 3096 df-rab 3098 df-v 3387 df-sbc 3634 df-csb 3729 df-dif 3772 df-un 3774 df-in 3776 df-ss 3783 df-nul 4116 df-if 4278 df-pw 4351 df-sn 4369 df-pr 4371 df-op 4375 df-uni 4629 df-iun 4712 df-br 4844 df-opab 4906 df-mpt 4923 df-id 5220 df-xp 5318 df-rel 5319 df-cnv 5320 df-co 5321 df-dm 5322 df-rn 5323 df-res 5324 df-ima 5325 df-iota 6064 df-fun 6103 df-fn 6104 df-f 6105 df-f1 6106 df-fo 6107 df-f1o 6108 df-fv 6109 df-riota 6839 df-ov 6881 df-oprab 6882 df-proset 17243 df-poset 17261 df-lub 17289 df-glb 17290 df-join 17291 df-meet 17292 df-lat 17361 df-ats 35288 df-atl 35319 df-cvlat 35343 df-hlat 35372 |
This theorem is referenced by: atcvr0eq 35447 lnnat 35448 atcvrj0 35449 atltcvr 35456 3dim2 35489 3dim3 35490 islln2a 35538 2at0mat0 35546 lplnnle2at 35562 lplnnleat 35563 islpln2a 35569 lvolnle3at 35603 lvolnleat 35604 lvolnlelln 35605 2atnelvolN 35608 islvol2aN 35613 dalempnes 35672 dalemqnet 35673 2llnma3r 35809 dalawlem12 35903 4atex2-0aOLDN 36099 idltrn 36171 trl0 36191 trlval3 36208 cdleme3b 36250 cdleme11h 36287 cdleme16c 36301 cdleme18b 36313 cdleme20j 36339 cdleme42ke 36506 cdleme50trn3 36574 cdlemb3 36627 cdlemg8a 36648 trlcone 36749 dia2dimlem13 37097 |
Copyright terms: Public domain | W3C validator |