Metamath Proof Explorer

Theorem oldmm1

Description: De Morgan's law for meet in an ortholattice. ( chdmm1 analog.) (Contributed by NM, 6-Nov-2011)

Ref Expression
Hypotheses oldmm1.b 
|- B = ( Base ` K )
oldmm1.j 
|- .\/ = ( join ` K )
oldmm1.m 
|- ./\ = ( meet ` K )
oldmm1.o 
|- ._|_ = ( oc ` K )
Assertion oldmm1 
|- ( ( K e. OL /\ X e. B /\ Y e. B ) -> ( ._|_ ` ( X ./\ Y ) ) = ( ( ._|_ ` X ) .\/ ( ._|_ ` Y ) ) )

Proof

Step Hyp Ref Expression
1 oldmm1.b 
 |-  B = ( Base ` K )
2 oldmm1.j 
 |-  .\/ = ( join ` K )
3 oldmm1.m 
 |-  ./\ = ( meet ` K )
4 oldmm1.o 
 |-  ._|_ = ( oc ` K )
5 eqid 
 |-  ( le ` K ) = ( le ` K )
6 ollat 
 |-  ( K e. OL -> K e. Lat )
7 6 3ad2ant1 
 |-  ( ( K e. OL /\ X e. B /\ Y e. B ) -> K e. Lat )
8 olop 
 |-  ( K e. OL -> K e. OP )
9 8 3ad2ant1 
 |-  ( ( K e. OL /\ X e. B /\ Y e. B ) -> K e. OP )
10 1 3 latmcl 
 |-  ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( X ./\ Y ) e. B )
11 6 10 syl3an1 
 |-  ( ( K e. OL /\ X e. B /\ Y e. B ) -> ( X ./\ Y ) e. B )
12 1 4 opoccl 
 |-  ( ( K e. OP /\ ( X ./\ Y ) e. B ) -> ( ._|_ ` ( X ./\ Y ) ) e. B )
13 9 11 12 syl2anc 
 |-  ( ( K e. OL /\ X e. B /\ Y e. B ) -> ( ._|_ ` ( X ./\ Y ) ) e. B )
14 1 4 opoccl 
 |-  ( ( K e. OP /\ X e. B ) -> ( ._|_ ` X ) e. B )
15 8 14 sylan 
 |-  ( ( K e. OL /\ X e. B ) -> ( ._|_ ` X ) e. B )
16 15 3adant3 
 |-  ( ( K e. OL /\ X e. B /\ Y e. B ) -> ( ._|_ ` X ) e. B )
17 1 4 opoccl 
 |-  ( ( K e. OP /\ Y e. B ) -> ( ._|_ ` Y ) e. B )
18 8 17 sylan 
 |-  ( ( K e. OL /\ Y e. B ) -> ( ._|_ ` Y ) e. B )
19 18 3adant2 
 |-  ( ( K e. OL /\ X e. B /\ Y e. B ) -> ( ._|_ ` Y ) e. B )
20 1 2 latjcl 
 |-  ( ( K e. Lat /\ ( ._|_ ` X ) e. B /\ ( ._|_ ` Y ) e. B ) -> ( ( ._|_ ` X ) .\/ ( ._|_ ` Y ) ) e. B )
21 7 16 19 20 syl3anc 
 |-  ( ( K e. OL /\ X e. B /\ Y e. B ) -> ( ( ._|_ ` X ) .\/ ( ._|_ ` Y ) ) e. B )
22 1 5 2 latlej1 
 |-  ( ( K e. Lat /\ ( ._|_ ` X ) e. B /\ ( ._|_ ` Y ) e. B ) -> ( ._|_ ` X ) ( le ` K ) ( ( ._|_ ` X ) .\/ ( ._|_ ` Y ) ) )
23 7 16 19 22 syl3anc 
 |-  ( ( K e. OL /\ X e. B /\ Y e. B ) -> ( ._|_ ` X ) ( le ` K ) ( ( ._|_ ` X ) .\/ ( ._|_ ` Y ) ) )
24 simp2 
 |-  ( ( K e. OL /\ X e. B /\ Y e. B ) -> X e. B )
25 1 5 4 oplecon1b 
 |-  ( ( K e. OP /\ X e. B /\ ( ( ._|_ ` X ) .\/ ( ._|_ ` Y ) ) e. B ) -> ( ( ._|_ ` X ) ( le ` K ) ( ( ._|_ ` X ) .\/ ( ._|_ ` Y ) ) <-> ( ._|_ ` ( ( ._|_ ` X ) .\/ ( ._|_ ` Y ) ) ) ( le ` K ) X ) )
26 9 24 21 25 syl3anc 
 |-  ( ( K e. OL /\ X e. B /\ Y e. B ) -> ( ( ._|_ ` X ) ( le ` K ) ( ( ._|_ ` X ) .\/ ( ._|_ ` Y ) ) <-> ( ._|_ ` ( ( ._|_ ` X ) .\/ ( ._|_ ` Y ) ) ) ( le ` K ) X ) )
27 23 26 mpbid 
 |-  ( ( K e. OL /\ X e. B /\ Y e. B ) -> ( ._|_ ` ( ( ._|_ ` X ) .\/ ( ._|_ ` Y ) ) ) ( le ` K ) X )
28 1 5 2 latlej2 
 |-  ( ( K e. Lat /\ ( ._|_ ` X ) e. B /\ ( ._|_ ` Y ) e. B ) -> ( ._|_ ` Y ) ( le ` K ) ( ( ._|_ ` X ) .\/ ( ._|_ ` Y ) ) )
29 7 16 19 28 syl3anc 
 |-  ( ( K e. OL /\ X e. B /\ Y e. B ) -> ( ._|_ ` Y ) ( le ` K ) ( ( ._|_ ` X ) .\/ ( ._|_ ` Y ) ) )
30 simp3 
 |-  ( ( K e. OL /\ X e. B /\ Y e. B ) -> Y e. B )
31 1 5 4 oplecon1b 
 |-  ( ( K e. OP /\ Y e. B /\ ( ( ._|_ ` X ) .\/ ( ._|_ ` Y ) ) e. B ) -> ( ( ._|_ ` Y ) ( le ` K ) ( ( ._|_ ` X ) .\/ ( ._|_ ` Y ) ) <-> ( ._|_ ` ( ( ._|_ ` X ) .\/ ( ._|_ ` Y ) ) ) ( le ` K ) Y ) )
32 9 30 21 31 syl3anc 
 |-  ( ( K e. OL /\ X e. B /\ Y e. B ) -> ( ( ._|_ ` Y ) ( le ` K ) ( ( ._|_ ` X ) .\/ ( ._|_ ` Y ) ) <-> ( ._|_ ` ( ( ._|_ ` X ) .\/ ( ._|_ ` Y ) ) ) ( le ` K ) Y ) )
33 29 32 mpbid 
 |-  ( ( K e. OL /\ X e. B /\ Y e. B ) -> ( ._|_ ` ( ( ._|_ ` X ) .\/ ( ._|_ ` Y ) ) ) ( le ` K ) Y )
34 1 4 opoccl 
 |-  ( ( K e. OP /\ ( ( ._|_ ` X ) .\/ ( ._|_ ` Y ) ) e. B ) -> ( ._|_ ` ( ( ._|_ ` X ) .\/ ( ._|_ ` Y ) ) ) e. B )
35 9 21 34 syl2anc 
 |-  ( ( K e. OL /\ X e. B /\ Y e. B ) -> ( ._|_ ` ( ( ._|_ ` X ) .\/ ( ._|_ ` Y ) ) ) e. B )
36 1 5 3 latlem12 
 |-  ( ( K e. Lat /\ ( ( ._|_ ` ( ( ._|_ ` X ) .\/ ( ._|_ ` Y ) ) ) e. B /\ X e. B /\ Y e. B ) ) -> ( ( ( ._|_ ` ( ( ._|_ ` X ) .\/ ( ._|_ ` Y ) ) ) ( le ` K ) X /\ ( ._|_ ` ( ( ._|_ ` X ) .\/ ( ._|_ ` Y ) ) ) ( le ` K ) Y ) <-> ( ._|_ ` ( ( ._|_ ` X ) .\/ ( ._|_ ` Y ) ) ) ( le ` K ) ( X ./\ Y ) ) )
37 7 35 24 30 36 syl13anc 
 |-  ( ( K e. OL /\ X e. B /\ Y e. B ) -> ( ( ( ._|_ ` ( ( ._|_ ` X ) .\/ ( ._|_ ` Y ) ) ) ( le ` K ) X /\ ( ._|_ ` ( ( ._|_ ` X ) .\/ ( ._|_ ` Y ) ) ) ( le ` K ) Y ) <-> ( ._|_ ` ( ( ._|_ ` X ) .\/ ( ._|_ ` Y ) ) ) ( le ` K ) ( X ./\ Y ) ) )
38 27 33 37 mpbi2and 
 |-  ( ( K e. OL /\ X e. B /\ Y e. B ) -> ( ._|_ ` ( ( ._|_ ` X ) .\/ ( ._|_ ` Y ) ) ) ( le ` K ) ( X ./\ Y ) )
39 1 5 4 oplecon1b 
 |-  ( ( K e. OP /\ ( ( ._|_ ` X ) .\/ ( ._|_ ` Y ) ) e. B /\ ( X ./\ Y ) e. B ) -> ( ( ._|_ ` ( ( ._|_ ` X ) .\/ ( ._|_ ` Y ) ) ) ( le ` K ) ( X ./\ Y ) <-> ( ._|_ ` ( X ./\ Y ) ) ( le ` K ) ( ( ._|_ ` X ) .\/ ( ._|_ ` Y ) ) ) )
40 9 21 11 39 syl3anc 
 |-  ( ( K e. OL /\ X e. B /\ Y e. B ) -> ( ( ._|_ ` ( ( ._|_ ` X ) .\/ ( ._|_ ` Y ) ) ) ( le ` K ) ( X ./\ Y ) <-> ( ._|_ ` ( X ./\ Y ) ) ( le ` K ) ( ( ._|_ ` X ) .\/ ( ._|_ ` Y ) ) ) )
41 38 40 mpbid 
 |-  ( ( K e. OL /\ X e. B /\ Y e. B ) -> ( ._|_ ` ( X ./\ Y ) ) ( le ` K ) ( ( ._|_ ` X ) .\/ ( ._|_ ` Y ) ) )
42 1 5 3 latmle1 
 |-  ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( X ./\ Y ) ( le ` K ) X )
43 6 42 syl3an1 
 |-  ( ( K e. OL /\ X e. B /\ Y e. B ) -> ( X ./\ Y ) ( le ` K ) X )
44 1 5 4 oplecon3b 
 |-  ( ( K e. OP /\ ( X ./\ Y ) e. B /\ X e. B ) -> ( ( X ./\ Y ) ( le ` K ) X <-> ( ._|_ ` X ) ( le ` K ) ( ._|_ ` ( X ./\ Y ) ) ) )
45 9 11 24 44 syl3anc 
 |-  ( ( K e. OL /\ X e. B /\ Y e. B ) -> ( ( X ./\ Y ) ( le ` K ) X <-> ( ._|_ ` X ) ( le ` K ) ( ._|_ ` ( X ./\ Y ) ) ) )
46 43 45 mpbid 
 |-  ( ( K e. OL /\ X e. B /\ Y e. B ) -> ( ._|_ ` X ) ( le ` K ) ( ._|_ ` ( X ./\ Y ) ) )
47 1 5 3 latmle2 
 |-  ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( X ./\ Y ) ( le ` K ) Y )
48 6 47 syl3an1 
 |-  ( ( K e. OL /\ X e. B /\ Y e. B ) -> ( X ./\ Y ) ( le ` K ) Y )
49 1 5 4 oplecon3b 
 |-  ( ( K e. OP /\ ( X ./\ Y ) e. B /\ Y e. B ) -> ( ( X ./\ Y ) ( le ` K ) Y <-> ( ._|_ ` Y ) ( le ` K ) ( ._|_ ` ( X ./\ Y ) ) ) )
50 9 11 30 49 syl3anc 
 |-  ( ( K e. OL /\ X e. B /\ Y e. B ) -> ( ( X ./\ Y ) ( le ` K ) Y <-> ( ._|_ ` Y ) ( le ` K ) ( ._|_ ` ( X ./\ Y ) ) ) )
51 48 50 mpbid 
 |-  ( ( K e. OL /\ X e. B /\ Y e. B ) -> ( ._|_ ` Y ) ( le ` K ) ( ._|_ ` ( X ./\ Y ) ) )
52 1 5 2 latjle12 
 |-  ( ( K e. Lat /\ ( ( ._|_ ` X ) e. B /\ ( ._|_ ` Y ) e. B /\ ( ._|_ ` ( X ./\ Y ) ) e. B ) ) -> ( ( ( ._|_ ` X ) ( le ` K ) ( ._|_ ` ( X ./\ Y ) ) /\ ( ._|_ ` Y ) ( le ` K ) ( ._|_ ` ( X ./\ Y ) ) ) <-> ( ( ._|_ ` X ) .\/ ( ._|_ ` Y ) ) ( le ` K ) ( ._|_ ` ( X ./\ Y ) ) ) )
53 7 16 19 13 52 syl13anc 
 |-  ( ( K e. OL /\ X e. B /\ Y e. B ) -> ( ( ( ._|_ ` X ) ( le ` K ) ( ._|_ ` ( X ./\ Y ) ) /\ ( ._|_ ` Y ) ( le ` K ) ( ._|_ ` ( X ./\ Y ) ) ) <-> ( ( ._|_ ` X ) .\/ ( ._|_ ` Y ) ) ( le ` K ) ( ._|_ ` ( X ./\ Y ) ) ) )
54 46 51 53 mpbi2and 
 |-  ( ( K e. OL /\ X e. B /\ Y e. B ) -> ( ( ._|_ ` X ) .\/ ( ._|_ ` Y ) ) ( le ` K ) ( ._|_ ` ( X ./\ Y ) ) )
55 1 5 7 13 21 41 54 latasymd 
 |-  ( ( K e. OL /\ X e. B /\ Y e. B ) -> ( ._|_ ` ( X ./\ Y ) ) = ( ( ._|_ ` X ) .\/ ( ._|_ ` Y ) ) )