Metamath Proof Explorer

Theorem pmapjat1

Description: The projective map of the join of a lattice element and an atom. (Contributed by NM, 28-Jan-2012)

Ref Expression
Hypotheses pmapjat.b 
|- B = ( Base ` K )
pmapjat.j 
|- .\/ = ( join ` K )
pmapjat.a 
|- A = ( Atoms ` K )
pmapjat.m 
|- M = ( pmap ` K )
pmapjat.p 
|- .+ = ( +P ` K )
Assertion pmapjat1 
|- ( ( K e. HL /\ X e. B /\ Q e. A ) -> ( M ` ( X .\/ Q ) ) = ( ( M ` X ) .+ ( M ` Q ) ) )

Proof

Step Hyp Ref Expression
1 pmapjat.b 
 |-  B = ( Base ` K )
2 pmapjat.j 
 |-  .\/ = ( join ` K )
3 pmapjat.a 
 |-  A = ( Atoms ` K )
4 pmapjat.m 
 |-  M = ( pmap ` K )
5 pmapjat.p 
 |-  .+ = ( +P ` K )
6 simp1 
 |-  ( ( K e. HL /\ X e. B /\ Q e. A ) -> K e. HL )
7 1 3 atbase 
 |-  ( Q e. A -> Q e. B )
8 7 3ad2ant3 
 |-  ( ( K e. HL /\ X e. B /\ Q e. A ) -> Q e. B )
9 1 3 4 pmapssat 
 |-  ( ( K e. HL /\ Q e. B ) -> ( M ` Q ) C_ A )
10 6 8 9 syl2anc 
 |-  ( ( K e. HL /\ X e. B /\ Q e. A ) -> ( M ` Q ) C_ A )
11 3 5 padd02 
 |-  ( ( K e. HL /\ ( M ` Q ) C_ A ) -> ( (/) .+ ( M ` Q ) ) = ( M ` Q ) )
12 6 10 11 syl2anc 
 |-  ( ( K e. HL /\ X e. B /\ Q e. A ) -> ( (/) .+ ( M ` Q ) ) = ( M ` Q ) )
13 12 adantr 
 |-  ( ( ( K e. HL /\ X e. B /\ Q e. A ) /\ X = ( 0. ` K ) ) -> ( (/) .+ ( M ` Q ) ) = ( M ` Q ) )
14 fveq2 
 |-  ( X = ( 0. ` K ) -> ( M ` X ) = ( M ` ( 0. ` K ) ) )
15 hlatl 
 |-  ( K e. HL -> K e. AtLat )
16 15 3ad2ant1 
 |-  ( ( K e. HL /\ X e. B /\ Q e. A ) -> K e. AtLat )
17 eqid 
 |-  ( 0. ` K ) = ( 0. ` K )
18 17 4 pmap0 
 |-  ( K e. AtLat -> ( M ` ( 0. ` K ) ) = (/) )
19 16 18 syl 
 |-  ( ( K e. HL /\ X e. B /\ Q e. A ) -> ( M ` ( 0. ` K ) ) = (/) )
20 14 19 sylan9eqr 
 |-  ( ( ( K e. HL /\ X e. B /\ Q e. A ) /\ X = ( 0. ` K ) ) -> ( M ` X ) = (/) )
21 20 oveq1d 
 |-  ( ( ( K e. HL /\ X e. B /\ Q e. A ) /\ X = ( 0. ` K ) ) -> ( ( M ` X ) .+ ( M ` Q ) ) = ( (/) .+ ( M ` Q ) ) )
22 oveq1 
 |-  ( X = ( 0. ` K ) -> ( X .\/ Q ) = ( ( 0. ` K ) .\/ Q ) )
23 hlol 
 |-  ( K e. HL -> K e. OL )
24 23 3ad2ant1 
 |-  ( ( K e. HL /\ X e. B /\ Q e. A ) -> K e. OL )
25 1 2 17 olj02 
 |-  ( ( K e. OL /\ Q e. B ) -> ( ( 0. ` K ) .\/ Q ) = Q )
26 24 8 25 syl2anc 
 |-  ( ( K e. HL /\ X e. B /\ Q e. A ) -> ( ( 0. ` K ) .\/ Q ) = Q )
27 22 26 sylan9eqr 
 |-  ( ( ( K e. HL /\ X e. B /\ Q e. A ) /\ X = ( 0. ` K ) ) -> ( X .\/ Q ) = Q )
28 27 fveq2d 
 |-  ( ( ( K e. HL /\ X e. B /\ Q e. A ) /\ X = ( 0. ` K ) ) -> ( M ` ( X .\/ Q ) ) = ( M ` Q ) )
29 13 21 28 3eqtr4rd 
 |-  ( ( ( K e. HL /\ X e. B /\ Q e. A ) /\ X = ( 0. ` K ) ) -> ( M ` ( X .\/ Q ) ) = ( ( M ` X ) .+ ( M ` Q ) ) )
30 simpll1 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Q e. A ) /\ X =/= ( 0. ` K ) ) /\ p e. A ) -> K e. HL )
31 30 adantr 
 |-  ( ( ( ( ( K e. HL /\ X e. B /\ Q e. A ) /\ X =/= ( 0. ` K ) ) /\ p e. A ) /\ p ( le ` K ) ( X .\/ Q ) ) -> K e. HL )
32 simpll2 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Q e. A ) /\ X =/= ( 0. ` K ) ) /\ p e. A ) -> X e. B )
33 32 adantr 
 |-  ( ( ( ( ( K e. HL /\ X e. B /\ Q e. A ) /\ X =/= ( 0. ` K ) ) /\ p e. A ) /\ p ( le ` K ) ( X .\/ Q ) ) -> X e. B )
34 simplr 
 |-  ( ( ( ( ( K e. HL /\ X e. B /\ Q e. A ) /\ X =/= ( 0. ` K ) ) /\ p e. A ) /\ p ( le ` K ) ( X .\/ Q ) ) -> p e. A )
35 simpll3 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Q e. A ) /\ X =/= ( 0. ` K ) ) /\ p e. A ) -> Q e. A )
36 35 adantr 
 |-  ( ( ( ( ( K e. HL /\ X e. B /\ Q e. A ) /\ X =/= ( 0. ` K ) ) /\ p e. A ) /\ p ( le ` K ) ( X .\/ Q ) ) -> Q e. A )
37 33 34 36 3jca 
 |-  ( ( ( ( ( K e. HL /\ X e. B /\ Q e. A ) /\ X =/= ( 0. ` K ) ) /\ p e. A ) /\ p ( le ` K ) ( X .\/ Q ) ) -> ( X e. B /\ p e. A /\ Q e. A ) )
38 simpllr 
 |-  ( ( ( ( ( K e. HL /\ X e. B /\ Q e. A ) /\ X =/= ( 0. ` K ) ) /\ p e. A ) /\ p ( le ` K ) ( X .\/ Q ) ) -> X =/= ( 0. ` K ) )
39 simpr 
 |-  ( ( ( ( ( K e. HL /\ X e. B /\ Q e. A ) /\ X =/= ( 0. ` K ) ) /\ p e. A ) /\ p ( le ` K ) ( X .\/ Q ) ) -> p ( le ` K ) ( X .\/ Q ) )
40 eqid 
 |-  ( le ` K ) = ( le ` K )
41 1 40 2 17 3 cvrat42 
 |-  ( ( K e. HL /\ ( X e. B /\ p e. A /\ Q e. A ) ) -> ( ( X =/= ( 0. ` K ) /\ p ( le ` K ) ( X .\/ Q ) ) -> E. q e. A ( q ( le ` K ) X /\ p ( le ` K ) ( q .\/ Q ) ) ) )
42 41 imp 
 |-  ( ( ( K e. HL /\ ( X e. B /\ p e. A /\ Q e. A ) ) /\ ( X =/= ( 0. ` K ) /\ p ( le ` K ) ( X .\/ Q ) ) ) -> E. q e. A ( q ( le ` K ) X /\ p ( le ` K ) ( q .\/ Q ) ) )
43 31 37 38 39 42 syl22anc 
 |-  ( ( ( ( ( K e. HL /\ X e. B /\ Q e. A ) /\ X =/= ( 0. ` K ) ) /\ p e. A ) /\ p ( le ` K ) ( X .\/ Q ) ) -> E. q e. A ( q ( le ` K ) X /\ p ( le ` K ) ( q .\/ Q ) ) )
44 43 ex 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Q e. A ) /\ X =/= ( 0. ` K ) ) /\ p e. A ) -> ( p ( le ` K ) ( X .\/ Q ) -> E. q e. A ( q ( le ` K ) X /\ p ( le ` K ) ( q .\/ Q ) ) ) )
45 1 40 3 4 elpmap 
 |-  ( ( K e. HL /\ X e. B ) -> ( q e. ( M ` X ) <-> ( q e. A /\ q ( le ` K ) X ) ) )
46 45 3adant3 
 |-  ( ( K e. HL /\ X e. B /\ Q e. A ) -> ( q e. ( M ` X ) <-> ( q e. A /\ q ( le ` K ) X ) ) )
47 df-rex 
 |-  ( E. r e. ( M ` Q ) p ( le ` K ) ( q .\/ r ) <-> E. r ( r e. ( M ` Q ) /\ p ( le ` K ) ( q .\/ r ) ) )
48 3 4 elpmapat 
 |-  ( ( K e. HL /\ Q e. A ) -> ( r e. ( M ` Q ) <-> r = Q ) )
49 48 3adant2 
 |-  ( ( K e. HL /\ X e. B /\ Q e. A ) -> ( r e. ( M ` Q ) <-> r = Q ) )
50 49 anbi1d 
 |-  ( ( K e. HL /\ X e. B /\ Q e. A ) -> ( ( r e. ( M ` Q ) /\ p ( le ` K ) ( q .\/ r ) ) <-> ( r = Q /\ p ( le ` K ) ( q .\/ r ) ) ) )
51 50 exbidv 
 |-  ( ( K e. HL /\ X e. B /\ Q e. A ) -> ( E. r ( r e. ( M ` Q ) /\ p ( le ` K ) ( q .\/ r ) ) <-> E. r ( r = Q /\ p ( le ` K ) ( q .\/ r ) ) ) )
52 47 51 bitr2id 
 |-  ( ( K e. HL /\ X e. B /\ Q e. A ) -> ( E. r ( r = Q /\ p ( le ` K ) ( q .\/ r ) ) <-> E. r e. ( M ` Q ) p ( le ` K ) ( q .\/ r ) ) )
53 oveq2 
 |-  ( r = Q -> ( q .\/ r ) = ( q .\/ Q ) )
54 53 breq2d 
 |-  ( r = Q -> ( p ( le ` K ) ( q .\/ r ) <-> p ( le ` K ) ( q .\/ Q ) ) )
55 54 ceqsexgv 
 |-  ( Q e. A -> ( E. r ( r = Q /\ p ( le ` K ) ( q .\/ r ) ) <-> p ( le ` K ) ( q .\/ Q ) ) )
56 55 3ad2ant3 
 |-  ( ( K e. HL /\ X e. B /\ Q e. A ) -> ( E. r ( r = Q /\ p ( le ` K ) ( q .\/ r ) ) <-> p ( le ` K ) ( q .\/ Q ) ) )
57 52 56 bitr3d 
 |-  ( ( K e. HL /\ X e. B /\ Q e. A ) -> ( E. r e. ( M ` Q ) p ( le ` K ) ( q .\/ r ) <-> p ( le ` K ) ( q .\/ Q ) ) )
58 46 57 anbi12d 
 |-  ( ( K e. HL /\ X e. B /\ Q e. A ) -> ( ( q e. ( M ` X ) /\ E. r e. ( M ` Q ) p ( le ` K ) ( q .\/ r ) ) <-> ( ( q e. A /\ q ( le ` K ) X ) /\ p ( le ` K ) ( q .\/ Q ) ) ) )
59 anass 
 |-  ( ( ( q e. A /\ q ( le ` K ) X ) /\ p ( le ` K ) ( q .\/ Q ) ) <-> ( q e. A /\ ( q ( le ` K ) X /\ p ( le ` K ) ( q .\/ Q ) ) ) )
60 58 59 bitrdi 
 |-  ( ( K e. HL /\ X e. B /\ Q e. A ) -> ( ( q e. ( M ` X ) /\ E. r e. ( M ` Q ) p ( le ` K ) ( q .\/ r ) ) <-> ( q e. A /\ ( q ( le ` K ) X /\ p ( le ` K ) ( q .\/ Q ) ) ) ) )
61 60 rexbidv2 
 |-  ( ( K e. HL /\ X e. B /\ Q e. A ) -> ( E. q e. ( M ` X ) E. r e. ( M ` Q ) p ( le ` K ) ( q .\/ r ) <-> E. q e. A ( q ( le ` K ) X /\ p ( le ` K ) ( q .\/ Q ) ) ) )
62 61 ad2antrr 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Q e. A ) /\ X =/= ( 0. ` K ) ) /\ p e. A ) -> ( E. q e. ( M ` X ) E. r e. ( M ` Q ) p ( le ` K ) ( q .\/ r ) <-> E. q e. A ( q ( le ` K ) X /\ p ( le ` K ) ( q .\/ Q ) ) ) )
63 44 62 sylibrd 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Q e. A ) /\ X =/= ( 0. ` K ) ) /\ p e. A ) -> ( p ( le ` K ) ( X .\/ Q ) -> E. q e. ( M ` X ) E. r e. ( M ` Q ) p ( le ` K ) ( q .\/ r ) ) )
64 63 imdistanda 
 |-  ( ( ( K e. HL /\ X e. B /\ Q e. A ) /\ X =/= ( 0. ` K ) ) -> ( ( p e. A /\ p ( le ` K ) ( X .\/ Q ) ) -> ( p e. A /\ E. q e. ( M ` X ) E. r e. ( M ` Q ) p ( le ` K ) ( q .\/ r ) ) ) )
65 hllat 
 |-  ( K e. HL -> K e. Lat )
66 65 3ad2ant1 
 |-  ( ( K e. HL /\ X e. B /\ Q e. A ) -> K e. Lat )
67 simp2 
 |-  ( ( K e. HL /\ X e. B /\ Q e. A ) -> X e. B )
68 1 2 latjcl 
 |-  ( ( K e. Lat /\ X e. B /\ Q e. B ) -> ( X .\/ Q ) e. B )
69 66 67 8 68 syl3anc 
 |-  ( ( K e. HL /\ X e. B /\ Q e. A ) -> ( X .\/ Q ) e. B )
70 1 40 3 4 elpmap 
 |-  ( ( K e. HL /\ ( X .\/ Q ) e. B ) -> ( p e. ( M ` ( X .\/ Q ) ) <-> ( p e. A /\ p ( le ` K ) ( X .\/ Q ) ) ) )
71 6 69 70 syl2anc 
 |-  ( ( K e. HL /\ X e. B /\ Q e. A ) -> ( p e. ( M ` ( X .\/ Q ) ) <-> ( p e. A /\ p ( le ` K ) ( X .\/ Q ) ) ) )
72 71 adantr 
 |-  ( ( ( K e. HL /\ X e. B /\ Q e. A ) /\ X =/= ( 0. ` K ) ) -> ( p e. ( M ` ( X .\/ Q ) ) <-> ( p e. A /\ p ( le ` K ) ( X .\/ Q ) ) ) )
73 1 3 4 pmapssat 
 |-  ( ( K e. HL /\ X e. B ) -> ( M ` X ) C_ A )
74 73 3adant3 
 |-  ( ( K e. HL /\ X e. B /\ Q e. A ) -> ( M ` X ) C_ A )
75 66 74 10 3jca 
 |-  ( ( K e. HL /\ X e. B /\ Q e. A ) -> ( K e. Lat /\ ( M ` X ) C_ A /\ ( M ` Q ) C_ A ) )
76 75 adantr 
 |-  ( ( ( K e. HL /\ X e. B /\ Q e. A ) /\ X =/= ( 0. ` K ) ) -> ( K e. Lat /\ ( M ` X ) C_ A /\ ( M ` Q ) C_ A ) )
77 1 17 4 pmapeq0 
 |-  ( ( K e. HL /\ X e. B ) -> ( ( M ` X ) = (/) <-> X = ( 0. ` K ) ) )
78 77 3adant3 
 |-  ( ( K e. HL /\ X e. B /\ Q e. A ) -> ( ( M ` X ) = (/) <-> X = ( 0. ` K ) ) )
79 78 necon3bid 
 |-  ( ( K e. HL /\ X e. B /\ Q e. A ) -> ( ( M ` X ) =/= (/) <-> X =/= ( 0. ` K ) ) )
80 79 biimpar 
 |-  ( ( ( K e. HL /\ X e. B /\ Q e. A ) /\ X =/= ( 0. ` K ) ) -> ( M ` X ) =/= (/) )
81 simp3 
 |-  ( ( K e. HL /\ X e. B /\ Q e. A ) -> Q e. A )
82 17 3 atn0 
 |-  ( ( K e. AtLat /\ Q e. A ) -> Q =/= ( 0. ` K ) )
83 16 81 82 syl2anc 
 |-  ( ( K e. HL /\ X e. B /\ Q e. A ) -> Q =/= ( 0. ` K ) )
84 1 17 4 pmapeq0 
 |-  ( ( K e. HL /\ Q e. B ) -> ( ( M ` Q ) = (/) <-> Q = ( 0. ` K ) ) )
85 6 8 84 syl2anc 
 |-  ( ( K e. HL /\ X e. B /\ Q e. A ) -> ( ( M ` Q ) = (/) <-> Q = ( 0. ` K ) ) )
86 85 necon3bid 
 |-  ( ( K e. HL /\ X e. B /\ Q e. A ) -> ( ( M ` Q ) =/= (/) <-> Q =/= ( 0. ` K ) ) )
87 83 86 mpbird 
 |-  ( ( K e. HL /\ X e. B /\ Q e. A ) -> ( M ` Q ) =/= (/) )
88 87 adantr 
 |-  ( ( ( K e. HL /\ X e. B /\ Q e. A ) /\ X =/= ( 0. ` K ) ) -> ( M ` Q ) =/= (/) )
89 40 2 3 5 elpaddn0 
 |-  ( ( ( K e. Lat /\ ( M ` X ) C_ A /\ ( M ` Q ) C_ A ) /\ ( ( M ` X ) =/= (/) /\ ( M ` Q ) =/= (/) ) ) -> ( p e. ( ( M ` X ) .+ ( M ` Q ) ) <-> ( p e. A /\ E. q e. ( M ` X ) E. r e. ( M ` Q ) p ( le ` K ) ( q .\/ r ) ) ) )
90 76 80 88 89 syl12anc 
 |-  ( ( ( K e. HL /\ X e. B /\ Q e. A ) /\ X =/= ( 0. ` K ) ) -> ( p e. ( ( M ` X ) .+ ( M ` Q ) ) <-> ( p e. A /\ E. q e. ( M ` X ) E. r e. ( M ` Q ) p ( le ` K ) ( q .\/ r ) ) ) )
91 64 72 90 3imtr4d 
 |-  ( ( ( K e. HL /\ X e. B /\ Q e. A ) /\ X =/= ( 0. ` K ) ) -> ( p e. ( M ` ( X .\/ Q ) ) -> p e. ( ( M ` X ) .+ ( M ` Q ) ) ) )
92 91 ssrdv 
 |-  ( ( ( K e. HL /\ X e. B /\ Q e. A ) /\ X =/= ( 0. ` K ) ) -> ( M ` ( X .\/ Q ) ) C_ ( ( M ` X ) .+ ( M ` Q ) ) )
93 1 2 4 5 pmapjoin 
 |-  ( ( K e. Lat /\ X e. B /\ Q e. B ) -> ( ( M ` X ) .+ ( M ` Q ) ) C_ ( M ` ( X .\/ Q ) ) )
94 66 67 8 93 syl3anc 
 |-  ( ( K e. HL /\ X e. B /\ Q e. A ) -> ( ( M ` X ) .+ ( M ` Q ) ) C_ ( M ` ( X .\/ Q ) ) )
95 94 adantr 
 |-  ( ( ( K e. HL /\ X e. B /\ Q e. A ) /\ X =/= ( 0. ` K ) ) -> ( ( M ` X ) .+ ( M ` Q ) ) C_ ( M ` ( X .\/ Q ) ) )
96 92 95 eqssd 
 |-  ( ( ( K e. HL /\ X e. B /\ Q e. A ) /\ X =/= ( 0. ` K ) ) -> ( M ` ( X .\/ Q ) ) = ( ( M ` X ) .+ ( M ` Q ) ) )
97 29 96 pm2.61dane 
 |-  ( ( K e. HL /\ X e. B /\ Q e. A ) -> ( M ` ( X .\/ Q ) ) = ( ( M ` X ) .+ ( M ` Q ) ) )