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