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 ∧ 𝑋𝐵𝑌𝐵 ) → ( 𝑃 ‘ ( 𝑋 𝑌 ) ) = ( ( 𝑃𝑋 ) ∩ ( 𝑃𝑌 ) ) )