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 ⊢ A = Atoms ⁡ K
paddun.p ⊢ + ˙ = + 𝑃 ⁡ K
paddun.o ⊢ ⊥ ˙ = ⊥ 𝑃 ⁡ K
Assertion poldmj1N ⊢ K ∈ HL ∧ S ⊆ A ∧ T ⊆ A → ⊥ ˙ ⁡ S + ˙ T = ⊥ ˙ ⁡ S ∩ ⊥ ˙ ⁡ T

Proof

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