Metamath Proof Explorer


Theorem poldmj1N

Description: De Morgan's law for polarity of projective sum. ( oldmj1 analog.) (Contributed by NM, 7-Mar-2012) (New usage is discouraged.)

Ref Expression
Hypotheses paddun.a 𝐴 = ( Atoms ‘ 𝐾 )
paddun.p + = ( +𝑃𝐾 )
paddun.o = ( ⊥𝑃𝐾 )
Assertion poldmj1N ( ( 𝐾 ∈ HL ∧ 𝑆𝐴𝑇𝐴 ) → ( ‘ ( 𝑆 + 𝑇 ) ) = ( ( 𝑆 ) ∩ ( 𝑇 ) ) )

Proof

Step Hyp Ref Expression
1 paddun.a 𝐴 = ( Atoms ‘ 𝐾 )
2 paddun.p + = ( +𝑃𝐾 )
3 paddun.o = ( ⊥𝑃𝐾 )
4 1 2 3 paddunN ( ( 𝐾 ∈ HL ∧ 𝑆𝐴𝑇𝐴 ) → ( ‘ ( 𝑆 + 𝑇 ) ) = ( ‘ ( 𝑆𝑇 ) ) )
5 simp1 ( ( 𝐾 ∈ HL ∧ 𝑆𝐴𝑇𝐴 ) → 𝐾 ∈ HL )
6 unss ( ( 𝑆𝐴𝑇𝐴 ) ↔ ( 𝑆𝑇 ) ⊆ 𝐴 )
7 6 biimpi ( ( 𝑆𝐴𝑇𝐴 ) → ( 𝑆𝑇 ) ⊆ 𝐴 )
8 7 3adant1 ( ( 𝐾 ∈ HL ∧ 𝑆𝐴𝑇𝐴 ) → ( 𝑆𝑇 ) ⊆ 𝐴 )
9 eqid ( lub ‘ 𝐾 ) = ( lub ‘ 𝐾 )
10 eqid ( oc ‘ 𝐾 ) = ( oc ‘ 𝐾 )
11 eqid ( pmap ‘ 𝐾 ) = ( pmap ‘ 𝐾 )
12 9 10 1 11 3 polval2N ( ( 𝐾 ∈ HL ∧ ( 𝑆𝑇 ) ⊆ 𝐴 ) → ( ‘ ( 𝑆𝑇 ) ) = ( ( pmap ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ ( 𝑆𝑇 ) ) ) ) )
13 5 8 12 syl2anc ( ( 𝐾 ∈ HL ∧ 𝑆𝐴𝑇𝐴 ) → ( ‘ ( 𝑆𝑇 ) ) = ( ( pmap ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ ( 𝑆𝑇 ) ) ) ) )
14 hlop ( 𝐾 ∈ HL → 𝐾 ∈ OP )
15 14 3ad2ant1 ( ( 𝐾 ∈ HL ∧ 𝑆𝐴𝑇𝐴 ) → 𝐾 ∈ OP )
16 hlclat ( 𝐾 ∈ HL → 𝐾 ∈ CLat )
17 16 3ad2ant1 ( ( 𝐾 ∈ HL ∧ 𝑆𝐴𝑇𝐴 ) → 𝐾 ∈ CLat )
18 simp2 ( ( 𝐾 ∈ HL ∧ 𝑆𝐴𝑇𝐴 ) → 𝑆𝐴 )
19 eqid ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
20 19 1 atssbase 𝐴 ⊆ ( Base ‘ 𝐾 )
21 18 20 sstrdi ( ( 𝐾 ∈ HL ∧ 𝑆𝐴𝑇𝐴 ) → 𝑆 ⊆ ( Base ‘ 𝐾 ) )
22 19 9 clatlubcl ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ ( Base ‘ 𝐾 ) ) → ( ( lub ‘ 𝐾 ) ‘ 𝑆 ) ∈ ( Base ‘ 𝐾 ) )
23 17 21 22 syl2anc ( ( 𝐾 ∈ HL ∧ 𝑆𝐴𝑇𝐴 ) → ( ( lub ‘ 𝐾 ) ‘ 𝑆 ) ∈ ( Base ‘ 𝐾 ) )
24 19 10 opoccl ( ( 𝐾 ∈ OP ∧ ( ( lub ‘ 𝐾 ) ‘ 𝑆 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑆 ) ) ∈ ( Base ‘ 𝐾 ) )
25 15 23 24 syl2anc ( ( 𝐾 ∈ HL ∧ 𝑆𝐴𝑇𝐴 ) → ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑆 ) ) ∈ ( Base ‘ 𝐾 ) )
26 simp3 ( ( 𝐾 ∈ HL ∧ 𝑆𝐴𝑇𝐴 ) → 𝑇𝐴 )
27 26 20 sstrdi ( ( 𝐾 ∈ HL ∧ 𝑆𝐴𝑇𝐴 ) → 𝑇 ⊆ ( Base ‘ 𝐾 ) )
28 19 9 clatlubcl ( ( 𝐾 ∈ CLat ∧ 𝑇 ⊆ ( Base ‘ 𝐾 ) ) → ( ( lub ‘ 𝐾 ) ‘ 𝑇 ) ∈ ( Base ‘ 𝐾 ) )
29 17 27 28 syl2anc ( ( 𝐾 ∈ HL ∧ 𝑆𝐴𝑇𝐴 ) → ( ( lub ‘ 𝐾 ) ‘ 𝑇 ) ∈ ( Base ‘ 𝐾 ) )
30 19 10 opoccl ( ( 𝐾 ∈ OP ∧ ( ( lub ‘ 𝐾 ) ‘ 𝑇 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑇 ) ) ∈ ( Base ‘ 𝐾 ) )
31 15 29 30 syl2anc ( ( 𝐾 ∈ HL ∧ 𝑆𝐴𝑇𝐴 ) → ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑇 ) ) ∈ ( Base ‘ 𝐾 ) )
32 eqid ( meet ‘ 𝐾 ) = ( meet ‘ 𝐾 )
33 19 32 1 11 pmapmeet ( ( 𝐾 ∈ HL ∧ ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑆 ) ) ∈ ( Base ‘ 𝐾 ) ∧ ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑇 ) ) ∈ ( Base ‘ 𝐾 ) ) → ( ( pmap ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑆 ) ) ( meet ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑇 ) ) ) ) = ( ( ( pmap ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑆 ) ) ) ∩ ( ( pmap ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑇 ) ) ) ) )
34 5 25 31 33 syl3anc ( ( 𝐾 ∈ HL ∧ 𝑆𝐴𝑇𝐴 ) → ( ( pmap ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑆 ) ) ( meet ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑇 ) ) ) ) = ( ( ( pmap ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑆 ) ) ) ∩ ( ( pmap ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑇 ) ) ) ) )
35 eqid ( join ‘ 𝐾 ) = ( join ‘ 𝐾 )
36 19 35 9 lubun ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ ( Base ‘ 𝐾 ) ∧ 𝑇 ⊆ ( Base ‘ 𝐾 ) ) → ( ( lub ‘ 𝐾 ) ‘ ( 𝑆𝑇 ) ) = ( ( ( lub ‘ 𝐾 ) ‘ 𝑆 ) ( join ‘ 𝐾 ) ( ( lub ‘ 𝐾 ) ‘ 𝑇 ) ) )
37 17 21 27 36 syl3anc ( ( 𝐾 ∈ HL ∧ 𝑆𝐴𝑇𝐴 ) → ( ( lub ‘ 𝐾 ) ‘ ( 𝑆𝑇 ) ) = ( ( ( lub ‘ 𝐾 ) ‘ 𝑆 ) ( join ‘ 𝐾 ) ( ( lub ‘ 𝐾 ) ‘ 𝑇 ) ) )
38 37 fveq2d ( ( 𝐾 ∈ HL ∧ 𝑆𝐴𝑇𝐴 ) → ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ ( 𝑆𝑇 ) ) ) = ( ( oc ‘ 𝐾 ) ‘ ( ( ( lub ‘ 𝐾 ) ‘ 𝑆 ) ( join ‘ 𝐾 ) ( ( lub ‘ 𝐾 ) ‘ 𝑇 ) ) ) )
39 hlol ( 𝐾 ∈ HL → 𝐾 ∈ OL )
40 39 3ad2ant1 ( ( 𝐾 ∈ HL ∧ 𝑆𝐴𝑇𝐴 ) → 𝐾 ∈ OL )
41 19 35 32 10 oldmj1 ( ( 𝐾 ∈ OL ∧ ( ( lub ‘ 𝐾 ) ‘ 𝑆 ) ∈ ( Base ‘ 𝐾 ) ∧ ( ( lub ‘ 𝐾 ) ‘ 𝑇 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( oc ‘ 𝐾 ) ‘ ( ( ( lub ‘ 𝐾 ) ‘ 𝑆 ) ( join ‘ 𝐾 ) ( ( lub ‘ 𝐾 ) ‘ 𝑇 ) ) ) = ( ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑆 ) ) ( meet ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑇 ) ) ) )
42 40 23 29 41 syl3anc ( ( 𝐾 ∈ HL ∧ 𝑆𝐴𝑇𝐴 ) → ( ( oc ‘ 𝐾 ) ‘ ( ( ( lub ‘ 𝐾 ) ‘ 𝑆 ) ( join ‘ 𝐾 ) ( ( lub ‘ 𝐾 ) ‘ 𝑇 ) ) ) = ( ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑆 ) ) ( meet ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑇 ) ) ) )
43 38 42 eqtrd ( ( 𝐾 ∈ HL ∧ 𝑆𝐴𝑇𝐴 ) → ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ ( 𝑆𝑇 ) ) ) = ( ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑆 ) ) ( meet ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑇 ) ) ) )
44 43 fveq2d ( ( 𝐾 ∈ HL ∧ 𝑆𝐴𝑇𝐴 ) → ( ( pmap ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ ( 𝑆𝑇 ) ) ) ) = ( ( pmap ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑆 ) ) ( meet ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑇 ) ) ) ) )
45 9 10 1 11 3 polval2N ( ( 𝐾 ∈ HL ∧ 𝑆𝐴 ) → ( 𝑆 ) = ( ( pmap ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑆 ) ) ) )
46 45 3adant3 ( ( 𝐾 ∈ HL ∧ 𝑆𝐴𝑇𝐴 ) → ( 𝑆 ) = ( ( pmap ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑆 ) ) ) )
47 9 10 1 11 3 polval2N ( ( 𝐾 ∈ HL ∧ 𝑇𝐴 ) → ( 𝑇 ) = ( ( pmap ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑇 ) ) ) )
48 47 3adant2 ( ( 𝐾 ∈ HL ∧ 𝑆𝐴𝑇𝐴 ) → ( 𝑇 ) = ( ( pmap ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑇 ) ) ) )
49 46 48 ineq12d ( ( 𝐾 ∈ HL ∧ 𝑆𝐴𝑇𝐴 ) → ( ( 𝑆 ) ∩ ( 𝑇 ) ) = ( ( ( pmap ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑆 ) ) ) ∩ ( ( pmap ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑇 ) ) ) ) )
50 34 44 49 3eqtr4d ( ( 𝐾 ∈ HL ∧ 𝑆𝐴𝑇𝐴 ) → ( ( pmap ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ ( 𝑆𝑇 ) ) ) ) = ( ( 𝑆 ) ∩ ( 𝑇 ) ) )
51 4 13 50 3eqtrd ( ( 𝐾 ∈ HL ∧ 𝑆𝐴𝑇𝐴 ) → ( ‘ ( 𝑆 + 𝑇 ) ) = ( ( 𝑆 ) ∩ ( 𝑇 ) ) )