Metamath Proof Explorer

Theorem lncvrat

Description: A line covers the atoms it contains. (Contributed by NM, 30-Apr-2012)

Ref Expression
Hypotheses lncvrat.b 
|- B = ( Base ` K )
lncvrat.l 
|- .<_ = ( le ` K )
lncvrat.c 
|- C = (
lncvrat.a 
|- A = ( Atoms ` K )
lncvrat.n 
|- N = ( Lines ` K )
lncvrat.m 
|- M = ( pmap ` K )
Assertion lncvrat 
|- ( ( ( K e. HL /\ X e. B /\ P e. A ) /\ ( ( M ` X ) e. N /\ P .<_ X ) ) -> P C X )

Proof

Step Hyp Ref Expression
1 lncvrat.b 
 |-  B = ( Base ` K )
2 lncvrat.l 
 |-  .<_ = ( le ` K )
3 lncvrat.c 
 |-  C = (
4 lncvrat.a 
 |-  A = ( Atoms ` K )
5 lncvrat.n 
 |-  N = ( Lines ` K )
6 lncvrat.m 
 |-  M = ( pmap ` K )
7 simprl 
 |-  ( ( ( K e. HL /\ X e. B /\ P e. A ) /\ ( ( M ` X ) e. N /\ P .<_ X ) ) -> ( M ` X ) e. N )
8 simpl1 
 |-  ( ( ( K e. HL /\ X e. B /\ P e. A ) /\ ( ( M ` X ) e. N /\ P .<_ X ) ) -> K e. HL )
9 simpl2 
 |-  ( ( ( K e. HL /\ X e. B /\ P e. A ) /\ ( ( M ` X ) e. N /\ P .<_ X ) ) -> X e. B )
10 eqid 
 |-  ( join ` K ) = ( join ` K )
11 1 10 4 5 6 isline3 
 |-  ( ( K e. HL /\ X e. B ) -> ( ( M ` X ) e. N <-> E. q e. A E. r e. A ( q =/= r /\ X = ( q ( join ` K ) r ) ) ) )
12 8 9 11 syl2anc 
 |-  ( ( ( K e. HL /\ X e. B /\ P e. A ) /\ ( ( M ` X ) e. N /\ P .<_ X ) ) -> ( ( M ` X ) e. N <-> E. q e. A E. r e. A ( q =/= r /\ X = ( q ( join ` K ) r ) ) ) )
13 7 12 mpbid 
 |-  ( ( ( K e. HL /\ X e. B /\ P e. A ) /\ ( ( M ` 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 /\ X e. B /\ P e. A ) /\ ( ( M ` X ) e. N /\ P .<_ X ) ) /\ ( q e. A /\ r e. A ) /\ ( q =/= r /\ X = ( q ( join ` K ) r ) ) ) -> K e. HL )
15 simp1l3 
 |-  ( ( ( ( K e. HL /\ X e. B /\ P e. A ) /\ ( ( M ` 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 /\ X e. B /\ P e. A ) /\ ( ( M ` 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 /\ X e. B /\ P e. A ) /\ ( ( M ` 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 /\ X e. B /\ P e. A ) /\ ( ( M ` X ) e. N /\ P .<_ X ) ) /\ ( q e. A /\ r e. A ) /\ ( q =/= r /\ X = ( q ( join ` K ) r ) ) ) -> q =/= r )
19 simp1rr 
 |-  ( ( ( ( K e. HL /\ X e. B /\ P e. A ) /\ ( ( M ` 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 /\ X e. B /\ P e. A ) /\ ( ( M ` 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 /\ X e. B /\ P e. A ) /\ ( ( M ` X ) e. N /\ P .<_ X ) ) /\ ( q e. A /\ r e. A ) /\ ( q =/= r /\ X = ( q ( join ` K ) r ) ) ) -> P .<_ ( q ( join ` K ) r ) )
22 2 10 3 4 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 /\ X e. B /\ P e. A ) /\ ( ( M ` 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 /\ X e. B /\ P e. A ) /\ ( ( M ` 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 /\ X e. B /\ P e. A ) /\ ( ( M ` 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 /\ X e. B /\ P e. A ) /\ ( ( M ` 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 /\ X e. B /\ P e. A ) /\ ( ( M ` X ) e. N /\ P .<_ X ) ) -> P C X )