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 ⊢ ≤ ˙ = ≤ K
pmaple.m ⊢ M = pmap ⁡ K
Assertion pmaple ⊢ K ∈ HL ∧ X ∈ B ∧ Y ∈ B → X ≤ ˙ Y ↔ M ⁡ X ⊆ M ⁡ Y

Proof

Step Hyp Ref Expression
1 pmaple.b ⊢ B = Base K
2 pmaple.l ⊢ ≤ ˙ = ≤ K
3 pmaple.m ⊢ M = pmap ⁡ K
4 hlpos ⊢ K ∈ HL → K ∈ Poset
5 eqid ⊢ Atoms ⁡ K = Atoms ⁡ K
6 1 5 atbase ⊢ p ∈ Atoms ⁡ K → p ∈ B
7 1 2 postr ⊢ K ∈ Poset ∧ p ∈ B ∧ X ∈ B ∧ Y ∈ B → p ≤ ˙ X ∧ X ≤ ˙ Y → p ≤ ˙ Y
8 7 exp4b ⊢ K ∈ Poset → p ∈ B ∧ X ∈ B ∧ Y ∈ B → p ≤ ˙ X → X ≤ ˙ Y → p ≤ ˙ Y
9 8 3expd ⊢ K ∈ Poset → p ∈ B → X ∈ B → Y ∈ B → p ≤ ˙ X → X ≤ ˙ Y → p ≤ ˙ Y
10 9 com23 ⊢ K ∈ Poset → X ∈ B → p ∈ B → Y ∈ B → p ≤ ˙ X → X ≤ ˙ Y → p ≤ ˙ Y
11 10 com34 ⊢ K ∈ Poset → X ∈ B → Y ∈ B → p ∈ B → p ≤ ˙ X → X ≤ ˙ Y → p ≤ ˙ Y
12 11 3imp ⊢ K ∈ Poset ∧ X ∈ B ∧ Y ∈ B → p ∈ B → p ≤ ˙ X → X ≤ ˙ Y → p ≤ ˙ Y
13 6 12 syl5 ⊢ K ∈ Poset ∧ X ∈ B ∧ Y ∈ B → p ∈ Atoms ⁡ K → p ≤ ˙ X → X ≤ ˙ Y → p ≤ ˙ Y
14 13 com34 ⊢ K ∈ Poset ∧ X ∈ B ∧ Y ∈ B → p ∈ Atoms ⁡ K → X ≤ ˙ Y → p ≤ ˙ X → p ≤ ˙ Y
15 14 com23 ⊢ K ∈ Poset ∧ X ∈ B ∧ Y ∈ B → X ≤ ˙ Y → p ∈ Atoms ⁡ K → p ≤ ˙ X → p ≤ ˙ Y
16 15 ralrimdv ⊢ K ∈ Poset ∧ X ∈ B ∧ Y ∈ B → X ≤ ˙ Y → ∀ p ∈ Atoms ⁡ K p ≤ ˙ X → p ≤ ˙ Y
17 4 16 syl3an1 ⊢ K ∈ HL ∧ X ∈ B ∧ Y ∈ B → X ≤ ˙ Y → ∀ p ∈ Atoms ⁡ K p ≤ ˙ X → p ≤ ˙ Y
18 ss2rab ⊢ p ∈ Atoms ⁡ K | p ≤ ˙ X ⊆ p ∈ Atoms ⁡ K | p ≤ ˙ Y ↔ ∀ p ∈ Atoms ⁡ K p ≤ ˙ X → p ≤ ˙ Y
19 17 18 imbitrrdi ⊢ K ∈ HL ∧ X ∈ B ∧ Y ∈ B → X ≤ ˙ Y → p ∈ Atoms ⁡ K | p ≤ ˙ X ⊆ p ∈ Atoms ⁡ K | p ≤ ˙ Y
20 hlclat ⊢ K ∈ HL → K ∈ CLat
21 ssrab2 ⊢ p ∈ Atoms ⁡ K | p ≤ ˙ Y ⊆ Atoms ⁡ K
22 1 5 atssbase ⊢ Atoms ⁡ K ⊆ B
23 21 22 sstri ⊢ p ∈ Atoms ⁡ K | p ≤ ˙ Y ⊆ B
24 eqid ⊢ lub ⁡ K = lub ⁡ K
25 1 2 24 lubss ⊢ K ∈ CLat ∧ p ∈ Atoms ⁡ K | p ≤ ˙ Y ⊆ B ∧ p ∈ Atoms ⁡ K | p ≤ ˙ X ⊆ p ∈ Atoms ⁡ K | p ≤ ˙ Y → lub ⁡ K ⁡ p ∈ Atoms ⁡ K | p ≤ ˙ X ≤ ˙ lub ⁡ K ⁡ p ∈ Atoms ⁡ K | p ≤ ˙ Y
26 23 25 mp3an2 ⊢ K ∈ CLat ∧ p ∈ Atoms ⁡ K | p ≤ ˙ X ⊆ p ∈ Atoms ⁡ K | p ≤ ˙ Y → lub ⁡ K ⁡ p ∈ Atoms ⁡ K | p ≤ ˙ X ≤ ˙ lub ⁡ K ⁡ p ∈ Atoms ⁡ K | p ≤ ˙ Y
27 26 ex ⊢ K ∈ CLat → p ∈ Atoms ⁡ K | p ≤ ˙ X ⊆ p ∈ Atoms ⁡ K | p ≤ ˙ Y → lub ⁡ K ⁡ p ∈ Atoms ⁡ K | p ≤ ˙ X ≤ ˙ lub ⁡ K ⁡ p ∈ Atoms ⁡ K | p ≤ ˙ Y
28 20 27 syl ⊢ K ∈ HL → p ∈ Atoms ⁡ K | p ≤ ˙ X ⊆ p ∈ Atoms ⁡ K | p ≤ ˙ Y → lub ⁡ K ⁡ p ∈ Atoms ⁡ K | p ≤ ˙ X ≤ ˙ lub ⁡ K ⁡ p ∈ Atoms ⁡ K | p ≤ ˙ Y
29 28 3ad2ant1 ⊢ K ∈ HL ∧ X ∈ B ∧ Y ∈ B → p ∈ Atoms ⁡ K | p ≤ ˙ X ⊆ p ∈ Atoms ⁡ K | p ≤ ˙ Y → lub ⁡ K ⁡ p ∈ Atoms ⁡ K | p ≤ ˙ X ≤ ˙ lub ⁡ K ⁡ p ∈ Atoms ⁡ K | p ≤ ˙ Y
30 hlomcmat ⊢ K ∈ HL → K ∈ OML ∧ K ∈ CLat ∧ K ∈ AtLat
31 30 3ad2ant1 ⊢ K ∈ HL ∧ X ∈ B ∧ Y ∈ B → K ∈ OML ∧ K ∈ CLat ∧ K ∈ AtLat
32 simp2 ⊢ K ∈ HL ∧ X ∈ B ∧ Y ∈ B → X ∈ B
33 1 2 24 5 atlatmstc ⊢ K ∈ OML ∧ K ∈ CLat ∧ K ∈ AtLat ∧ X ∈ B → lub ⁡ K ⁡ p ∈ Atoms ⁡ K | p ≤ ˙ X = X
34 31 32 33 syl2anc ⊢ K ∈ HL ∧ X ∈ B ∧ Y ∈ B → lub ⁡ K ⁡ p ∈ Atoms ⁡ K | p ≤ ˙ X = X
35 simp3 ⊢ K ∈ HL ∧ X ∈ B ∧ Y ∈ B → Y ∈ B
36 1 2 24 5 atlatmstc ⊢ K ∈ OML ∧ K ∈ CLat ∧ K ∈ AtLat ∧ Y ∈ B → lub ⁡ K ⁡ p ∈ Atoms ⁡ K | p ≤ ˙ Y = Y
37 31 35 36 syl2anc ⊢ K ∈ HL ∧ X ∈ B ∧ Y ∈ B → lub ⁡ K ⁡ p ∈ Atoms ⁡ K | p ≤ ˙ Y = Y
38 34 37 breq12d ⊢ K ∈ HL ∧ X ∈ B ∧ Y ∈ B → lub ⁡ K ⁡ p ∈ Atoms ⁡ K | p ≤ ˙ X ≤ ˙ lub ⁡ K ⁡ p ∈ Atoms ⁡ K | p ≤ ˙ Y ↔ X ≤ ˙ Y
39 29 38 sylibd ⊢ K ∈ HL ∧ X ∈ B ∧ Y ∈ B → p ∈ Atoms ⁡ K | p ≤ ˙ X ⊆ p ∈ Atoms ⁡ K | p ≤ ˙ Y → X ≤ ˙ Y
40 19 39 impbid ⊢ K ∈ HL ∧ X ∈ B ∧ Y ∈ B → X ≤ ˙ Y ↔ p ∈ Atoms ⁡ K | p ≤ ˙ X ⊆ p ∈ Atoms ⁡ K | p ≤ ˙ Y
41 1 2 5 3 pmapval ⊢ K ∈ HL ∧ X ∈ B → M ⁡ X = p ∈ Atoms ⁡ K | p ≤ ˙ X
42 41 3adant3 ⊢ K ∈ HL ∧ X ∈ B ∧ Y ∈ B → M ⁡ X = p ∈ Atoms ⁡ K | p ≤ ˙ X
43 1 2 5 3 pmapval ⊢ K ∈ HL ∧ Y ∈ B → M ⁡ Y = p ∈ Atoms ⁡ K | p ≤ ˙ Y
44 43 3adant2 ⊢ K ∈ HL ∧ X ∈ B ∧ Y ∈ B → M ⁡ Y = p ∈ Atoms ⁡ K | p ≤ ˙ Y
45 42 44 sseq12d ⊢ K ∈ HL ∧ X ∈ B ∧ Y ∈ B → M ⁡ X ⊆ M ⁡ Y ↔ p ∈ Atoms ⁡ K | p ≤ ˙ X ⊆ p ∈ Atoms ⁡ K | p ≤ ˙ Y
46 40 45 bitr4d ⊢ K ∈ HL ∧ X ∈ B ∧ Y ∈ B → X ≤ ˙ Y ↔ M ⁡ X ⊆ M ⁡ Y