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 ) ) )