Metamath Proof Explorer

Theorem cvrat2

Description: A Hilbert lattice element covered by the join of two distinct atoms is an atom. ( atcvat2i analog.) (Contributed by NM, 30-Nov-2011)

Ref Expression
Hypotheses cvrat2.b 
|- B = ( Base ` K )
cvrat2.j 
|- .\/ = ( join ` K )
cvrat2.c 
|- C = (
cvrat2.a 
|- A = ( Atoms ` K )
Assertion cvrat2 
|- ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) /\ ( P =/= Q /\ X C ( P .\/ Q ) ) ) -> X e. A )

Proof

Step Hyp Ref Expression
1 cvrat2.b 
 |-  B = ( Base ` K )
2 cvrat2.j 
 |-  .\/ = ( join ` K )
3 cvrat2.c 
 |-  C = (
4 cvrat2.a 
 |-  A = ( Atoms ` K )
5 eqid 
 |-  ( 0. ` K ) = ( 0. ` K )
6 1 2 5 3 4 atcvrj0 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) /\ X C ( P .\/ Q ) ) -> ( X = ( 0. ` K ) <-> P = Q ) )
7 6 3expa 
 |-  ( ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) /\ X C ( P .\/ Q ) ) -> ( X = ( 0. ` K ) <-> P = Q ) )
8 7 necon3bid 
 |-  ( ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) /\ X C ( P .\/ Q ) ) -> ( X =/= ( 0. ` K ) <-> P =/= Q ) )
9 simpl 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) -> K e. HL )
10 simpr1 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) -> X e. B )
11 hllat 
 |-  ( K e. HL -> K e. Lat )
12 11 adantr 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) -> K e. Lat )
13 simpr2 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) -> P e. A )
14 1 4 atbase 
 |-  ( P e. A -> P e. B )
15 13 14 syl 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) -> P e. B )
16 simpr3 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) -> Q e. A )
17 1 4 atbase 
 |-  ( Q e. A -> Q e. B )
18 16 17 syl 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) -> Q e. B )
19 1 2 latjcl 
 |-  ( ( K e. Lat /\ P e. B /\ Q e. B ) -> ( P .\/ Q ) e. B )
20 12 15 18 19 syl3anc 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) -> ( P .\/ Q ) e. B )
21 eqid 
 |-  ( lt ` K ) = ( lt ` K )
22 1 21 3 cvrlt 
 |-  ( ( ( K e. HL /\ X e. B /\ ( P .\/ Q ) e. B ) /\ X C ( P .\/ Q ) ) -> X ( lt ` K ) ( P .\/ Q ) )
23 22 ex 
 |-  ( ( K e. HL /\ X e. B /\ ( P .\/ Q ) e. B ) -> ( X C ( P .\/ Q ) -> X ( lt ` K ) ( P .\/ Q ) ) )
24 9 10 20 23 syl3anc 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) -> ( X C ( P .\/ Q ) -> X ( lt ` K ) ( P .\/ Q ) ) )
25 1 21 2 5 4 cvrat 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) -> ( ( X =/= ( 0. ` K ) /\ X ( lt ` K ) ( P .\/ Q ) ) -> X e. A ) )
26 25 expcomd 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) -> ( X ( lt ` K ) ( P .\/ Q ) -> ( X =/= ( 0. ` K ) -> X e. A ) ) )
27 24 26 syld 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) -> ( X C ( P .\/ Q ) -> ( X =/= ( 0. ` K ) -> X e. A ) ) )
28 27 imp 
 |-  ( ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) /\ X C ( P .\/ Q ) ) -> ( X =/= ( 0. ` K ) -> X e. A ) )
29 8 28 sylbird 
 |-  ( ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) /\ X C ( P .\/ Q ) ) -> ( P =/= Q -> X e. A ) )
30 29 ex 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) -> ( X C ( P .\/ Q ) -> ( P =/= Q -> X e. A ) ) )
31 30 com23 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) -> ( P =/= Q -> ( X C ( P .\/ Q ) -> X e. A ) ) )
32 31 impd 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) -> ( ( P =/= Q /\ X C ( P .\/ Q ) ) -> X e. A ) )
33 32 3impia 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) /\ ( P =/= Q /\ X C ( P .\/ Q ) ) ) -> X e. A )