Metamath Proof Explorer

Theorem lneq2at

Description: A line equals the join of any two of its distinct points (atoms). (Contributed by NM, 29-Apr-2012)

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

Proof

Step Hyp Ref Expression
1 lneq2at.b 
 |-  B = ( Base ` K )
2 lneq2at.l 
 |-  .<_ = ( le ` K )
3 lneq2at.j 
 |-  .\/ = ( join ` K )
4 lneq2at.a 
 |-  A = ( Atoms ` K )
5 lneq2at.n 
 |-  N = ( Lines ` K )
6 lneq2at.m 
 |-  M = ( pmap ` K )
7 simp11 
 |-  ( ( ( K e. HL /\ X e. B /\ ( M ` X ) e. N ) /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( P .<_ X /\ Q .<_ X ) ) -> K e. HL )
8 simp12 
 |-  ( ( ( K e. HL /\ X e. B /\ ( M ` X ) e. N ) /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( P .<_ X /\ Q .<_ X ) ) -> X e. B )
9 7 8 jca 
 |-  ( ( ( K e. HL /\ X e. B /\ ( M ` X ) e. N ) /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( P .<_ X /\ Q .<_ X ) ) -> ( K e. HL /\ X e. B ) )
10 simp13 
 |-  ( ( ( K e. HL /\ X e. B /\ ( M ` X ) e. N ) /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( P .<_ X /\ Q .<_ X ) ) -> ( M ` X ) e. N )
11 1 3 4 5 6 isline3 
 |-  ( ( K e. HL /\ X e. B ) -> ( ( M ` X ) e. N <-> E. r e. A E. s e. A ( r =/= s /\ X = ( r .\/ s ) ) ) )
12 11 biimpd 
 |-  ( ( K e. HL /\ X e. B ) -> ( ( M ` X ) e. N -> E. r e. A E. s e. A ( r =/= s /\ X = ( r .\/ s ) ) ) )
13 9 10 12 sylc 
 |-  ( ( ( K e. HL /\ X e. B /\ ( M ` X ) e. N ) /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( P .<_ X /\ Q .<_ X ) ) -> E. r e. A E. s e. A ( r =/= s /\ X = ( r .\/ s ) ) )
14 simp3r 
 |-  ( ( ( ( K e. HL /\ X e. B /\ ( M ` X ) e. N ) /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( P .<_ X /\ Q .<_ X ) ) /\ ( r e. A /\ s e. A ) /\ ( r =/= s /\ X = ( r .\/ s ) ) ) -> X = ( r .\/ s ) )
15 simp111 
 |-  ( ( ( ( K e. HL /\ X e. B /\ ( M ` X ) e. N ) /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( P .<_ X /\ Q .<_ X ) ) /\ ( r e. A /\ s e. A ) /\ ( r =/= s /\ X = ( r .\/ s ) ) ) -> K e. HL )
16 simp121 
 |-  ( ( ( ( K e. HL /\ X e. B /\ ( M ` X ) e. N ) /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( P .<_ X /\ Q .<_ X ) ) /\ ( r e. A /\ s e. A ) /\ ( r =/= s /\ X = ( r .\/ s ) ) ) -> P e. A )
17 simp122 
 |-  ( ( ( ( K e. HL /\ X e. B /\ ( M ` X ) e. N ) /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( P .<_ X /\ Q .<_ X ) ) /\ ( r e. A /\ s e. A ) /\ ( r =/= s /\ X = ( r .\/ s ) ) ) -> Q e. A )
18 16 17 jca 
 |-  ( ( ( ( K e. HL /\ X e. B /\ ( M ` X ) e. N ) /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( P .<_ X /\ Q .<_ X ) ) /\ ( r e. A /\ s e. A ) /\ ( r =/= s /\ X = ( r .\/ s ) ) ) -> ( P e. A /\ Q e. A ) )
19 simp2 
 |-  ( ( ( ( K e. HL /\ X e. B /\ ( M ` X ) e. N ) /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( P .<_ X /\ Q .<_ X ) ) /\ ( r e. A /\ s e. A ) /\ ( r =/= s /\ X = ( r .\/ s ) ) ) -> ( r e. A /\ s e. A ) )
20 15 18 19 3jca 
 |-  ( ( ( ( K e. HL /\ X e. B /\ ( M ` X ) e. N ) /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( P .<_ X /\ Q .<_ X ) ) /\ ( r e. A /\ s e. A ) /\ ( r =/= s /\ X = ( r .\/ s ) ) ) -> ( K e. HL /\ ( P e. A /\ Q e. A ) /\ ( r e. A /\ s e. A ) ) )
21 simp123 
 |-  ( ( ( ( K e. HL /\ X e. B /\ ( M ` X ) e. N ) /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( P .<_ X /\ Q .<_ X ) ) /\ ( r e. A /\ s e. A ) /\ ( r =/= s /\ X = ( r .\/ s ) ) ) -> P =/= Q )
22 20 21 jca 
 |-  ( ( ( ( K e. HL /\ X e. B /\ ( M ` X ) e. N ) /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( P .<_ X /\ Q .<_ X ) ) /\ ( r e. A /\ s e. A ) /\ ( r =/= s /\ X = ( r .\/ s ) ) ) -> ( ( K e. HL /\ ( P e. A /\ Q e. A ) /\ ( r e. A /\ s e. A ) ) /\ P =/= Q ) )
23 7 hllatd 
 |-  ( ( ( K e. HL /\ X e. B /\ ( M ` X ) e. N ) /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( P .<_ X /\ Q .<_ X ) ) -> K e. Lat )
24 simp21 
 |-  ( ( ( K e. HL /\ X e. B /\ ( M ` X ) e. N ) /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( P .<_ X /\ Q .<_ X ) ) -> P e. A )
25 1 4 atbase 
 |-  ( P e. A -> P e. B )
26 24 25 syl 
 |-  ( ( ( K e. HL /\ X e. B /\ ( M ` X ) e. N ) /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( P .<_ X /\ Q .<_ X ) ) -> P e. B )
27 simp22 
 |-  ( ( ( K e. HL /\ X e. B /\ ( M ` X ) e. N ) /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( P .<_ X /\ Q .<_ X ) ) -> Q e. A )
28 1 4 atbase 
 |-  ( Q e. A -> Q e. B )
29 27 28 syl 
 |-  ( ( ( K e. HL /\ X e. B /\ ( M ` X ) e. N ) /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( P .<_ X /\ Q .<_ X ) ) -> Q e. B )
30 26 29 8 3jca 
 |-  ( ( ( K e. HL /\ X e. B /\ ( M ` X ) e. N ) /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( P .<_ X /\ Q .<_ X ) ) -> ( P e. B /\ Q e. B /\ X e. B ) )
31 23 30 jca 
 |-  ( ( ( K e. HL /\ X e. B /\ ( M ` X ) e. N ) /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( P .<_ X /\ Q .<_ X ) ) -> ( K e. Lat /\ ( P e. B /\ Q e. B /\ X e. B ) ) )
32 simp3 
 |-  ( ( ( K e. HL /\ X e. B /\ ( M ` X ) e. N ) /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( P .<_ X /\ Q .<_ X ) ) -> ( P .<_ X /\ Q .<_ X ) )
33 1 2 3 latjle12 
 |-  ( ( K e. Lat /\ ( P e. B /\ Q e. B /\ X e. B ) ) -> ( ( P .<_ X /\ Q .<_ X ) <-> ( P .\/ Q ) .<_ X ) )
34 33 biimpd 
 |-  ( ( K e. Lat /\ ( P e. B /\ Q e. B /\ X e. B ) ) -> ( ( P .<_ X /\ Q .<_ X ) -> ( P .\/ Q ) .<_ X ) )
35 31 32 34 sylc 
 |-  ( ( ( K e. HL /\ X e. B /\ ( M ` X ) e. N ) /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( P .<_ X /\ Q .<_ X ) ) -> ( P .\/ Q ) .<_ X )
36 35 3ad2ant1 
 |-  ( ( ( ( K e. HL /\ X e. B /\ ( M ` X ) e. N ) /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( P .<_ X /\ Q .<_ X ) ) /\ ( r e. A /\ s e. A ) /\ ( r =/= s /\ X = ( r .\/ s ) ) ) -> ( P .\/ Q ) .<_ X )
37 36 14 breqtrd 
 |-  ( ( ( ( K e. HL /\ X e. B /\ ( M ` X ) e. N ) /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( P .<_ X /\ Q .<_ X ) ) /\ ( r e. A /\ s e. A ) /\ ( r =/= s /\ X = ( r .\/ s ) ) ) -> ( P .\/ Q ) .<_ ( r .\/ s ) )
38 simpl1 
 |-  ( ( ( K e. HL /\ ( P e. A /\ Q e. A ) /\ ( r e. A /\ s e. A ) ) /\ P =/= Q ) -> K e. HL )
39 simpl2l 
 |-  ( ( ( K e. HL /\ ( P e. A /\ Q e. A ) /\ ( r e. A /\ s e. A ) ) /\ P =/= Q ) -> P e. A )
40 simpl2r 
 |-  ( ( ( K e. HL /\ ( P e. A /\ Q e. A ) /\ ( r e. A /\ s e. A ) ) /\ P =/= Q ) -> Q e. A )
41 simpr 
 |-  ( ( ( K e. HL /\ ( P e. A /\ Q e. A ) /\ ( r e. A /\ s e. A ) ) /\ P =/= Q ) -> P =/= Q )
42 simpl3 
 |-  ( ( ( K e. HL /\ ( P e. A /\ Q e. A ) /\ ( r e. A /\ s e. A ) ) /\ P =/= Q ) -> ( r e. A /\ s e. A ) )
43 2 3 4 ps-1 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( r e. A /\ s e. A ) ) -> ( ( P .\/ Q ) .<_ ( r .\/ s ) <-> ( P .\/ Q ) = ( r .\/ s ) ) )
44 38 39 40 41 42 43 syl131anc 
 |-  ( ( ( K e. HL /\ ( P e. A /\ Q e. A ) /\ ( r e. A /\ s e. A ) ) /\ P =/= Q ) -> ( ( P .\/ Q ) .<_ ( r .\/ s ) <-> ( P .\/ Q ) = ( r .\/ s ) ) )
45 44 biimpd 
 |-  ( ( ( K e. HL /\ ( P e. A /\ Q e. A ) /\ ( r e. A /\ s e. A ) ) /\ P =/= Q ) -> ( ( P .\/ Q ) .<_ ( r .\/ s ) -> ( P .\/ Q ) = ( r .\/ s ) ) )
46 22 37 45 sylc 
 |-  ( ( ( ( K e. HL /\ X e. B /\ ( M ` X ) e. N ) /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( P .<_ X /\ Q .<_ X ) ) /\ ( r e. A /\ s e. A ) /\ ( r =/= s /\ X = ( r .\/ s ) ) ) -> ( P .\/ Q ) = ( r .\/ s ) )
47 14 46 eqtr4d 
 |-  ( ( ( ( K e. HL /\ X e. B /\ ( M ` X ) e. N ) /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( P .<_ X /\ Q .<_ X ) ) /\ ( r e. A /\ s e. A ) /\ ( r =/= s /\ X = ( r .\/ s ) ) ) -> X = ( P .\/ Q ) )
48 47 3exp 
 |-  ( ( ( K e. HL /\ X e. B /\ ( M ` X ) e. N ) /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( P .<_ X /\ Q .<_ X ) ) -> ( ( r e. A /\ s e. A ) -> ( ( r =/= s /\ X = ( r .\/ s ) ) -> X = ( P .\/ Q ) ) ) )
49 48 rexlimdvv 
 |-  ( ( ( K e. HL /\ X e. B /\ ( M ` X ) e. N ) /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( P .<_ X /\ Q .<_ X ) ) -> ( E. r e. A E. s e. A ( r =/= s /\ X = ( r .\/ s ) ) -> X = ( P .\/ Q ) ) )
50 13 49 mpd 
 |-  ( ( ( K e. HL /\ X e. B /\ ( M ` X ) e. N ) /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( P .<_ X /\ Q .<_ X ) ) -> X = ( P .\/ Q ) )