![]() |
Mathbox for Norm Megill |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > lhpat | Structured version Visualization version GIF version |
Description: Create an atom under a co-atom. Part of proof of Lemma B in [Crawley] p. 112. (Contributed by NM, 23-May-2012.) |
Ref | Expression |
---|---|
lhpat.l | ⊢ ≤ = (le‘𝐾) |
lhpat.j | ⊢ ∨ = (join‘𝐾) |
lhpat.m | ⊢ ∧ = (meet‘𝐾) |
lhpat.a | ⊢ 𝐴 = (Atoms‘𝐾) |
lhpat.h | ⊢ 𝐻 = (LHyp‘𝐾) |
Ref | Expression |
---|---|
lhpat | ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄)) → ((𝑃 ∨ 𝑄) ∧ 𝑊) ∈ 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simp1l 1237 | . 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄)) → 𝐾 ∈ HL) | |
2 | simp2l 1239 | . 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄)) → 𝑃 ∈ 𝐴) | |
3 | simp3l 1241 | . 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄)) → 𝑄 ∈ 𝐴) | |
4 | simp1r 1238 | . . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄)) → 𝑊 ∈ 𝐻) | |
5 | eqid 2752 | . . . 4 ⊢ (Base‘𝐾) = (Base‘𝐾) | |
6 | lhpat.h | . . . 4 ⊢ 𝐻 = (LHyp‘𝐾) | |
7 | 5, 6 | lhpbase 35779 | . . 3 ⊢ (𝑊 ∈ 𝐻 → 𝑊 ∈ (Base‘𝐾)) |
8 | 4, 7 | syl 17 | . 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄)) → 𝑊 ∈ (Base‘𝐾)) |
9 | simp3r 1242 | . 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄)) → 𝑃 ≠ 𝑄) | |
10 | eqid 2752 | . . . 4 ⊢ (1.‘𝐾) = (1.‘𝐾) | |
11 | eqid 2752 | . . . 4 ⊢ ( ⋖ ‘𝐾) = ( ⋖ ‘𝐾) | |
12 | 10, 11, 6 | lhp1cvr 35780 | . . 3 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 𝑊( ⋖ ‘𝐾)(1.‘𝐾)) |
13 | 12 | 3ad2ant1 1127 | . 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄)) → 𝑊( ⋖ ‘𝐾)(1.‘𝐾)) |
14 | simp2r 1240 | . 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄)) → ¬ 𝑃 ≤ 𝑊) | |
15 | lhpat.l | . . 3 ⊢ ≤ = (le‘𝐾) | |
16 | lhpat.j | . . 3 ⊢ ∨ = (join‘𝐾) | |
17 | lhpat.m | . . 3 ⊢ ∧ = (meet‘𝐾) | |
18 | lhpat.a | . . 3 ⊢ 𝐴 = (Atoms‘𝐾) | |
19 | 5, 15, 16, 17, 10, 11, 18 | 1cvrat 35257 | . 2 ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑊 ∈ (Base‘𝐾)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑊( ⋖ ‘𝐾)(1.‘𝐾) ∧ ¬ 𝑃 ≤ 𝑊)) → ((𝑃 ∨ 𝑄) ∧ 𝑊) ∈ 𝐴) |
20 | 1, 2, 3, 8, 9, 13, 14, 19 | syl133anc 1496 | 1 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄)) → ((𝑃 ∨ 𝑄) ∧ 𝑊) ∈ 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 383 ∧ w3a 1072 = wceq 1624 ∈ wcel 2131 ≠ wne 2924 class class class wbr 4796 ‘cfv 6041 (class class class)co 6805 Basecbs 16051 lecple 16142 joincjn 17137 meetcmee 17138 1.cp1 17231 ⋖ ccvr 35044 Atomscatm 35045 HLchlt 35132 LHypclh 35765 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1863 ax-4 1878 ax-5 1980 ax-6 2046 ax-7 2082 ax-8 2133 ax-9 2140 ax-10 2160 ax-11 2175 ax-12 2188 ax-13 2383 ax-ext 2732 ax-rep 4915 ax-sep 4925 ax-nul 4933 ax-pow 4984 ax-pr 5047 ax-un 7106 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3an 1074 df-tru 1627 df-ex 1846 df-nf 1851 df-sb 2039 df-eu 2603 df-mo 2604 df-clab 2739 df-cleq 2745 df-clel 2748 df-nfc 2883 df-ne 2925 df-ral 3047 df-rex 3048 df-reu 3049 df-rab 3051 df-v 3334 df-sbc 3569 df-csb 3667 df-dif 3710 df-un 3712 df-in 3714 df-ss 3721 df-nul 4051 df-if 4223 df-pw 4296 df-sn 4314 df-pr 4316 df-op 4320 df-uni 4581 df-iun 4666 df-br 4797 df-opab 4857 df-mpt 4874 df-id 5166 df-xp 5264 df-rel 5265 df-cnv 5266 df-co 5267 df-dm 5268 df-rn 5269 df-res 5270 df-ima 5271 df-iota 6004 df-fun 6043 df-fn 6044 df-f 6045 df-f1 6046 df-fo 6047 df-f1o 6048 df-fv 6049 df-riota 6766 df-ov 6808 df-oprab 6809 df-preset 17121 df-poset 17139 df-plt 17151 df-lub 17167 df-glb 17168 df-join 17169 df-meet 17170 df-p0 17232 df-p1 17233 df-lat 17239 df-clat 17301 df-oposet 34958 df-ol 34960 df-oml 34961 df-covers 35048 df-ats 35049 df-atl 35080 df-cvlat 35104 df-hlat 35133 df-lhyp 35769 |
This theorem is referenced by: lhpat2 35826 4atexlemex6 35855 trlat 35951 cdlemc5 35977 cdleme3e 36014 cdleme7b 36026 cdleme11k 36050 cdleme16e 36064 cdleme16f 36065 cdlemeda 36080 cdleme22cN 36124 cdleme22d 36125 cdleme23b 36132 cdlemf2 36344 cdlemg12g 36431 cdlemg17dALTN 36446 cdlemg19a 36465 |
Copyright terms: Public domain | W3C validator |