Theorem pmaple 36930

Description: The projective map of a Hilbert lattice preserves ordering. Part of Theorem 15.5 of [MaedaMaeda] p. 62. (Contributed by NM, 22-Oct-2011.)

Hypotheses

Ref	Expression
pmaple.b	⊢ 𝐵 = (Base‘𝐾)
pmaple.l	⊢ ≤ = (le‘𝐾)
pmaple.m	⊢ 𝑀 = (pmap‘𝐾)

Assertion

Ref	Expression
pmaple	⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ≤ 𝑌 ↔ (𝑀‘𝑋) ⊆ (𝑀‘𝑌)))

Proof of Theorem pmaple

Dummy variable 𝑝 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		hlpos 36535	. . . . 5 ⊢ (𝐾 ∈ HL → 𝐾 ∈ Poset)
2		pmaple.b	. . . . . . . . . 10 ⊢ 𝐵 = (Base‘𝐾)
3		eqid 2820	. . . . . . . . . 10 ⊢ (Atoms‘𝐾) = (Atoms‘𝐾)
4	2, 3	atbase 36458	. . . . . . . . 9 ⊢ (𝑝 ∈ (Atoms‘𝐾) → 𝑝 ∈ 𝐵)
5		pmaple.l	. . . . . . . . . . . . . . 15 ⊢ ≤ = (le‘𝐾)
6	2, 5	postr 17558	. . . . . . . . . . . . . 14 ⊢ ((𝐾 ∈ Poset ∧ (𝑝 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → ((𝑝 ≤ 𝑋 ∧ 𝑋 ≤ 𝑌) → 𝑝 ≤ 𝑌))
7	6	exp4b 433	. . . . . . . . . . . . 13 ⊢ (𝐾 ∈ Poset → ((𝑝 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑝 ≤ 𝑋 → (𝑋 ≤ 𝑌 → 𝑝 ≤ 𝑌))))
8	7	3expd 1348	. . . . . . . . . . . 12 ⊢ (𝐾 ∈ Poset → (𝑝 ∈ 𝐵 → (𝑋 ∈ 𝐵 → (𝑌 ∈ 𝐵 → (𝑝 ≤ 𝑋 → (𝑋 ≤ 𝑌 → 𝑝 ≤ 𝑌))))))
9	8	com23 86	. . . . . . . . . . 11 ⊢ (𝐾 ∈ Poset → (𝑋 ∈ 𝐵 → (𝑝 ∈ 𝐵 → (𝑌 ∈ 𝐵 → (𝑝 ≤ 𝑋 → (𝑋 ≤ 𝑌 → 𝑝 ≤ 𝑌))))))
10	9	com34 91	. . . . . . . . . 10 ⊢ (𝐾 ∈ Poset → (𝑋 ∈ 𝐵 → (𝑌 ∈ 𝐵 → (𝑝 ∈ 𝐵 → (𝑝 ≤ 𝑋 → (𝑋 ≤ 𝑌 → 𝑝 ≤ 𝑌))))))
11	10	3imp 1106	. . . . . . . . 9 ⊢ ((𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑝 ∈ 𝐵 → (𝑝 ≤ 𝑋 → (𝑋 ≤ 𝑌 → 𝑝 ≤ 𝑌))))
12	4, 11	syl5 34	. . . . . . . 8 ⊢ ((𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑝 ∈ (Atoms‘𝐾) → (𝑝 ≤ 𝑋 → (𝑋 ≤ 𝑌 → 𝑝 ≤ 𝑌))))
13	12	com34 91	. . . . . . 7 ⊢ ((𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑝 ∈ (Atoms‘𝐾) → (𝑋 ≤ 𝑌 → (𝑝 ≤ 𝑋 → 𝑝 ≤ 𝑌))))
14	13	com23 86	. . . . . 6 ⊢ ((𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ≤ 𝑌 → (𝑝 ∈ (Atoms‘𝐾) → (𝑝 ≤ 𝑋 → 𝑝 ≤ 𝑌))))
15	14	ralrimdv 3187	. . . . 5 ⊢ ((𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ≤ 𝑌 → ∀𝑝 ∈ (Atoms‘𝐾)(𝑝 ≤ 𝑋 → 𝑝 ≤ 𝑌)))
16	1, 15	syl3an1 1158	. . . 4 ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ≤ 𝑌 → ∀𝑝 ∈ (Atoms‘𝐾)(𝑝 ≤ 𝑋 → 𝑝 ≤ 𝑌)))
17		ss2rab 4040	. . . 4 ⊢ ({𝑝 ∈ (Atoms‘𝐾) ∣ 𝑝 ≤ 𝑋} ⊆ {𝑝 ∈ (Atoms‘𝐾) ∣ 𝑝 ≤ 𝑌} ↔ ∀𝑝 ∈ (Atoms‘𝐾)(𝑝 ≤ 𝑋 → 𝑝 ≤ 𝑌))
18	16, 17	syl6ibr 254	. . 3 ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ≤ 𝑌 → {𝑝 ∈ (Atoms‘𝐾) ∣ 𝑝 ≤ 𝑋} ⊆ {𝑝 ∈ (Atoms‘𝐾) ∣ 𝑝 ≤ 𝑌}))
19		hlclat 36527	. . . . . 6 ⊢ (𝐾 ∈ HL → 𝐾 ∈ CLat)
20		ssrab2 4049	. . . . . . . . 9 ⊢ {𝑝 ∈ (Atoms‘𝐾) ∣ 𝑝 ≤ 𝑌} ⊆ (Atoms‘𝐾)
21	2, 3	atssbase 36459	. . . . . . . . 9 ⊢ (Atoms‘𝐾) ⊆ 𝐵
22	20, 21	sstri 3969	. . . . . . . 8 ⊢ {𝑝 ∈ (Atoms‘𝐾) ∣ 𝑝 ≤ 𝑌} ⊆ 𝐵
23		eqid 2820	. . . . . . . . 9 ⊢ (lub‘𝐾) = (lub‘𝐾)
24	2, 5, 23	lubss 17726	. . . . . . . 8 ⊢ ((𝐾 ∈ CLat ∧ {𝑝 ∈ (Atoms‘𝐾) ∣ 𝑝 ≤ 𝑌} ⊆ 𝐵 ∧ {𝑝 ∈ (Atoms‘𝐾) ∣ 𝑝 ≤ 𝑋} ⊆ {𝑝 ∈ (Atoms‘𝐾) ∣ 𝑝 ≤ 𝑌}) → ((lub‘𝐾)‘{𝑝 ∈ (Atoms‘𝐾) ∣ 𝑝 ≤ 𝑋}) ≤ ((lub‘𝐾)‘{𝑝 ∈ (Atoms‘𝐾) ∣ 𝑝 ≤ 𝑌}))
25	22, 24	mp3an2 1444	. . . . . . 7 ⊢ ((𝐾 ∈ CLat ∧ {𝑝 ∈ (Atoms‘𝐾) ∣ 𝑝 ≤ 𝑋} ⊆ {𝑝 ∈ (Atoms‘𝐾) ∣ 𝑝 ≤ 𝑌}) → ((lub‘𝐾)‘{𝑝 ∈ (Atoms‘𝐾) ∣ 𝑝 ≤ 𝑋}) ≤ ((lub‘𝐾)‘{𝑝 ∈ (Atoms‘𝐾) ∣ 𝑝 ≤ 𝑌}))
26	25	ex 415	. . . . . 6 ⊢ (𝐾 ∈ CLat → ({𝑝 ∈ (Atoms‘𝐾) ∣ 𝑝 ≤ 𝑋} ⊆ {𝑝 ∈ (Atoms‘𝐾) ∣ 𝑝 ≤ 𝑌} → ((lub‘𝐾)‘{𝑝 ∈ (Atoms‘𝐾) ∣ 𝑝 ≤ 𝑋}) ≤ ((lub‘𝐾)‘{𝑝 ∈ (Atoms‘𝐾) ∣ 𝑝 ≤ 𝑌})))
27	19, 26	syl 17	. . . . 5 ⊢ (𝐾 ∈ HL → ({𝑝 ∈ (Atoms‘𝐾) ∣ 𝑝 ≤ 𝑋} ⊆ {𝑝 ∈ (Atoms‘𝐾) ∣ 𝑝 ≤ 𝑌} → ((lub‘𝐾)‘{𝑝 ∈ (Atoms‘𝐾) ∣ 𝑝 ≤ 𝑋}) ≤ ((lub‘𝐾)‘{𝑝 ∈ (Atoms‘𝐾) ∣ 𝑝 ≤ 𝑌})))
28	27	3ad2ant1 1128	. . . 4 ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ({𝑝 ∈ (Atoms‘𝐾) ∣ 𝑝 ≤ 𝑋} ⊆ {𝑝 ∈ (Atoms‘𝐾) ∣ 𝑝 ≤ 𝑌} → ((lub‘𝐾)‘{𝑝 ∈ (Atoms‘𝐾) ∣ 𝑝 ≤ 𝑋}) ≤ ((lub‘𝐾)‘{𝑝 ∈ (Atoms‘𝐾) ∣ 𝑝 ≤ 𝑌})))
29		hlomcmat 36534	. . . . . . 7 ⊢ (𝐾 ∈ HL → (𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat))
30	29	3ad2ant1 1128	. . . . . 6 ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat))
31		simp2 1132	. . . . . 6 ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝑋 ∈ 𝐵)
32	2, 5, 23, 3	atlatmstc 36488	. . . . . 6 ⊢ (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋 ∈ 𝐵) → ((lub‘𝐾)‘{𝑝 ∈ (Atoms‘𝐾) ∣ 𝑝 ≤ 𝑋}) = 𝑋)
33	30, 31, 32	syl2anc 586	. . . . 5 ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((lub‘𝐾)‘{𝑝 ∈ (Atoms‘𝐾) ∣ 𝑝 ≤ 𝑋}) = 𝑋)
34		simp3 1133	. . . . . 6 ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝑌 ∈ 𝐵)
35	2, 5, 23, 3	atlatmstc 36488	. . . . . 6 ⊢ (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑌 ∈ 𝐵) → ((lub‘𝐾)‘{𝑝 ∈ (Atoms‘𝐾) ∣ 𝑝 ≤ 𝑌}) = 𝑌)
36	30, 34, 35	syl2anc 586	. . . . 5 ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((lub‘𝐾)‘{𝑝 ∈ (Atoms‘𝐾) ∣ 𝑝 ≤ 𝑌}) = 𝑌)
37	33, 36	breq12d 5072	. . . 4 ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (((lub‘𝐾)‘{𝑝 ∈ (Atoms‘𝐾) ∣ 𝑝 ≤ 𝑋}) ≤ ((lub‘𝐾)‘{𝑝 ∈ (Atoms‘𝐾) ∣ 𝑝 ≤ 𝑌}) ↔ 𝑋 ≤ 𝑌))
38	28, 37	sylibd 241	. . 3 ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ({𝑝 ∈ (Atoms‘𝐾) ∣ 𝑝 ≤ 𝑋} ⊆ {𝑝 ∈ (Atoms‘𝐾) ∣ 𝑝 ≤ 𝑌} → 𝑋 ≤ 𝑌))
39	18, 38	impbid 214	. 2 ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ≤ 𝑌 ↔ {𝑝 ∈ (Atoms‘𝐾) ∣ 𝑝 ≤ 𝑋} ⊆ {𝑝 ∈ (Atoms‘𝐾) ∣ 𝑝 ≤ 𝑌}))
40		pmaple.m	. . . . 5 ⊢ 𝑀 = (pmap‘𝐾)
41	2, 5, 3, 40	pmapval 36926	. . . 4 ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵) → (𝑀‘𝑋) = {𝑝 ∈ (Atoms‘𝐾) ∣ 𝑝 ≤ 𝑋})
42	41	3adant3 1127	. . 3 ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑀‘𝑋) = {𝑝 ∈ (Atoms‘𝐾) ∣ 𝑝 ≤ 𝑋})
43	2, 5, 3, 40	pmapval 36926	. . . 4 ⊢ ((𝐾 ∈ HL ∧ 𝑌 ∈ 𝐵) → (𝑀‘𝑌) = {𝑝 ∈ (Atoms‘𝐾) ∣ 𝑝 ≤ 𝑌})
44	43	3adant2 1126	. . 3 ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑀‘𝑌) = {𝑝 ∈ (Atoms‘𝐾) ∣ 𝑝 ≤ 𝑌})
45	42, 44	sseq12d 3993	. 2 ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑀‘𝑋) ⊆ (𝑀‘𝑌) ↔ {𝑝 ∈ (Atoms‘𝐾) ∣ 𝑝 ≤ 𝑋} ⊆ {𝑝 ∈ (Atoms‘𝐾) ∣ 𝑝 ≤ 𝑌}))
46	39, 45	bitr4d 284	1 ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ≤ 𝑌 ↔ (𝑀‘𝑋) ⊆ (𝑀‘𝑌)))

Syntax hints:   → wi 4   ↔ wb 208   ∧ w3a 1082   = wceq 1536   ∈ wcel 2113  ∀wral 3137  {crab 3141   ⊆ wss 3929   class class class wbr 5059  ‘cfv 6348  Basecbs 16478  lecple 16567  Posetcpo 17545  lubclub 17547  CLatccla 17712  OMLcoml 36344  Atomscatm 36432  AtLatcal 36433  HLchlt 36519  pmapcpmap 36666

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2792  ax-rep 5183  ax-sep 5196  ax-nul 5203  ax-pow 5259  ax-pr 5323  ax-un 7454

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1084  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-mo 2621  df-eu 2653  df-clab 2799  df-cleq 2813  df-clel 2892  df-nfc 2962  df-ne 3016  df-ral 3142  df-rex 3143  df-reu 3144  df-rab 3146  df-v 3493  df-sbc 3769  df-csb 3877  df-dif 3932  df-un 3934  df-in 3936  df-ss 3945  df-nul 4285  df-if 4461  df-pw 4534  df-sn 4561  df-pr 4563  df-op 4567  df-uni 4832  df-iun 4914  df-br 5060  df-opab 5122  df-mpt 5140  df-id 5453  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-riota 7107  df-ov 7152  df-oprab 7153  df-proset 17533  df-poset 17551  df-plt 17563  df-lub 17579  df-glb 17580  df-join 17581  df-meet 17582  df-p0 17644  df-lat 17651  df-clat 17713  df-oposet 36345  df-ol 36347  df-oml 36348  df-covers 36435  df-ats 36436  df-atl 36467  df-cvlat 36491  df-hlat 36520  df-pmap 36673

This theorem is referenced by:  pmap11  36931  hlmod1i  37025  paddunN  37096  pmapojoinN  37137  pl42N  37152