Theorem pmaple 29229

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	|- B = ( Base ` K )
pmaple.l	|- .<_ = ( le ` K )
pmaple.m	|- M = ( pmap ` K )

Assertion

Ref	Expression
pmaple	|- ( ( K e. HL /\ X e. B /\ Y e. B ) -> ( X .<_ Y <-> ( M ` X ) C_ ( M ` Y ) ) )

Proof of Theorem pmaple

Dummy variable p is distinct from all other variables.

Step	Hyp	Ref	Expression
1		hlpos 28834	. . . . 5 |- ( K e. HL -> K e. Poset )
2		pmaple.b	. . . . . . . . . 10 |- B = ( Base ` K )
3		eqid 2284	. . . . . . . . . 10 |- ( Atoms ` K ) = ( Atoms ` K )
4	2, 3	atbase 28758	. . . . . . . . 9 |- ( p e. ( Atoms ` K ) -> p e. B )
5		pmaple.l	. . . . . . . . . . . . . . 15 |- .<_ = ( le ` K )
6	2, 5	postr 14083	. . . . . . . . . . . . . 14 |- ( ( K e. Poset /\ ( p e. B /\ X e. B /\ Y e. B ) ) -> ( ( p .<_ X /\ X .<_ Y ) -> p .<_ Y ) )
7	6	exp4b 590	. . . . . . . . . . . . 13 |- ( K e. Poset -> ( ( p e. B /\ X e. B /\ Y e. B ) -> ( p .<_ X -> ( X .<_ Y -> p .<_ Y ) ) ) )
8	7	3expd 1168	. . . . . . . . . . . 12 |- ( K e. Poset -> ( p e. B -> ( X e. B -> ( Y e. B -> ( p .<_ X -> ( X .<_ Y -> p .<_ Y ) ) ) ) ) )
9	8	com23 72	. . . . . . . . . . 11 |- ( K e. Poset -> ( X e. B -> ( p e. B -> ( Y e. B -> ( p .<_ X -> ( X .<_ Y -> p .<_ Y ) ) ) ) ) )
10	9	com34 77	. . . . . . . . . 10 |- ( K e. Poset -> ( X e. B -> ( Y e. B -> ( p e. B -> ( p .<_ X -> ( X .<_ Y -> p .<_ Y ) ) ) ) ) )
11	10	3imp 1145	. . . . . . . . 9 |- ( ( K e. Poset /\ X e. B /\ Y e. B ) -> ( p e. B -> ( p .<_ X -> ( X .<_ Y -> p .<_ Y ) ) ) )
12	4, 11	syl5 28	. . . . . . . 8 |- ( ( K e. Poset /\ X e. B /\ Y e. B ) -> ( p e. ( Atoms ` K ) -> ( p .<_ X -> ( X .<_ Y -> p .<_ Y ) ) ) )
13	12	com34 77	. . . . . . 7 |- ( ( K e. Poset /\ X e. B /\ Y e. B ) -> ( p e. ( Atoms ` K ) -> ( X .<_ Y -> ( p .<_ X -> p .<_ Y ) ) ) )
14	13	com23 72	. . . . . 6 |- ( ( K e. Poset /\ X e. B /\ Y e. B ) -> ( X .<_ Y -> ( p e. ( Atoms ` K ) -> ( p .<_ X -> p .<_ Y ) ) ) )
15	14	ralrimdv 2633	. . . . 5 |- ( ( K e. Poset /\ X e. B /\ Y e. B ) -> ( X .<_ Y -> A. p e. ( Atoms ` K ) ( p .<_ X -> p .<_ Y ) ) )
16	1, 15	syl3an1 1215	. . . 4 |- ( ( K e. HL /\ X e. B /\ Y e. B ) -> ( X .<_ Y -> A. p e. ( Atoms ` K ) ( p .<_ X -> p .<_ Y ) ) )
17		ss2rab 3250	. . . 4 |- ( { p e. ( Atoms ` K ) | p .<_ X } C_ { p e. ( Atoms ` K ) | p .<_ Y } <-> A. p e. ( Atoms ` K ) ( p .<_ X -> p .<_ Y ) )
18	16, 17	syl6ibr 218	. . 3 |- ( ( K e. HL /\ X e. B /\ Y e. B ) -> ( X .<_ Y -> { p e. ( Atoms ` K ) | p .<_ X } C_ { p e. ( Atoms ` K ) | p .<_ Y } ) )
19		hlclat 28827	. . . . . 6 |- ( K e. HL -> K e. CLat )
20		ssrab2 3259	. . . . . . . . 9 |- { p e. ( Atoms ` K ) | p .<_ Y } C_ ( Atoms ` K )
21	2, 3	atssbase 28759	. . . . . . . . 9 |- ( Atoms ` K ) C_ B
22	20, 21	sstri 3189	. . . . . . . 8 |- { p e. ( Atoms ` K ) | p .<_ Y } C_ B
23		eqid 2284	. . . . . . . . 9 |- ( lub ` K ) = ( lub ` K )
24	2, 5, 23	lubss 14221	. . . . . . . 8 |- ( ( 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 } ) )
25	22, 24	mp3an2 1265	. . . . . . 7 |- ( ( 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 } ) )
26	25	ex 423	. . . . . 6 |- ( 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	19, 26	syl 15	. . . . 5 |- ( 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 } ) ) )
28	27	3ad2ant1 976	. . . 4 |- ( ( 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 } ) ) )
29		hlomcmat 28833	. . . . . . 7 |- ( K e. HL -> ( K e. OML /\ K e. CLat /\ K e. AtLat ) )
30	29	3ad2ant1 976	. . . . . 6 |- ( ( K e. HL /\ X e. B /\ Y e. B ) -> ( K e. OML /\ K e. CLat /\ K e. AtLat ) )
31		simp2 956	. . . . . 6 |- ( ( K e. HL /\ X e. B /\ Y e. B ) -> X e. B )
32	2, 5, 23, 3	atlatmstc 28788	. . . . . 6 |- ( ( ( K e. OML /\ K e. CLat /\ K e. AtLat ) /\ X e. B ) -> ( ( lub ` K ) ` { p e. ( Atoms ` K ) | p .<_ X } ) = X )
33	30, 31, 32	syl2anc 642	. . . . 5 |- ( ( K e. HL /\ X e. B /\ Y e. B ) -> ( ( lub ` K ) ` { p e. ( Atoms ` K ) | p .<_ X } ) = X )
34		simp3 957	. . . . . 6 |- ( ( K e. HL /\ X e. B /\ Y e. B ) -> Y e. B )
35	2, 5, 23, 3	atlatmstc 28788	. . . . . 6 |- ( ( ( K e. OML /\ K e. CLat /\ K e. AtLat ) /\ Y e. B ) -> ( ( lub ` K ) ` { p e. ( Atoms ` K ) | p .<_ Y } ) = Y )
36	30, 34, 35	syl2anc 642	. . . . 5 |- ( ( K e. HL /\ X e. B /\ Y e. B ) -> ( ( lub ` K ) ` { p e. ( Atoms ` K ) | p .<_ Y } ) = Y )
37	33, 36	breq12d 4037	. . . 4 |- ( ( 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 ) )
38	28, 37	sylibd 205	. . 3 |- ( ( K e. HL /\ X e. B /\ Y e. B ) -> ( { p e. ( Atoms ` K ) | p .<_ X } C_ { p e. ( Atoms ` K ) | p .<_ Y } -> X .<_ Y ) )
39	18, 38	impbid 183	. 2 |- ( ( K e. HL /\ X e. B /\ Y e. B ) -> ( X .<_ Y <-> { p e. ( Atoms ` K ) | p .<_ X } C_ { p e. ( Atoms ` K ) | p .<_ Y } ) )
40		pmaple.m	. . . . 5 |- M = ( pmap ` K )
41	2, 5, 3, 40	pmapval 29225	. . . 4 |- ( ( K e. HL /\ X e. B ) -> ( M ` X ) = { p e. ( Atoms ` K ) | p .<_ X } )
42	41	3adant3 975	. . 3 |- ( ( K e. HL /\ X e. B /\ Y e. B ) -> ( M ` X ) = { p e. ( Atoms ` K ) | p .<_ X } )
43	2, 5, 3, 40	pmapval 29225	. . . 4 |- ( ( K e. HL /\ Y e. B ) -> ( M ` Y ) = { p e. ( Atoms ` K ) | p .<_ Y } )
44	43	3adant2 974	. . 3 |- ( ( K e. HL /\ X e. B /\ Y e. B ) -> ( M ` Y ) = { p e. ( Atoms ` K ) | p .<_ Y } )
45	42, 44	sseq12d 3208	. 2 |- ( ( 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	39, 45	bitr4d 247	1 |- ( ( K e. HL /\ X e. B /\ Y e. B ) -> ( X .<_ Y <-> ( M ` X ) C_ ( M ` Y ) ) )

Syntax hints:   -> wi 4   <-> wb 176   /\ w3a 934   = wceq 1623   e. wcel 1685   A.wral 2544   {crab 2548   C_ wss 3153   class class class wbr 4024   ` cfv 5221   Basecbs 13144   lecple 13211   Posetcpo 14070   lubclub 14072   CLatccla 14209   OMLcoml 28644   Atomscatm 28732   AtLatcal 28733   HLchlt 28819   pmapcpmap 28965

This theorem is referenced by:  pmap11  29230  hlmod1i  29324  paddunN  29395  pmapojoinN  29436  pl42N  29451

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1636  ax-8 1644  ax-13 1687  ax-14 1689  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2265  ax-rep 4132  ax-sep 4142  ax-nul 4150  ax-pow 4187  ax-pr 4213  ax-un 4511

This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1631  df-eu 2148  df-mo 2149  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-ne 2449  df-nel 2450  df-ral 2549  df-rex 2550  df-reu 2551  df-rab 2553  df-v 2791  df-sbc 2993  df-csb 3083  df-dif 3156  df-un 3158  df-in 3160  df-ss 3167  df-nul 3457  df-if 3567  df-pw 3628  df-sn 3647  df-pr 3648  df-op 3650  df-uni 3829  df-iun 3908  df-br 4025  df-opab 4079  df-mpt 4080  df-id 4308  df-xp 4694  df-rel 4695  df-cnv 4696  df-co 4697  df-dm 4698  df-rn 4699  df-res 4700  df-ima 4701  df-fun 5223  df-fn 5224  df-f 5225  df-f1 5226  df-fo 5227  df-f1o 5228  df-fv 5229  df-ov 5823  df-oprab 5824  df-mpt2 5825  df-1st 6084  df-2nd 6085  df-iota 6253  df-undef 6292  df-riota 6300  df-poset 14076  df-plt 14088  df-lub 14104  df-glb 14105  df-join 14106  df-meet 14107  df-p0 14141  df-lat 14148  df-clat 14210  df-oposet 28645  df-ol 28647  df-oml 28648  df-covers 28735  df-ats 28736  df-atl 28767  df-cvlat 28791  df-hlat 28820  df-pmap 28972