Metamath Proof Explorer

Theorem pmapglbx

Description: The projective map of the GLB of a set of lattice elements. Index-set version of pmapglb , where we read S as S ( i ) . Theorem 15.5.2 of MaedaMaeda p. 62. (Contributed by NM, 5-Dec-2011)

Ref Expression
Hypotheses pmapglb.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
pmapglb.g ⊢ 𝐺 = ( glb ‘ 𝐾 )
pmapglb.m ⊢ 𝑀 = ( pmap ‘ 𝐾 )
Assertion pmapglbx ( ( 𝐾 ∈ HL ∧ ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 ∧ 𝐼 ≠ ∅ ) → ( 𝑀 ‘ ( 𝐺 ‘ { 𝑦 ∣ ∃ 𝑖 ∈ 𝐼 𝑦 = 𝑆 } ) ) = ∩ 𝑖 ∈ 𝐼 ( 𝑀 ‘ 𝑆 ) )

Proof

Step Hyp Ref Expression
1 pmapglb.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 pmapglb.g ⊢ 𝐺 = ( glb ‘ 𝐾 )
3 pmapglb.m ⊢ 𝑀 = ( pmap ‘ 𝐾 )
4 hlclat ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ CLat )
5 4 ad2antrr ⊢ ( ( ( 𝐾 ∈ HL ∧ ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ) → 𝐾 ∈ CLat )
6 eqid ⊢ ( Atoms ‘ 𝐾 ) = ( Atoms ‘ 𝐾 )
7 1 6 atbase ⊢ ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) → 𝑝 ∈ 𝐵 )
8 7 adantl ⊢ ( ( ( 𝐾 ∈ HL ∧ ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ) → 𝑝 ∈ 𝐵 )
9 r19.29 ⊢ ( ( ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 ∧ ∃ 𝑖 ∈ 𝐼 𝑦 = 𝑆 ) → ∃ 𝑖 ∈ 𝐼 ( 𝑆 ∈ 𝐵 ∧ 𝑦 = 𝑆 ) )
10 eleq1a ⊢ ( 𝑆 ∈ 𝐵 → ( 𝑦 = 𝑆 → 𝑦 ∈ 𝐵 ) )
11 10 imp ⊢ ( ( 𝑆 ∈ 𝐵 ∧ 𝑦 = 𝑆 ) → 𝑦 ∈ 𝐵 )
12 11 rexlimivw ⊢ ( ∃ 𝑖 ∈ 𝐼 ( 𝑆 ∈ 𝐵 ∧ 𝑦 = 𝑆 ) → 𝑦 ∈ 𝐵 )
13 9 12 syl ⊢ ( ( ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 ∧ ∃ 𝑖 ∈ 𝐼 𝑦 = 𝑆 ) → 𝑦 ∈ 𝐵 )
14 13 ex ⊢ ( ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 → ( ∃ 𝑖 ∈ 𝐼 𝑦 = 𝑆 → 𝑦 ∈ 𝐵 ) )
15 14 ad2antlr ⊢ ( ( ( 𝐾 ∈ HL ∧ ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ) → ( ∃ 𝑖 ∈ 𝐼 𝑦 = 𝑆 → 𝑦 ∈ 𝐵 ) )
16 15 abssdv ⊢ ( ( ( 𝐾 ∈ HL ∧ ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ) → { 𝑦 ∣ ∃ 𝑖 ∈ 𝐼 𝑦 = 𝑆 } ⊆ 𝐵 )
17 eqid ⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
18 1 17 2 clatleglb ⊢ ( ( 𝐾 ∈ CLat ∧ 𝑝 ∈ 𝐵 ∧ { 𝑦 ∣ ∃ 𝑖 ∈ 𝐼 𝑦 = 𝑆 } ⊆ 𝐵 ) → ( 𝑝 ( le ‘ 𝐾 ) ( 𝐺 ‘ { 𝑦 ∣ ∃ 𝑖 ∈ 𝐼 𝑦 = 𝑆 } ) ↔ ∀ 𝑧 ∈ { 𝑦 ∣ ∃ 𝑖 ∈ 𝐼 𝑦 = 𝑆 } 𝑝 ( le ‘ 𝐾 ) 𝑧 ) )
19 5 8 16 18 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ) → ( 𝑝 ( le ‘ 𝐾 ) ( 𝐺 ‘ { 𝑦 ∣ ∃ 𝑖 ∈ 𝐼 𝑦 = 𝑆 } ) ↔ ∀ 𝑧 ∈ { 𝑦 ∣ ∃ 𝑖 ∈ 𝐼 𝑦 = 𝑆 } 𝑝 ( le ‘ 𝐾 ) 𝑧 ) )
20 vex ⊢ 𝑧 ∈ V
21 eqeq1 ⊢ ( 𝑦 = 𝑧 → ( 𝑦 = 𝑆 ↔ 𝑧 = 𝑆 ) )
22 21 rexbidv ⊢ ( 𝑦 = 𝑧 → ( ∃ 𝑖 ∈ 𝐼 𝑦 = 𝑆 ↔ ∃ 𝑖 ∈ 𝐼 𝑧 = 𝑆 ) )
23 20 22 elab ⊢ ( 𝑧 ∈ { 𝑦 ∣ ∃ 𝑖 ∈ 𝐼 𝑦 = 𝑆 } ↔ ∃ 𝑖 ∈ 𝐼 𝑧 = 𝑆 )
24 23 imbi1i ⊢ ( ( 𝑧 ∈ { 𝑦 ∣ ∃ 𝑖 ∈ 𝐼 𝑦 = 𝑆 } → 𝑝 ( le ‘ 𝐾 ) 𝑧 ) ↔ ( ∃ 𝑖 ∈ 𝐼 𝑧 = 𝑆 → 𝑝 ( le ‘ 𝐾 ) 𝑧 ) )
25 r19.23v ⊢ ( ∀ 𝑖 ∈ 𝐼 ( 𝑧 = 𝑆 → 𝑝 ( le ‘ 𝐾 ) 𝑧 ) ↔ ( ∃ 𝑖 ∈ 𝐼 𝑧 = 𝑆 → 𝑝 ( le ‘ 𝐾 ) 𝑧 ) )
26 24 25 bitr4i ⊢ ( ( 𝑧 ∈ { 𝑦 ∣ ∃ 𝑖 ∈ 𝐼 𝑦 = 𝑆 } → 𝑝 ( le ‘ 𝐾 ) 𝑧 ) ↔ ∀ 𝑖 ∈ 𝐼 ( 𝑧 = 𝑆 → 𝑝 ( le ‘ 𝐾 ) 𝑧 ) )
27 26 albii ⊢ ( ∀ 𝑧 ( 𝑧 ∈ { 𝑦 ∣ ∃ 𝑖 ∈ 𝐼 𝑦 = 𝑆 } → 𝑝 ( le ‘ 𝐾 ) 𝑧 ) ↔ ∀ 𝑧 ∀ 𝑖 ∈ 𝐼 ( 𝑧 = 𝑆 → 𝑝 ( le ‘ 𝐾 ) 𝑧 ) )
28 df-ral ⊢ ( ∀ 𝑧 ∈ { 𝑦 ∣ ∃ 𝑖 ∈ 𝐼 𝑦 = 𝑆 } 𝑝 ( le ‘ 𝐾 ) 𝑧 ↔ ∀ 𝑧 ( 𝑧 ∈ { 𝑦 ∣ ∃ 𝑖 ∈ 𝐼 𝑦 = 𝑆 } → 𝑝 ( le ‘ 𝐾 ) 𝑧 ) )
29 ralcom4 ⊢ ( ∀ 𝑖 ∈ 𝐼 ∀ 𝑧 ( 𝑧 = 𝑆 → 𝑝 ( le ‘ 𝐾 ) 𝑧 ) ↔ ∀ 𝑧 ∀ 𝑖 ∈ 𝐼 ( 𝑧 = 𝑆 → 𝑝 ( le ‘ 𝐾 ) 𝑧 ) )
30 27 28 29 3bitr4i ⊢ ( ∀ 𝑧 ∈ { 𝑦 ∣ ∃ 𝑖 ∈ 𝐼 𝑦 = 𝑆 } 𝑝 ( le ‘ 𝐾 ) 𝑧 ↔ ∀ 𝑖 ∈ 𝐼 ∀ 𝑧 ( 𝑧 = 𝑆 → 𝑝 ( le ‘ 𝐾 ) 𝑧 ) )
31 nfv ⊢ Ⅎ 𝑧 𝑝 ( le ‘ 𝐾 ) 𝑆
32 breq2 ⊢ ( 𝑧 = 𝑆 → ( 𝑝 ( le ‘ 𝐾 ) 𝑧 ↔ 𝑝 ( le ‘ 𝐾 ) 𝑆 ) )
33 31 32 ceqsalg ⊢ ( 𝑆 ∈ 𝐵 → ( ∀ 𝑧 ( 𝑧 = 𝑆 → 𝑝 ( le ‘ 𝐾 ) 𝑧 ) ↔ 𝑝 ( le ‘ 𝐾 ) 𝑆 ) )
34 33 ralimi ⊢ ( ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 → ∀ 𝑖 ∈ 𝐼 ( ∀ 𝑧 ( 𝑧 = 𝑆 → 𝑝 ( le ‘ 𝐾 ) 𝑧 ) ↔ 𝑝 ( le ‘ 𝐾 ) 𝑆 ) )
35 ralbi ⊢ ( ∀ 𝑖 ∈ 𝐼 ( ∀ 𝑧 ( 𝑧 = 𝑆 → 𝑝 ( le ‘ 𝐾 ) 𝑧 ) ↔ 𝑝 ( le ‘ 𝐾 ) 𝑆 ) → ( ∀ 𝑖 ∈ 𝐼 ∀ 𝑧 ( 𝑧 = 𝑆 → 𝑝 ( le ‘ 𝐾 ) 𝑧 ) ↔ ∀ 𝑖 ∈ 𝐼 𝑝 ( le ‘ 𝐾 ) 𝑆 ) )
36 34 35 syl ⊢ ( ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 → ( ∀ 𝑖 ∈ 𝐼 ∀ 𝑧 ( 𝑧 = 𝑆 → 𝑝 ( le ‘ 𝐾 ) 𝑧 ) ↔ ∀ 𝑖 ∈ 𝐼 𝑝 ( le ‘ 𝐾 ) 𝑆 ) )
37 30 36 syl5bb ⊢ ( ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 → ( ∀ 𝑧 ∈ { 𝑦 ∣ ∃ 𝑖 ∈ 𝐼 𝑦 = 𝑆 } 𝑝 ( le ‘ 𝐾 ) 𝑧 ↔ ∀ 𝑖 ∈ 𝐼 𝑝 ( le ‘ 𝐾 ) 𝑆 ) )
38 37 ad2antlr ⊢ ( ( ( 𝐾 ∈ HL ∧ ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ) → ( ∀ 𝑧 ∈ { 𝑦 ∣ ∃ 𝑖 ∈ 𝐼 𝑦 = 𝑆 } 𝑝 ( le ‘ 𝐾 ) 𝑧 ↔ ∀ 𝑖 ∈ 𝐼 𝑝 ( le ‘ 𝐾 ) 𝑆 ) )
39 19 38 bitrd ⊢ ( ( ( 𝐾 ∈ HL ∧ ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ) → ( 𝑝 ( le ‘ 𝐾 ) ( 𝐺 ‘ { 𝑦 ∣ ∃ 𝑖 ∈ 𝐼 𝑦 = 𝑆 } ) ↔ ∀ 𝑖 ∈ 𝐼 𝑝 ( le ‘ 𝐾 ) 𝑆 ) )
40 39 rabbidva ⊢ ( ( 𝐾 ∈ HL ∧ ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 ) → { 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑝 ( le ‘ 𝐾 ) ( 𝐺 ‘ { 𝑦 ∣ ∃ 𝑖 ∈ 𝐼 𝑦 = 𝑆 } ) } = { 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∣ ∀ 𝑖 ∈ 𝐼 𝑝 ( le ‘ 𝐾 ) 𝑆 } )
41 40 3adant3 ⊢ ( ( 𝐾 ∈ HL ∧ ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 ∧ 𝐼 ≠ ∅ ) → { 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑝 ( le ‘ 𝐾 ) ( 𝐺 ‘ { 𝑦 ∣ ∃ 𝑖 ∈ 𝐼 𝑦 = 𝑆 } ) } = { 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∣ ∀ 𝑖 ∈ 𝐼 𝑝 ( le ‘ 𝐾 ) 𝑆 } )
42 simp1 ⊢ ( ( 𝐾 ∈ HL ∧ ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 ∧ 𝐼 ≠ ∅ ) → 𝐾 ∈ HL )
43 14 abssdv ⊢ ( ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 → { 𝑦 ∣ ∃ 𝑖 ∈ 𝐼 𝑦 = 𝑆 } ⊆ 𝐵 )
44 1 2 clatglbcl ⊢ ( ( 𝐾 ∈ CLat ∧ { 𝑦 ∣ ∃ 𝑖 ∈ 𝐼 𝑦 = 𝑆 } ⊆ 𝐵 ) → ( 𝐺 ‘ { 𝑦 ∣ ∃ 𝑖 ∈ 𝐼 𝑦 = 𝑆 } ) ∈ 𝐵 )
45 4 43 44 syl2an ⊢ ( ( 𝐾 ∈ HL ∧ ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 ) → ( 𝐺 ‘ { 𝑦 ∣ ∃ 𝑖 ∈ 𝐼 𝑦 = 𝑆 } ) ∈ 𝐵 )
46 45 3adant3 ⊢ ( ( 𝐾 ∈ HL ∧ ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 ∧ 𝐼 ≠ ∅ ) → ( 𝐺 ‘ { 𝑦 ∣ ∃ 𝑖 ∈ 𝐼 𝑦 = 𝑆 } ) ∈ 𝐵 )
47 1 17 6 3 pmapval ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝐺 ‘ { 𝑦 ∣ ∃ 𝑖 ∈ 𝐼 𝑦 = 𝑆 } ) ∈ 𝐵 ) → ( 𝑀 ‘ ( 𝐺 ‘ { 𝑦 ∣ ∃ 𝑖 ∈ 𝐼 𝑦 = 𝑆 } ) ) = { 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑝 ( le ‘ 𝐾 ) ( 𝐺 ‘ { 𝑦 ∣ ∃ 𝑖 ∈ 𝐼 𝑦 = 𝑆 } ) } )
48 42 46 47 syl2anc ⊢ ( ( 𝐾 ∈ HL ∧ ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 ∧ 𝐼 ≠ ∅ ) → ( 𝑀 ‘ ( 𝐺 ‘ { 𝑦 ∣ ∃ 𝑖 ∈ 𝐼 𝑦 = 𝑆 } ) ) = { 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑝 ( le ‘ 𝐾 ) ( 𝐺 ‘ { 𝑦 ∣ ∃ 𝑖 ∈ 𝐼 𝑦 = 𝑆 } ) } )
49 iinrab ⊢ ( 𝐼 ≠ ∅ → ∩ 𝑖 ∈ 𝐼 { 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑝 ( le ‘ 𝐾 ) 𝑆 } = { 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∣ ∀ 𝑖 ∈ 𝐼 𝑝 ( le ‘ 𝐾 ) 𝑆 } )
50 49 3ad2ant3 ⊢ ( ( 𝐾 ∈ HL ∧ ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 ∧ 𝐼 ≠ ∅ ) → ∩ 𝑖 ∈ 𝐼 { 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑝 ( le ‘ 𝐾 ) 𝑆 } = { 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∣ ∀ 𝑖 ∈ 𝐼 𝑝 ( le ‘ 𝐾 ) 𝑆 } )
51 41 48 50 3eqtr4d ⊢ ( ( 𝐾 ∈ HL ∧ ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 ∧ 𝐼 ≠ ∅ ) → ( 𝑀 ‘ ( 𝐺 ‘ { 𝑦 ∣ ∃ 𝑖 ∈ 𝐼 𝑦 = 𝑆 } ) ) = ∩ 𝑖 ∈ 𝐼 { 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑝 ( le ‘ 𝐾 ) 𝑆 } )
52 nfv ⊢ Ⅎ 𝑖 𝐾 ∈ HL
53 nfra1 ⊢ Ⅎ 𝑖 ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵
54 nfv ⊢ Ⅎ 𝑖 𝐼 ≠ ∅
55 52 53 54 nf3an ⊢ Ⅎ 𝑖 ( 𝐾 ∈ HL ∧ ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 ∧ 𝐼 ≠ ∅ )
56 simpl1 ⊢ ( ( ( 𝐾 ∈ HL ∧ ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 ∧ 𝐼 ≠ ∅ ) ∧ 𝑖 ∈ 𝐼 ) → 𝐾 ∈ HL )
57 rspa ⊢ ( ( ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 ∧ 𝑖 ∈ 𝐼 ) → 𝑆 ∈ 𝐵 )
58 57 3ad2antl2 ⊢ ( ( ( 𝐾 ∈ HL ∧ ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 ∧ 𝐼 ≠ ∅ ) ∧ 𝑖 ∈ 𝐼 ) → 𝑆 ∈ 𝐵 )
59 1 17 6 3 pmapval ⊢ ( ( 𝐾 ∈ HL ∧ 𝑆 ∈ 𝐵 ) → ( 𝑀 ‘ 𝑆 ) = { 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑝 ( le ‘ 𝐾 ) 𝑆 } )
60 56 58 59 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 ∧ 𝐼 ≠ ∅ ) ∧ 𝑖 ∈ 𝐼 ) → ( 𝑀 ‘ 𝑆 ) = { 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑝 ( le ‘ 𝐾 ) 𝑆 } )
61 55 60 iineq2d ⊢ ( ( 𝐾 ∈ HL ∧ ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 ∧ 𝐼 ≠ ∅ ) → ∩ 𝑖 ∈ 𝐼 ( 𝑀 ‘ 𝑆 ) = ∩ 𝑖 ∈ 𝐼 { 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑝 ( le ‘ 𝐾 ) 𝑆 } )
62 51 61 eqtr4d ⊢ ( ( 𝐾 ∈ HL ∧ ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 ∧ 𝐼 ≠ ∅ ) → ( 𝑀 ‘ ( 𝐺 ‘ { 𝑦 ∣ ∃ 𝑖 ∈ 𝐼 𝑦 = 𝑆 } ) ) = ∩ 𝑖 ∈ 𝐼 ( 𝑀 ‘ 𝑆 ) )