Metamath Proof Explorer

Theorem atcvrlln2

Description: An atom under a line is covered by it. (Contributed by NM, 2-Jul-2012)

Ref Expression
Hypotheses atcvrlln2.l 
|- .<_ = ( le ` K )
atcvrlln2.c 
|- C = (
atcvrlln2.a 
|- A = ( Atoms ` K )
atcvrlln2.n 
|- N = ( LLines ` K )
Assertion atcvrlln2 
|- ( ( ( K e. HL /\ P e. A /\ X e. N ) /\ P .<_ X ) -> P C X )

Proof

Step Hyp Ref Expression
1 atcvrlln2.l 
 |-  .<_ = ( le ` K )
2 atcvrlln2.c 
 |-  C = (
3 atcvrlln2.a 
 |-  A = ( Atoms ` K )
4 atcvrlln2.n 
 |-  N = ( LLines ` K )
5 simpl3 
 |-  ( ( ( K e. HL /\ P e. A /\ X e. N ) /\ P .<_ X ) -> X e. N )
6 simpl1 
 |-  ( ( ( K e. HL /\ P e. A /\ X e. N ) /\ P .<_ X ) -> K e. HL )
7 eqid 
 |-  ( Base ` K ) = ( Base ` K )
8 7 4 llnbase 
 |-  ( X e. N -> X e. ( Base ` K ) )
9 5 8 syl 
 |-  ( ( ( K e. HL /\ P e. A /\ X e. N ) /\ P .<_ X ) -> X e. ( Base ` K ) )
10 eqid 
 |-  ( join ` K ) = ( join ` K )
11 7 10 3 4 islln3 
 |-  ( ( K e. HL /\ X e. ( Base ` K ) ) -> ( X e. N <-> E. q e. A E. r e. A ( q =/= r /\ X = ( q ( join ` K ) r ) ) ) )
12 6 9 11 syl2anc 
 |-  ( ( ( K e. HL /\ P e. A /\ X e. N ) /\ P .<_ X ) -> ( X e. N <-> E. q e. A E. r e. A ( q =/= r /\ X = ( q ( join ` K ) r ) ) ) )
13 5 12 mpbid 
 |-  ( ( ( K e. HL /\ P e. A /\ X e. N ) /\ P .<_ X ) -> E. q e. A E. r e. A ( q =/= r /\ X = ( q ( join ` K ) r ) ) )
14 simp1l1 
 |-  ( ( ( ( K e. HL /\ P e. A /\ X e. N ) /\ P .<_ X ) /\ ( q e. A /\ r e. A ) /\ ( q =/= r /\ X = ( q ( join ` K ) r ) ) ) -> K e. HL )
15 simp1l2 
 |-  ( ( ( ( K e. HL /\ P e. A /\ X e. N ) /\ P .<_ X ) /\ ( q e. A /\ r e. A ) /\ ( q =/= r /\ X = ( q ( join ` K ) r ) ) ) -> P e. A )
16 simp2l 
 |-  ( ( ( ( K e. HL /\ P e. A /\ X e. N ) /\ P .<_ X ) /\ ( q e. A /\ r e. A ) /\ ( q =/= r /\ X = ( q ( join ` K ) r ) ) ) -> q e. A )
17 simp2r 
 |-  ( ( ( ( K e. HL /\ P e. A /\ X e. N ) /\ P .<_ X ) /\ ( q e. A /\ r e. A ) /\ ( q =/= r /\ X = ( q ( join ` K ) r ) ) ) -> r e. A )
18 simp3l 
 |-  ( ( ( ( K e. HL /\ P e. A /\ X e. N ) /\ P .<_ X ) /\ ( q e. A /\ r e. A ) /\ ( q =/= r /\ X = ( q ( join ` K ) r ) ) ) -> q =/= r )
19 simp1r 
 |-  ( ( ( ( K e. HL /\ P e. A /\ X e. N ) /\ P .<_ X ) /\ ( q e. A /\ r e. A ) /\ ( q =/= r /\ X = ( q ( join ` K ) r ) ) ) -> P .<_ X )
20 simp3r 
 |-  ( ( ( ( K e. HL /\ P e. A /\ X e. N ) /\ P .<_ X ) /\ ( q e. A /\ r e. A ) /\ ( q =/= r /\ X = ( q ( join ` K ) r ) ) ) -> X = ( q ( join ` K ) r ) )
21 19 20 breqtrd 
 |-  ( ( ( ( K e. HL /\ P e. A /\ X e. N ) /\ P .<_ X ) /\ ( q e. A /\ r e. A ) /\ ( q =/= r /\ X = ( q ( join ` K ) r ) ) ) -> P .<_ ( q ( join ` K ) r ) )
22 1 10 2 3 atcvrj2 
 |-  ( ( K e. HL /\ ( P e. A /\ q e. A /\ r e. A ) /\ ( q =/= r /\ P .<_ ( q ( join ` K ) r ) ) ) -> P C ( q ( join ` K ) r ) )
23 14 15 16 17 18 21 22 syl132anc 
 |-  ( ( ( ( K e. HL /\ P e. A /\ X e. N ) /\ P .<_ X ) /\ ( q e. A /\ r e. A ) /\ ( q =/= r /\ X = ( q ( join ` K ) r ) ) ) -> P C ( q ( join ` K ) r ) )
24 23 20 breqtrrd 
 |-  ( ( ( ( K e. HL /\ P e. A /\ X e. N ) /\ P .<_ X ) /\ ( q e. A /\ r e. A ) /\ ( q =/= r /\ X = ( q ( join ` K ) r ) ) ) -> P C X )
25 24 3exp 
 |-  ( ( ( K e. HL /\ P e. A /\ X e. N ) /\ P .<_ X ) -> ( ( q e. A /\ r e. A ) -> ( ( q =/= r /\ X = ( q ( join ` K ) r ) ) -> P C X ) ) )
26 25 rexlimdvv 
 |-  ( ( ( K e. HL /\ P e. A /\ X e. N ) /\ P .<_ X ) -> ( E. q e. A E. r e. A ( q =/= r /\ X = ( q ( join ` K ) r ) ) -> P C X ) )
27 13 26 mpd 
 |-  ( ( ( K e. HL /\ P e. A /\ X e. N ) /\ P .<_ X ) -> P C X )