This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐵 = ( Base ‘ 𝐾 )
pmapocj.j ⊢ ∨ = ( join ‘ 𝐾 )
pmapocj.m ⊢ ∧ = ( meet ‘ 𝐾 )
pmapocj.o ⊢ ⊥ = ( oc ‘ 𝐾 )
pmapocj.f ⊢ 𝐹 = ( pmap ‘ 𝐾 )
pmapocj.p ⊢ + = ( +𝑃 ‘ 𝐾 )
pmapocj.r ⊢ 𝑁 = ( ⊥𝑃 ‘ 𝐾 )
Assertion pmapocjN ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝐹 ‘ ( ⊥ ‘ ( 𝑋 ∨ 𝑌 ) ) ) = ( 𝑁 ‘ ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑌 ) ) ) )

Proof

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