Metamath Proof Explorer

Theorem pmapocjN

Description: The projective map of the orthocomplement of the join of two lattice elements. (Contributed by NM, 14-Mar-2012) (New usage is discouraged.)

Ref Expression
Hypotheses pmapocj.b ⊢ B = Base K
pmapocj.j ⊢ ∨ ˙ = join ⁡ K
pmapocj.m ⊢ ∧ ˙ = meet ⁡ K
pmapocj.o ⊢ ⊥ ˙ = oc ⁡ K
pmapocj.f ⊢ F = pmap ⁡ K
pmapocj.p ⊢ + ˙ = + 𝑃 ⁡ K
pmapocj.r ⊢ N = ⊥ 𝑃 ⁡ K
Assertion pmapocjN ⊢ K ∈ HL ∧ X ∈ B ∧ Y ∈ B → F ⁡ ⊥ ˙ ⁡ X ∨ ˙ Y = N ⁡ F ⁡ X + ˙ F ⁡ Y

Proof

Step Hyp Ref Expression
1 pmapocj.b ⊢ B = Base K
2 pmapocj.j ⊢ ∨ ˙ = join ⁡ K
3 pmapocj.m ⊢ ∧ ˙ = meet ⁡ K
4 pmapocj.o ⊢ ⊥ ˙ = oc ⁡ K
5 pmapocj.f ⊢ F = pmap ⁡ K
6 pmapocj.p ⊢ + ˙ = + 𝑃 ⁡ K
7 pmapocj.r ⊢ N = ⊥ 𝑃 ⁡ K
8 1 2 5 6 7 pmapj2N ⊢ K ∈ HL ∧ X ∈ B ∧ Y ∈ B → F ⁡ X ∨ ˙ Y = N ⁡ N ⁡ F ⁡ X + ˙ F ⁡ Y
9 8 fveq2d ⊢ K ∈ HL ∧ X ∈ B ∧ Y ∈ B → N ⁡ F ⁡ X ∨ ˙ Y = N ⁡ N ⁡ N ⁡ F ⁡ X + ˙ F ⁡ Y
10 simp1 ⊢ K ∈ HL ∧ X ∈ B ∧ Y ∈ B → K ∈ HL
11 hllat ⊢ K ∈ HL → K ∈ Lat
12 1 2 latjcl ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B → X ∨ ˙ Y ∈ B
13 11 12 syl3an1 ⊢ K ∈ HL ∧ X ∈ B ∧ Y ∈ B → X ∨ ˙ Y ∈ B
14 1 4 5 7 polpmapN ⊢ K ∈ HL ∧ X ∨ ˙ Y ∈ B → N ⁡ F ⁡ X ∨ ˙ Y = F ⁡ ⊥ ˙ ⁡ X ∨ ˙ Y
15 10 13 14 syl2anc ⊢ K ∈ HL ∧ X ∈ B ∧ Y ∈ B → N ⁡ F ⁡ X ∨ ˙ Y = F ⁡ ⊥ ˙ ⁡ X ∨ ˙ Y
16 eqid ⊢ Atoms ⁡ K = Atoms ⁡ K
17 1 16 5 pmapssat ⊢ K ∈ HL ∧ X ∈ B → F ⁡ X ⊆ Atoms ⁡ K
18 17 3adant3 ⊢ K ∈ HL ∧ X ∈ B ∧ Y ∈ B → F ⁡ X ⊆ Atoms ⁡ K
19 1 16 5 pmapssat ⊢ K ∈ HL ∧ Y ∈ B → F ⁡ Y ⊆ Atoms ⁡ K
20 19 3adant2 ⊢ K ∈ HL ∧ X ∈ B ∧ Y ∈ B → F ⁡ Y ⊆ Atoms ⁡ K
21 16 6 paddssat ⊢ K ∈ HL ∧ F ⁡ X ⊆ Atoms ⁡ K ∧ F ⁡ Y ⊆ Atoms ⁡ K → F ⁡ X + ˙ F ⁡ Y ⊆ Atoms ⁡ K
22 10 18 20 21 syl3anc ⊢ K ∈ HL ∧ X ∈ B ∧ Y ∈ B → F ⁡ X + ˙ F ⁡ Y ⊆ Atoms ⁡ K
23 16 7 3polN ⊢ K ∈ HL ∧ F ⁡ X + ˙ F ⁡ Y ⊆ Atoms ⁡ K → N ⁡ N ⁡ N ⁡ F ⁡ X + ˙ F ⁡ Y = N ⁡ F ⁡ X + ˙ F ⁡ Y
24 10 22 23 syl2anc ⊢ K ∈ HL ∧ X ∈ B ∧ Y ∈ B → N ⁡ N ⁡ N ⁡ F ⁡ X + ˙ F ⁡ Y = N ⁡ F ⁡ X + ˙ F ⁡ Y
25 9 15 24 3eqtr3d ⊢ K ∈ HL ∧ X ∈ B ∧ Y ∈ B → F ⁡ ⊥ ˙ ⁡ X ∨ ˙ Y = N ⁡ F ⁡ X + ˙ F ⁡ Y