Mathbox for Norm Megill |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > pol1N | Structured version Visualization version GIF version |
Description: The polarity of the whole projective subspace is the empty space. Remark in [Holland95] p. 223. (Contributed by NM, 24-Jan-2012.) (New usage is discouraged.) |
Ref | Expression |
---|---|
polssat.a | ⊢ 𝐴 = (Atoms‘𝐾) |
polssat.p | ⊢ ⊥ = (⊥𝑃‘𝐾) |
Ref | Expression |
---|---|
pol1N | ⊢ (𝐾 ∈ HL → ( ⊥ ‘𝐴) = ∅) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ssid 3938 | . . 3 ⊢ 𝐴 ⊆ 𝐴 | |
2 | eqid 2738 | . . . 4 ⊢ (lub‘𝐾) = (lub‘𝐾) | |
3 | eqid 2738 | . . . 4 ⊢ (oc‘𝐾) = (oc‘𝐾) | |
4 | polssat.a | . . . 4 ⊢ 𝐴 = (Atoms‘𝐾) | |
5 | eqid 2738 | . . . 4 ⊢ (pmap‘𝐾) = (pmap‘𝐾) | |
6 | polssat.p | . . . 4 ⊢ ⊥ = (⊥𝑃‘𝐾) | |
7 | 2, 3, 4, 5, 6 | polval2N 37684 | . . 3 ⊢ ((𝐾 ∈ HL ∧ 𝐴 ⊆ 𝐴) → ( ⊥ ‘𝐴) = ((pmap‘𝐾)‘((oc‘𝐾)‘((lub‘𝐾)‘𝐴)))) |
8 | 1, 7 | mpan2 691 | . 2 ⊢ (𝐾 ∈ HL → ( ⊥ ‘𝐴) = ((pmap‘𝐾)‘((oc‘𝐾)‘((lub‘𝐾)‘𝐴)))) |
9 | hlop 37140 | . . . . . . . . . 10 ⊢ (𝐾 ∈ HL → 𝐾 ∈ OP) | |
10 | eqid 2738 | . . . . . . . . . . 11 ⊢ (Base‘𝐾) = (Base‘𝐾) | |
11 | 10, 4 | atbase 37067 | . . . . . . . . . 10 ⊢ (𝑝 ∈ 𝐴 → 𝑝 ∈ (Base‘𝐾)) |
12 | eqid 2738 | . . . . . . . . . . 11 ⊢ (le‘𝐾) = (le‘𝐾) | |
13 | eqid 2738 | . . . . . . . . . . 11 ⊢ (1.‘𝐾) = (1.‘𝐾) | |
14 | 10, 12, 13 | ople1 36969 | . . . . . . . . . 10 ⊢ ((𝐾 ∈ OP ∧ 𝑝 ∈ (Base‘𝐾)) → 𝑝(le‘𝐾)(1.‘𝐾)) |
15 | 9, 11, 14 | syl2an 599 | . . . . . . . . 9 ⊢ ((𝐾 ∈ HL ∧ 𝑝 ∈ 𝐴) → 𝑝(le‘𝐾)(1.‘𝐾)) |
16 | 15 | ralrimiva 3106 | . . . . . . . 8 ⊢ (𝐾 ∈ HL → ∀𝑝 ∈ 𝐴 𝑝(le‘𝐾)(1.‘𝐾)) |
17 | rabid2 3306 | . . . . . . . 8 ⊢ (𝐴 = {𝑝 ∈ 𝐴 ∣ 𝑝(le‘𝐾)(1.‘𝐾)} ↔ ∀𝑝 ∈ 𝐴 𝑝(le‘𝐾)(1.‘𝐾)) | |
18 | 16, 17 | sylibr 237 | . . . . . . 7 ⊢ (𝐾 ∈ HL → 𝐴 = {𝑝 ∈ 𝐴 ∣ 𝑝(le‘𝐾)(1.‘𝐾)}) |
19 | 18 | fveq2d 6740 | . . . . . 6 ⊢ (𝐾 ∈ HL → ((lub‘𝐾)‘𝐴) = ((lub‘𝐾)‘{𝑝 ∈ 𝐴 ∣ 𝑝(le‘𝐾)(1.‘𝐾)})) |
20 | hlomcmat 37143 | . . . . . . 7 ⊢ (𝐾 ∈ HL → (𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat)) | |
21 | 10, 13 | op1cl 36963 | . . . . . . . 8 ⊢ (𝐾 ∈ OP → (1.‘𝐾) ∈ (Base‘𝐾)) |
22 | 9, 21 | syl 17 | . . . . . . 7 ⊢ (𝐾 ∈ HL → (1.‘𝐾) ∈ (Base‘𝐾)) |
23 | 10, 12, 2, 4 | atlatmstc 37097 | . . . . . . 7 ⊢ (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ (1.‘𝐾) ∈ (Base‘𝐾)) → ((lub‘𝐾)‘{𝑝 ∈ 𝐴 ∣ 𝑝(le‘𝐾)(1.‘𝐾)}) = (1.‘𝐾)) |
24 | 20, 22, 23 | syl2anc 587 | . . . . . 6 ⊢ (𝐾 ∈ HL → ((lub‘𝐾)‘{𝑝 ∈ 𝐴 ∣ 𝑝(le‘𝐾)(1.‘𝐾)}) = (1.‘𝐾)) |
25 | 19, 24 | eqtr2d 2779 | . . . . 5 ⊢ (𝐾 ∈ HL → (1.‘𝐾) = ((lub‘𝐾)‘𝐴)) |
26 | 25 | fveq2d 6740 | . . . 4 ⊢ (𝐾 ∈ HL → ((oc‘𝐾)‘(1.‘𝐾)) = ((oc‘𝐾)‘((lub‘𝐾)‘𝐴))) |
27 | eqid 2738 | . . . . . 6 ⊢ (0.‘𝐾) = (0.‘𝐾) | |
28 | 27, 13, 3 | opoc1 36980 | . . . . 5 ⊢ (𝐾 ∈ OP → ((oc‘𝐾)‘(1.‘𝐾)) = (0.‘𝐾)) |
29 | 9, 28 | syl 17 | . . . 4 ⊢ (𝐾 ∈ HL → ((oc‘𝐾)‘(1.‘𝐾)) = (0.‘𝐾)) |
30 | 26, 29 | eqtr3d 2780 | . . 3 ⊢ (𝐾 ∈ HL → ((oc‘𝐾)‘((lub‘𝐾)‘𝐴)) = (0.‘𝐾)) |
31 | 30 | fveq2d 6740 | . 2 ⊢ (𝐾 ∈ HL → ((pmap‘𝐾)‘((oc‘𝐾)‘((lub‘𝐾)‘𝐴))) = ((pmap‘𝐾)‘(0.‘𝐾))) |
32 | hlatl 37138 | . . 3 ⊢ (𝐾 ∈ HL → 𝐾 ∈ AtLat) | |
33 | 27, 5 | pmap0 37543 | . . 3 ⊢ (𝐾 ∈ AtLat → ((pmap‘𝐾)‘(0.‘𝐾)) = ∅) |
34 | 32, 33 | syl 17 | . 2 ⊢ (𝐾 ∈ HL → ((pmap‘𝐾)‘(0.‘𝐾)) = ∅) |
35 | 8, 31, 34 | 3eqtrd 2782 | 1 ⊢ (𝐾 ∈ HL → ( ⊥ ‘𝐴) = ∅) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1089 = wceq 1543 ∈ wcel 2111 ∀wral 3062 {crab 3066 ⊆ wss 3881 ∅c0 4252 class class class wbr 5068 ‘cfv 6398 Basecbs 16785 lecple 16834 occoc 16835 lubclub 17841 0.cp0 17954 1.cp1 17955 CLatccla 18029 OPcops 36950 OMLcoml 36953 Atomscatm 37041 AtLatcal 37042 HLchlt 37128 pmapcpmap 37275 ⊥𝑃cpolN 37680 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2159 ax-12 2176 ax-ext 2709 ax-rep 5194 ax-sep 5207 ax-nul 5214 ax-pow 5273 ax-pr 5337 ax-un 7542 ax-riotaBAD 36731 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-nf 1792 df-sb 2072 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2817 df-nfc 2887 df-ne 2942 df-ral 3067 df-rex 3068 df-reu 3069 df-rmo 3070 df-rab 3071 df-v 3423 df-sbc 3710 df-csb 3827 df-dif 3884 df-un 3886 df-in 3888 df-ss 3898 df-nul 4253 df-if 4455 df-pw 4530 df-sn 4557 df-pr 4559 df-op 4563 df-uni 4835 df-iun 4921 df-iin 4922 df-br 5069 df-opab 5131 df-mpt 5151 df-id 5470 df-xp 5572 df-rel 5573 df-cnv 5574 df-co 5575 df-dm 5576 df-rn 5577 df-res 5578 df-ima 5579 df-iota 6356 df-fun 6400 df-fn 6401 df-f 6402 df-f1 6403 df-fo 6404 df-f1o 6405 df-fv 6406 df-riota 7189 df-ov 7235 df-oprab 7236 df-undef 8036 df-proset 17827 df-poset 17845 df-plt 17861 df-lub 17877 df-glb 17878 df-join 17879 df-meet 17880 df-p0 17956 df-p1 17957 df-lat 17963 df-clat 18030 df-oposet 36954 df-ol 36956 df-oml 36957 df-covers 37044 df-ats 37045 df-atl 37076 df-cvlat 37100 df-hlat 37129 df-pmap 37282 df-polarityN 37681 |
This theorem is referenced by: 2pol0N 37689 1psubclN 37722 |
Copyright terms: Public domain | W3C validator |