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