Metamath Proof Explorer

Theorem atcvrlln

Description: An element covering an atom is a lattice line and vice-versa. (Contributed by NM, 18-Jun-2012)

Ref Expression
Hypotheses atcvrlln.b 
|- B = ( Base ` K )
atcvrlln.c 
|- C = (
atcvrlln.a 
|- A = ( Atoms ` K )
atcvrlln.n 
|- N = ( LLines ` K )
Assertion atcvrlln 
|- ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) -> ( X e. A <-> Y e. N ) )

Proof

Step Hyp Ref Expression
1 atcvrlln.b 
 |-  B = ( Base ` K )
2 atcvrlln.c 
 |-  C = (
3 atcvrlln.a 
 |-  A = ( Atoms ` K )
4 atcvrlln.n 
 |-  N = ( LLines ` K )
5 simpll1 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ X e. A ) -> K e. HL )
6 simpll3 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ X e. A ) -> Y e. B )
7 simpr 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ X e. A ) -> X e. A )
8 simplr 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ X e. A ) -> X C Y )
9 1 2 3 4 llni 
 |-  ( ( ( K e. HL /\ Y e. B /\ X e. A ) /\ X C Y ) -> Y e. N )
10 5 6 7 8 9 syl31anc 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ X e. A ) -> Y e. N )
11 simpr 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ Y e. N ) -> Y e. N )
12 simpll1 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ Y e. N ) -> K e. HL )
13 simpll3 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ Y e. N ) -> Y e. B )
14 eqid 
 |-  ( join ` K ) = ( join ` K )
15 1 14 3 4 islln3 
 |-  ( ( K e. HL /\ Y e. B ) -> ( Y e. N <-> E. p e. A E. q e. A ( p =/= q /\ Y = ( p ( join ` K ) q ) ) ) )
16 12 13 15 syl2anc 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ Y e. N ) -> ( Y e. N <-> E. p e. A E. q e. A ( p =/= q /\ Y = ( p ( join ` K ) q ) ) ) )
17 11 16 mpbid 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ Y e. N ) -> E. p e. A E. q e. A ( p =/= q /\ Y = ( p ( join ` K ) q ) ) )
18 simp1l1 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ ( p e. A /\ q e. A ) /\ ( p =/= q /\ Y = ( p ( join ` K ) q ) ) ) -> K e. HL )
19 simp1l2 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ ( p e. A /\ q e. A ) /\ ( p =/= q /\ Y = ( p ( join ` K ) q ) ) ) -> X e. B )
20 simp2l 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ ( p e. A /\ q e. A ) /\ ( p =/= q /\ Y = ( p ( join ` K ) q ) ) ) -> p e. A )
21 simp2r 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ ( p e. A /\ q e. A ) /\ ( p =/= q /\ Y = ( p ( join ` K ) q ) ) ) -> q e. A )
22 simp3l 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ ( p e. A /\ q e. A ) /\ ( p =/= q /\ Y = ( p ( join ` K ) q ) ) ) -> p =/= q )
23 simp1r 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ ( p e. A /\ q e. A ) /\ ( p =/= q /\ Y = ( p ( join ` K ) q ) ) ) -> X C Y )
24 simp3r 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ ( p e. A /\ q e. A ) /\ ( p =/= q /\ Y = ( p ( join ` K ) q ) ) ) -> Y = ( p ( join ` K ) q ) )
25 23 24 breqtrd 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ ( p e. A /\ q e. A ) /\ ( p =/= q /\ Y = ( p ( join ` K ) q ) ) ) -> X C ( p ( join ` K ) q ) )
26 1 14 2 3 cvrat2 
 |-  ( ( K e. HL /\ ( X e. B /\ p e. A /\ q e. A ) /\ ( p =/= q /\ X C ( p ( join ` K ) q ) ) ) -> X e. A )
27 18 19 20 21 22 25 26 syl132anc 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ ( p e. A /\ q e. A ) /\ ( p =/= q /\ Y = ( p ( join ` K ) q ) ) ) -> X e. A )
28 27 3exp 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) -> ( ( p e. A /\ q e. A ) -> ( ( p =/= q /\ Y = ( p ( join ` K ) q ) ) -> X e. A ) ) )
29 28 rexlimdvv 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) -> ( E. p e. A E. q e. A ( p =/= q /\ Y = ( p ( join ` K ) q ) ) -> X e. A ) )
30 29 adantr 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ Y e. N ) -> ( E. p e. A E. q e. A ( p =/= q /\ Y = ( p ( join ` K ) q ) ) -> X e. A ) )
31 17 30 mpd 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ Y e. N ) -> X e. A )
32 10 31 impbida 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) -> ( X e. A <-> Y e. N ) )