Metamath Proof Explorer

Theorem pmapj2N

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

Ref Expression
Hypotheses pmapj2.b 
|- B = ( Base ` K )
pmapj2.j 
|- .\/ = ( join ` K )
pmapj2.m 
|- M = ( pmap ` K )
pmapj2.p 
|- .+ = ( +P ` K )
pmapj2.o 
|- ._|_ = ( _|_P ` K )
Assertion pmapj2N 
|- ( ( K e. HL /\ X e. B /\ Y e. B ) -> ( M ` ( X .\/ Y ) ) = ( ._|_ ` ( ._|_ ` ( ( M ` X ) .+ ( M ` Y ) ) ) ) )

Proof

Step Hyp Ref Expression
1 pmapj2.b 
 |-  B = ( Base ` K )
2 pmapj2.j 
 |-  .\/ = ( join ` K )
3 pmapj2.m 
 |-  M = ( pmap ` K )
4 pmapj2.p 
 |-  .+ = ( +P ` K )
5 pmapj2.o 
 |-  ._|_ = ( _|_P ` K )
6 simp1 
 |-  ( ( K e. HL /\ X e. B /\ Y e. B ) -> K e. HL )
7 hllat 
 |-  ( K e. HL -> K e. Lat )
8 7 3ad2ant1 
 |-  ( ( K e. HL /\ X e. B /\ Y e. B ) -> K e. Lat )
9 hlop 
 |-  ( K e. HL -> K e. OP )
10 9 3ad2ant1 
 |-  ( ( K e. HL /\ X e. B /\ Y e. B ) -> K e. OP )
11 simp2 
 |-  ( ( K e. HL /\ X e. B /\ Y e. B ) -> X e. B )
12 eqid 
 |-  ( oc ` K ) = ( oc ` K )
13 1 12 opoccl 
 |-  ( ( K e. OP /\ X e. B ) -> ( ( oc ` K ) ` X ) e. B )
14 10 11 13 syl2anc 
 |-  ( ( K e. HL /\ X e. B /\ Y e. B ) -> ( ( oc ` K ) ` X ) e. B )
15 simp3 
 |-  ( ( K e. HL /\ X e. B /\ Y e. B ) -> Y e. B )
16 1 12 opoccl 
 |-  ( ( K e. OP /\ Y e. B ) -> ( ( oc ` K ) ` Y ) e. B )
17 10 15 16 syl2anc 
 |-  ( ( K e. HL /\ X e. B /\ Y e. B ) -> ( ( oc ` K ) ` Y ) e. B )
18 eqid 
 |-  ( meet ` K ) = ( meet ` K )
19 1 18 latmcl 
 |-  ( ( K e. Lat /\ ( ( oc ` K ) ` X ) e. B /\ ( ( oc ` K ) ` Y ) e. B ) -> ( ( ( oc ` K ) ` X ) ( meet ` K ) ( ( oc ` K ) ` Y ) ) e. B )
20 8 14 17 19 syl3anc 
 |-  ( ( K e. HL /\ X e. B /\ Y e. B ) -> ( ( ( oc ` K ) ` X ) ( meet ` K ) ( ( oc ` K ) ` Y ) ) e. B )
21 1 12 3 5 polpmapN 
 |-  ( ( K e. HL /\ ( ( ( oc ` K ) ` X ) ( meet ` K ) ( ( oc ` K ) ` Y ) ) e. B ) -> ( ._|_ ` ( M ` ( ( ( oc ` K ) ` X ) ( meet ` K ) ( ( oc ` K ) ` Y ) ) ) ) = ( M ` ( ( oc ` K ) ` ( ( ( oc ` K ) ` X ) ( meet ` K ) ( ( oc ` K ) ` Y ) ) ) ) )
22 6 20 21 syl2anc 
 |-  ( ( K e. HL /\ X e. B /\ Y e. B ) -> ( ._|_ ` ( M ` ( ( ( oc ` K ) ` X ) ( meet ` K ) ( ( oc ` K ) ` Y ) ) ) ) = ( M ` ( ( oc ` K ) ` ( ( ( oc ` K ) ` X ) ( meet ` K ) ( ( oc ` K ) ` Y ) ) ) ) )
23 1 12 3 5 polpmapN 
 |-  ( ( K e. HL /\ X e. B ) -> ( ._|_ ` ( M ` X ) ) = ( M ` ( ( oc ` K ) ` X ) ) )
24 23 3adant3 
 |-  ( ( K e. HL /\ X e. B /\ Y e. B ) -> ( ._|_ ` ( M ` X ) ) = ( M ` ( ( oc ` K ) ` X ) ) )
25 1 12 3 5 polpmapN 
 |-  ( ( K e. HL /\ Y e. B ) -> ( ._|_ ` ( M ` Y ) ) = ( M ` ( ( oc ` K ) ` Y ) ) )
26 25 3adant2 
 |-  ( ( K e. HL /\ X e. B /\ Y e. B ) -> ( ._|_ ` ( M ` Y ) ) = ( M ` ( ( oc ` K ) ` Y ) ) )
27 24 26 ineq12d 
 |-  ( ( K e. HL /\ X e. B /\ Y e. B ) -> ( ( ._|_ ` ( M ` X ) ) i^i ( ._|_ ` ( M ` Y ) ) ) = ( ( M ` ( ( oc ` K ) ` X ) ) i^i ( M ` ( ( oc ` K ) ` Y ) ) ) )
28 eqid 
 |-  ( Atoms ` K ) = ( Atoms ` K )
29 1 28 3 pmapssat 
 |-  ( ( K e. HL /\ X e. B ) -> ( M ` X ) C_ ( Atoms ` K ) )
30 29 3adant3 
 |-  ( ( K e. HL /\ X e. B /\ Y e. B ) -> ( M ` X ) C_ ( Atoms ` K ) )
31 1 28 3 pmapssat 
 |-  ( ( K e. HL /\ Y e. B ) -> ( M ` Y ) C_ ( Atoms ` K ) )
32 31 3adant2 
 |-  ( ( K e. HL /\ X e. B /\ Y e. B ) -> ( M ` Y ) C_ ( Atoms ` K ) )
33 28 4 5 poldmj1N 
 |-  ( ( K e. HL /\ ( M ` X ) C_ ( Atoms ` K ) /\ ( M ` Y ) C_ ( Atoms ` K ) ) -> ( ._|_ ` ( ( M ` X ) .+ ( M ` Y ) ) ) = ( ( ._|_ ` ( M ` X ) ) i^i ( ._|_ ` ( M ` Y ) ) ) )
34 6 30 32 33 syl3anc 
 |-  ( ( K e. HL /\ X e. B /\ Y e. B ) -> ( ._|_ ` ( ( M ` X ) .+ ( M ` Y ) ) ) = ( ( ._|_ ` ( M ` X ) ) i^i ( ._|_ ` ( M ` Y ) ) ) )
35 1 18 28 3 pmapmeet 
 |-  ( ( K e. HL /\ ( ( oc ` K ) ` X ) e. B /\ ( ( oc ` K ) ` Y ) e. B ) -> ( M ` ( ( ( oc ` K ) ` X ) ( meet ` K ) ( ( oc ` K ) ` Y ) ) ) = ( ( M ` ( ( oc ` K ) ` X ) ) i^i ( M ` ( ( oc ` K ) ` Y ) ) ) )
36 6 14 17 35 syl3anc 
 |-  ( ( K e. HL /\ X e. B /\ Y e. B ) -> ( M ` ( ( ( oc ` K ) ` X ) ( meet ` K ) ( ( oc ` K ) ` Y ) ) ) = ( ( M ` ( ( oc ` K ) ` X ) ) i^i ( M ` ( ( oc ` K ) ` Y ) ) ) )
37 27 34 36 3eqtr4rd 
 |-  ( ( K e. HL /\ X e. B /\ Y e. B ) -> ( M ` ( ( ( oc ` K ) ` X ) ( meet ` K ) ( ( oc ` K ) ` Y ) ) ) = ( ._|_ ` ( ( M ` X ) .+ ( M ` Y ) ) ) )
38 37 fveq2d 
 |-  ( ( K e. HL /\ X e. B /\ Y e. B ) -> ( ._|_ ` ( M ` ( ( ( oc ` K ) ` X ) ( meet ` K ) ( ( oc ` K ) ` Y ) ) ) ) = ( ._|_ ` ( ._|_ ` ( ( M ` X ) .+ ( M ` Y ) ) ) ) )
39 hlol 
 |-  ( K e. HL -> K e. OL )
40 1 2 18 12 oldmm4 
 |-  ( ( K e. OL /\ X e. B /\ Y e. B ) -> ( ( oc ` K ) ` ( ( ( oc ` K ) ` X ) ( meet ` K ) ( ( oc ` K ) ` Y ) ) ) = ( X .\/ Y ) )
41 39 40 syl3an1 
 |-  ( ( K e. HL /\ X e. B /\ Y e. B ) -> ( ( oc ` K ) ` ( ( ( oc ` K ) ` X ) ( meet ` K ) ( ( oc ` K ) ` Y ) ) ) = ( X .\/ Y ) )
42 41 fveq2d 
 |-  ( ( K e. HL /\ X e. B /\ Y e. B ) -> ( M ` ( ( oc ` K ) ` ( ( ( oc ` K ) ` X ) ( meet ` K ) ( ( oc ` K ) ` Y ) ) ) ) = ( M ` ( X .\/ Y ) ) )
43 22 38 42 3eqtr3rd 
 |-  ( ( K e. HL /\ X e. B /\ Y e. B ) -> ( M ` ( X .\/ Y ) ) = ( ._|_ ` ( ._|_ ` ( ( M ` X ) .+ ( M ` Y ) ) ) ) )