Metamath Proof Explorer

Theorem pmapsub

Description: The projective map of a Hilbert lattice maps to projective subspaces. Part of Theorem 15.5 of MaedaMaeda p. 62. (Contributed by NM, 17-Oct-2011)

Ref Expression
Hypotheses pmapsub.b ⊢B=BaseK
pmapsub.s ⊢S=PSubSp⁡K
pmapsub.m ⊢M=pmap⁡K
Assertion pmapsub ⊢K∈Lat∧X∈B→M⁡X∈S

Proof

Step Hyp Ref Expression
1 pmapsub.b ⊢B=BaseK
2 pmapsub.s ⊢S=PSubSp⁡K
3 pmapsub.m ⊢M=pmap⁡K
4 eqid ⊢≤K=≤K
5 eqid ⊢Atoms⁡K=Atoms⁡K
6 1 4 5 3 pmapval ⊢K∈Lat∧X∈B→M⁡X=c∈Atoms⁡K|c≤KX
7 breq1 ⊢c=p→c≤KX↔p≤KX
8 7 elrab ⊢p∈c∈Atoms⁡K|c≤KX↔p∈Atoms⁡K∧p≤KX
9 1 5 atbase ⊢p∈Atoms⁡K→p∈B
10 9 anim1i ⊢p∈Atoms⁡K∧p≤KX→p∈B∧p≤KX
11 8 10 sylbi ⊢p∈c∈Atoms⁡K|c≤KX→p∈B∧p≤KX
12 breq1 ⊢c=q→c≤KX↔q≤KX
13 12 elrab ⊢q∈c∈Atoms⁡K|c≤KX↔q∈Atoms⁡K∧q≤KX
14 1 5 atbase ⊢q∈Atoms⁡K→q∈B
15 14 anim1i ⊢q∈Atoms⁡K∧q≤KX→q∈B∧q≤KX
16 13 15 sylbi ⊢q∈c∈Atoms⁡K|c≤KX→q∈B∧q≤KX
17 11 16 anim12i ⊢p∈c∈Atoms⁡K|c≤KX∧q∈c∈Atoms⁡K|c≤KX→p∈B∧p≤KX∧q∈B∧q≤KX
18 an4 ⊢p∈B∧p≤KX∧q∈B∧q≤KX↔p∈B∧q∈B∧p≤KX∧q≤KX
19 17 18 sylib ⊢p∈c∈Atoms⁡K|c≤KX∧q∈c∈Atoms⁡K|c≤KX→p∈B∧q∈B∧p≤KX∧q≤KX
20 19 anim2i ⊢K∈Lat∧X∈B∧p∈c∈Atoms⁡K|c≤KX∧q∈c∈Atoms⁡K|c≤KX→K∈Lat∧X∈B∧p∈B∧q∈B∧p≤KX∧q≤KX
21 1 5 atbase ⊢r∈Atoms⁡K→r∈B
22 eqid ⊢join⁡K=join⁡K
23 1 4 22 latjle12 ⊢K∈Lat∧p∈B∧q∈B∧X∈B→p≤KX∧q≤KX↔pjoin⁡Kq≤KX
24 23 biimpd ⊢K∈Lat∧p∈B∧q∈B∧X∈B→p≤KX∧q≤KX→pjoin⁡Kq≤KX
25 24 3exp2 ⊢K∈Lat→p∈B→q∈B→X∈B→p≤KX∧q≤KX→pjoin⁡Kq≤KX
26 25 impd ⊢K∈Lat→p∈B∧q∈B→X∈B→p≤KX∧q≤KX→pjoin⁡Kq≤KX
27 26 com23 ⊢K∈Lat→X∈B→p∈B∧q∈B→p≤KX∧q≤KX→pjoin⁡Kq≤KX
28 27 imp43 ⊢K∈Lat∧X∈B∧p∈B∧q∈B∧p≤KX∧q≤KX→pjoin⁡Kq≤KX
29 28 adantr ⊢K∈Lat∧X∈B∧p∈B∧q∈B∧p≤KX∧q≤KX∧r∈B→pjoin⁡Kq≤KX
30 1 22 latjcl ⊢K∈Lat∧p∈B∧q∈B→pjoin⁡Kq∈B
31 30 3expib ⊢K∈Lat→p∈B∧q∈B→pjoin⁡Kq∈B
32 1 4 lattr ⊢K∈Lat∧r∈B∧pjoin⁡Kq∈B∧X∈B→r≤Kpjoin⁡Kq∧pjoin⁡Kq≤KX→r≤KX
33 32 3exp2 ⊢K∈Lat→r∈B→pjoin⁡Kq∈B→X∈B→r≤Kpjoin⁡Kq∧pjoin⁡Kq≤KX→r≤KX
34 33 com24 ⊢K∈Lat→X∈B→pjoin⁡Kq∈B→r∈B→r≤Kpjoin⁡Kq∧pjoin⁡Kq≤KX→r≤KX
35 31 34 syl5d ⊢K∈Lat→X∈B→p∈B∧q∈B→r∈B→r≤Kpjoin⁡Kq∧pjoin⁡Kq≤KX→r≤KX
36 35 imp41 ⊢K∈Lat∧X∈B∧p∈B∧q∈B∧r∈B→r≤Kpjoin⁡Kq∧pjoin⁡Kq≤KX→r≤KX
37 36 adantlrr ⊢K∈Lat∧X∈B∧p∈B∧q∈B∧p≤KX∧q≤KX∧r∈B→r≤Kpjoin⁡Kq∧pjoin⁡Kq≤KX→r≤KX
38 29 37 mpan2d ⊢K∈Lat∧X∈B∧p∈B∧q∈B∧p≤KX∧q≤KX∧r∈B→r≤Kpjoin⁡Kq→r≤KX
39 20 21 38 syl2an ⊢K∈Lat∧X∈B∧p∈c∈Atoms⁡K|c≤KX∧q∈c∈Atoms⁡K|c≤KX∧r∈Atoms⁡K→r≤Kpjoin⁡Kq→r≤KX
40 simpr ⊢K∈Lat∧X∈B∧p∈c∈Atoms⁡K|c≤KX∧q∈c∈Atoms⁡K|c≤KX∧r∈Atoms⁡K→r∈Atoms⁡K
41 39 40 jctild ⊢K∈Lat∧X∈B∧p∈c∈Atoms⁡K|c≤KX∧q∈c∈Atoms⁡K|c≤KX∧r∈Atoms⁡K→r≤Kpjoin⁡Kq→r∈Atoms⁡K∧r≤KX
42 breq1 ⊢c=r→c≤KX↔r≤KX
43 42 elrab ⊢r∈c∈Atoms⁡K|c≤KX↔r∈Atoms⁡K∧r≤KX
44 41 43 syl6ibr ⊢K∈Lat∧X∈B∧p∈c∈Atoms⁡K|c≤KX∧q∈c∈Atoms⁡K|c≤KX∧r∈Atoms⁡K→r≤Kpjoin⁡Kq→r∈c∈Atoms⁡K|c≤KX
45 44 ralrimiva ⊢K∈Lat∧X∈B∧p∈c∈Atoms⁡K|c≤KX∧q∈c∈Atoms⁡K|c≤KX→∀r∈Atoms⁡Kr≤Kpjoin⁡Kq→r∈c∈Atoms⁡K|c≤KX
46 45 ralrimivva ⊢K∈Lat∧X∈B→∀p∈c∈Atoms⁡K|c≤KX∀q∈c∈Atoms⁡K|c≤KX∀r∈Atoms⁡Kr≤Kpjoin⁡Kq→r∈c∈Atoms⁡K|c≤KX
47 ssrab2 ⊢c∈Atoms⁡K|c≤KX⊆Atoms⁡K
48 46 47 jctil ⊢K∈Lat∧X∈B→c∈Atoms⁡K|c≤KX⊆Atoms⁡K∧∀p∈c∈Atoms⁡K|c≤KX∀q∈c∈Atoms⁡K|c≤KX∀r∈Atoms⁡Kr≤Kpjoin⁡Kq→r∈c∈Atoms⁡K|c≤KX
49 4 22 5 2 ispsubsp ⊢K∈Lat→c∈Atoms⁡K|c≤KX∈S↔c∈Atoms⁡K|c≤KX⊆Atoms⁡K∧∀p∈c∈Atoms⁡K|c≤KX∀q∈c∈Atoms⁡K|c≤KX∀r∈Atoms⁡Kr≤Kpjoin⁡Kq→r∈c∈Atoms⁡K|c≤KX
50 49 adantr ⊢K∈Lat∧X∈B→c∈Atoms⁡K|c≤KX∈S↔c∈Atoms⁡K|c≤KX⊆Atoms⁡K∧∀p∈c∈Atoms⁡K|c≤KX∀q∈c∈Atoms⁡K|c≤KX∀r∈Atoms⁡Kr≤Kpjoin⁡Kq→r∈c∈Atoms⁡K|c≤KX
51 48 50 mpbird ⊢K∈Lat∧X∈B→c∈Atoms⁡K|c≤KX∈S
52 6 51 eqeltrd ⊢K∈Lat∧X∈B→M⁡X∈S