Metamath Proof Explorer

Theorem pmaple

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)

Ref Expression
Hypotheses pmaple.b ⊢B=BaseK
pmaple.l ⊢≤˙=≤K
pmaple.m ⊢M=pmap⁡K
Assertion pmaple ⊢K∈HL∧X∈B∧Y∈B→X≤˙Y↔M⁡X⊆M⁡Y

Proof

Step Hyp Ref Expression
1 pmaple.b ⊢B=BaseK
2 pmaple.l ⊢≤˙=≤K
3 pmaple.m ⊢M=pmap⁡K
4 hlpos ⊢K∈HL→K∈Poset
5 eqid ⊢Atoms⁡K=Atoms⁡K
6 1 5 atbase ⊢p∈Atoms⁡K→p∈B
7 1 2 postr ⊢K∈Poset∧p∈B∧X∈B∧Y∈B→p≤˙X∧X≤˙Y→p≤˙Y
8 7 exp4b ⊢K∈Poset→p∈B∧X∈B∧Y∈B→p≤˙X→X≤˙Y→p≤˙Y
9 8 3expd ⊢K∈Poset→p∈B→X∈B→Y∈B→p≤˙X→X≤˙Y→p≤˙Y
10 9 com23 ⊢K∈Poset→X∈B→p∈B→Y∈B→p≤˙X→X≤˙Y→p≤˙Y
11 10 com34 ⊢K∈Poset→X∈B→Y∈B→p∈B→p≤˙X→X≤˙Y→p≤˙Y
12 11 3imp ⊢K∈Poset∧X∈B∧Y∈B→p∈B→p≤˙X→X≤˙Y→p≤˙Y
13 6 12 syl5 ⊢K∈Poset∧X∈B∧Y∈B→p∈Atoms⁡K→p≤˙X→X≤˙Y→p≤˙Y
14 13 com34 ⊢K∈Poset∧X∈B∧Y∈B→p∈Atoms⁡K→X≤˙Y→p≤˙X→p≤˙Y
15 14 com23 ⊢K∈Poset∧X∈B∧Y∈B→X≤˙Y→p∈Atoms⁡K→p≤˙X→p≤˙Y
16 15 ralrimdv ⊢K∈Poset∧X∈B∧Y∈B→X≤˙Y→∀p∈Atoms⁡Kp≤˙X→p≤˙Y
17 4 16 syl3an1 ⊢K∈HL∧X∈B∧Y∈B→X≤˙Y→∀p∈Atoms⁡Kp≤˙X→p≤˙Y
18 ss2rab ⊢p∈Atoms⁡K|p≤˙X⊆p∈Atoms⁡K|p≤˙Y↔∀p∈Atoms⁡Kp≤˙X→p≤˙Y
19 17 18 syl6ibr ⊢K∈HL∧X∈B∧Y∈B→X≤˙Y→p∈Atoms⁡K|p≤˙X⊆p∈Atoms⁡K|p≤˙Y
20 hlclat ⊢K∈HL→K∈CLat
21 ssrab2 ⊢p∈Atoms⁡K|p≤˙Y⊆Atoms⁡K
22 1 5 atssbase ⊢Atoms⁡K⊆B
23 21 22 sstri ⊢p∈Atoms⁡K|p≤˙Y⊆B
24 eqid ⊢lub⁡K=lub⁡K
25 1 2 24 lubss ⊢K∈CLat∧p∈Atoms⁡K|p≤˙Y⊆B∧p∈Atoms⁡K|p≤˙X⊆p∈Atoms⁡K|p≤˙Y→lub⁡K⁡p∈Atoms⁡K|p≤˙X≤˙lub⁡K⁡p∈Atoms⁡K|p≤˙Y
26 23 25 mp3an2 ⊢K∈CLat∧p∈Atoms⁡K|p≤˙X⊆p∈Atoms⁡K|p≤˙Y→lub⁡K⁡p∈Atoms⁡K|p≤˙X≤˙lub⁡K⁡p∈Atoms⁡K|p≤˙Y
27 26 ex ⊢K∈CLat→p∈Atoms⁡K|p≤˙X⊆p∈Atoms⁡K|p≤˙Y→lub⁡K⁡p∈Atoms⁡K|p≤˙X≤˙lub⁡K⁡p∈Atoms⁡K|p≤˙Y
28 20 27 syl ⊢K∈HL→p∈Atoms⁡K|p≤˙X⊆p∈Atoms⁡K|p≤˙Y→lub⁡K⁡p∈Atoms⁡K|p≤˙X≤˙lub⁡K⁡p∈Atoms⁡K|p≤˙Y
29 28 3ad2ant1 ⊢K∈HL∧X∈B∧Y∈B→p∈Atoms⁡K|p≤˙X⊆p∈Atoms⁡K|p≤˙Y→lub⁡K⁡p∈Atoms⁡K|p≤˙X≤˙lub⁡K⁡p∈Atoms⁡K|p≤˙Y
30 hlomcmat ⊢K∈HL→K∈OML∧K∈CLat∧K∈AtLat
31 30 3ad2ant1 ⊢K∈HL∧X∈B∧Y∈B→K∈OML∧K∈CLat∧K∈AtLat
32 simp2 ⊢K∈HL∧X∈B∧Y∈B→X∈B
33 1 2 24 5 atlatmstc ⊢K∈OML∧K∈CLat∧K∈AtLat∧X∈B→lub⁡K⁡p∈Atoms⁡K|p≤˙X=X
34 31 32 33 syl2anc ⊢K∈HL∧X∈B∧Y∈B→lub⁡K⁡p∈Atoms⁡K|p≤˙X=X
35 simp3 ⊢K∈HL∧X∈B∧Y∈B→Y∈B
36 1 2 24 5 atlatmstc ⊢K∈OML∧K∈CLat∧K∈AtLat∧Y∈B→lub⁡K⁡p∈Atoms⁡K|p≤˙Y=Y
37 31 35 36 syl2anc ⊢K∈HL∧X∈B∧Y∈B→lub⁡K⁡p∈Atoms⁡K|p≤˙Y=Y
38 34 37 breq12d ⊢K∈HL∧X∈B∧Y∈B→lub⁡K⁡p∈Atoms⁡K|p≤˙X≤˙lub⁡K⁡p∈Atoms⁡K|p≤˙Y↔X≤˙Y
39 29 38 sylibd ⊢K∈HL∧X∈B∧Y∈B→p∈Atoms⁡K|p≤˙X⊆p∈Atoms⁡K|p≤˙Y→X≤˙Y
40 19 39 impbid ⊢K∈HL∧X∈B∧Y∈B→X≤˙Y↔p∈Atoms⁡K|p≤˙X⊆p∈Atoms⁡K|p≤˙Y
41 1 2 5 3 pmapval ⊢K∈HL∧X∈B→M⁡X=p∈Atoms⁡K|p≤˙X
42 41 3adant3 ⊢K∈HL∧X∈B∧Y∈B→M⁡X=p∈Atoms⁡K|p≤˙X
43 1 2 5 3 pmapval ⊢K∈HL∧Y∈B→M⁡Y=p∈Atoms⁡K|p≤˙Y
44 43 3adant2 ⊢K∈HL∧X∈B∧Y∈B→M⁡Y=p∈Atoms⁡K|p≤˙Y
45 42 44 sseq12d ⊢K∈HL∧X∈B∧Y∈B→M⁡X⊆M⁡Y↔p∈Atoms⁡K|p≤˙X⊆p∈Atoms⁡K|p≤˙Y
46 40 45 bitr4d ⊢K∈HL∧X∈B∧Y∈B→X≤˙Y↔M⁡X⊆M⁡Y