Metamath Proof Explorer

Theorem cvrval5

Description: Binary relation expressing X covers X ./\ Y . (Contributed by NM, 7-Dec-2012)

Ref Expression
Hypotheses cvrval5.b 
|- B = ( Base ` K )
cvrval5.l 
|- .<_ = ( le ` K )
cvrval5.j 
|- .\/ = ( join ` K )
cvrval5.m 
|- ./\ = ( meet ` K )
cvrval5.c 
|- C = (
cvrval5.a 
|- A = ( Atoms ` K )
Assertion cvrval5 
|- ( ( K e. HL /\ X e. B /\ Y e. B ) -> ( ( X ./\ Y ) C X <-> E. p e. A ( -. p .<_ Y /\ ( p .\/ ( X ./\ Y ) ) = X ) ) )

Proof

Step Hyp Ref Expression
1 cvrval5.b 
 |-  B = ( Base ` K )
2 cvrval5.l 
 |-  .<_ = ( le ` K )
3 cvrval5.j 
 |-  .\/ = ( join ` K )
4 cvrval5.m 
 |-  ./\ = ( meet ` K )
5 cvrval5.c 
 |-  C = (
6 cvrval5.a 
 |-  A = ( Atoms ` K )
7 simp1 
 |-  ( ( K e. HL /\ X e. B /\ Y e. B ) -> K e. HL )
8 hllat 
 |-  ( K e. HL -> K e. Lat )
9 1 4 latmcl 
 |-  ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( X ./\ Y ) e. B )
10 8 9 syl3an1 
 |-  ( ( K e. HL /\ X e. B /\ Y e. B ) -> ( X ./\ Y ) e. B )
11 simp2 
 |-  ( ( K e. HL /\ X e. B /\ Y e. B ) -> X e. B )
12 1 2 3 5 6 cvrval3 
 |-  ( ( K e. HL /\ ( X ./\ Y ) e. B /\ X e. B ) -> ( ( X ./\ Y ) C X <-> E. p e. A ( -. p .<_ ( X ./\ Y ) /\ ( ( X ./\ Y ) .\/ p ) = X ) ) )
13 7 10 11 12 syl3anc 
 |-  ( ( K e. HL /\ X e. B /\ Y e. B ) -> ( ( X ./\ Y ) C X <-> E. p e. A ( -. p .<_ ( X ./\ Y ) /\ ( ( X ./\ Y ) .\/ p ) = X ) ) )
14 8 3ad2ant1 
 |-  ( ( K e. HL /\ X e. B /\ Y e. B ) -> K e. Lat )
15 14 ad2antrr 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ p e. A ) /\ ( ( X ./\ Y ) .\/ p ) = X ) -> K e. Lat )
16 10 ad2antrr 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ p e. A ) /\ ( ( X ./\ Y ) .\/ p ) = X ) -> ( X ./\ Y ) e. B )
17 1 6 atbase 
 |-  ( p e. A -> p e. B )
18 17 ad2antlr 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ p e. A ) /\ ( ( X ./\ Y ) .\/ p ) = X ) -> p e. B )
19 1 2 3 latlej2 
 |-  ( ( K e. Lat /\ ( X ./\ Y ) e. B /\ p e. B ) -> p .<_ ( ( X ./\ Y ) .\/ p ) )
20 15 16 18 19 syl3anc 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ p e. A ) /\ ( ( X ./\ Y ) .\/ p ) = X ) -> p .<_ ( ( X ./\ Y ) .\/ p ) )
21 simpr 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ p e. A ) /\ ( ( X ./\ Y ) .\/ p ) = X ) -> ( ( X ./\ Y ) .\/ p ) = X )
22 20 21 breqtrd 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ p e. A ) /\ ( ( X ./\ Y ) .\/ p ) = X ) -> p .<_ X )
23 22 biantrurd 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ p e. A ) /\ ( ( X ./\ Y ) .\/ p ) = X ) -> ( p .<_ Y <-> ( p .<_ X /\ p .<_ Y ) ) )
24 simpll2 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ p e. A ) /\ ( ( X ./\ Y ) .\/ p ) = X ) -> X e. B )
25 simpll3 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ p e. A ) /\ ( ( X ./\ Y ) .\/ p ) = X ) -> Y e. B )
26 1 2 4 latlem12 
 |-  ( ( K e. Lat /\ ( p e. B /\ X e. B /\ Y e. B ) ) -> ( ( p .<_ X /\ p .<_ Y ) <-> p .<_ ( X ./\ Y ) ) )
27 15 18 24 25 26 syl13anc 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ p e. A ) /\ ( ( X ./\ Y ) .\/ p ) = X ) -> ( ( p .<_ X /\ p .<_ Y ) <-> p .<_ ( X ./\ Y ) ) )
28 23 27 bitr2d 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ p e. A ) /\ ( ( X ./\ Y ) .\/ p ) = X ) -> ( p .<_ ( X ./\ Y ) <-> p .<_ Y ) )
29 28 notbid 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ p e. A ) /\ ( ( X ./\ Y ) .\/ p ) = X ) -> ( -. p .<_ ( X ./\ Y ) <-> -. p .<_ Y ) )
30 29 ex 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ p e. A ) -> ( ( ( X ./\ Y ) .\/ p ) = X -> ( -. p .<_ ( X ./\ Y ) <-> -. p .<_ Y ) ) )
31 30 pm5.32rd 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ p e. A ) -> ( ( -. p .<_ ( X ./\ Y ) /\ ( ( X ./\ Y ) .\/ p ) = X ) <-> ( -. p .<_ Y /\ ( ( X ./\ Y ) .\/ p ) = X ) ) )
32 14 adantr 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ p e. A ) -> K e. Lat )
33 10 adantr 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ p e. A ) -> ( X ./\ Y ) e. B )
34 17 adantl 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ p e. A ) -> p e. B )
35 1 3 latjcom 
 |-  ( ( K e. Lat /\ ( X ./\ Y ) e. B /\ p e. B ) -> ( ( X ./\ Y ) .\/ p ) = ( p .\/ ( X ./\ Y ) ) )
36 32 33 34 35 syl3anc 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ p e. A ) -> ( ( X ./\ Y ) .\/ p ) = ( p .\/ ( X ./\ Y ) ) )
37 36 eqeq1d 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ p e. A ) -> ( ( ( X ./\ Y ) .\/ p ) = X <-> ( p .\/ ( X ./\ Y ) ) = X ) )
38 37 anbi2d 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ p e. A ) -> ( ( -. p .<_ Y /\ ( ( X ./\ Y ) .\/ p ) = X ) <-> ( -. p .<_ Y /\ ( p .\/ ( X ./\ Y ) ) = X ) ) )
39 31 38 bitrd 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ p e. A ) -> ( ( -. p .<_ ( X ./\ Y ) /\ ( ( X ./\ Y ) .\/ p ) = X ) <-> ( -. p .<_ Y /\ ( p .\/ ( X ./\ Y ) ) = X ) ) )
40 39 rexbidva 
 |-  ( ( K e. HL /\ X e. B /\ Y e. B ) -> ( E. p e. A ( -. p .<_ ( X ./\ Y ) /\ ( ( X ./\ Y ) .\/ p ) = X ) <-> E. p e. A ( -. p .<_ Y /\ ( p .\/ ( X ./\ Y ) ) = X ) ) )
41 13 40 bitrd 
 |-  ( ( K e. HL /\ X e. B /\ Y e. B ) -> ( ( X ./\ Y ) C X <-> E. p e. A ( -. p .<_ Y /\ ( p .\/ ( X ./\ Y ) ) = X ) ) )