![]() |
Mathbox for Norm Megill |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > atmod3i1 | Structured version Visualization version GIF version |
Description: Version of modular law that holds in a Hilbert lattice, when one element is an atom. (Contributed by NM, 4-Jun-2012.) (Revised by Mario Carneiro, 10-May-2013.) |
Ref | Expression |
---|---|
atmod.b | ⊢ 𝐵 = (Base‘𝐾) |
atmod.l | ⊢ ≤ = (le‘𝐾) |
atmod.j | ⊢ ∨ = (join‘𝐾) |
atmod.m | ⊢ ∧ = (meet‘𝐾) |
atmod.a | ⊢ 𝐴 = (Atoms‘𝐾) |
Ref | Expression |
---|---|
atmod3i1 | ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑃 ≤ 𝑋) → (𝑃 ∨ (𝑋 ∧ 𝑌)) = (𝑋 ∧ (𝑃 ∨ 𝑌))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simp1 1127 | . . 3 ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑃 ≤ 𝑋) → 𝐾 ∈ HL) | |
2 | simp21 1220 | . . 3 ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑃 ≤ 𝑋) → 𝑃 ∈ 𝐴) | |
3 | simp23 1222 | . . 3 ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑃 ≤ 𝑋) → 𝑌 ∈ 𝐵) | |
4 | simp22 1221 | . . 3 ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑃 ≤ 𝑋) → 𝑋 ∈ 𝐵) | |
5 | simp3 1129 | . . 3 ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑃 ≤ 𝑋) → 𝑃 ≤ 𝑋) | |
6 | atmod.b | . . . 4 ⊢ 𝐵 = (Base‘𝐾) | |
7 | atmod.l | . . . 4 ⊢ ≤ = (le‘𝐾) | |
8 | atmod.j | . . . 4 ⊢ ∨ = (join‘𝐾) | |
9 | atmod.m | . . . 4 ⊢ ∧ = (meet‘𝐾) | |
10 | atmod.a | . . . 4 ⊢ 𝐴 = (Atoms‘𝐾) | |
11 | 6, 7, 8, 9, 10 | atmod1i1 36016 | . . 3 ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) ∧ 𝑃 ≤ 𝑋) → (𝑃 ∨ (𝑌 ∧ 𝑋)) = ((𝑃 ∨ 𝑌) ∧ 𝑋)) |
12 | 1, 2, 3, 4, 5, 11 | syl131anc 1451 | . 2 ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑃 ≤ 𝑋) → (𝑃 ∨ (𝑌 ∧ 𝑋)) = ((𝑃 ∨ 𝑌) ∧ 𝑋)) |
13 | hllat 35522 | . . . . 5 ⊢ (𝐾 ∈ HL → 𝐾 ∈ Lat) | |
14 | 13 | 3ad2ant1 1124 | . . . 4 ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑃 ≤ 𝑋) → 𝐾 ∈ Lat) |
15 | 6, 9 | latmcom 17465 | . . . 4 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∧ 𝑌) = (𝑌 ∧ 𝑋)) |
16 | 14, 4, 3, 15 | syl3anc 1439 | . . 3 ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑃 ≤ 𝑋) → (𝑋 ∧ 𝑌) = (𝑌 ∧ 𝑋)) |
17 | 16 | oveq2d 6940 | . 2 ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑃 ≤ 𝑋) → (𝑃 ∨ (𝑋 ∧ 𝑌)) = (𝑃 ∨ (𝑌 ∧ 𝑋))) |
18 | 6, 10 | atbase 35448 | . . . . 5 ⊢ (𝑃 ∈ 𝐴 → 𝑃 ∈ 𝐵) |
19 | 2, 18 | syl 17 | . . . 4 ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑃 ≤ 𝑋) → 𝑃 ∈ 𝐵) |
20 | 6, 8 | latjcl 17441 | . . . 4 ⊢ ((𝐾 ∈ Lat ∧ 𝑃 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑃 ∨ 𝑌) ∈ 𝐵) |
21 | 14, 19, 3, 20 | syl3anc 1439 | . . 3 ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑃 ≤ 𝑋) → (𝑃 ∨ 𝑌) ∈ 𝐵) |
22 | 6, 9 | latmcom 17465 | . . 3 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ (𝑃 ∨ 𝑌) ∈ 𝐵) → (𝑋 ∧ (𝑃 ∨ 𝑌)) = ((𝑃 ∨ 𝑌) ∧ 𝑋)) |
23 | 14, 4, 21, 22 | syl3anc 1439 | . 2 ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑃 ≤ 𝑋) → (𝑋 ∧ (𝑃 ∨ 𝑌)) = ((𝑃 ∨ 𝑌) ∧ 𝑋)) |
24 | 12, 17, 23 | 3eqtr4d 2824 | 1 ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑃 ≤ 𝑋) → (𝑃 ∨ (𝑋 ∧ 𝑌)) = (𝑋 ∧ (𝑃 ∨ 𝑌))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1071 = wceq 1601 ∈ wcel 2107 class class class wbr 4888 ‘cfv 6137 (class class class)co 6924 Basecbs 16259 lecple 16349 joincjn 17334 meetcmee 17335 Latclat 17435 Atomscatm 35422 HLchlt 35509 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2055 ax-8 2109 ax-9 2116 ax-10 2135 ax-11 2150 ax-12 2163 ax-13 2334 ax-ext 2754 ax-rep 5008 ax-sep 5019 ax-nul 5027 ax-pow 5079 ax-pr 5140 ax-un 7228 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 837 df-3an 1073 df-tru 1605 df-ex 1824 df-nf 1828 df-sb 2012 df-mo 2551 df-eu 2587 df-clab 2764 df-cleq 2770 df-clel 2774 df-nfc 2921 df-ne 2970 df-ral 3095 df-rex 3096 df-reu 3097 df-rab 3099 df-v 3400 df-sbc 3653 df-csb 3752 df-dif 3795 df-un 3797 df-in 3799 df-ss 3806 df-nul 4142 df-if 4308 df-pw 4381 df-sn 4399 df-pr 4401 df-op 4405 df-uni 4674 df-iun 4757 df-iin 4758 df-br 4889 df-opab 4951 df-mpt 4968 df-id 5263 df-xp 5363 df-rel 5364 df-cnv 5365 df-co 5366 df-dm 5367 df-rn 5368 df-res 5369 df-ima 5370 df-iota 6101 df-fun 6139 df-fn 6140 df-f 6141 df-f1 6142 df-fo 6143 df-f1o 6144 df-fv 6145 df-riota 6885 df-ov 6927 df-oprab 6928 df-mpt2 6929 df-1st 7447 df-2nd 7448 df-proset 17318 df-poset 17336 df-plt 17348 df-lub 17364 df-glb 17365 df-join 17366 df-meet 17367 df-p0 17429 df-lat 17436 df-clat 17498 df-oposet 35335 df-ol 35337 df-oml 35338 df-covers 35425 df-ats 35426 df-atl 35457 df-cvlat 35481 df-hlat 35510 df-psubsp 35662 df-pmap 35663 df-padd 35955 |
This theorem is referenced by: dalawlem2 36031 dalawlem3 36032 dalawlem6 36035 lhpmcvr3 36184 cdleme0cp 36373 cdleme0cq 36374 cdleme1 36386 cdleme4 36397 cdleme5 36399 cdleme8 36409 cdleme9 36412 cdleme10 36413 cdleme15b 36434 cdleme22e 36503 cdleme22eALTN 36504 cdleme23c 36510 cdleme35b 36609 cdleme35e 36612 cdleme42a 36630 trlcoabs2N 36881 cdlemi1 36977 cdlemk4 36993 dia2dimlem1 37223 dia2dimlem2 37224 cdlemn10 37365 dihglbcpreN 37459 |
Copyright terms: Public domain | W3C validator |