Metamath Proof Explorer


Theorem pmapocjN

Description: The projective map of the orthocomplement of the join of two lattice elements. (Contributed by NM, 14-Mar-2012) (New usage is discouraged.)

Ref Expression
Hypotheses pmapocj.b
|- B = ( Base ` K )
pmapocj.j
|- .\/ = ( join ` K )
pmapocj.m
|- ./\ = ( meet ` K )
pmapocj.o
|- ._|_ = ( oc ` K )
pmapocj.f
|- F = ( pmap ` K )
pmapocj.p
|- .+ = ( +P ` K )
pmapocj.r
|- N = ( _|_P ` K )
Assertion pmapocjN
|- ( ( K e. HL /\ X e. B /\ Y e. B ) -> ( F ` ( ._|_ ` ( X .\/ Y ) ) ) = ( N ` ( ( F ` X ) .+ ( F ` Y ) ) ) )

Proof

Step Hyp Ref Expression
1 pmapocj.b
 |-  B = ( Base ` K )
2 pmapocj.j
 |-  .\/ = ( join ` K )
3 pmapocj.m
 |-  ./\ = ( meet ` K )
4 pmapocj.o
 |-  ._|_ = ( oc ` K )
5 pmapocj.f
 |-  F = ( pmap ` K )
6 pmapocj.p
 |-  .+ = ( +P ` K )
7 pmapocj.r
 |-  N = ( _|_P ` K )
8 1 2 5 6 7 pmapj2N
 |-  ( ( K e. HL /\ X e. B /\ Y e. B ) -> ( F ` ( X .\/ Y ) ) = ( N ` ( N ` ( ( F ` X ) .+ ( F ` Y ) ) ) ) )
9 8 fveq2d
 |-  ( ( K e. HL /\ X e. B /\ Y e. B ) -> ( N ` ( F ` ( X .\/ Y ) ) ) = ( N ` ( N ` ( N ` ( ( F ` X ) .+ ( F ` Y ) ) ) ) ) )
10 simp1
 |-  ( ( K e. HL /\ X e. B /\ Y e. B ) -> K e. HL )
11 hllat
 |-  ( K e. HL -> K e. Lat )
12 1 2 latjcl
 |-  ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( X .\/ Y ) e. B )
13 11 12 syl3an1
 |-  ( ( K e. HL /\ X e. B /\ Y e. B ) -> ( X .\/ Y ) e. B )
14 1 4 5 7 polpmapN
 |-  ( ( K e. HL /\ ( X .\/ Y ) e. B ) -> ( N ` ( F ` ( X .\/ Y ) ) ) = ( F ` ( ._|_ ` ( X .\/ Y ) ) ) )
15 10 13 14 syl2anc
 |-  ( ( K e. HL /\ X e. B /\ Y e. B ) -> ( N ` ( F ` ( X .\/ Y ) ) ) = ( F ` ( ._|_ ` ( X .\/ Y ) ) ) )
16 eqid
 |-  ( Atoms ` K ) = ( Atoms ` K )
17 1 16 5 pmapssat
 |-  ( ( K e. HL /\ X e. B ) -> ( F ` X ) C_ ( Atoms ` K ) )
18 17 3adant3
 |-  ( ( K e. HL /\ X e. B /\ Y e. B ) -> ( F ` X ) C_ ( Atoms ` K ) )
19 1 16 5 pmapssat
 |-  ( ( K e. HL /\ Y e. B ) -> ( F ` Y ) C_ ( Atoms ` K ) )
20 19 3adant2
 |-  ( ( K e. HL /\ X e. B /\ Y e. B ) -> ( F ` Y ) C_ ( Atoms ` K ) )
21 16 6 paddssat
 |-  ( ( K e. HL /\ ( F ` X ) C_ ( Atoms ` K ) /\ ( F ` Y ) C_ ( Atoms ` K ) ) -> ( ( F ` X ) .+ ( F ` Y ) ) C_ ( Atoms ` K ) )
22 10 18 20 21 syl3anc
 |-  ( ( K e. HL /\ X e. B /\ Y e. B ) -> ( ( F ` X ) .+ ( F ` Y ) ) C_ ( Atoms ` K ) )
23 16 7 3polN
 |-  ( ( K e. HL /\ ( ( F ` X ) .+ ( F ` Y ) ) C_ ( Atoms ` K ) ) -> ( N ` ( N ` ( N ` ( ( F ` X ) .+ ( F ` Y ) ) ) ) ) = ( N ` ( ( F ` X ) .+ ( F ` Y ) ) ) )
24 10 22 23 syl2anc
 |-  ( ( K e. HL /\ X e. B /\ Y e. B ) -> ( N ` ( N ` ( N ` ( ( F ` X ) .+ ( F ` Y ) ) ) ) ) = ( N ` ( ( F ` X ) .+ ( F ` Y ) ) ) )
25 9 15 24 3eqtr3d
 |-  ( ( K e. HL /\ X e. B /\ Y e. B ) -> ( F ` ( ._|_ ` ( X .\/ Y ) ) ) = ( N ` ( ( F ` X ) .+ ( F ` Y ) ) ) )