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

Theorem pmapsub 39479
Description: The projective map of a Hilbert lattice maps to projective subspaces. Part of Theorem 15.5 of [MaedaMaeda] p. 62. (Contributed by NM, 17-Oct-2011.)
Hypotheses
Ref Expression
pmapsub.b 𝐵 = (Base‘𝐾)
pmapsub.s 𝑆 = (PSubSp‘𝐾)
pmapsub.m 𝑀 = (pmap‘𝐾)
Assertion
Ref Expression
pmapsub ((𝐾 ∈ Lat ∧ 𝑋𝐵) → (𝑀𝑋) ∈ 𝑆)

Proof of Theorem pmapsub
Dummy variables 𝑞 𝑝 𝑟 𝑐 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 pmapsub.b . . 3 𝐵 = (Base‘𝐾)
2 eqid 2726 . . 3 (le‘𝐾) = (le‘𝐾)
3 eqid 2726 . . 3 (Atoms‘𝐾) = (Atoms‘𝐾)
4 pmapsub.m . . 3 𝑀 = (pmap‘𝐾)
51, 2, 3, 4pmapval 39468 . 2 ((𝐾 ∈ Lat ∧ 𝑋𝐵) → (𝑀𝑋) = {𝑐 ∈ (Atoms‘𝐾) ∣ 𝑐(le‘𝐾)𝑋})
6 breq1 5148 . . . . . . . . . . . . . 14 (𝑐 = 𝑝 → (𝑐(le‘𝐾)𝑋𝑝(le‘𝐾)𝑋))
76elrab 3682 . . . . . . . . . . . . 13 (𝑝 ∈ {𝑐 ∈ (Atoms‘𝐾) ∣ 𝑐(le‘𝐾)𝑋} ↔ (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑝(le‘𝐾)𝑋))
81, 3atbase 38999 . . . . . . . . . . . . . 14 (𝑝 ∈ (Atoms‘𝐾) → 𝑝𝐵)
98anim1i 613 . . . . . . . . . . . . 13 ((𝑝 ∈ (Atoms‘𝐾) ∧ 𝑝(le‘𝐾)𝑋) → (𝑝𝐵𝑝(le‘𝐾)𝑋))
107, 9sylbi 216 . . . . . . . . . . . 12 (𝑝 ∈ {𝑐 ∈ (Atoms‘𝐾) ∣ 𝑐(le‘𝐾)𝑋} → (𝑝𝐵𝑝(le‘𝐾)𝑋))
11 breq1 5148 . . . . . . . . . . . . . 14 (𝑐 = 𝑞 → (𝑐(le‘𝐾)𝑋𝑞(le‘𝐾)𝑋))
1211elrab 3682 . . . . . . . . . . . . 13 (𝑞 ∈ {𝑐 ∈ (Atoms‘𝐾) ∣ 𝑐(le‘𝐾)𝑋} ↔ (𝑞 ∈ (Atoms‘𝐾) ∧ 𝑞(le‘𝐾)𝑋))
131, 3atbase 38999 . . . . . . . . . . . . . 14 (𝑞 ∈ (Atoms‘𝐾) → 𝑞𝐵)
1413anim1i 613 . . . . . . . . . . . . 13 ((𝑞 ∈ (Atoms‘𝐾) ∧ 𝑞(le‘𝐾)𝑋) → (𝑞𝐵𝑞(le‘𝐾)𝑋))
1512, 14sylbi 216 . . . . . . . . . . . 12 (𝑞 ∈ {𝑐 ∈ (Atoms‘𝐾) ∣ 𝑐(le‘𝐾)𝑋} → (𝑞𝐵𝑞(le‘𝐾)𝑋))
1610, 15anim12i 611 . . . . . . . . . . 11 ((𝑝 ∈ {𝑐 ∈ (Atoms‘𝐾) ∣ 𝑐(le‘𝐾)𝑋} ∧ 𝑞 ∈ {𝑐 ∈ (Atoms‘𝐾) ∣ 𝑐(le‘𝐾)𝑋}) → ((𝑝𝐵𝑝(le‘𝐾)𝑋) ∧ (𝑞𝐵𝑞(le‘𝐾)𝑋)))
17 an4 654 . . . . . . . . . . 11 (((𝑝𝐵𝑝(le‘𝐾)𝑋) ∧ (𝑞𝐵𝑞(le‘𝐾)𝑋)) ↔ ((𝑝𝐵𝑞𝐵) ∧ (𝑝(le‘𝐾)𝑋𝑞(le‘𝐾)𝑋)))
1816, 17sylib 217 . . . . . . . . . 10 ((𝑝 ∈ {𝑐 ∈ (Atoms‘𝐾) ∣ 𝑐(le‘𝐾)𝑋} ∧ 𝑞 ∈ {𝑐 ∈ (Atoms‘𝐾) ∣ 𝑐(le‘𝐾)𝑋}) → ((𝑝𝐵𝑞𝐵) ∧ (𝑝(le‘𝐾)𝑋𝑞(le‘𝐾)𝑋)))
1918anim2i 615 . . . . . . . . 9 (((𝐾 ∈ Lat ∧ 𝑋𝐵) ∧ (𝑝 ∈ {𝑐 ∈ (Atoms‘𝐾) ∣ 𝑐(le‘𝐾)𝑋} ∧ 𝑞 ∈ {𝑐 ∈ (Atoms‘𝐾) ∣ 𝑐(le‘𝐾)𝑋})) → ((𝐾 ∈ Lat ∧ 𝑋𝐵) ∧ ((𝑝𝐵𝑞𝐵) ∧ (𝑝(le‘𝐾)𝑋𝑞(le‘𝐾)𝑋))))
201, 3atbase 38999 . . . . . . . . 9 (𝑟 ∈ (Atoms‘𝐾) → 𝑟𝐵)
21 eqid 2726 . . . . . . . . . . . . . . . . 17 (join‘𝐾) = (join‘𝐾)
221, 2, 21latjle12 18469 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ Lat ∧ (𝑝𝐵𝑞𝐵𝑋𝐵)) → ((𝑝(le‘𝐾)𝑋𝑞(le‘𝐾)𝑋) ↔ (𝑝(join‘𝐾)𝑞)(le‘𝐾)𝑋))
2322biimpd 228 . . . . . . . . . . . . . . 15 ((𝐾 ∈ Lat ∧ (𝑝𝐵𝑞𝐵𝑋𝐵)) → ((𝑝(le‘𝐾)𝑋𝑞(le‘𝐾)𝑋) → (𝑝(join‘𝐾)𝑞)(le‘𝐾)𝑋))
24233exp2 1351 . . . . . . . . . . . . . 14 (𝐾 ∈ Lat → (𝑝𝐵 → (𝑞𝐵 → (𝑋𝐵 → ((𝑝(le‘𝐾)𝑋𝑞(le‘𝐾)𝑋) → (𝑝(join‘𝐾)𝑞)(le‘𝐾)𝑋)))))
2524impd 409 . . . . . . . . . . . . 13 (𝐾 ∈ Lat → ((𝑝𝐵𝑞𝐵) → (𝑋𝐵 → ((𝑝(le‘𝐾)𝑋𝑞(le‘𝐾)𝑋) → (𝑝(join‘𝐾)𝑞)(le‘𝐾)𝑋))))
2625com23 86 . . . . . . . . . . . 12 (𝐾 ∈ Lat → (𝑋𝐵 → ((𝑝𝐵𝑞𝐵) → ((𝑝(le‘𝐾)𝑋𝑞(le‘𝐾)𝑋) → (𝑝(join‘𝐾)𝑞)(le‘𝐾)𝑋))))
2726imp43 426 . . . . . . . . . . 11 (((𝐾 ∈ Lat ∧ 𝑋𝐵) ∧ ((𝑝𝐵𝑞𝐵) ∧ (𝑝(le‘𝐾)𝑋𝑞(le‘𝐾)𝑋))) → (𝑝(join‘𝐾)𝑞)(le‘𝐾)𝑋)
2827adantr 479 . . . . . . . . . 10 ((((𝐾 ∈ Lat ∧ 𝑋𝐵) ∧ ((𝑝𝐵𝑞𝐵) ∧ (𝑝(le‘𝐾)𝑋𝑞(le‘𝐾)𝑋))) ∧ 𝑟𝐵) → (𝑝(join‘𝐾)𝑞)(le‘𝐾)𝑋)
291, 21latjcl 18458 . . . . . . . . . . . . . 14 ((𝐾 ∈ Lat ∧ 𝑝𝐵𝑞𝐵) → (𝑝(join‘𝐾)𝑞) ∈ 𝐵)
30293expib 1119 . . . . . . . . . . . . 13 (𝐾 ∈ Lat → ((𝑝𝐵𝑞𝐵) → (𝑝(join‘𝐾)𝑞) ∈ 𝐵))
311, 2lattr 18463 . . . . . . . . . . . . . . 15 ((𝐾 ∈ Lat ∧ (𝑟𝐵 ∧ (𝑝(join‘𝐾)𝑞) ∈ 𝐵𝑋𝐵)) → ((𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞) ∧ (𝑝(join‘𝐾)𝑞)(le‘𝐾)𝑋) → 𝑟(le‘𝐾)𝑋))
32313exp2 1351 . . . . . . . . . . . . . 14 (𝐾 ∈ Lat → (𝑟𝐵 → ((𝑝(join‘𝐾)𝑞) ∈ 𝐵 → (𝑋𝐵 → ((𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞) ∧ (𝑝(join‘𝐾)𝑞)(le‘𝐾)𝑋) → 𝑟(le‘𝐾)𝑋)))))
3332com24 95 . . . . . . . . . . . . 13 (𝐾 ∈ Lat → (𝑋𝐵 → ((𝑝(join‘𝐾)𝑞) ∈ 𝐵 → (𝑟𝐵 → ((𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞) ∧ (𝑝(join‘𝐾)𝑞)(le‘𝐾)𝑋) → 𝑟(le‘𝐾)𝑋)))))
3430, 33syl5d 73 . . . . . . . . . . . 12 (𝐾 ∈ Lat → (𝑋𝐵 → ((𝑝𝐵𝑞𝐵) → (𝑟𝐵 → ((𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞) ∧ (𝑝(join‘𝐾)𝑞)(le‘𝐾)𝑋) → 𝑟(le‘𝐾)𝑋)))))
3534imp41 424 . . . . . . . . . . 11 ((((𝐾 ∈ Lat ∧ 𝑋𝐵) ∧ (𝑝𝐵𝑞𝐵)) ∧ 𝑟𝐵) → ((𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞) ∧ (𝑝(join‘𝐾)𝑞)(le‘𝐾)𝑋) → 𝑟(le‘𝐾)𝑋))
3635adantlrr 719 . . . . . . . . . 10 ((((𝐾 ∈ Lat ∧ 𝑋𝐵) ∧ ((𝑝𝐵𝑞𝐵) ∧ (𝑝(le‘𝐾)𝑋𝑞(le‘𝐾)𝑋))) ∧ 𝑟𝐵) → ((𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞) ∧ (𝑝(join‘𝐾)𝑞)(le‘𝐾)𝑋) → 𝑟(le‘𝐾)𝑋))
3728, 36mpan2d 692 . . . . . . . . 9 ((((𝐾 ∈ Lat ∧ 𝑋𝐵) ∧ ((𝑝𝐵𝑞𝐵) ∧ (𝑝(le‘𝐾)𝑋𝑞(le‘𝐾)𝑋))) ∧ 𝑟𝐵) → (𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞) → 𝑟(le‘𝐾)𝑋))
3819, 20, 37syl2an 594 . . . . . . . 8 ((((𝐾 ∈ Lat ∧ 𝑋𝐵) ∧ (𝑝 ∈ {𝑐 ∈ (Atoms‘𝐾) ∣ 𝑐(le‘𝐾)𝑋} ∧ 𝑞 ∈ {𝑐 ∈ (Atoms‘𝐾) ∣ 𝑐(le‘𝐾)𝑋})) ∧ 𝑟 ∈ (Atoms‘𝐾)) → (𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞) → 𝑟(le‘𝐾)𝑋))
39 simpr 483 . . . . . . . 8 ((((𝐾 ∈ Lat ∧ 𝑋𝐵) ∧ (𝑝 ∈ {𝑐 ∈ (Atoms‘𝐾) ∣ 𝑐(le‘𝐾)𝑋} ∧ 𝑞 ∈ {𝑐 ∈ (Atoms‘𝐾) ∣ 𝑐(le‘𝐾)𝑋})) ∧ 𝑟 ∈ (Atoms‘𝐾)) → 𝑟 ∈ (Atoms‘𝐾))
4038, 39jctild 524 . . . . . . 7 ((((𝐾 ∈ Lat ∧ 𝑋𝐵) ∧ (𝑝 ∈ {𝑐 ∈ (Atoms‘𝐾) ∣ 𝑐(le‘𝐾)𝑋} ∧ 𝑞 ∈ {𝑐 ∈ (Atoms‘𝐾) ∣ 𝑐(le‘𝐾)𝑋})) ∧ 𝑟 ∈ (Atoms‘𝐾)) → (𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞) → (𝑟 ∈ (Atoms‘𝐾) ∧ 𝑟(le‘𝐾)𝑋)))
41 breq1 5148 . . . . . . . 8 (𝑐 = 𝑟 → (𝑐(le‘𝐾)𝑋𝑟(le‘𝐾)𝑋))
4241elrab 3682 . . . . . . 7 (𝑟 ∈ {𝑐 ∈ (Atoms‘𝐾) ∣ 𝑐(le‘𝐾)𝑋} ↔ (𝑟 ∈ (Atoms‘𝐾) ∧ 𝑟(le‘𝐾)𝑋))
4340, 42imbitrrdi 251 . . . . . 6 ((((𝐾 ∈ Lat ∧ 𝑋𝐵) ∧ (𝑝 ∈ {𝑐 ∈ (Atoms‘𝐾) ∣ 𝑐(le‘𝐾)𝑋} ∧ 𝑞 ∈ {𝑐 ∈ (Atoms‘𝐾) ∣ 𝑐(le‘𝐾)𝑋})) ∧ 𝑟 ∈ (Atoms‘𝐾)) → (𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞) → 𝑟 ∈ {𝑐 ∈ (Atoms‘𝐾) ∣ 𝑐(le‘𝐾)𝑋}))
4443ralrimiva 3136 . . . . 5 (((𝐾 ∈ Lat ∧ 𝑋𝐵) ∧ (𝑝 ∈ {𝑐 ∈ (Atoms‘𝐾) ∣ 𝑐(le‘𝐾)𝑋} ∧ 𝑞 ∈ {𝑐 ∈ (Atoms‘𝐾) ∣ 𝑐(le‘𝐾)𝑋})) → ∀𝑟 ∈ (Atoms‘𝐾)(𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞) → 𝑟 ∈ {𝑐 ∈ (Atoms‘𝐾) ∣ 𝑐(le‘𝐾)𝑋}))
4544ralrimivva 3191 . . . 4 ((𝐾 ∈ Lat ∧ 𝑋𝐵) → ∀𝑝 ∈ {𝑐 ∈ (Atoms‘𝐾) ∣ 𝑐(le‘𝐾)𝑋}∀𝑞 ∈ {𝑐 ∈ (Atoms‘𝐾) ∣ 𝑐(le‘𝐾)𝑋}∀𝑟 ∈ (Atoms‘𝐾)(𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞) → 𝑟 ∈ {𝑐 ∈ (Atoms‘𝐾) ∣ 𝑐(le‘𝐾)𝑋}))
46 ssrab2 4075 . . . 4 {𝑐 ∈ (Atoms‘𝐾) ∣ 𝑐(le‘𝐾)𝑋} ⊆ (Atoms‘𝐾)
4745, 46jctil 518 . . 3 ((𝐾 ∈ Lat ∧ 𝑋𝐵) → ({𝑐 ∈ (Atoms‘𝐾) ∣ 𝑐(le‘𝐾)𝑋} ⊆ (Atoms‘𝐾) ∧ ∀𝑝 ∈ {𝑐 ∈ (Atoms‘𝐾) ∣ 𝑐(le‘𝐾)𝑋}∀𝑞 ∈ {𝑐 ∈ (Atoms‘𝐾) ∣ 𝑐(le‘𝐾)𝑋}∀𝑟 ∈ (Atoms‘𝐾)(𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞) → 𝑟 ∈ {𝑐 ∈ (Atoms‘𝐾) ∣ 𝑐(le‘𝐾)𝑋})))
48 pmapsub.s . . . . 5 𝑆 = (PSubSp‘𝐾)
492, 21, 3, 48ispsubsp 39456 . . . 4 (𝐾 ∈ Lat → ({𝑐 ∈ (Atoms‘𝐾) ∣ 𝑐(le‘𝐾)𝑋} ∈ 𝑆 ↔ ({𝑐 ∈ (Atoms‘𝐾) ∣ 𝑐(le‘𝐾)𝑋} ⊆ (Atoms‘𝐾) ∧ ∀𝑝 ∈ {𝑐 ∈ (Atoms‘𝐾) ∣ 𝑐(le‘𝐾)𝑋}∀𝑞 ∈ {𝑐 ∈ (Atoms‘𝐾) ∣ 𝑐(le‘𝐾)𝑋}∀𝑟 ∈ (Atoms‘𝐾)(𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞) → 𝑟 ∈ {𝑐 ∈ (Atoms‘𝐾) ∣ 𝑐(le‘𝐾)𝑋}))))
5049adantr 479 . . 3 ((𝐾 ∈ Lat ∧ 𝑋𝐵) → ({𝑐 ∈ (Atoms‘𝐾) ∣ 𝑐(le‘𝐾)𝑋} ∈ 𝑆 ↔ ({𝑐 ∈ (Atoms‘𝐾) ∣ 𝑐(le‘𝐾)𝑋} ⊆ (Atoms‘𝐾) ∧ ∀𝑝 ∈ {𝑐 ∈ (Atoms‘𝐾) ∣ 𝑐(le‘𝐾)𝑋}∀𝑞 ∈ {𝑐 ∈ (Atoms‘𝐾) ∣ 𝑐(le‘𝐾)𝑋}∀𝑟 ∈ (Atoms‘𝐾)(𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞) → 𝑟 ∈ {𝑐 ∈ (Atoms‘𝐾) ∣ 𝑐(le‘𝐾)𝑋}))))
5147, 50mpbird 256 . 2 ((𝐾 ∈ Lat ∧ 𝑋𝐵) → {𝑐 ∈ (Atoms‘𝐾) ∣ 𝑐(le‘𝐾)𝑋} ∈ 𝑆)
525, 51eqeltrd 2826 1 ((𝐾 ∈ Lat ∧ 𝑋𝐵) → (𝑀𝑋) ∈ 𝑆)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 394  w3a 1084   = wceq 1534  wcel 2099  wral 3051  {crab 3420  wss 3948   class class class wbr 5145  cfv 6545  (class class class)co 7415  Basecbs 17207  lecple 17267  joincjn 18330  Latclat 18450  Atomscatm 38973  PSubSpcpsubsp 39207  pmapcpmap 39208
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2697  ax-rep 5282  ax-sep 5296  ax-nul 5303  ax-pow 5361  ax-pr 5425  ax-un 7737
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2704  df-cleq 2718  df-clel 2803  df-nfc 2878  df-ne 2931  df-ral 3052  df-rex 3061  df-rmo 3365  df-reu 3366  df-rab 3421  df-v 3466  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4325  df-if 4526  df-pw 4601  df-sn 4626  df-pr 4628  df-op 4632  df-uni 4908  df-iun 4997  df-br 5146  df-opab 5208  df-mpt 5229  df-id 5572  df-xp 5680  df-rel 5681  df-cnv 5682  df-co 5683  df-dm 5684  df-rn 5685  df-res 5686  df-ima 5687  df-iota 6497  df-fun 6547  df-fn 6548  df-f 6549  df-f1 6550  df-fo 6551  df-f1o 6552  df-fv 6553  df-riota 7371  df-ov 7418  df-oprab 7419  df-poset 18332  df-lub 18365  df-glb 18366  df-join 18367  df-meet 18368  df-lat 18451  df-ats 38977  df-psubsp 39214  df-pmap 39215
This theorem is referenced by:  hlmod1i  39567  polsubN  39618  pl42lem4N  39693
  Copyright terms: Public domain W3C validator