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

Metamath Proof Explorer

Theorem pmapglb2xN

Description: The projective map of the GLB of a set of lattice elements. Index-set version of pmapglb2N , where we read S as S ( i ) . Extension of Theorem 15.5.2 of MaedaMaeda p. 62 that allows I = (/) . (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 pmapglb2xN ( ( 𝐾 ∈ 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 rexeq ⊢ ( 𝐼 = ∅ → ( ∃ 𝑖 ∈ 𝐼 𝑦 = 𝑆 ↔ ∃ 𝑖 ∈ ∅ 𝑦 = 𝑆 ) )
13 12 abbidv ⊢ ( 𝐼 = ∅ → { 𝑦 ∣ ∃ 𝑖 ∈ 𝐼 𝑦 = 𝑆 } = { 𝑦 ∣ ∃ 𝑖 ∈ ∅ 𝑦 = 𝑆 } )
14 rex0 ⊢ ¬ ∃ 𝑖 ∈ ∅ 𝑦 = 𝑆
15 14 abf ⊢ { 𝑦 ∣ ∃ 𝑖 ∈ ∅ 𝑦 = 𝑆 } = ∅
16 13 15 eqtrdi ⊢ ( 𝐼 = ∅ → { 𝑦 ∣ ∃ 𝑖 ∈ 𝐼 𝑦 = 𝑆 } = ∅ )
17 16 fveq2d ⊢ ( 𝐼 = ∅ → ( 𝐺 ‘ { 𝑦 ∣ ∃ 𝑖 ∈ 𝐼 𝑦 = 𝑆 } ) = ( 𝐺 ‘ ∅ ) )
18 17 fveq2d ⊢ ( 𝐼 = ∅ → ( 𝑀 ‘ ( 𝐺 ‘ { 𝑦 ∣ ∃ 𝑖 ∈ 𝐼 𝑦 = 𝑆 } ) ) = ( 𝑀 ‘ ( 𝐺 ‘ ∅ ) ) )
19 riin0 ⊢ ( 𝐼 = ∅ → ( 𝐴 ∩ ∩ 𝑖 ∈ 𝐼 ( 𝑀 ‘ 𝑆 ) ) = 𝐴 )
20 18 19 eqeq12d ⊢ ( 𝐼 = ∅ → ( ( 𝑀 ‘ ( 𝐺 ‘ { 𝑦 ∣ ∃ 𝑖 ∈ 𝐼 𝑦 = 𝑆 } ) ) = ( 𝐴 ∩ ∩ 𝑖 ∈ 𝐼 ( 𝑀 ‘ 𝑆 ) ) ↔ ( 𝑀 ‘ ( 𝐺 ‘ ∅ ) ) = 𝐴 ) )
21 11 20 syl5ibrcom ⊢ ( 𝐾 ∈ HL → ( 𝐼 = ∅ → ( 𝑀 ‘ ( 𝐺 ‘ { 𝑦 ∣ ∃ 𝑖 ∈ 𝐼 𝑦 = 𝑆 } ) ) = ( 𝐴 ∩ ∩ 𝑖 ∈ 𝐼 ( 𝑀 ‘ 𝑆 ) ) ) )
22 21 adantr ⊢ ( ( 𝐾 ∈ HL ∧ ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 ) → ( 𝐼 = ∅ → ( 𝑀 ‘ ( 𝐺 ‘ { 𝑦 ∣ ∃ 𝑖 ∈ 𝐼 𝑦 = 𝑆 } ) ) = ( 𝐴 ∩ ∩ 𝑖 ∈ 𝐼 ( 𝑀 ‘ 𝑆 ) ) ) )
23 1 2 4 pmapglbx ⊢ ( ( 𝐾 ∈ HL ∧ ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 ∧ 𝐼 ≠ ∅ ) → ( 𝑀 ‘ ( 𝐺 ‘ { 𝑦 ∣ ∃ 𝑖 ∈ 𝐼 𝑦 = 𝑆 } ) ) = ∩ 𝑖 ∈ 𝐼 ( 𝑀 ‘ 𝑆 ) )
24 nfv ⊢ Ⅎ 𝑖 𝐾 ∈ HL
25 nfra1 ⊢ Ⅎ 𝑖 ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵
26 24 25 nfan ⊢ Ⅎ 𝑖 ( 𝐾 ∈ HL ∧ ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 )
27 simpr ⊢ ( ( ( 𝐾 ∈ HL ∧ ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) → 𝑖 ∈ 𝐼 )
28 simpll ⊢ ( ( ( 𝐾 ∈ HL ∧ ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) → 𝐾 ∈ HL )
29 rspa ⊢ ( ( ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 ∧ 𝑖 ∈ 𝐼 ) → 𝑆 ∈ 𝐵 )
30 29 adantll ⊢ ( ( ( 𝐾 ∈ HL ∧ ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) → 𝑆 ∈ 𝐵 )
31 1 3 4 pmapssat ⊢ ( ( 𝐾 ∈ HL ∧ 𝑆 ∈ 𝐵 ) → ( 𝑀 ‘ 𝑆 ) ⊆ 𝐴 )
32 28 30 31 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) → ( 𝑀 ‘ 𝑆 ) ⊆ 𝐴 )
33 27 32 jca ⊢ ( ( ( 𝐾 ∈ HL ∧ ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) → ( 𝑖 ∈ 𝐼 ∧ ( 𝑀 ‘ 𝑆 ) ⊆ 𝐴 ) )
34 33 ex ⊢ ( ( 𝐾 ∈ HL ∧ ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 ) → ( 𝑖 ∈ 𝐼 → ( 𝑖 ∈ 𝐼 ∧ ( 𝑀 ‘ 𝑆 ) ⊆ 𝐴 ) ) )
35 26 34 eximd ⊢ ( ( 𝐾 ∈ HL ∧ ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 ) → ( ∃ 𝑖 𝑖 ∈ 𝐼 → ∃ 𝑖 ( 𝑖 ∈ 𝐼 ∧ ( 𝑀 ‘ 𝑆 ) ⊆ 𝐴 ) ) )
36 n0 ⊢ ( 𝐼 ≠ ∅ ↔ ∃ 𝑖 𝑖 ∈ 𝐼 )
37 df-rex ⊢ ( ∃ 𝑖 ∈ 𝐼 ( 𝑀 ‘ 𝑆 ) ⊆ 𝐴 ↔ ∃ 𝑖 ( 𝑖 ∈ 𝐼 ∧ ( 𝑀 ‘ 𝑆 ) ⊆ 𝐴 ) )
38 35 36 37 3imtr4g ⊢ ( ( 𝐾 ∈ HL ∧ ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 ) → ( 𝐼 ≠ ∅ → ∃ 𝑖 ∈ 𝐼 ( 𝑀 ‘ 𝑆 ) ⊆ 𝐴 ) )
39 38 3impia ⊢ ( ( 𝐾 ∈ HL ∧ ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 ∧ 𝐼 ≠ ∅ ) → ∃ 𝑖 ∈ 𝐼 ( 𝑀 ‘ 𝑆 ) ⊆ 𝐴 )
40 iinss ⊢ ( ∃ 𝑖 ∈ 𝐼 ( 𝑀 ‘ 𝑆 ) ⊆ 𝐴 → ∩ 𝑖 ∈ 𝐼 ( 𝑀 ‘ 𝑆 ) ⊆ 𝐴 )
41 39 40 syl ⊢ ( ( 𝐾 ∈ HL ∧ ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 ∧ 𝐼 ≠ ∅ ) → ∩ 𝑖 ∈ 𝐼 ( 𝑀 ‘ 𝑆 ) ⊆ 𝐴 )
42 sseqin2 ⊢ ( ∩ 𝑖 ∈ 𝐼 ( 𝑀 ‘ 𝑆 ) ⊆ 𝐴 ↔ ( 𝐴 ∩ ∩ 𝑖 ∈ 𝐼 ( 𝑀 ‘ 𝑆 ) ) = ∩ 𝑖 ∈ 𝐼 ( 𝑀 ‘ 𝑆 ) )
43 41 42 sylib ⊢ ( ( 𝐾 ∈ HL ∧ ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 ∧ 𝐼 ≠ ∅ ) → ( 𝐴 ∩ ∩ 𝑖 ∈ 𝐼 ( 𝑀 ‘ 𝑆 ) ) = ∩ 𝑖 ∈ 𝐼 ( 𝑀 ‘ 𝑆 ) )
44 23 43 eqtr4d ⊢ ( ( 𝐾 ∈ HL ∧ ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 ∧ 𝐼 ≠ ∅ ) → ( 𝑀 ‘ ( 𝐺 ‘ { 𝑦 ∣ ∃ 𝑖 ∈ 𝐼 𝑦 = 𝑆 } ) ) = ( 𝐴 ∩ ∩ 𝑖 ∈ 𝐼 ( 𝑀 ‘ 𝑆 ) ) )
45 44 3expia ⊢ ( ( 𝐾 ∈ HL ∧ ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 ) → ( 𝐼 ≠ ∅ → ( 𝑀 ‘ ( 𝐺 ‘ { 𝑦 ∣ ∃ 𝑖 ∈ 𝐼 𝑦 = 𝑆 } ) ) = ( 𝐴 ∩ ∩ 𝑖 ∈ 𝐼 ( 𝑀 ‘ 𝑆 ) ) ) )
46 22 45 pm2.61dne ⊢ ( ( 𝐾 ∈ HL ∧ ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 ) → ( 𝑀 ‘ ( 𝐺 ‘ { 𝑦 ∣ ∃ 𝑖 ∈ 𝐼 𝑦 = 𝑆 } ) ) = ( 𝐴 ∩ ∩ 𝑖 ∈ 𝐼 ( 𝑀 ‘ 𝑆 ) ) )