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 ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴 ) → ( ⊥ ‘ ( 𝑆 + 𝑇 ) ) = ( ( ⊥ ‘ 𝑆 ) ∩ ( ⊥ ‘ 𝑇 ) ) )