Metamath Proof Explorer

Theorem paddunN

Description: The closure of the projective sum of two sets of atoms is the same as the closure of their union. (Closure is actually double polarity, which can be trivially inferred from this theorem using fveq2d .) (Contributed by NM, 6-Mar-2012) (New usage is discouraged.)

Ref Expression
Hypotheses paddun.a 
|- A = ( Atoms ` K )
paddun.p 
|- .+ = ( +P ` K )
paddun.o 
|- ._|_ = ( _|_P ` K )
Assertion paddunN 
|- ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( ._|_ ` ( S .+ T ) ) = ( ._|_ ` ( S u. T ) ) )

Proof

Step Hyp Ref Expression
1 paddun.a 
 |-  A = ( Atoms ` K )
2 paddun.p 
 |-  .+ = ( +P ` K )
3 paddun.o 
 |-  ._|_ = ( _|_P ` K )
4 simp1 
 |-  ( ( K e. HL /\ S C_ A /\ T C_ A ) -> K e. HL )
5 1 2 paddssat 
 |-  ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( S .+ T ) C_ A )
6 1 2 paddunssN 
 |-  ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( S u. T ) C_ ( S .+ T ) )
7 1 3 polcon3N 
 |-  ( ( K e. HL /\ ( S .+ T ) C_ A /\ ( S u. T ) C_ ( S .+ T ) ) -> ( ._|_ ` ( S .+ T ) ) C_ ( ._|_ ` ( S u. T ) ) )
8 4 5 6 7 syl3anc 
 |-  ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( ._|_ ` ( S .+ T ) ) C_ ( ._|_ ` ( S u. T ) ) )
9 hlclat 
 |-  ( K e. HL -> K e. CLat )
10 9 3ad2ant1 
 |-  ( ( K e. HL /\ S C_ A /\ T C_ A ) -> K e. CLat )
11 unss 
 |-  ( ( S C_ A /\ T C_ A ) <-> ( S u. T ) C_ A )
12 11 biimpi 
 |-  ( ( S C_ A /\ T C_ A ) -> ( S u. T ) C_ A )
13 12 3adant1 
 |-  ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( S u. T ) C_ A )
14 eqid 
 |-  ( Base ` K ) = ( Base ` K )
15 14 1 atssbase 
 |-  A C_ ( Base ` K )
16 13 15 sstrdi 
 |-  ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( S u. T ) C_ ( Base ` K ) )
17 eqid 
 |-  ( lub ` K ) = ( lub ` K )
18 14 17 clatlubcl 
 |-  ( ( K e. CLat /\ ( S u. T ) C_ ( Base ` K ) ) -> ( ( lub ` K ) ` ( S u. T ) ) e. ( Base ` K ) )
19 10 16 18 syl2anc 
 |-  ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( ( lub ` K ) ` ( S u. T ) ) e. ( Base ` K ) )
20 eqid 
 |-  ( pmap ` K ) = ( pmap ` K )
21 14 20 pmapssbaN 
 |-  ( ( K e. HL /\ ( ( lub ` K ) ` ( S u. T ) ) e. ( Base ` K ) ) -> ( ( pmap ` K ) ` ( ( lub ` K ) ` ( S u. T ) ) ) C_ ( Base ` K ) )
22 4 19 21 syl2anc 
 |-  ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( ( pmap ` K ) ` ( ( lub ` K ) ` ( S u. T ) ) ) C_ ( Base ` K ) )
23 1 3 polssatN 
 |-  ( ( K e. HL /\ S C_ A ) -> ( ._|_ ` S ) C_ A )
24 23 3adant3 
 |-  ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( ._|_ ` S ) C_ A )
25 1 3 polssatN 
 |-  ( ( K e. HL /\ ( ._|_ ` S ) C_ A ) -> ( ._|_ ` ( ._|_ ` S ) ) C_ A )
26 4 24 25 syl2anc 
 |-  ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( ._|_ ` ( ._|_ ` S ) ) C_ A )
27 1 3 polssatN 
 |-  ( ( K e. HL /\ T C_ A ) -> ( ._|_ ` T ) C_ A )
28 27 3adant2 
 |-  ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( ._|_ ` T ) C_ A )
29 1 3 polssatN 
 |-  ( ( K e. HL /\ ( ._|_ ` T ) C_ A ) -> ( ._|_ ` ( ._|_ ` T ) ) C_ A )
30 4 28 29 syl2anc 
 |-  ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( ._|_ ` ( ._|_ ` T ) ) C_ A )
31 4 26 30 3jca 
 |-  ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( K e. HL /\ ( ._|_ ` ( ._|_ ` S ) ) C_ A /\ ( ._|_ ` ( ._|_ ` T ) ) C_ A ) )
32 1 3 2polssN 
 |-  ( ( K e. HL /\ S C_ A ) -> S C_ ( ._|_ ` ( ._|_ ` S ) ) )
33 32 3adant3 
 |-  ( ( K e. HL /\ S C_ A /\ T C_ A ) -> S C_ ( ._|_ ` ( ._|_ ` S ) ) )
34 1 3 2polssN 
 |-  ( ( K e. HL /\ T C_ A ) -> T C_ ( ._|_ ` ( ._|_ ` T ) ) )
35 34 3adant2 
 |-  ( ( K e. HL /\ S C_ A /\ T C_ A ) -> T C_ ( ._|_ ` ( ._|_ ` T ) ) )
36 33 35 jca 
 |-  ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( S C_ ( ._|_ ` ( ._|_ ` S ) ) /\ T C_ ( ._|_ ` ( ._|_ ` T ) ) ) )
37 1 2 paddss12 
 |-  ( ( K e. HL /\ ( ._|_ ` ( ._|_ ` S ) ) C_ A /\ ( ._|_ ` ( ._|_ ` T ) ) C_ A ) -> ( ( S C_ ( ._|_ ` ( ._|_ ` S ) ) /\ T C_ ( ._|_ ` ( ._|_ ` T ) ) ) -> ( S .+ T ) C_ ( ( ._|_ ` ( ._|_ ` S ) ) .+ ( ._|_ ` ( ._|_ ` T ) ) ) ) )
38 31 36 37 sylc 
 |-  ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( S .+ T ) C_ ( ( ._|_ ` ( ._|_ ` S ) ) .+ ( ._|_ ` ( ._|_ ` T ) ) ) )
39 17 1 20 3 2polvalN 
 |-  ( ( K e. HL /\ S C_ A ) -> ( ._|_ ` ( ._|_ ` S ) ) = ( ( pmap ` K ) ` ( ( lub ` K ) ` S ) ) )
40 39 3adant3 
 |-  ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( ._|_ ` ( ._|_ ` S ) ) = ( ( pmap ` K ) ` ( ( lub ` K ) ` S ) ) )
41 17 1 20 3 2polvalN 
 |-  ( ( K e. HL /\ T C_ A ) -> ( ._|_ ` ( ._|_ ` T ) ) = ( ( pmap ` K ) ` ( ( lub ` K ) ` T ) ) )
42 41 3adant2 
 |-  ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( ._|_ ` ( ._|_ ` T ) ) = ( ( pmap ` K ) ` ( ( lub ` K ) ` T ) ) )
43 40 42 oveq12d 
 |-  ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( ( ._|_ ` ( ._|_ ` S ) ) .+ ( ._|_ ` ( ._|_ ` T ) ) ) = ( ( ( pmap ` K ) ` ( ( lub ` K ) ` S ) ) .+ ( ( pmap ` K ) ` ( ( lub ` K ) ` T ) ) ) )
44 38 43 sseqtrd 
 |-  ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( S .+ T ) C_ ( ( ( pmap ` K ) ` ( ( lub ` K ) ` S ) ) .+ ( ( pmap ` K ) ` ( ( lub ` K ) ` T ) ) ) )
45 hllat 
 |-  ( K e. HL -> K e. Lat )
46 45 3ad2ant1 
 |-  ( ( K e. HL /\ S C_ A /\ T C_ A ) -> K e. Lat )
47 simp2 
 |-  ( ( K e. HL /\ S C_ A /\ T C_ A ) -> S C_ A )
48 47 15 sstrdi 
 |-  ( ( K e. HL /\ S C_ A /\ T C_ A ) -> S C_ ( Base ` K ) )
49 14 17 clatlubcl 
 |-  ( ( K e. CLat /\ S C_ ( Base ` K ) ) -> ( ( lub ` K ) ` S ) e. ( Base ` K ) )
50 10 48 49 syl2anc 
 |-  ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( ( lub ` K ) ` S ) e. ( Base ` K ) )
51 simp3 
 |-  ( ( K e. HL /\ S C_ A /\ T C_ A ) -> T C_ A )
52 51 15 sstrdi 
 |-  ( ( K e. HL /\ S C_ A /\ T C_ A ) -> T C_ ( Base ` K ) )
53 14 17 clatlubcl 
 |-  ( ( K e. CLat /\ T C_ ( Base ` K ) ) -> ( ( lub ` K ) ` T ) e. ( Base ` K ) )
54 10 52 53 syl2anc 
 |-  ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( ( lub ` K ) ` T ) e. ( Base ` K ) )
55 eqid 
 |-  ( join ` K ) = ( join ` K )
56 14 55 20 2 pmapjoin 
 |-  ( ( K e. Lat /\ ( ( lub ` K ) ` S ) e. ( Base ` K ) /\ ( ( lub ` K ) ` T ) e. ( Base ` K ) ) -> ( ( ( pmap ` K ) ` ( ( lub ` K ) ` S ) ) .+ ( ( pmap ` K ) ` ( ( lub ` K ) ` T ) ) ) C_ ( ( pmap ` K ) ` ( ( ( lub ` K ) ` S ) ( join ` K ) ( ( lub ` K ) ` T ) ) ) )
57 46 50 54 56 syl3anc 
 |-  ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( ( ( pmap ` K ) ` ( ( lub ` K ) ` S ) ) .+ ( ( pmap ` K ) ` ( ( lub ` K ) ` T ) ) ) C_ ( ( pmap ` K ) ` ( ( ( lub ` K ) ` S ) ( join ` K ) ( ( lub ` K ) ` T ) ) ) )
58 44 57 sstrd 
 |-  ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( S .+ T ) C_ ( ( pmap ` K ) ` ( ( ( lub ` K ) ` S ) ( join ` K ) ( ( lub ` K ) ` T ) ) ) )
59 14 55 17 lubun 
 |-  ( ( K e. CLat /\ S C_ ( Base ` K ) /\ T C_ ( Base ` K ) ) -> ( ( lub ` K ) ` ( S u. T ) ) = ( ( ( lub ` K ) ` S ) ( join ` K ) ( ( lub ` K ) ` T ) ) )
60 10 48 52 59 syl3anc 
 |-  ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( ( lub ` K ) ` ( S u. T ) ) = ( ( ( lub ` K ) ` S ) ( join ` K ) ( ( lub ` K ) ` T ) ) )
61 60 fveq2d 
 |-  ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( ( pmap ` K ) ` ( ( lub ` K ) ` ( S u. T ) ) ) = ( ( pmap ` K ) ` ( ( ( lub ` K ) ` S ) ( join ` K ) ( ( lub ` K ) ` T ) ) ) )
62 58 61 sseqtrrd 
 |-  ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( S .+ T ) C_ ( ( pmap ` K ) ` ( ( lub ` K ) ` ( S u. T ) ) ) )
63 eqid 
 |-  ( le ` K ) = ( le ` K )
64 14 63 17 lubss 
 |-  ( ( K e. CLat /\ ( ( pmap ` K ) ` ( ( lub ` K ) ` ( S u. T ) ) ) C_ ( Base ` K ) /\ ( S .+ T ) C_ ( ( pmap ` K ) ` ( ( lub ` K ) ` ( S u. T ) ) ) ) -> ( ( lub ` K ) ` ( S .+ T ) ) ( le ` K ) ( ( lub ` K ) ` ( ( pmap ` K ) ` ( ( lub ` K ) ` ( S u. T ) ) ) ) )
65 10 22 62 64 syl3anc 
 |-  ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( ( lub ` K ) ` ( S .+ T ) ) ( le ` K ) ( ( lub ` K ) ` ( ( pmap ` K ) ` ( ( lub ` K ) ` ( S u. T ) ) ) ) )
66 5 15 sstrdi 
 |-  ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( S .+ T ) C_ ( Base ` K ) )
67 14 17 clatlubcl 
 |-  ( ( K e. CLat /\ ( S .+ T ) C_ ( Base ` K ) ) -> ( ( lub ` K ) ` ( S .+ T ) ) e. ( Base ` K ) )
68 10 66 67 syl2anc 
 |-  ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( ( lub ` K ) ` ( S .+ T ) ) e. ( Base ` K ) )
69 14 17 clatlubcl 
 |-  ( ( K e. CLat /\ ( ( pmap ` K ) ` ( ( lub ` K ) ` ( S u. T ) ) ) C_ ( Base ` K ) ) -> ( ( lub ` K ) ` ( ( pmap ` K ) ` ( ( lub ` K ) ` ( S u. T ) ) ) ) e. ( Base ` K ) )
70 10 22 69 syl2anc 
 |-  ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( ( lub ` K ) ` ( ( pmap ` K ) ` ( ( lub ` K ) ` ( S u. T ) ) ) ) e. ( Base ` K ) )
71 14 63 20 pmaple 
 |-  ( ( K e. HL /\ ( ( lub ` K ) ` ( S .+ T ) ) e. ( Base ` K ) /\ ( ( lub ` K ) ` ( ( pmap ` K ) ` ( ( lub ` K ) ` ( S u. T ) ) ) ) e. ( Base ` K ) ) -> ( ( ( lub ` K ) ` ( S .+ T ) ) ( le ` K ) ( ( lub ` K ) ` ( ( pmap ` K ) ` ( ( lub ` K ) ` ( S u. T ) ) ) ) <-> ( ( pmap ` K ) ` ( ( lub ` K ) ` ( S .+ T ) ) ) C_ ( ( pmap ` K ) ` ( ( lub ` K ) ` ( ( pmap ` K ) ` ( ( lub ` K ) ` ( S u. T ) ) ) ) ) ) )
72 4 68 70 71 syl3anc 
 |-  ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( ( ( lub ` K ) ` ( S .+ T ) ) ( le ` K ) ( ( lub ` K ) ` ( ( pmap ` K ) ` ( ( lub ` K ) ` ( S u. T ) ) ) ) <-> ( ( pmap ` K ) ` ( ( lub ` K ) ` ( S .+ T ) ) ) C_ ( ( pmap ` K ) ` ( ( lub ` K ) ` ( ( pmap ` K ) ` ( ( lub ` K ) ` ( S u. T ) ) ) ) ) ) )
73 65 72 mpbid 
 |-  ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( ( pmap ` K ) ` ( ( lub ` K ) ` ( S .+ T ) ) ) C_ ( ( pmap ` K ) ` ( ( lub ` K ) ` ( ( pmap ` K ) ` ( ( lub ` K ) ` ( S u. T ) ) ) ) ) )
74 17 1 20 3 2polvalN 
 |-  ( ( K e. HL /\ ( S .+ T ) C_ A ) -> ( ._|_ ` ( ._|_ ` ( S .+ T ) ) ) = ( ( pmap ` K ) ` ( ( lub ` K ) ` ( S .+ T ) ) ) )
75 4 5 74 syl2anc 
 |-  ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( ._|_ ` ( ._|_ ` ( S .+ T ) ) ) = ( ( pmap ` K ) ` ( ( lub ` K ) ` ( S .+ T ) ) ) )
76 17 1 20 3 2polvalN 
 |-  ( ( K e. HL /\ ( S u. T ) C_ A ) -> ( ._|_ ` ( ._|_ ` ( S u. T ) ) ) = ( ( pmap ` K ) ` ( ( lub ` K ) ` ( S u. T ) ) ) )
77 4 13 76 syl2anc 
 |-  ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( ._|_ ` ( ._|_ ` ( S u. T ) ) ) = ( ( pmap ` K ) ` ( ( lub ` K ) ` ( S u. T ) ) ) )
78 17 1 20 2pmaplubN 
 |-  ( ( K e. HL /\ ( S u. T ) C_ A ) -> ( ( pmap ` K ) ` ( ( lub ` K ) ` ( ( pmap ` K ) ` ( ( lub ` K ) ` ( S u. T ) ) ) ) ) = ( ( pmap ` K ) ` ( ( lub ` K ) ` ( S u. T ) ) ) )
79 4 13 78 syl2anc 
 |-  ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( ( pmap ` K ) ` ( ( lub ` K ) ` ( ( pmap ` K ) ` ( ( lub ` K ) ` ( S u. T ) ) ) ) ) = ( ( pmap ` K ) ` ( ( lub ` K ) ` ( S u. T ) ) ) )
80 77 79 eqtr4d 
 |-  ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( ._|_ ` ( ._|_ ` ( S u. T ) ) ) = ( ( pmap ` K ) ` ( ( lub ` K ) ` ( ( pmap ` K ) ` ( ( lub ` K ) ` ( S u. T ) ) ) ) ) )
81 73 75 80 3sstr4d 
 |-  ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( ._|_ ` ( ._|_ ` ( S .+ T ) ) ) C_ ( ._|_ ` ( ._|_ ` ( S u. T ) ) ) )
82 1 3 2polcon4bN 
 |-  ( ( K e. HL /\ ( S .+ T ) C_ A /\ ( S u. T ) C_ A ) -> ( ( ._|_ ` ( ._|_ ` ( S .+ T ) ) ) C_ ( ._|_ ` ( ._|_ ` ( S u. T ) ) ) <-> ( ._|_ ` ( S u. T ) ) C_ ( ._|_ ` ( S .+ T ) ) ) )
83 4 5 13 82 syl3anc 
 |-  ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( ( ._|_ ` ( ._|_ ` ( S .+ T ) ) ) C_ ( ._|_ ` ( ._|_ ` ( S u. T ) ) ) <-> ( ._|_ ` ( S u. T ) ) C_ ( ._|_ ` ( S .+ T ) ) ) )
84 81 83 mpbid 
 |-  ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( ._|_ ` ( S u. T ) ) C_ ( ._|_ ` ( S .+ T ) ) )
85 8 84 eqssd 
 |-  ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( ._|_ ` ( S .+ T ) ) = ( ._|_ ` ( S u. T ) ) )