Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  snatpsubN Structured version   Visualization version   GIF version

Theorem snatpsubN 37527
Description: The singleton of an atom is a projective subspace. (Contributed by NM, 9-Sep-2013.) (New usage is discouraged.)
Hypotheses
Ref Expression
snpsub.a 𝐴 = (Atoms‘𝐾)
snpsub.s 𝑆 = (PSubSp‘𝐾)
Assertion
Ref Expression
snatpsubN ((𝐾 ∈ AtLat ∧ 𝑃𝐴) → {𝑃} ∈ 𝑆)

Proof of Theorem snatpsubN
Dummy variables 𝑞 𝑝 𝑟 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 snssi 4735 . . . . . 6 (𝑃𝐴 → {𝑃} ⊆ 𝐴)
21adantl 485 . . . . 5 ((𝐾 ∈ AtLat ∧ 𝑃𝐴) → {𝑃} ⊆ 𝐴)
3 atllat 37077 . . . . . . . . . . . . . . 15 (𝐾 ∈ AtLat → 𝐾 ∈ Lat)
4 eqid 2738 . . . . . . . . . . . . . . . 16 (Base‘𝐾) = (Base‘𝐾)
5 snpsub.a . . . . . . . . . . . . . . . 16 𝐴 = (Atoms‘𝐾)
64, 5atbase 37066 . . . . . . . . . . . . . . 15 (𝑃𝐴𝑃 ∈ (Base‘𝐾))
7 eqid 2738 . . . . . . . . . . . . . . . 16 (join‘𝐾) = (join‘𝐾)
84, 7latjidm 17992 . . . . . . . . . . . . . . 15 ((𝐾 ∈ Lat ∧ 𝑃 ∈ (Base‘𝐾)) → (𝑃(join‘𝐾)𝑃) = 𝑃)
93, 6, 8syl2an 599 . . . . . . . . . . . . . 14 ((𝐾 ∈ AtLat ∧ 𝑃𝐴) → (𝑃(join‘𝐾)𝑃) = 𝑃)
109adantr 484 . . . . . . . . . . . . 13 (((𝐾 ∈ AtLat ∧ 𝑃𝐴) ∧ 𝑟𝐴) → (𝑃(join‘𝐾)𝑃) = 𝑃)
1110breq2d 5079 . . . . . . . . . . . 12 (((𝐾 ∈ AtLat ∧ 𝑃𝐴) ∧ 𝑟𝐴) → (𝑟(le‘𝐾)(𝑃(join‘𝐾)𝑃) ↔ 𝑟(le‘𝐾)𝑃))
12 eqid 2738 . . . . . . . . . . . . . . . 16 (le‘𝐾) = (le‘𝐾)
1312, 5atcmp 37088 . . . . . . . . . . . . . . 15 ((𝐾 ∈ AtLat ∧ 𝑟𝐴𝑃𝐴) → (𝑟(le‘𝐾)𝑃𝑟 = 𝑃))
14133com23 1128 . . . . . . . . . . . . . 14 ((𝐾 ∈ AtLat ∧ 𝑃𝐴𝑟𝐴) → (𝑟(le‘𝐾)𝑃𝑟 = 𝑃))
15143expa 1120 . . . . . . . . . . . . 13 (((𝐾 ∈ AtLat ∧ 𝑃𝐴) ∧ 𝑟𝐴) → (𝑟(le‘𝐾)𝑃𝑟 = 𝑃))
1615biimpd 232 . . . . . . . . . . . 12 (((𝐾 ∈ AtLat ∧ 𝑃𝐴) ∧ 𝑟𝐴) → (𝑟(le‘𝐾)𝑃𝑟 = 𝑃))
1711, 16sylbid 243 . . . . . . . . . . 11 (((𝐾 ∈ AtLat ∧ 𝑃𝐴) ∧ 𝑟𝐴) → (𝑟(le‘𝐾)(𝑃(join‘𝐾)𝑃) → 𝑟 = 𝑃))
1817adantld 494 . . . . . . . . . 10 (((𝐾 ∈ AtLat ∧ 𝑃𝐴) ∧ 𝑟𝐴) → (((𝑝 = 𝑃𝑞 = 𝑃) ∧ 𝑟(le‘𝐾)(𝑃(join‘𝐾)𝑃)) → 𝑟 = 𝑃))
19 velsn 4571 . . . . . . . . . . . . 13 (𝑝 ∈ {𝑃} ↔ 𝑝 = 𝑃)
20 velsn 4571 . . . . . . . . . . . . 13 (𝑞 ∈ {𝑃} ↔ 𝑞 = 𝑃)
2119, 20anbi12i 630 . . . . . . . . . . . 12 ((𝑝 ∈ {𝑃} ∧ 𝑞 ∈ {𝑃}) ↔ (𝑝 = 𝑃𝑞 = 𝑃))
2221anbi1i 627 . . . . . . . . . . 11 (((𝑝 ∈ {𝑃} ∧ 𝑞 ∈ {𝑃}) ∧ 𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞)) ↔ ((𝑝 = 𝑃𝑞 = 𝑃) ∧ 𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞)))
23 oveq12 7240 . . . . . . . . . . . . 13 ((𝑝 = 𝑃𝑞 = 𝑃) → (𝑝(join‘𝐾)𝑞) = (𝑃(join‘𝐾)𝑃))
2423breq2d 5079 . . . . . . . . . . . 12 ((𝑝 = 𝑃𝑞 = 𝑃) → (𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞) ↔ 𝑟(le‘𝐾)(𝑃(join‘𝐾)𝑃)))
2524pm5.32i 578 . . . . . . . . . . 11 (((𝑝 = 𝑃𝑞 = 𝑃) ∧ 𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞)) ↔ ((𝑝 = 𝑃𝑞 = 𝑃) ∧ 𝑟(le‘𝐾)(𝑃(join‘𝐾)𝑃)))
2622, 25bitri 278 . . . . . . . . . 10 (((𝑝 ∈ {𝑃} ∧ 𝑞 ∈ {𝑃}) ∧ 𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞)) ↔ ((𝑝 = 𝑃𝑞 = 𝑃) ∧ 𝑟(le‘𝐾)(𝑃(join‘𝐾)𝑃)))
27 velsn 4571 . . . . . . . . . 10 (𝑟 ∈ {𝑃} ↔ 𝑟 = 𝑃)
2818, 26, 273imtr4g 299 . . . . . . . . 9 (((𝐾 ∈ AtLat ∧ 𝑃𝐴) ∧ 𝑟𝐴) → (((𝑝 ∈ {𝑃} ∧ 𝑞 ∈ {𝑃}) ∧ 𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞)) → 𝑟 ∈ {𝑃}))
2928exp4b 434 . . . . . . . 8 ((𝐾 ∈ AtLat ∧ 𝑃𝐴) → (𝑟𝐴 → ((𝑝 ∈ {𝑃} ∧ 𝑞 ∈ {𝑃}) → (𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞) → 𝑟 ∈ {𝑃}))))
3029com23 86 . . . . . . 7 ((𝐾 ∈ AtLat ∧ 𝑃𝐴) → ((𝑝 ∈ {𝑃} ∧ 𝑞 ∈ {𝑃}) → (𝑟𝐴 → (𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞) → 𝑟 ∈ {𝑃}))))
3130ralrimdv 3110 . . . . . 6 ((𝐾 ∈ AtLat ∧ 𝑃𝐴) → ((𝑝 ∈ {𝑃} ∧ 𝑞 ∈ {𝑃}) → ∀𝑟𝐴 (𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞) → 𝑟 ∈ {𝑃})))
3231ralrimivv 3112 . . . . 5 ((𝐾 ∈ AtLat ∧ 𝑃𝐴) → ∀𝑝 ∈ {𝑃}∀𝑞 ∈ {𝑃}∀𝑟𝐴 (𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞) → 𝑟 ∈ {𝑃}))
332, 32jca 515 . . . 4 ((𝐾 ∈ AtLat ∧ 𝑃𝐴) → ({𝑃} ⊆ 𝐴 ∧ ∀𝑝 ∈ {𝑃}∀𝑞 ∈ {𝑃}∀𝑟𝐴 (𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞) → 𝑟 ∈ {𝑃})))
3433ex 416 . . 3 (𝐾 ∈ AtLat → (𝑃𝐴 → ({𝑃} ⊆ 𝐴 ∧ ∀𝑝 ∈ {𝑃}∀𝑞 ∈ {𝑃}∀𝑟𝐴 (𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞) → 𝑟 ∈ {𝑃}))))
35 snpsub.s . . . 4 𝑆 = (PSubSp‘𝐾)
3612, 7, 5, 35ispsubsp 37522 . . 3 (𝐾 ∈ AtLat → ({𝑃} ∈ 𝑆 ↔ ({𝑃} ⊆ 𝐴 ∧ ∀𝑝 ∈ {𝑃}∀𝑞 ∈ {𝑃}∀𝑟𝐴 (𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞) → 𝑟 ∈ {𝑃}))))
3734, 36sylibrd 262 . 2 (𝐾 ∈ AtLat → (𝑃𝐴 → {𝑃} ∈ 𝑆))
3837imp 410 1 ((𝐾 ∈ AtLat ∧ 𝑃𝐴) → {𝑃} ∈ 𝑆)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399   = wceq 1543  wcel 2111  wral 3062  wss 3880  {csn 4555   class class class wbr 5067  cfv 6397  (class class class)co 7231  Basecbs 16784  lecple 16833  joincjn 17842  Latclat 17961  Atomscatm 37040  AtLatcal 37041  PSubSpcpsubsp 37273
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 5193  ax-sep 5206  ax-nul 5213  ax-pow 5272  ax-pr 5336  ax-un 7541
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-rab 3071  df-v 3422  df-sbc 3709  df-csb 3826  df-dif 3883  df-un 3885  df-in 3887  df-ss 3897  df-nul 4252  df-if 4454  df-pw 4529  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4834  df-iun 4920  df-br 5068  df-opab 5130  df-mpt 5150  df-id 5469  df-xp 5571  df-rel 5572  df-cnv 5573  df-co 5574  df-dm 5575  df-rn 5576  df-res 5577  df-ima 5578  df-iota 6355  df-fun 6399  df-fn 6400  df-f 6401  df-f1 6402  df-fo 6403  df-f1o 6404  df-fv 6405  df-riota 7188  df-ov 7234  df-oprab 7235  df-proset 17826  df-poset 17844  df-plt 17860  df-lub 17876  df-glb 17877  df-join 17878  df-meet 17879  df-p0 17955  df-lat 17962  df-covers 37043  df-ats 37044  df-atl 37075  df-psubsp 37280
This theorem is referenced by:  pointpsubN  37528  pclfinN  37677  pclfinclN  37727
  Copyright terms: Public domain W3C validator