Mathbox for Norm Megill < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  pmaple Structured version   Unicode version

Theorem pmaple 30459
 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
pmaple.l
pmaple.m
Assertion
Ref Expression
pmaple

Proof of Theorem pmaple
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 hlpos 30064 . . . . 5
2 pmaple.b . . . . . . . . . 10
3 eqid 2435 . . . . . . . . . 10
42, 3atbase 29988 . . . . . . . . 9
5 pmaple.l . . . . . . . . . . . . . . 15
62, 5postr 14400 . . . . . . . . . . . . . 14
76exp4b 591 . . . . . . . . . . . . 13
873expd 1170 . . . . . . . . . . . 12
98com23 74 . . . . . . . . . . 11
109com34 79 . . . . . . . . . 10
11103imp 1147 . . . . . . . . 9
124, 11syl5 30 . . . . . . . 8
1312com34 79 . . . . . . 7
1413com23 74 . . . . . 6
1514ralrimdv 2787 . . . . 5
161, 15syl3an1 1217 . . . 4
17 ss2rab 3411 . . . 4
1816, 17syl6ibr 219 . . 3
19 hlclat 30057 . . . . . 6
20 ssrab2 3420 . . . . . . . . 9
212, 3atssbase 29989 . . . . . . . . 9
2220, 21sstri 3349 . . . . . . . 8
23 eqid 2435 . . . . . . . . 9
242, 5, 23lubss 14538 . . . . . . . 8
2522, 24mp3an2 1267 . . . . . . 7
2625ex 424 . . . . . 6
2719, 26syl 16 . . . . 5
28273ad2ant1 978 . . . 4
29 hlomcmat 30063 . . . . . . 7
30293ad2ant1 978 . . . . . 6
31 simp2 958 . . . . . 6
322, 5, 23, 3atlatmstc 30018 . . . . . 6
3330, 31, 32syl2anc 643 . . . . 5
34 simp3 959 . . . . . 6
352, 5, 23, 3atlatmstc 30018 . . . . . 6
3630, 34, 35syl2anc 643 . . . . 5
3733, 36breq12d 4217 . . . 4
3828, 37sylibd 206 . . 3
3918, 38impbid 184 . 2
40 pmaple.m . . . . 5
412, 5, 3, 40pmapval 30455 . . . 4