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 ∧ 𝑋𝐵𝑌𝐵 ) → ( 𝐹 ‘ ( ‘ ( 𝑋 𝑌 ) ) ) = ( 𝑁 ‘ ( ( 𝐹𝑋 ) + ( 𝐹𝑌 ) ) ) )