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 = ( Base ` K )
pmaple.l 
|- .<_ = ( le ` K )
pmaple.m 
|- M = ( pmap ` K )
Assertion pmaple 
|- ( ( K e. HL /\ X e. B /\ Y e. B ) -> ( X .<_ Y <-> ( M ` X ) C_ ( M ` Y ) ) )

Proof

Step Hyp Ref Expression
1 pmaple.b 
 |-  B = ( Base ` K )
2 pmaple.l 
 |-  .<_ = ( le ` K )
3 pmaple.m 
 |-  M = ( pmap ` K )
4 hlpos 
 |-  ( K e. HL -> K e. Poset )
5 eqid 
 |-  ( Atoms ` K ) = ( Atoms ` K )
6 1 5 atbase 
 |-  ( p e. ( Atoms ` K ) -> p e. B )
7 1 2 postr 
 |-  ( ( K e. Poset /\ ( p e. B /\ X e. B /\ Y e. B ) ) -> ( ( p .<_ X /\ X .<_ Y ) -> p .<_ Y ) )
8 7 exp4b 
 |-  ( K e. Poset -> ( ( p e. B /\ X e. B /\ Y e. B ) -> ( p .<_ X -> ( X .<_ Y -> p .<_ Y ) ) ) )
9 8 3expd 
 |-  ( K e. Poset -> ( p e. B -> ( X e. B -> ( Y e. B -> ( p .<_ X -> ( X .<_ Y -> p .<_ Y ) ) ) ) ) )
10 9 com23 
 |-  ( K e. Poset -> ( X e. B -> ( p e. B -> ( Y e. B -> ( p .<_ X -> ( X .<_ Y -> p .<_ Y ) ) ) ) ) )
11 10 com34 
 |-  ( K e. Poset -> ( X e. B -> ( Y e. B -> ( p e. B -> ( p .<_ X -> ( X .<_ Y -> p .<_ Y ) ) ) ) ) )
12 11 3imp 
 |-  ( ( K e. Poset /\ X e. B /\ Y e. B ) -> ( p e. B -> ( p .<_ X -> ( X .<_ Y -> p .<_ Y ) ) ) )
13 6 12 syl5 
 |-  ( ( K e. Poset /\ X e. B /\ Y e. B ) -> ( p e. ( Atoms ` K ) -> ( p .<_ X -> ( X .<_ Y -> p .<_ Y ) ) ) )
14 13 com34 
 |-  ( ( K e. Poset /\ X e. B /\ Y e. B ) -> ( p e. ( Atoms ` K ) -> ( X .<_ Y -> ( p .<_ X -> p .<_ Y ) ) ) )
15 14 com23 
 |-  ( ( K e. Poset /\ X e. B /\ Y e. B ) -> ( X .<_ Y -> ( p e. ( Atoms ` K ) -> ( p .<_ X -> p .<_ Y ) ) ) )
16 15 ralrimdv 
 |-  ( ( K e. Poset /\ X e. B /\ Y e. B ) -> ( X .<_ Y -> A. p e. ( Atoms ` K ) ( p .<_ X -> p .<_ Y ) ) )
17 4 16 syl3an1 
 |-  ( ( K e. HL /\ X e. B /\ Y e. B ) -> ( X .<_ Y -> A. p e. ( Atoms ` K ) ( p .<_ X -> p .<_ Y ) ) )
18 ss2rab 
 |-  ( { p e. ( Atoms ` K ) | p .<_ X } C_ { p e. ( Atoms ` K ) | p .<_ Y } <-> A. p e. ( Atoms ` K ) ( p .<_ X -> p .<_ Y ) )
19 17 18 syl6ibr 
 |-  ( ( K e. HL /\ X e. B /\ Y e. B ) -> ( X .<_ Y -> { p e. ( Atoms ` K ) | p .<_ X } C_ { p e. ( Atoms ` K ) | p .<_ Y } ) )
20 hlclat 
 |-  ( K e. HL -> K e. CLat )
21 ssrab2 
 |-  { p e. ( Atoms ` K ) | p .<_ Y } C_ ( Atoms ` K )
22 1 5 atssbase 
 |-  ( Atoms ` K ) C_ B
23 21 22 sstri 
 |-  { p e. ( Atoms ` K ) | p .<_ Y } C_ B
24 eqid 
 |-  ( lub ` K ) = ( lub ` K )
25 1 2 24 lubss 
 |-  ( ( K e. CLat /\ { p e. ( Atoms ` K ) | p .<_ Y } C_ B /\ { p e. ( Atoms ` K ) | p .<_ X } C_ { p e. ( Atoms ` K ) | p .<_ Y } ) -> ( ( lub ` K ) ` { p e. ( Atoms ` K ) | p .<_ X } ) .<_ ( ( lub ` K ) ` { p e. ( Atoms ` K ) | p .<_ Y } ) )
26 23 25 mp3an2 
 |-  ( ( K e. CLat /\ { p e. ( Atoms ` K ) | p .<_ X } C_ { p e. ( Atoms ` K ) | p .<_ Y } ) -> ( ( lub ` K ) ` { p e. ( Atoms ` K ) | p .<_ X } ) .<_ ( ( lub ` K ) ` { p e. ( Atoms ` K ) | p .<_ Y } ) )
27 26 ex 
 |-  ( K e. CLat -> ( { p e. ( Atoms ` K ) | p .<_ X } C_ { p e. ( Atoms ` K ) | p .<_ Y } -> ( ( lub ` K ) ` { p e. ( Atoms ` K ) | p .<_ X } ) .<_ ( ( lub ` K ) ` { p e. ( Atoms ` K ) | p .<_ Y } ) ) )
28 20 27 syl 
 |-  ( K e. HL -> ( { p e. ( Atoms ` K ) | p .<_ X } C_ { p e. ( Atoms ` K ) | p .<_ Y } -> ( ( lub ` K ) ` { p e. ( Atoms ` K ) | p .<_ X } ) .<_ ( ( lub ` K ) ` { p e. ( Atoms ` K ) | p .<_ Y } ) ) )
29 28 3ad2ant1 
 |-  ( ( K e. HL /\ X e. B /\ Y e. B ) -> ( { p e. ( Atoms ` K ) | p .<_ X } C_ { p e. ( Atoms ` K ) | p .<_ Y } -> ( ( lub ` K ) ` { p e. ( Atoms ` K ) | p .<_ X } ) .<_ ( ( lub ` K ) ` { p e. ( Atoms ` K ) | p .<_ Y } ) ) )
30 hlomcmat 
 |-  ( K e. HL -> ( K e. OML /\ K e. CLat /\ K e. AtLat ) )
31 30 3ad2ant1 
 |-  ( ( K e. HL /\ X e. B /\ Y e. B ) -> ( K e. OML /\ K e. CLat /\ K e. AtLat ) )
32 simp2 
 |-  ( ( K e. HL /\ X e. B /\ Y e. B ) -> X e. B )
33 1 2 24 5 atlatmstc 
 |-  ( ( ( K e. OML /\ K e. CLat /\ K e. AtLat ) /\ X e. B ) -> ( ( lub ` K ) ` { p e. ( Atoms ` K ) | p .<_ X } ) = X )
34 31 32 33 syl2anc 
 |-  ( ( K e. HL /\ X e. B /\ Y e. B ) -> ( ( lub ` K ) ` { p e. ( Atoms ` K ) | p .<_ X } ) = X )
35 simp3 
 |-  ( ( K e. HL /\ X e. B /\ Y e. B ) -> Y e. B )
36 1 2 24 5 atlatmstc 
 |-  ( ( ( K e. OML /\ K e. CLat /\ K e. AtLat ) /\ Y e. B ) -> ( ( lub ` K ) ` { p e. ( Atoms ` K ) | p .<_ Y } ) = Y )
37 31 35 36 syl2anc 
 |-  ( ( K e. HL /\ X e. B /\ Y e. B ) -> ( ( lub ` K ) ` { p e. ( Atoms ` K ) | p .<_ Y } ) = Y )
38 34 37 breq12d 
 |-  ( ( K e. HL /\ X e. B /\ Y e. B ) -> ( ( ( lub ` K ) ` { p e. ( Atoms ` K ) | p .<_ X } ) .<_ ( ( lub ` K ) ` { p e. ( Atoms ` K ) | p .<_ Y } ) <-> X .<_ Y ) )
39 29 38 sylibd 
 |-  ( ( K e. HL /\ X e. B /\ Y e. B ) -> ( { p e. ( Atoms ` K ) | p .<_ X } C_ { p e. ( Atoms ` K ) | p .<_ Y } -> X .<_ Y ) )
40 19 39 impbid 
 |-  ( ( K e. HL /\ X e. B /\ Y e. B ) -> ( X .<_ Y <-> { p e. ( Atoms ` K ) | p .<_ X } C_ { p e. ( Atoms ` K ) | p .<_ Y } ) )
41 1 2 5 3 pmapval 
 |-  ( ( K e. HL /\ X e. B ) -> ( M ` X ) = { p e. ( Atoms ` K ) | p .<_ X } )
42 41 3adant3 
 |-  ( ( K e. HL /\ X e. B /\ Y e. B ) -> ( M ` X ) = { p e. ( Atoms ` K ) | p .<_ X } )
43 1 2 5 3 pmapval 
 |-  ( ( K e. HL /\ Y e. B ) -> ( M ` Y ) = { p e. ( Atoms ` K ) | p .<_ Y } )
44 43 3adant2 
 |-  ( ( K e. HL /\ X e. B /\ Y e. B ) -> ( M ` Y ) = { p e. ( Atoms ` K ) | p .<_ Y } )
45 42 44 sseq12d 
 |-  ( ( K e. HL /\ X e. B /\ Y e. B ) -> ( ( M ` X ) C_ ( M ` Y ) <-> { p e. ( Atoms ` K ) | p .<_ X } C_ { p e. ( Atoms ` K ) | p .<_ Y } ) )
46 40 45 bitr4d 
 |-  ( ( K e. HL /\ X e. B /\ Y e. B ) -> ( X .<_ Y <-> ( M ` X ) C_ ( M ` Y ) ) )