Metamath Proof Explorer

Theorem pmapjoin

Description: The projective map of the join of two lattice elements. Part of Equation 15.5.3 of MaedaMaeda p. 63. (Contributed by NM, 27-Jan-2012)

Ref Expression
Hypotheses pmapjoin.b 
|- B = ( Base ` K )
pmapjoin.j 
|- .\/ = ( join ` K )
pmapjoin.m 
|- M = ( pmap ` K )
pmapjoin.p 
|- .+ = ( +P ` K )
Assertion pmapjoin 
|- ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( ( M ` X ) .+ ( M ` Y ) ) C_ ( M ` ( X .\/ Y ) ) )

Proof

Step Hyp Ref Expression
1 pmapjoin.b 
 |-  B = ( Base ` K )
2 pmapjoin.j 
 |-  .\/ = ( join ` K )
3 pmapjoin.m 
 |-  M = ( pmap ` K )
4 pmapjoin.p 
 |-  .+ = ( +P ` K )
5 simpl 
 |-  ( ( p e. ( Atoms ` K ) /\ p ( le ` K ) X ) -> p e. ( Atoms ` K ) )
6 5 a1i 
 |-  ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( ( p e. ( Atoms ` K ) /\ p ( le ` K ) X ) -> p e. ( Atoms ` K ) ) )
7 eqid 
 |-  ( Atoms ` K ) = ( Atoms ` K )
8 1 7 atbase 
 |-  ( p e. ( Atoms ` K ) -> p e. B )
9 eqid 
 |-  ( le ` K ) = ( le ` K )
10 1 9 2 latlej1 
 |-  ( ( K e. Lat /\ X e. B /\ Y e. B ) -> X ( le ` K ) ( X .\/ Y ) )
11 10 adantr 
 |-  ( ( ( K e. Lat /\ X e. B /\ Y e. B ) /\ p e. B ) -> X ( le ` K ) ( X .\/ Y ) )
12 simpl1 
 |-  ( ( ( K e. Lat /\ X e. B /\ Y e. B ) /\ p e. B ) -> K e. Lat )
13 simpr 
 |-  ( ( ( K e. Lat /\ X e. B /\ Y e. B ) /\ p e. B ) -> p e. B )
14 simpl2 
 |-  ( ( ( K e. Lat /\ X e. B /\ Y e. B ) /\ p e. B ) -> X e. B )
15 1 2 latjcl 
 |-  ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( X .\/ Y ) e. B )
16 15 adantr 
 |-  ( ( ( K e. Lat /\ X e. B /\ Y e. B ) /\ p e. B ) -> ( X .\/ Y ) e. B )
17 1 9 lattr 
 |-  ( ( K e. Lat /\ ( p e. B /\ X e. B /\ ( X .\/ Y ) e. B ) ) -> ( ( p ( le ` K ) X /\ X ( le ` K ) ( X .\/ Y ) ) -> p ( le ` K ) ( X .\/ Y ) ) )
18 12 13 14 16 17 syl13anc 
 |-  ( ( ( K e. Lat /\ X e. B /\ Y e. B ) /\ p e. B ) -> ( ( p ( le ` K ) X /\ X ( le ` K ) ( X .\/ Y ) ) -> p ( le ` K ) ( X .\/ Y ) ) )
19 11 18 mpan2d 
 |-  ( ( ( K e. Lat /\ X e. B /\ Y e. B ) /\ p e. B ) -> ( p ( le ` K ) X -> p ( le ` K ) ( X .\/ Y ) ) )
20 19 expimpd 
 |-  ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( ( p e. B /\ p ( le ` K ) X ) -> p ( le ` K ) ( X .\/ Y ) ) )
21 8 20 sylani 
 |-  ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( ( p e. ( Atoms ` K ) /\ p ( le ` K ) X ) -> p ( le ` K ) ( X .\/ Y ) ) )
22 6 21 jcad 
 |-  ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( ( p e. ( Atoms ` K ) /\ p ( le ` K ) X ) -> ( p e. ( Atoms ` K ) /\ p ( le ` K ) ( X .\/ Y ) ) ) )
23 simpl 
 |-  ( ( p e. ( Atoms ` K ) /\ p ( le ` K ) Y ) -> p e. ( Atoms ` K ) )
24 23 a1i 
 |-  ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( ( p e. ( Atoms ` K ) /\ p ( le ` K ) Y ) -> p e. ( Atoms ` K ) ) )
25 1 9 2 latlej2 
 |-  ( ( K e. Lat /\ X e. B /\ Y e. B ) -> Y ( le ` K ) ( X .\/ Y ) )
26 25 adantr 
 |-  ( ( ( K e. Lat /\ X e. B /\ Y e. B ) /\ p e. B ) -> Y ( le ` K ) ( X .\/ Y ) )
27 simpl3 
 |-  ( ( ( K e. Lat /\ X e. B /\ Y e. B ) /\ p e. B ) -> Y e. B )
28 1 9 lattr 
 |-  ( ( K e. Lat /\ ( p e. B /\ Y e. B /\ ( X .\/ Y ) e. B ) ) -> ( ( p ( le ` K ) Y /\ Y ( le ` K ) ( X .\/ Y ) ) -> p ( le ` K ) ( X .\/ Y ) ) )
29 12 13 27 16 28 syl13anc 
 |-  ( ( ( K e. Lat /\ X e. B /\ Y e. B ) /\ p e. B ) -> ( ( p ( le ` K ) Y /\ Y ( le ` K ) ( X .\/ Y ) ) -> p ( le ` K ) ( X .\/ Y ) ) )
30 26 29 mpan2d 
 |-  ( ( ( K e. Lat /\ X e. B /\ Y e. B ) /\ p e. B ) -> ( p ( le ` K ) Y -> p ( le ` K ) ( X .\/ Y ) ) )
31 30 expimpd 
 |-  ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( ( p e. B /\ p ( le ` K ) Y ) -> p ( le ` K ) ( X .\/ Y ) ) )
32 8 31 sylani 
 |-  ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( ( p e. ( Atoms ` K ) /\ p ( le ` K ) Y ) -> p ( le ` K ) ( X .\/ Y ) ) )
33 24 32 jcad 
 |-  ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( ( p e. ( Atoms ` K ) /\ p ( le ` K ) Y ) -> ( p e. ( Atoms ` K ) /\ p ( le ` K ) ( X .\/ Y ) ) ) )
34 22 33 jaod 
 |-  ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( ( ( p e. ( Atoms ` K ) /\ p ( le ` K ) X ) \/ ( p e. ( Atoms ` K ) /\ p ( le ` K ) Y ) ) -> ( p e. ( Atoms ` K ) /\ p ( le ` K ) ( X .\/ Y ) ) ) )
35 simpl 
 |-  ( ( p e. ( Atoms ` K ) /\ E. q e. ( M ` X ) E. r e. ( M ` Y ) p ( le ` K ) ( q .\/ r ) ) -> p e. ( Atoms ` K ) )
36 35 a1i 
 |-  ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( ( p e. ( Atoms ` K ) /\ E. q e. ( M ` X ) E. r e. ( M ` Y ) p ( le ` K ) ( q .\/ r ) ) -> p e. ( Atoms ` K ) ) )
37 1 9 7 3 elpmap 
 |-  ( ( K e. Lat /\ X e. B ) -> ( q e. ( M ` X ) <-> ( q e. ( Atoms ` K ) /\ q ( le ` K ) X ) ) )
38 37 3adant3 
 |-  ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( q e. ( M ` X ) <-> ( q e. ( Atoms ` K ) /\ q ( le ` K ) X ) ) )
39 1 9 7 3 elpmap 
 |-  ( ( K e. Lat /\ Y e. B ) -> ( r e. ( M ` Y ) <-> ( r e. ( Atoms ` K ) /\ r ( le ` K ) Y ) ) )
40 39 3adant2 
 |-  ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( r e. ( M ` Y ) <-> ( r e. ( Atoms ` K ) /\ r ( le ` K ) Y ) ) )
41 38 40 anbi12d 
 |-  ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( ( q e. ( M ` X ) /\ r e. ( M ` Y ) ) <-> ( ( q e. ( Atoms ` K ) /\ q ( le ` K ) X ) /\ ( r e. ( Atoms ` K ) /\ r ( le ` K ) Y ) ) ) )
42 an4 
 |-  ( ( ( q e. ( Atoms ` K ) /\ q ( le ` K ) X ) /\ ( r e. ( Atoms ` K ) /\ r ( le ` K ) Y ) ) <-> ( ( q e. ( Atoms ` K ) /\ r e. ( Atoms ` K ) ) /\ ( q ( le ` K ) X /\ r ( le ` K ) Y ) ) )
43 41 42 bitrdi 
 |-  ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( ( q e. ( M ` X ) /\ r e. ( M ` Y ) ) <-> ( ( q e. ( Atoms ` K ) /\ r e. ( Atoms ` K ) ) /\ ( q ( le ` K ) X /\ r ( le ` K ) Y ) ) ) )
44 43 adantr 
 |-  ( ( ( K e. Lat /\ X e. B /\ Y e. B ) /\ p e. B ) -> ( ( q e. ( M ` X ) /\ r e. ( M ` Y ) ) <-> ( ( q e. ( Atoms ` K ) /\ r e. ( Atoms ` K ) ) /\ ( q ( le ` K ) X /\ r ( le ` K ) Y ) ) ) )
45 1 7 atbase 
 |-  ( q e. ( Atoms ` K ) -> q e. B )
46 1 7 atbase 
 |-  ( r e. ( Atoms ` K ) -> r e. B )
47 45 46 anim12i 
 |-  ( ( q e. ( Atoms ` K ) /\ r e. ( Atoms ` K ) ) -> ( q e. B /\ r e. B ) )
48 simpll1 
 |-  ( ( ( ( K e. Lat /\ X e. B /\ Y e. B ) /\ p e. B ) /\ ( q e. B /\ r e. B ) ) -> K e. Lat )
49 simprl 
 |-  ( ( ( ( K e. Lat /\ X e. B /\ Y e. B ) /\ p e. B ) /\ ( q e. B /\ r e. B ) ) -> q e. B )
50 simpll2 
 |-  ( ( ( ( K e. Lat /\ X e. B /\ Y e. B ) /\ p e. B ) /\ ( q e. B /\ r e. B ) ) -> X e. B )
51 simprr 
 |-  ( ( ( ( K e. Lat /\ X e. B /\ Y e. B ) /\ p e. B ) /\ ( q e. B /\ r e. B ) ) -> r e. B )
52 simpll3 
 |-  ( ( ( ( K e. Lat /\ X e. B /\ Y e. B ) /\ p e. B ) /\ ( q e. B /\ r e. B ) ) -> Y e. B )
53 1 9 2 latjlej12 
 |-  ( ( K e. Lat /\ ( q e. B /\ X e. B ) /\ ( r e. B /\ Y e. B ) ) -> ( ( q ( le ` K ) X /\ r ( le ` K ) Y ) -> ( q .\/ r ) ( le ` K ) ( X .\/ Y ) ) )
54 48 49 50 51 52 53 syl122anc 
 |-  ( ( ( ( K e. Lat /\ X e. B /\ Y e. B ) /\ p e. B ) /\ ( q e. B /\ r e. B ) ) -> ( ( q ( le ` K ) X /\ r ( le ` K ) Y ) -> ( q .\/ r ) ( le ` K ) ( X .\/ Y ) ) )
55 simplr 
 |-  ( ( ( ( K e. Lat /\ X e. B /\ Y e. B ) /\ p e. B ) /\ ( q e. B /\ r e. B ) ) -> p e. B )
56 1 2 latjcl 
 |-  ( ( K e. Lat /\ q e. B /\ r e. B ) -> ( q .\/ r ) e. B )
57 48 49 51 56 syl3anc 
 |-  ( ( ( ( K e. Lat /\ X e. B /\ Y e. B ) /\ p e. B ) /\ ( q e. B /\ r e. B ) ) -> ( q .\/ r ) e. B )
58 15 ad2antrr 
 |-  ( ( ( ( K e. Lat /\ X e. B /\ Y e. B ) /\ p e. B ) /\ ( q e. B /\ r e. B ) ) -> ( X .\/ Y ) e. B )
59 1 9 lattr 
 |-  ( ( K e. Lat /\ ( p e. B /\ ( q .\/ r ) e. B /\ ( X .\/ Y ) e. B ) ) -> ( ( p ( le ` K ) ( q .\/ r ) /\ ( q .\/ r ) ( le ` K ) ( X .\/ Y ) ) -> p ( le ` K ) ( X .\/ Y ) ) )
60 48 55 57 58 59 syl13anc 
 |-  ( ( ( ( K e. Lat /\ X e. B /\ Y e. B ) /\ p e. B ) /\ ( q e. B /\ r e. B ) ) -> ( ( p ( le ` K ) ( q .\/ r ) /\ ( q .\/ r ) ( le ` K ) ( X .\/ Y ) ) -> p ( le ` K ) ( X .\/ Y ) ) )
61 60 expcomd 
 |-  ( ( ( ( K e. Lat /\ X e. B /\ Y e. B ) /\ p e. B ) /\ ( q e. B /\ r e. B ) ) -> ( ( q .\/ r ) ( le ` K ) ( X .\/ Y ) -> ( p ( le ` K ) ( q .\/ r ) -> p ( le ` K ) ( X .\/ Y ) ) ) )
62 54 61 syld 
 |-  ( ( ( ( K e. Lat /\ X e. B /\ Y e. B ) /\ p e. B ) /\ ( q e. B /\ r e. B ) ) -> ( ( q ( le ` K ) X /\ r ( le ` K ) Y ) -> ( p ( le ` K ) ( q .\/ r ) -> p ( le ` K ) ( X .\/ Y ) ) ) )
63 62 expimpd 
 |-  ( ( ( K e. Lat /\ X e. B /\ Y e. B ) /\ p e. B ) -> ( ( ( q e. B /\ r e. B ) /\ ( q ( le ` K ) X /\ r ( le ` K ) Y ) ) -> ( p ( le ` K ) ( q .\/ r ) -> p ( le ` K ) ( X .\/ Y ) ) ) )
64 47 63 sylani 
 |-  ( ( ( K e. Lat /\ X e. B /\ Y e. B ) /\ p e. B ) -> ( ( ( q e. ( Atoms ` K ) /\ r e. ( Atoms ` K ) ) /\ ( q ( le ` K ) X /\ r ( le ` K ) Y ) ) -> ( p ( le ` K ) ( q .\/ r ) -> p ( le ` K ) ( X .\/ Y ) ) ) )
65 44 64 sylbid 
 |-  ( ( ( K e. Lat /\ X e. B /\ Y e. B ) /\ p e. B ) -> ( ( q e. ( M ` X ) /\ r e. ( M ` Y ) ) -> ( p ( le ` K ) ( q .\/ r ) -> p ( le ` K ) ( X .\/ Y ) ) ) )
66 65 rexlimdvv 
 |-  ( ( ( K e. Lat /\ X e. B /\ Y e. B ) /\ p e. B ) -> ( E. q e. ( M ` X ) E. r e. ( M ` Y ) p ( le ` K ) ( q .\/ r ) -> p ( le ` K ) ( X .\/ Y ) ) )
67 66 expimpd 
 |-  ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( ( p e. B /\ E. q e. ( M ` X ) E. r e. ( M ` Y ) p ( le ` K ) ( q .\/ r ) ) -> p ( le ` K ) ( X .\/ Y ) ) )
68 8 67 sylani 
 |-  ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( ( p e. ( Atoms ` K ) /\ E. q e. ( M ` X ) E. r e. ( M ` Y ) p ( le ` K ) ( q .\/ r ) ) -> p ( le ` K ) ( X .\/ Y ) ) )
69 36 68 jcad 
 |-  ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( ( p e. ( Atoms ` K ) /\ E. q e. ( M ` X ) E. r e. ( M ` Y ) p ( le ` K ) ( q .\/ r ) ) -> ( p e. ( Atoms ` K ) /\ p ( le ` K ) ( X .\/ Y ) ) ) )
70 34 69 jaod 
 |-  ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( ( ( ( p e. ( Atoms ` K ) /\ p ( le ` K ) X ) \/ ( p e. ( Atoms ` K ) /\ p ( le ` K ) Y ) ) \/ ( p e. ( Atoms ` K ) /\ E. q e. ( M ` X ) E. r e. ( M ` Y ) p ( le ` K ) ( q .\/ r ) ) ) -> ( p e. ( Atoms ` K ) /\ p ( le ` K ) ( X .\/ Y ) ) ) )
71 simp1 
 |-  ( ( K e. Lat /\ X e. B /\ Y e. B ) -> K e. Lat )
72 1 7 3 pmapssat 
 |-  ( ( K e. Lat /\ X e. B ) -> ( M ` X ) C_ ( Atoms ` K ) )
73 72 3adant3 
 |-  ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( M ` X ) C_ ( Atoms ` K ) )
74 1 7 3 pmapssat 
 |-  ( ( K e. Lat /\ Y e. B ) -> ( M ` Y ) C_ ( Atoms ` K ) )
75 74 3adant2 
 |-  ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( M ` Y ) C_ ( Atoms ` K ) )
76 9 2 7 4 elpadd 
 |-  ( ( K e. Lat /\ ( M ` X ) C_ ( Atoms ` K ) /\ ( M ` Y ) C_ ( Atoms ` K ) ) -> ( p e. ( ( M ` X ) .+ ( M ` Y ) ) <-> ( ( p e. ( M ` X ) \/ p e. ( M ` Y ) ) \/ ( p e. ( Atoms ` K ) /\ E. q e. ( M ` X ) E. r e. ( M ` Y ) p ( le ` K ) ( q .\/ r ) ) ) ) )
77 71 73 75 76 syl3anc 
 |-  ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( p e. ( ( M ` X ) .+ ( M ` Y ) ) <-> ( ( p e. ( M ` X ) \/ p e. ( M ` Y ) ) \/ ( p e. ( Atoms ` K ) /\ E. q e. ( M ` X ) E. r e. ( M ` Y ) p ( le ` K ) ( q .\/ r ) ) ) ) )
78 1 9 7 3 elpmap 
 |-  ( ( K e. Lat /\ X e. B ) -> ( p e. ( M ` X ) <-> ( p e. ( Atoms ` K ) /\ p ( le ` K ) X ) ) )
79 78 3adant3 
 |-  ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( p e. ( M ` X ) <-> ( p e. ( Atoms ` K ) /\ p ( le ` K ) X ) ) )
80 1 9 7 3 elpmap 
 |-  ( ( K e. Lat /\ Y e. B ) -> ( p e. ( M ` Y ) <-> ( p e. ( Atoms ` K ) /\ p ( le ` K ) Y ) ) )
81 80 3adant2 
 |-  ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( p e. ( M ` Y ) <-> ( p e. ( Atoms ` K ) /\ p ( le ` K ) Y ) ) )
82 79 81 orbi12d 
 |-  ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( ( p e. ( M ` X ) \/ p e. ( M ` Y ) ) <-> ( ( p e. ( Atoms ` K ) /\ p ( le ` K ) X ) \/ ( p e. ( Atoms ` K ) /\ p ( le ` K ) Y ) ) ) )
83 82 orbi1d 
 |-  ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( ( ( p e. ( M ` X ) \/ p e. ( M ` Y ) ) \/ ( p e. ( Atoms ` K ) /\ E. q e. ( M ` X ) E. r e. ( M ` Y ) p ( le ` K ) ( q .\/ r ) ) ) <-> ( ( ( p e. ( Atoms ` K ) /\ p ( le ` K ) X ) \/ ( p e. ( Atoms ` K ) /\ p ( le ` K ) Y ) ) \/ ( p e. ( Atoms ` K ) /\ E. q e. ( M ` X ) E. r e. ( M ` Y ) p ( le ` K ) ( q .\/ r ) ) ) ) )
84 77 83 bitrd 
 |-  ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( p e. ( ( M ` X ) .+ ( M ` Y ) ) <-> ( ( ( p e. ( Atoms ` K ) /\ p ( le ` K ) X ) \/ ( p e. ( Atoms ` K ) /\ p ( le ` K ) Y ) ) \/ ( p e. ( Atoms ` K ) /\ E. q e. ( M ` X ) E. r e. ( M ` Y ) p ( le ` K ) ( q .\/ r ) ) ) ) )
85 1 9 7 3 elpmap 
 |-  ( ( K e. Lat /\ ( X .\/ Y ) e. B ) -> ( p e. ( M ` ( X .\/ Y ) ) <-> ( p e. ( Atoms ` K ) /\ p ( le ` K ) ( X .\/ Y ) ) ) )
86 71 15 85 syl2anc 
 |-  ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( p e. ( M ` ( X .\/ Y ) ) <-> ( p e. ( Atoms ` K ) /\ p ( le ` K ) ( X .\/ Y ) ) ) )
87 70 84 86 3imtr4d 
 |-  ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( p e. ( ( M ` X ) .+ ( M ` Y ) ) -> p e. ( M ` ( X .\/ Y ) ) ) )
88 87 ssrdv 
 |-  ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( ( M ` X ) .+ ( M ` Y ) ) C_ ( M ` ( X .\/ Y ) ) )