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