Metamath Proof Explorer

Theorem cvrexchlem

Description: Lemma for cvrexch . ( cvexchlem analog.) (Contributed by NM, 18-Nov-2011)

Ref Expression
Hypotheses cvrexch.b 
|- B = ( Base ` K )
cvrexch.j 
|- .\/ = ( join ` K )
cvrexch.m 
|- ./\ = ( meet ` K )
cvrexch.c 
|- C = (
Assertion cvrexchlem 
|- ( ( K e. HL /\ X e. B /\ Y e. B ) -> ( ( X ./\ Y ) C Y -> X C ( X .\/ Y ) ) )

Proof

Step Hyp Ref Expression
1 cvrexch.b 
 |-  B = ( Base ` K )
2 cvrexch.j 
 |-  .\/ = ( join ` K )
3 cvrexch.m 
 |-  ./\ = ( meet ` K )
4 cvrexch.c 
 |-  C = (
5 hllat 
 |-  ( K e. HL -> K e. Lat )
6 1 3 latmcl 
 |-  ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( X ./\ Y ) e. B )
7 5 6 syl3an1 
 |-  ( ( K e. HL /\ X e. B /\ Y e. B ) -> ( X ./\ Y ) e. B )
8 eqid 
 |-  ( lt ` K ) = ( lt ` K )
9 1 8 4 cvrlt 
 |-  ( ( ( K e. HL /\ ( X ./\ Y ) e. B /\ Y e. B ) /\ ( X ./\ Y ) C Y ) -> ( X ./\ Y ) ( lt ` K ) Y )
10 9 ex 
 |-  ( ( K e. HL /\ ( X ./\ Y ) e. B /\ Y e. B ) -> ( ( X ./\ Y ) C Y -> ( X ./\ Y ) ( lt ` K ) Y ) )
11 7 10 syld3an2 
 |-  ( ( K e. HL /\ X e. B /\ Y e. B ) -> ( ( X ./\ Y ) C Y -> ( X ./\ Y ) ( lt ` K ) Y ) )
12 eqid 
 |-  ( le ` K ) = ( le ` K )
13 eqid 
 |-  ( Atoms ` K ) = ( Atoms ` K )
14 1 12 8 13 hlrelat1 
 |-  ( ( K e. HL /\ ( X ./\ Y ) e. B /\ Y e. B ) -> ( ( X ./\ Y ) ( lt ` K ) Y -> E. p e. ( Atoms ` K ) ( -. p ( le ` K ) ( X ./\ Y ) /\ p ( le ` K ) Y ) ) )
15 7 14 syld3an2 
 |-  ( ( K e. HL /\ X e. B /\ Y e. B ) -> ( ( X ./\ Y ) ( lt ` K ) Y -> E. p e. ( Atoms ` K ) ( -. p ( le ` K ) ( X ./\ Y ) /\ p ( le ` K ) Y ) ) )
16 11 15 syld 
 |-  ( ( K e. HL /\ X e. B /\ Y e. B ) -> ( ( X ./\ Y ) C Y -> E. p e. ( Atoms ` K ) ( -. p ( le ` K ) ( X ./\ Y ) /\ p ( le ` K ) Y ) ) )
17 16 imp 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( X ./\ Y ) C Y ) -> E. p e. ( Atoms ` K ) ( -. p ( le ` K ) ( X ./\ Y ) /\ p ( le ` K ) Y ) )
18 simpl1 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ p e. ( Atoms ` K ) ) -> K e. HL )
19 18 hllatd 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ p e. ( Atoms ` K ) ) -> K e. Lat )
20 1 13 atbase 
 |-  ( p e. ( Atoms ` K ) -> p e. B )
21 20 adantl 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ p e. ( Atoms ` K ) ) -> p e. B )
22 simpl2 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ p e. ( Atoms ` K ) ) -> X e. B )
23 simpl3 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ p e. ( Atoms ` K ) ) -> Y e. B )
24 1 12 3 latlem12 
 |-  ( ( K e. Lat /\ ( p e. B /\ X e. B /\ Y e. B ) ) -> ( ( p ( le ` K ) X /\ p ( le ` K ) Y ) <-> p ( le ` K ) ( X ./\ Y ) ) )
25 19 21 22 23 24 syl13anc 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ p e. ( Atoms ` K ) ) -> ( ( p ( le ` K ) X /\ p ( le ` K ) Y ) <-> p ( le ` K ) ( X ./\ Y ) ) )
26 25 biimpd 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ p e. ( Atoms ` K ) ) -> ( ( p ( le ` K ) X /\ p ( le ` K ) Y ) -> p ( le ` K ) ( X ./\ Y ) ) )
27 26 expcomd 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ p e. ( Atoms ` K ) ) -> ( p ( le ` K ) Y -> ( p ( le ` K ) X -> p ( le ` K ) ( X ./\ Y ) ) ) )
28 con3 
 |-  ( ( p ( le ` K ) X -> p ( le ` K ) ( X ./\ Y ) ) -> ( -. p ( le ` K ) ( X ./\ Y ) -> -. p ( le ` K ) X ) )
29 27 28 syl6 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ p e. ( Atoms ` K ) ) -> ( p ( le ` K ) Y -> ( -. p ( le ` K ) ( X ./\ Y ) -> -. p ( le ` K ) X ) ) )
30 29 com23 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ p e. ( Atoms ` K ) ) -> ( -. p ( le ` K ) ( X ./\ Y ) -> ( p ( le ` K ) Y -> -. p ( le ` K ) X ) ) )
31 30 a1d 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ p e. ( Atoms ` K ) ) -> ( ( X ./\ Y ) C Y -> ( -. p ( le ` K ) ( X ./\ Y ) -> ( p ( le ` K ) Y -> -. p ( le ` K ) X ) ) ) )
32 31 imp4d 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ p e. ( Atoms ` K ) ) -> ( ( ( X ./\ Y ) C Y /\ ( -. p ( le ` K ) ( X ./\ Y ) /\ p ( le ` K ) Y ) ) -> -. p ( le ` K ) X ) )
33 simpr 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ p e. ( Atoms ` K ) ) -> p e. ( Atoms ` K ) )
34 1 12 2 4 13 cvr1 
 |-  ( ( K e. HL /\ X e. B /\ p e. ( Atoms ` K ) ) -> ( -. p ( le ` K ) X <-> X C ( X .\/ p ) ) )
35 18 22 33 34 syl3anc 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ p e. ( Atoms ` K ) ) -> ( -. p ( le ` K ) X <-> X C ( X .\/ p ) ) )
36 32 35 sylibd 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ p e. ( Atoms ` K ) ) -> ( ( ( X ./\ Y ) C Y /\ ( -. p ( le ` K ) ( X ./\ Y ) /\ p ( le ` K ) Y ) ) -> X C ( X .\/ p ) ) )
37 36 imp 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ p e. ( Atoms ` K ) ) /\ ( ( X ./\ Y ) C Y /\ ( -. p ( le ` K ) ( X ./\ Y ) /\ p ( le ` K ) Y ) ) ) -> X C ( X .\/ p ) )
38 simpl1 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ p e. B ) -> K e. HL )
39 38 hllatd 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ p e. B ) -> K e. Lat )
40 simpl2 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ p e. B ) -> X e. B )
41 simpl3 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ p e. B ) -> Y e. B )
42 39 40 41 6 syl3anc 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ p e. B ) -> ( X ./\ Y ) e. B )
43 simpr 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ p e. B ) -> p e. B )
44 1 2 latjass 
 |-  ( ( K e. Lat /\ ( X e. B /\ ( X ./\ Y ) e. B /\ p e. B ) ) -> ( ( X .\/ ( X ./\ Y ) ) .\/ p ) = ( X .\/ ( ( X ./\ Y ) .\/ p ) ) )
45 39 40 42 43 44 syl13anc 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ p e. B ) -> ( ( X .\/ ( X ./\ Y ) ) .\/ p ) = ( X .\/ ( ( X ./\ Y ) .\/ p ) ) )
46 1 2 3 latabs1 
 |-  ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( X .\/ ( X ./\ Y ) ) = X )
47 5 46 syl3an1 
 |-  ( ( K e. HL /\ X e. B /\ Y e. B ) -> ( X .\/ ( X ./\ Y ) ) = X )
48 47 adantr 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ p e. B ) -> ( X .\/ ( X ./\ Y ) ) = X )
49 48 oveq1d 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ p e. B ) -> ( ( X .\/ ( X ./\ Y ) ) .\/ p ) = ( X .\/ p ) )
50 45 49 eqtr3d 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ p e. B ) -> ( X .\/ ( ( X ./\ Y ) .\/ p ) ) = ( X .\/ p ) )
51 50 adantr 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ p e. B ) /\ ( ( X ./\ Y ) C Y /\ ( -. p ( le ` K ) ( X ./\ Y ) /\ p ( le ` K ) Y ) ) ) -> ( X .\/ ( ( X ./\ Y ) .\/ p ) ) = ( X .\/ p ) )
52 1 12 8 2 latnle 
 |-  ( ( K e. Lat /\ ( X ./\ Y ) e. B /\ p e. B ) -> ( -. p ( le ` K ) ( X ./\ Y ) <-> ( X ./\ Y ) ( lt ` K ) ( ( X ./\ Y ) .\/ p ) ) )
53 39 42 43 52 syl3anc 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ p e. B ) -> ( -. p ( le ` K ) ( X ./\ Y ) <-> ( X ./\ Y ) ( lt ` K ) ( ( X ./\ Y ) .\/ p ) ) )
54 1 12 3 latmle2 
 |-  ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( X ./\ Y ) ( le ` K ) Y )
55 39 40 41 54 syl3anc 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ p e. B ) -> ( X ./\ Y ) ( le ` K ) Y )
56 55 biantrurd 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ p e. B ) -> ( p ( le ` K ) Y <-> ( ( X ./\ Y ) ( le ` K ) Y /\ p ( le ` K ) Y ) ) )
57 1 12 2 latjle12 
 |-  ( ( K e. Lat /\ ( ( X ./\ Y ) e. B /\ p e. B /\ Y e. B ) ) -> ( ( ( X ./\ Y ) ( le ` K ) Y /\ p ( le ` K ) Y ) <-> ( ( X ./\ Y ) .\/ p ) ( le ` K ) Y ) )
58 39 42 43 41 57 syl13anc 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ p e. B ) -> ( ( ( X ./\ Y ) ( le ` K ) Y /\ p ( le ` K ) Y ) <-> ( ( X ./\ Y ) .\/ p ) ( le ` K ) Y ) )
59 56 58 bitrd 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ p e. B ) -> ( p ( le ` K ) Y <-> ( ( X ./\ Y ) .\/ p ) ( le ` K ) Y ) )
60 53 59 anbi12d 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ p e. B ) -> ( ( -. p ( le ` K ) ( X ./\ Y ) /\ p ( le ` K ) Y ) <-> ( ( X ./\ Y ) ( lt ` K ) ( ( X ./\ Y ) .\/ p ) /\ ( ( X ./\ Y ) .\/ p ) ( le ` K ) Y ) ) )
61 hlpos 
 |-  ( K e. HL -> K e. Poset )
62 38 61 syl 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ p e. B ) -> K e. Poset )
63 1 2 latjcl 
 |-  ( ( K e. Lat /\ ( X ./\ Y ) e. B /\ p e. B ) -> ( ( X ./\ Y ) .\/ p ) e. B )
64 39 42 43 63 syl3anc 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ p e. B ) -> ( ( X ./\ Y ) .\/ p ) e. B )
65 42 41 64 3jca 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ p e. B ) -> ( ( X ./\ Y ) e. B /\ Y e. B /\ ( ( X ./\ Y ) .\/ p ) e. B ) )
66 1 12 8 4 cvrnbtwn2 
 |-  ( ( K e. Poset /\ ( ( X ./\ Y ) e. B /\ Y e. B /\ ( ( X ./\ Y ) .\/ p ) e. B ) /\ ( X ./\ Y ) C Y ) -> ( ( ( X ./\ Y ) ( lt ` K ) ( ( X ./\ Y ) .\/ p ) /\ ( ( X ./\ Y ) .\/ p ) ( le ` K ) Y ) <-> ( ( X ./\ Y ) .\/ p ) = Y ) )
67 66 biimpd 
 |-  ( ( K e. Poset /\ ( ( X ./\ Y ) e. B /\ Y e. B /\ ( ( X ./\ Y ) .\/ p ) e. B ) /\ ( X ./\ Y ) C Y ) -> ( ( ( X ./\ Y ) ( lt ` K ) ( ( X ./\ Y ) .\/ p ) /\ ( ( X ./\ Y ) .\/ p ) ( le ` K ) Y ) -> ( ( X ./\ Y ) .\/ p ) = Y ) )
68 67 3exp 
 |-  ( K e. Poset -> ( ( ( X ./\ Y ) e. B /\ Y e. B /\ ( ( X ./\ Y ) .\/ p ) e. B ) -> ( ( X ./\ Y ) C Y -> ( ( ( X ./\ Y ) ( lt ` K ) ( ( X ./\ Y ) .\/ p ) /\ ( ( X ./\ Y ) .\/ p ) ( le ` K ) Y ) -> ( ( X ./\ Y ) .\/ p ) = Y ) ) ) )
69 62 65 68 sylc 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ p e. B ) -> ( ( X ./\ Y ) C Y -> ( ( ( X ./\ Y ) ( lt ` K ) ( ( X ./\ Y ) .\/ p ) /\ ( ( X ./\ Y ) .\/ p ) ( le ` K ) Y ) -> ( ( X ./\ Y ) .\/ p ) = Y ) ) )
70 69 com23 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ p e. B ) -> ( ( ( X ./\ Y ) ( lt ` K ) ( ( X ./\ Y ) .\/ p ) /\ ( ( X ./\ Y ) .\/ p ) ( le ` K ) Y ) -> ( ( X ./\ Y ) C Y -> ( ( X ./\ Y ) .\/ p ) = Y ) ) )
71 60 70 sylbid 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ p e. B ) -> ( ( -. p ( le ` K ) ( X ./\ Y ) /\ p ( le ` K ) Y ) -> ( ( X ./\ Y ) C Y -> ( ( X ./\ Y ) .\/ p ) = Y ) ) )
72 71 com23 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ p e. B ) -> ( ( X ./\ Y ) C Y -> ( ( -. p ( le ` K ) ( X ./\ Y ) /\ p ( le ` K ) Y ) -> ( ( X ./\ Y ) .\/ p ) = Y ) ) )
73 72 imp32 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ p e. B ) /\ ( ( X ./\ Y ) C Y /\ ( -. p ( le ` K ) ( X ./\ Y ) /\ p ( le ` K ) Y ) ) ) -> ( ( X ./\ Y ) .\/ p ) = Y )
74 73 oveq2d 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ p e. B ) /\ ( ( X ./\ Y ) C Y /\ ( -. p ( le ` K ) ( X ./\ Y ) /\ p ( le ` K ) Y ) ) ) -> ( X .\/ ( ( X ./\ Y ) .\/ p ) ) = ( X .\/ Y ) )
75 51 74 eqtr3d 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ p e. B ) /\ ( ( X ./\ Y ) C Y /\ ( -. p ( le ` K ) ( X ./\ Y ) /\ p ( le ` K ) Y ) ) ) -> ( X .\/ p ) = ( X .\/ Y ) )
76 20 75 sylanl2 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ p e. ( Atoms ` K ) ) /\ ( ( X ./\ Y ) C Y /\ ( -. p ( le ` K ) ( X ./\ Y ) /\ p ( le ` K ) Y ) ) ) -> ( X .\/ p ) = ( X .\/ Y ) )
77 37 76 breqtrd 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ p e. ( Atoms ` K ) ) /\ ( ( X ./\ Y ) C Y /\ ( -. p ( le ` K ) ( X ./\ Y ) /\ p ( le ` K ) Y ) ) ) -> X C ( X .\/ Y ) )
78 77 expr 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ p e. ( Atoms ` K ) ) /\ ( X ./\ Y ) C Y ) -> ( ( -. p ( le ` K ) ( X ./\ Y ) /\ p ( le ` K ) Y ) -> X C ( X .\/ Y ) ) )
79 78 an32s 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( X ./\ Y ) C Y ) /\ p e. ( Atoms ` K ) ) -> ( ( -. p ( le ` K ) ( X ./\ Y ) /\ p ( le ` K ) Y ) -> X C ( X .\/ Y ) ) )
80 79 rexlimdva 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( X ./\ Y ) C Y ) -> ( E. p e. ( Atoms ` K ) ( -. p ( le ` K ) ( X ./\ Y ) /\ p ( le ` K ) Y ) -> X C ( X .\/ Y ) ) )
81 17 80 mpd 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( X ./\ Y ) C Y ) -> X C ( X .\/ Y ) )
82 81 ex 
 |-  ( ( K e. HL /\ X e. B /\ Y e. B ) -> ( ( X ./\ Y ) C Y -> X C ( X .\/ Y ) ) )