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

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 ) ) ) )