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