This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem pmapglb2N

Description: The projective map of the GLB of a set of lattice elements S . Variant of Theorem 15.5.2 of MaedaMaeda p. 62. Allows S = (/) . (Contributed by NM, 21-Jan-2012) (New usage is discouraged.)

Ref Expression
Hypotheses pmapglb2.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
pmapglb2.g ⊢ 𝐺 = ( glb ‘ 𝐾 )
pmapglb2.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
pmapglb2.m ⊢ 𝑀 = ( pmap ‘ 𝐾 )
Assertion pmapglb2N ( ( 𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐵 ) → ( 𝑀 ‘ ( 𝐺 ‘ 𝑆 ) ) = ( 𝐴 ∩ ∩ 𝑥 ∈ 𝑆 ( 𝑀 ‘ 𝑥 ) ) )

Proof

Step Hyp Ref Expression
1 pmapglb2.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 pmapglb2.g ⊢ 𝐺 = ( glb ‘ 𝐾 )
3 pmapglb2.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4 pmapglb2.m ⊢ 𝑀 = ( pmap ‘ 𝐾 )
5 hlop ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OP )
6 eqid ⊢ ( 1. ‘ 𝐾 ) = ( 1. ‘ 𝐾 )
7 2 6 glb0N ⊢ ( 𝐾 ∈ OP → ( 𝐺 ‘ ∅ ) = ( 1. ‘ 𝐾 ) )
8 7 fveq2d ⊢ ( 𝐾 ∈ OP → ( 𝑀 ‘ ( 𝐺 ‘ ∅ ) ) = ( 𝑀 ‘ ( 1. ‘ 𝐾 ) ) )
9 6 3 4 pmap1N ⊢ ( 𝐾 ∈ OP → ( 𝑀 ‘ ( 1. ‘ 𝐾 ) ) = 𝐴 )
10 8 9 eqtrd ⊢ ( 𝐾 ∈ OP → ( 𝑀 ‘ ( 𝐺 ‘ ∅ ) ) = 𝐴 )
11 5 10 syl ⊢ ( 𝐾 ∈ HL → ( 𝑀 ‘ ( 𝐺 ‘ ∅ ) ) = 𝐴 )
12 2fveq3 ⊢ ( 𝑆 = ∅ → ( 𝑀 ‘ ( 𝐺 ‘ 𝑆 ) ) = ( 𝑀 ‘ ( 𝐺 ‘ ∅ ) ) )
13 riin0 ⊢ ( 𝑆 = ∅ → ( 𝐴 ∩ ∩ 𝑥 ∈ 𝑆 ( 𝑀 ‘ 𝑥 ) ) = 𝐴 )
14 12 13 eqeq12d ⊢ ( 𝑆 = ∅ → ( ( 𝑀 ‘ ( 𝐺 ‘ 𝑆 ) ) = ( 𝐴 ∩ ∩ 𝑥 ∈ 𝑆 ( 𝑀 ‘ 𝑥 ) ) ↔ ( 𝑀 ‘ ( 𝐺 ‘ ∅ ) ) = 𝐴 ) )
15 11 14 syl5ibrcom ⊢ ( 𝐾 ∈ HL → ( 𝑆 = ∅ → ( 𝑀 ‘ ( 𝐺 ‘ 𝑆 ) ) = ( 𝐴 ∩ ∩ 𝑥 ∈ 𝑆 ( 𝑀 ‘ 𝑥 ) ) ) )
16 15 adantr ⊢ ( ( 𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐵 ) → ( 𝑆 = ∅ → ( 𝑀 ‘ ( 𝐺 ‘ 𝑆 ) ) = ( 𝐴 ∩ ∩ 𝑥 ∈ 𝑆 ( 𝑀 ‘ 𝑥 ) ) ) )
17 1 2 4 pmapglb ⊢ ( ( 𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) → ( 𝑀 ‘ ( 𝐺 ‘ 𝑆 ) ) = ∩ 𝑥 ∈ 𝑆 ( 𝑀 ‘ 𝑥 ) )
18 simpr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐵 ) ∧ 𝑥 ∈ 𝑆 ) → 𝑥 ∈ 𝑆 )
19 simpll ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐵 ) ∧ 𝑥 ∈ 𝑆 ) → 𝐾 ∈ HL )
20 ssel2 ⊢ ( ( 𝑆 ⊆ 𝐵 ∧ 𝑥 ∈ 𝑆 ) → 𝑥 ∈ 𝐵 )
21 20 adantll ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐵 ) ∧ 𝑥 ∈ 𝑆 ) → 𝑥 ∈ 𝐵 )
22 1 3 4 pmapssat ⊢ ( ( 𝐾 ∈ HL ∧ 𝑥 ∈ 𝐵 ) → ( 𝑀 ‘ 𝑥 ) ⊆ 𝐴 )
23 19 21 22 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐵 ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝑀 ‘ 𝑥 ) ⊆ 𝐴 )
24 18 23 jca ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐵 ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝑥 ∈ 𝑆 ∧ ( 𝑀 ‘ 𝑥 ) ⊆ 𝐴 ) )
25 24 ex ⊢ ( ( 𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐵 ) → ( 𝑥 ∈ 𝑆 → ( 𝑥 ∈ 𝑆 ∧ ( 𝑀 ‘ 𝑥 ) ⊆ 𝐴 ) ) )
26 25 eximdv ⊢ ( ( 𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐵 ) → ( ∃ 𝑥 𝑥 ∈ 𝑆 → ∃ 𝑥 ( 𝑥 ∈ 𝑆 ∧ ( 𝑀 ‘ 𝑥 ) ⊆ 𝐴 ) ) )
27 n0 ⊢ ( 𝑆 ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ 𝑆 )
28 df-rex ⊢ ( ∃ 𝑥 ∈ 𝑆 ( 𝑀 ‘ 𝑥 ) ⊆ 𝐴 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑆 ∧ ( 𝑀 ‘ 𝑥 ) ⊆ 𝐴 ) )
29 26 27 28 3imtr4g ⊢ ( ( 𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐵 ) → ( 𝑆 ≠ ∅ → ∃ 𝑥 ∈ 𝑆 ( 𝑀 ‘ 𝑥 ) ⊆ 𝐴 ) )
30 29 3impia ⊢ ( ( 𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) → ∃ 𝑥 ∈ 𝑆 ( 𝑀 ‘ 𝑥 ) ⊆ 𝐴 )
31 iinss ⊢ ( ∃ 𝑥 ∈ 𝑆 ( 𝑀 ‘ 𝑥 ) ⊆ 𝐴 → ∩ 𝑥 ∈ 𝑆 ( 𝑀 ‘ 𝑥 ) ⊆ 𝐴 )
32 30 31 syl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) → ∩ 𝑥 ∈ 𝑆 ( 𝑀 ‘ 𝑥 ) ⊆ 𝐴 )
33 sseqin2 ⊢ ( ∩ 𝑥 ∈ 𝑆 ( 𝑀 ‘ 𝑥 ) ⊆ 𝐴 ↔ ( 𝐴 ∩ ∩ 𝑥 ∈ 𝑆 ( 𝑀 ‘ 𝑥 ) ) = ∩ 𝑥 ∈ 𝑆 ( 𝑀 ‘ 𝑥 ) )
34 32 33 sylib ⊢ ( ( 𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) → ( 𝐴 ∩ ∩ 𝑥 ∈ 𝑆 ( 𝑀 ‘ 𝑥 ) ) = ∩ 𝑥 ∈ 𝑆 ( 𝑀 ‘ 𝑥 ) )
35 17 34 eqtr4d ⊢ ( ( 𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) → ( 𝑀 ‘ ( 𝐺 ‘ 𝑆 ) ) = ( 𝐴 ∩ ∩ 𝑥 ∈ 𝑆 ( 𝑀 ‘ 𝑥 ) ) )
36 35 3expia ⊢ ( ( 𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐵 ) → ( 𝑆 ≠ ∅ → ( 𝑀 ‘ ( 𝐺 ‘ 𝑆 ) ) = ( 𝐴 ∩ ∩ 𝑥 ∈ 𝑆 ( 𝑀 ‘ 𝑥 ) ) ) )
37 16 36 pm2.61dne ⊢ ( ( 𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐵 ) → ( 𝑀 ‘ ( 𝐺 ‘ 𝑆 ) ) = ( 𝐴 ∩ ∩ 𝑥 ∈ 𝑆 ( 𝑀 ‘ 𝑥 ) ) )