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 + ˙ = + 𝑃 K
pmapj2.o ˙ = 𝑃 K
Assertion pmapj2N K HL X B Y 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 + ˙ = + 𝑃 K
5 pmapj2.o ˙ = 𝑃 K
6 simp1 K HL X B Y B K HL
7 hllat K HL K Lat
8 7 3ad2ant1 K HL X B Y B K Lat
9 hlop K HL K OP
10 9 3ad2ant1 K HL X B Y B K OP
11 simp2 K HL X B Y B X B
12 eqid oc K = oc K
13 1 12 opoccl K OP X B oc K X B
14 10 11 13 syl2anc K HL X B Y B oc K X B
15 simp3 K HL X B Y B Y B
16 1 12 opoccl K OP Y B oc K Y B
17 10 15 16 syl2anc K HL X B Y B oc K Y B
18 eqid meet K = meet K
19 1 18 latmcl K Lat oc K X B oc K Y B oc K X meet K oc K Y B
20 8 14 17 19 syl3anc K HL X B Y B oc K X meet K oc K Y B
21 1 12 3 5 polpmapN K HL oc K X meet K oc K Y 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 HL X B Y 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 HL X B ˙ M X = M oc K X
24 23 3adant3 K HL X B Y B ˙ M X = M oc K X
25 1 12 3 5 polpmapN K HL Y B ˙ M Y = M oc K Y
26 25 3adant2 K HL X B Y B ˙ M Y = M oc K Y
27 24 26 ineq12d K HL X B Y B ˙ M X ˙ M Y = M oc K X M oc K Y
28 eqid Atoms K = Atoms K
29 1 28 3 pmapssat K HL X B M X Atoms K
30 29 3adant3 K HL X B Y B M X Atoms K
31 1 28 3 pmapssat K HL Y B M Y Atoms K
32 31 3adant2 K HL X B Y B M Y Atoms K
33 28 4 5 poldmj1N K HL M X Atoms K M Y Atoms K ˙ M X + ˙ M Y = ˙ M X ˙ M Y
34 6 30 32 33 syl3anc K HL X B Y B ˙ M X + ˙ M Y = ˙ M X ˙ M Y
35 1 18 28 3 pmapmeet K HL oc K X B oc K Y B M oc K X meet K oc K Y = M oc K X M oc K Y
36 6 14 17 35 syl3anc K HL X B Y B M oc K X meet K oc K Y = M oc K X M oc K Y
37 27 34 36 3eqtr4rd K HL X B Y B M oc K X meet K oc K Y = ˙ M X + ˙ M Y
38 37 fveq2d K HL X B Y B ˙ M oc K X meet K oc K Y = ˙ ˙ M X + ˙ M Y
39 hlol K HL K OL
40 1 2 18 12 oldmm4 K OL X B Y B oc K oc K X meet K oc K Y = X ˙ Y
41 39 40 syl3an1 K HL X B Y B oc K oc K X meet K oc K Y = X ˙ Y
42 41 fveq2d K HL X B Y B M oc K oc K X meet K oc K Y = M X ˙ Y
43 22 38 42 3eqtr3rd K HL X B Y B M X ˙ Y = ˙ ˙ M X + ˙ M Y