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

Metamath Proof Explorer

Theorem pmapmeet

Description: The projective map of a meet. (Contributed by NM, 25-Jan-2012)

Ref Expression
Hypotheses pmapmeet.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
pmapmeet.m ⊢ ∧ = ( meet ‘ 𝐾 )
pmapmeet.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
pmapmeet.p ⊢ 𝑃 = ( pmap ‘ 𝐾 )
Assertion pmapmeet ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑃 ‘ ( 𝑋 ∧ 𝑌 ) ) = ( ( 𝑃 ‘ 𝑋 ) ∩ ( 𝑃 ‘ 𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 pmapmeet.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 pmapmeet.m ⊢ ∧ = ( meet ‘ 𝐾 )
3 pmapmeet.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4 pmapmeet.p ⊢ 𝑃 = ( pmap ‘ 𝐾 )
5 eqid ⊢ ( glb ‘ 𝐾 ) = ( glb ‘ 𝐾 )
6 simp1 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝐾 ∈ HL )
7 simp2 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑋 ∈ 𝐵 )
8 simp3 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑌 ∈ 𝐵 )
9 5 2 6 7 8 meetval ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ∧ 𝑌 ) = ( ( glb ‘ 𝐾 ) ‘ { 𝑋 , 𝑌 } ) )
10 9 fveq2d ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑃 ‘ ( 𝑋 ∧ 𝑌 ) ) = ( 𝑃 ‘ ( ( glb ‘ 𝐾 ) ‘ { 𝑋 , 𝑌 } ) ) )
11 prssi ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → { 𝑋 , 𝑌 } ⊆ 𝐵 )
12 11 3adant1 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → { 𝑋 , 𝑌 } ⊆ 𝐵 )
13 prnzg ⊢ ( 𝑋 ∈ 𝐵 → { 𝑋 , 𝑌 } ≠ ∅ )
14 13 3ad2ant2 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → { 𝑋 , 𝑌 } ≠ ∅ )
15 1 5 4 pmapglb ⊢ ( ( 𝐾 ∈ HL ∧ { 𝑋 , 𝑌 } ⊆ 𝐵 ∧ { 𝑋 , 𝑌 } ≠ ∅ ) → ( 𝑃 ‘ ( ( glb ‘ 𝐾 ) ‘ { 𝑋 , 𝑌 } ) ) = ∩ 𝑥 ∈ { 𝑋 , 𝑌 } ( 𝑃 ‘ 𝑥 ) )
16 6 12 14 15 syl3anc ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑃 ‘ ( ( glb ‘ 𝐾 ) ‘ { 𝑋 , 𝑌 } ) ) = ∩ 𝑥 ∈ { 𝑋 , 𝑌 } ( 𝑃 ‘ 𝑥 ) )
17 fveq2 ⊢ ( 𝑥 = 𝑋 → ( 𝑃 ‘ 𝑥 ) = ( 𝑃 ‘ 𝑋 ) )
18 fveq2 ⊢ ( 𝑥 = 𝑌 → ( 𝑃 ‘ 𝑥 ) = ( 𝑃 ‘ 𝑌 ) )
19 17 18 iinxprg ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ∩ 𝑥 ∈ { 𝑋 , 𝑌 } ( 𝑃 ‘ 𝑥 ) = ( ( 𝑃 ‘ 𝑋 ) ∩ ( 𝑃 ‘ 𝑌 ) ) )
20 19 3adant1 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ∩ 𝑥 ∈ { 𝑋 , 𝑌 } ( 𝑃 ‘ 𝑥 ) = ( ( 𝑃 ‘ 𝑋 ) ∩ ( 𝑃 ‘ 𝑌 ) ) )
21 10 16 20 3eqtrd ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑃 ‘ ( 𝑋 ∧ 𝑌 ) ) = ( ( 𝑃 ‘ 𝑋 ) ∩ ( 𝑃 ‘ 𝑌 ) ) )