This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 
|- .+ = ( +P ` K )
paddun.o 
|- ._|_ = ( _|_P ` K )
Assertion poldmj1N 
|- ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( ._|_ ` ( S .+ T ) ) = ( ( ._|_ ` S ) i^i ( ._|_ ` T ) ) )

Proof

Step Hyp Ref Expression
1 paddun.a 
 |-  A = ( Atoms ` K )
2 paddun.p 
 |-  .+ = ( +P ` K )
3 paddun.o 
 |-  ._|_ = ( _|_P ` K )
4 1 2 3 paddunN 
 |-  ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( ._|_ ` ( S .+ T ) ) = ( ._|_ ` ( S u. T ) ) )
5 simp1 
 |-  ( ( K e. HL /\ S C_ A /\ T C_ A ) -> K e. HL )
6 unss 
 |-  ( ( S C_ A /\ T C_ A ) <-> ( S u. T ) C_ A )
7 6 biimpi 
 |-  ( ( S C_ A /\ T C_ A ) -> ( S u. T ) C_ A )
8 7 3adant1 
 |-  ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( S u. T ) C_ 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 e. HL /\ ( S u. T ) C_ A ) -> ( ._|_ ` ( S u. T ) ) = ( ( pmap ` K ) ` ( ( oc ` K ) ` ( ( lub ` K ) ` ( S u. T ) ) ) ) )
13 5 8 12 syl2anc 
 |-  ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( ._|_ ` ( S u. T ) ) = ( ( pmap ` K ) ` ( ( oc ` K ) ` ( ( lub ` K ) ` ( S u. T ) ) ) ) )
14 hlop 
 |-  ( K e. HL -> K e. OP )
15 14 3ad2ant1 
 |-  ( ( K e. HL /\ S C_ A /\ T C_ A ) -> K e. OP )
16 hlclat 
 |-  ( K e. HL -> K e. CLat )
17 16 3ad2ant1 
 |-  ( ( K e. HL /\ S C_ A /\ T C_ A ) -> K e. CLat )
18 simp2 
 |-  ( ( K e. HL /\ S C_ A /\ T C_ A ) -> S C_ A )
19 eqid 
 |-  ( Base ` K ) = ( Base ` K )
20 19 1 atssbase 
 |-  A C_ ( Base ` K )
21 18 20 sstrdi 
 |-  ( ( K e. HL /\ S C_ A /\ T C_ A ) -> S C_ ( Base ` K ) )
22 19 9 clatlubcl 
 |-  ( ( K e. CLat /\ S C_ ( Base ` K ) ) -> ( ( lub ` K ) ` S ) e. ( Base ` K ) )
23 17 21 22 syl2anc 
 |-  ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( ( lub ` K ) ` S ) e. ( Base ` K ) )
24 19 10 opoccl 
 |-  ( ( K e. OP /\ ( ( lub ` K ) ` S ) e. ( Base ` K ) ) -> ( ( oc ` K ) ` ( ( lub ` K ) ` S ) ) e. ( Base ` K ) )
25 15 23 24 syl2anc 
 |-  ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( ( oc ` K ) ` ( ( lub ` K ) ` S ) ) e. ( Base ` K ) )
26 simp3 
 |-  ( ( K e. HL /\ S C_ A /\ T C_ A ) -> T C_ A )
27 26 20 sstrdi 
 |-  ( ( K e. HL /\ S C_ A /\ T C_ A ) -> T C_ ( Base ` K ) )
28 19 9 clatlubcl 
 |-  ( ( K e. CLat /\ T C_ ( Base ` K ) ) -> ( ( lub ` K ) ` T ) e. ( Base ` K ) )
29 17 27 28 syl2anc 
 |-  ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( ( lub ` K ) ` T ) e. ( Base ` K ) )
30 19 10 opoccl 
 |-  ( ( K e. OP /\ ( ( lub ` K ) ` T ) e. ( Base ` K ) ) -> ( ( oc ` K ) ` ( ( lub ` K ) ` T ) ) e. ( Base ` K ) )
31 15 29 30 syl2anc 
 |-  ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( ( oc ` K ) ` ( ( lub ` K ) ` T ) ) e. ( Base ` K ) )
32 eqid 
 |-  ( meet ` K ) = ( meet ` K )
33 19 32 1 11 pmapmeet 
 |-  ( ( K e. HL /\ ( ( oc ` K ) ` ( ( lub ` K ) ` S ) ) e. ( Base ` K ) /\ ( ( oc ` K ) ` ( ( lub ` K ) ` T ) ) e. ( Base ` K ) ) -> ( ( pmap ` K ) ` ( ( ( oc ` K ) ` ( ( lub ` K ) ` S ) ) ( meet ` K ) ( ( oc ` K ) ` ( ( lub ` K ) ` T ) ) ) ) = ( ( ( pmap ` K ) ` ( ( oc ` K ) ` ( ( lub ` K ) ` S ) ) ) i^i ( ( pmap ` K ) ` ( ( oc ` K ) ` ( ( lub ` K ) ` T ) ) ) ) )
34 5 25 31 33 syl3anc 
 |-  ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( ( pmap ` K ) ` ( ( ( oc ` K ) ` ( ( lub ` K ) ` S ) ) ( meet ` K ) ( ( oc ` K ) ` ( ( lub ` K ) ` T ) ) ) ) = ( ( ( pmap ` K ) ` ( ( oc ` K ) ` ( ( lub ` K ) ` S ) ) ) i^i ( ( pmap ` K ) ` ( ( oc ` K ) ` ( ( lub ` K ) ` T ) ) ) ) )
35 eqid 
 |-  ( join ` K ) = ( join ` K )
36 19 35 9 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 ) ) )
37 17 21 27 36 syl3anc 
 |-  ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( ( lub ` K ) ` ( S u. T ) ) = ( ( ( lub ` K ) ` S ) ( join ` K ) ( ( lub ` K ) ` T ) ) )
38 37 fveq2d 
 |-  ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( ( oc ` K ) ` ( ( lub ` K ) ` ( S u. T ) ) ) = ( ( oc ` K ) ` ( ( ( lub ` K ) ` S ) ( join ` K ) ( ( lub ` K ) ` T ) ) ) )
39 hlol 
 |-  ( K e. HL -> K e. OL )
40 39 3ad2ant1 
 |-  ( ( K e. HL /\ S C_ A /\ T C_ A ) -> K e. OL )
41 19 35 32 10 oldmj1 
 |-  ( ( K e. OL /\ ( ( lub ` K ) ` S ) e. ( Base ` K ) /\ ( ( lub ` K ) ` T ) e. ( 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 e. HL /\ S C_ A /\ T C_ 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 e. HL /\ S C_ A /\ T C_ A ) -> ( ( oc ` K ) ` ( ( lub ` K ) ` ( S u. T ) ) ) = ( ( ( oc ` K ) ` ( ( lub ` K ) ` S ) ) ( meet ` K ) ( ( oc ` K ) ` ( ( lub ` K ) ` T ) ) ) )
44 43 fveq2d 
 |-  ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( ( pmap ` K ) ` ( ( oc ` K ) ` ( ( lub ` K ) ` ( S u. T ) ) ) ) = ( ( pmap ` K ) ` ( ( ( oc ` K ) ` ( ( lub ` K ) ` S ) ) ( meet ` K ) ( ( oc ` K ) ` ( ( lub ` K ) ` T ) ) ) ) )
45 9 10 1 11 3 polval2N 
 |-  ( ( K e. HL /\ S C_ A ) -> ( ._|_ ` S ) = ( ( pmap ` K ) ` ( ( oc ` K ) ` ( ( lub ` K ) ` S ) ) ) )
46 45 3adant3 
 |-  ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( ._|_ ` S ) = ( ( pmap ` K ) ` ( ( oc ` K ) ` ( ( lub ` K ) ` S ) ) ) )
47 9 10 1 11 3 polval2N 
 |-  ( ( K e. HL /\ T C_ A ) -> ( ._|_ ` T ) = ( ( pmap ` K ) ` ( ( oc ` K ) ` ( ( lub ` K ) ` T ) ) ) )
48 47 3adant2 
 |-  ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( ._|_ ` T ) = ( ( pmap ` K ) ` ( ( oc ` K ) ` ( ( lub ` K ) ` T ) ) ) )
49 46 48 ineq12d 
 |-  ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( ( ._|_ ` S ) i^i ( ._|_ ` T ) ) = ( ( ( pmap ` K ) ` ( ( oc ` K ) ` ( ( lub ` K ) ` S ) ) ) i^i ( ( pmap ` K ) ` ( ( oc ` K ) ` ( ( lub ` K ) ` T ) ) ) ) )
50 34 44 49 3eqtr4d 
 |-  ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( ( pmap ` K ) ` ( ( oc ` K ) ` ( ( lub ` K ) ` ( S u. T ) ) ) ) = ( ( ._|_ ` S ) i^i ( ._|_ ` T ) ) )
51 4 13 50 3eqtrd 
 |-  ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( ._|_ ` ( S .+ T ) ) = ( ( ._|_ ` S ) i^i ( ._|_ ` T ) ) )