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 ⊢ 𝐵 = ( Base ‘ 𝐾 )
pmaple.l ⊢ ≤ = ( le ‘ 𝐾 )
pmaple.m ⊢ 𝑀 = ( pmap ‘ 𝐾 )
Assertion pmaple ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ≤ 𝑌 ↔ ( 𝑀 ‘ 𝑋 ) ⊆ ( 𝑀 ‘ 𝑌 ) ) )

Proof

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