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 ⊢ 𝐵 = ( Base ‘ 𝐾 )
pmapj2.j ⊢ ∨ = ( join ‘ 𝐾 )
pmapj2.m ⊢ 𝑀 = ( pmap ‘ 𝐾 )
pmapj2.p ⊢ + = ( +𝑃 ‘ 𝐾 )
pmapj2.o ⊢ ⊥ = ( ⊥𝑃 ‘ 𝐾 )
Assertion pmapj2N ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑀 ‘ ( 𝑋 ∨ 𝑌 ) ) = ( ⊥ ‘ ( ⊥ ‘ ( ( 𝑀 ‘ 𝑋 ) + ( 𝑀 ‘ 𝑌 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 pmapj2.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 pmapj2.j ⊢ ∨ = ( join ‘ 𝐾 )
3 pmapj2.m ⊢ 𝑀 = ( pmap ‘ 𝐾 )
4 pmapj2.p ⊢ + = ( +𝑃 ‘ 𝐾 )
5 pmapj2.o ⊢ ⊥ = ( ⊥𝑃 ‘ 𝐾 )
6 simp1 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝐾 ∈ HL )
7 hllat ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ Lat )
8 7 3ad2ant1 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝐾 ∈ Lat )
9 hlop ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OP )
10 9 3ad2ant1 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝐾 ∈ OP )
11 simp2 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑋 ∈ 𝐵 )
12 eqid ⊢ ( oc ‘ 𝐾 ) = ( oc ‘ 𝐾 )
13 1 12 opoccl ⊢ ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ) → ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∈ 𝐵 )
14 10 11 13 syl2anc ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∈ 𝐵 )
15 simp3 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑌 ∈ 𝐵 )
16 1 12 opoccl ⊢ ( ( 𝐾 ∈ OP ∧ 𝑌 ∈ 𝐵 ) → ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ∈ 𝐵 )
17 10 15 16 syl2anc ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ∈ 𝐵 )
18 eqid ⊢ ( meet ‘ 𝐾 ) = ( meet ‘ 𝐾 )
19 1 18 latmcl ⊢ ( ( 𝐾 ∈ Lat ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∈ 𝐵 ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ∈ 𝐵 ) → ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( meet ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ∈ 𝐵 )
20 8 14 17 19 syl3anc ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( meet ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ∈ 𝐵 )
21 1 12 3 5 polpmapN ⊢ ( ( 𝐾 ∈ HL ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( meet ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ∈ 𝐵 ) → ( ⊥ ‘ ( 𝑀 ‘ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( meet ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ) ) = ( 𝑀 ‘ ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( meet ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ) ) )
22 6 20 21 syl2anc ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ⊥ ‘ ( 𝑀 ‘ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( meet ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ) ) = ( 𝑀 ‘ ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( meet ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ) ) )
23 1 12 3 5 polpmapN ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) → ( ⊥ ‘ ( 𝑀 ‘ 𝑋 ) ) = ( 𝑀 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ) )
24 23 3adant3 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ⊥ ‘ ( 𝑀 ‘ 𝑋 ) ) = ( 𝑀 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ) )
25 1 12 3 5 polpmapN ⊢ ( ( 𝐾 ∈ HL ∧ 𝑌 ∈ 𝐵 ) → ( ⊥ ‘ ( 𝑀 ‘ 𝑌 ) ) = ( 𝑀 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) )
26 25 3adant2 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ⊥ ‘ ( 𝑀 ‘ 𝑌 ) ) = ( 𝑀 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) )
27 24 26 ineq12d ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( ⊥ ‘ ( 𝑀 ‘ 𝑋 ) ) ∩ ( ⊥ ‘ ( 𝑀 ‘ 𝑌 ) ) ) = ( ( 𝑀 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ) ∩ ( 𝑀 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ) )
28 eqid ⊢ ( Atoms ‘ 𝐾 ) = ( Atoms ‘ 𝐾 )
29 1 28 3 pmapssat ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) → ( 𝑀 ‘ 𝑋 ) ⊆ ( Atoms ‘ 𝐾 ) )
30 29 3adant3 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑀 ‘ 𝑋 ) ⊆ ( Atoms ‘ 𝐾 ) )
31 1 28 3 pmapssat ⊢ ( ( 𝐾 ∈ HL ∧ 𝑌 ∈ 𝐵 ) → ( 𝑀 ‘ 𝑌 ) ⊆ ( Atoms ‘ 𝐾 ) )
32 31 3adant2 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑀 ‘ 𝑌 ) ⊆ ( Atoms ‘ 𝐾 ) )
33 28 4 5 poldmj1N ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑀 ‘ 𝑋 ) ⊆ ( Atoms ‘ 𝐾 ) ∧ ( 𝑀 ‘ 𝑌 ) ⊆ ( Atoms ‘ 𝐾 ) ) → ( ⊥ ‘ ( ( 𝑀 ‘ 𝑋 ) + ( 𝑀 ‘ 𝑌 ) ) ) = ( ( ⊥ ‘ ( 𝑀 ‘ 𝑋 ) ) ∩ ( ⊥ ‘ ( 𝑀 ‘ 𝑌 ) ) ) )
34 6 30 32 33 syl3anc ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ⊥ ‘ ( ( 𝑀 ‘ 𝑋 ) + ( 𝑀 ‘ 𝑌 ) ) ) = ( ( ⊥ ‘ ( 𝑀 ‘ 𝑋 ) ) ∩ ( ⊥ ‘ ( 𝑀 ‘ 𝑌 ) ) ) )
35 1 18 28 3 pmapmeet ⊢ ( ( 𝐾 ∈ HL ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∈ 𝐵 ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ∈ 𝐵 ) → ( 𝑀 ‘ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( meet ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ) = ( ( 𝑀 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ) ∩ ( 𝑀 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ) )
36 6 14 17 35 syl3anc ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑀 ‘ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( meet ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ) = ( ( 𝑀 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ) ∩ ( 𝑀 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ) )
37 27 34 36 3eqtr4rd ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑀 ‘ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( meet ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ) = ( ⊥ ‘ ( ( 𝑀 ‘ 𝑋 ) + ( 𝑀 ‘ 𝑌 ) ) ) )
38 37 fveq2d ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ⊥ ‘ ( 𝑀 ‘ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( meet ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ) ) = ( ⊥ ‘ ( ⊥ ‘ ( ( 𝑀 ‘ 𝑋 ) + ( 𝑀 ‘ 𝑌 ) ) ) ) )
39 hlol ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OL )
40 1 2 18 12 oldmm4 ⊢ ( ( 𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( meet ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ) = ( 𝑋 ∨ 𝑌 ) )
41 39 40 syl3an1 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( meet ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ) = ( 𝑋 ∨ 𝑌 ) )
42 41 fveq2d ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑀 ‘ ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( meet ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ) ) = ( 𝑀 ‘ ( 𝑋 ∨ 𝑌 ) ) )
43 22 38 42 3eqtr3rd ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑀 ‘ ( 𝑋 ∨ 𝑌 ) ) = ( ⊥ ‘ ( ⊥ ‘ ( ( 𝑀 ‘ 𝑋 ) + ( 𝑀 ‘ 𝑌 ) ) ) ) )