Metamath Proof Explorer


Theorem pmapmeet

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

Ref Expression
Hypotheses pmapmeet.b B=BaseK
pmapmeet.m ˙=meetK
pmapmeet.a A=AtomsK
pmapmeet.p P=pmapK
Assertion pmapmeet KHLXBYBPX˙Y=PXPY

Proof

Step Hyp Ref Expression
1 pmapmeet.b B=BaseK
2 pmapmeet.m ˙=meetK
3 pmapmeet.a A=AtomsK
4 pmapmeet.p P=pmapK
5 eqid glbK=glbK
6 simp1 KHLXBYBKHL
7 simp2 KHLXBYBXB
8 simp3 KHLXBYBYB
9 5 2 6 7 8 meetval KHLXBYBX˙Y=glbKXY
10 9 fveq2d KHLXBYBPX˙Y=PglbKXY
11 prssi XBYBXYB
12 11 3adant1 KHLXBYBXYB
13 prnzg XBXY
14 13 3ad2ant2 KHLXBYBXY
15 1 5 4 pmapglb KHLXYBXYPglbKXY=xXYPx
16 6 12 14 15 syl3anc KHLXBYBPglbKXY=xXYPx
17 fveq2 x=XPx=PX
18 fveq2 x=YPx=PY
19 17 18 iinxprg XBYBxXYPx=PXPY
20 19 3adant1 KHLXBYBxXYPx=PXPY
21 10 16 20 3eqtrd KHLXBYBPX˙Y=PXPY