Metamath Proof Explorer

Theorem ps-1

Description: The join of two atoms R .\/ S (specifying a projective geometry line) is determined uniquely by any two atoms (specifying two points) less than or equal to that join. Part of Lemma 16.4 of MaedaMaeda p. 69, showing projective space postulate PS1 in MaedaMaeda p. 67. (Contributed by NM, 15-Nov-2011)

Ref Expression
Hypotheses ps1.l 
|- .<_ = ( le ` K )
ps1.j 
|- .\/ = ( join ` K )
ps1.a 
|- A = ( Atoms ` K )
Assertion 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 ) ) )

Proof

Step Hyp Ref Expression
1 ps1.l 
 |-  .<_ = ( le ` K )
2 ps1.j 
 |-  .\/ = ( join ` K )
3 ps1.a 
 |-  A = ( Atoms ` K )
4 oveq1 
 |-  ( R = P -> ( R .\/ S ) = ( P .\/ S ) )
5 4 breq2d 
 |-  ( R = P -> ( ( P .\/ Q ) .<_ ( R .\/ S ) <-> ( P .\/ Q ) .<_ ( P .\/ S ) ) )
6 4 eqeq2d 
 |-  ( R = P -> ( ( P .\/ Q ) = ( R .\/ S ) <-> ( P .\/ Q ) = ( P .\/ S ) ) )
7 5 6 imbi12d 
 |-  ( R = P -> ( ( ( P .\/ Q ) .<_ ( R .\/ S ) -> ( P .\/ Q ) = ( R .\/ S ) ) <-> ( ( P .\/ Q ) .<_ ( P .\/ S ) -> ( P .\/ Q ) = ( P .\/ S ) ) ) )
8 7 eqcoms 
 |-  ( P = R -> ( ( ( P .\/ Q ) .<_ ( R .\/ S ) -> ( P .\/ Q ) = ( R .\/ S ) ) <-> ( ( P .\/ Q ) .<_ ( P .\/ S ) -> ( P .\/ Q ) = ( P .\/ S ) ) ) )
9 simp3 
 |-  ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( R e. A /\ S e. A ) ) /\ P =/= R /\ ( P .\/ Q ) .<_ ( R .\/ S ) ) -> ( P .\/ Q ) .<_ ( R .\/ S ) )
10 simp1 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( R e. A /\ S e. A ) ) -> K e. HL )
11 simp21 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( R e. A /\ S e. A ) ) -> P e. A )
12 simp3l 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( R e. A /\ S e. A ) ) -> R e. A )
13 2 3 hlatjcom 
 |-  ( ( K e. HL /\ P e. A /\ R e. A ) -> ( P .\/ R ) = ( R .\/ P ) )
14 10 11 12 13 syl3anc 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( R e. A /\ S e. A ) ) -> ( P .\/ R ) = ( R .\/ P ) )
15 14 3ad2ant1 
 |-  ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( R e. A /\ S e. A ) ) /\ P =/= R /\ ( P .\/ Q ) .<_ ( R .\/ S ) ) -> ( P .\/ R ) = ( R .\/ P ) )
16 hllat 
 |-  ( K e. HL -> K e. Lat )
17 16 3ad2ant1 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( R e. A /\ S e. A ) ) -> K e. Lat )
18 eqid 
 |-  ( Base ` K ) = ( Base ` K )
19 18 3 atbase 
 |-  ( P e. A -> P e. ( Base ` K ) )
20 11 19 syl 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( R e. A /\ S e. A ) ) -> P e. ( Base ` K ) )
21 simp22 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( R e. A /\ S e. A ) ) -> Q e. A )
22 18 3 atbase 
 |-  ( Q e. A -> Q e. ( Base ` K ) )
23 21 22 syl 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( R e. A /\ S e. A ) ) -> Q e. ( Base ` K ) )
24 simp3r 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( R e. A /\ S e. A ) ) -> S e. A )
25 18 2 3 hlatjcl 
 |-  ( ( K e. HL /\ R e. A /\ S e. A ) -> ( R .\/ S ) e. ( Base ` K ) )
26 10 12 24 25 syl3anc 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( R e. A /\ S e. A ) ) -> ( R .\/ S ) e. ( Base ` K ) )
27 18 1 2 latjle12 
 |-  ( ( K e. Lat /\ ( P e. ( Base ` K ) /\ Q e. ( Base ` K ) /\ ( R .\/ S ) e. ( Base ` K ) ) ) -> ( ( P .<_ ( R .\/ S ) /\ Q .<_ ( R .\/ S ) ) <-> ( P .\/ Q ) .<_ ( R .\/ S ) ) )
28 17 20 23 26 27 syl13anc 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( R e. A /\ S e. A ) ) -> ( ( P .<_ ( R .\/ S ) /\ Q .<_ ( R .\/ S ) ) <-> ( P .\/ Q ) .<_ ( R .\/ S ) ) )
29 simpl 
 |-  ( ( P .<_ ( R .\/ S ) /\ Q .<_ ( R .\/ S ) ) -> P .<_ ( R .\/ S ) )
30 28 29 biimtrrdi 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( R e. A /\ S e. A ) ) -> ( ( P .\/ Q ) .<_ ( R .\/ S ) -> P .<_ ( R .\/ S ) ) )
31 30 adantr 
 |-  ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( R e. A /\ S e. A ) ) /\ P =/= R ) -> ( ( P .\/ Q ) .<_ ( R .\/ S ) -> P .<_ ( R .\/ S ) ) )
32 simpl1 
 |-  ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( R e. A /\ S e. A ) ) /\ P =/= R ) -> K e. HL )
33 simpl21 
 |-  ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( R e. A /\ S e. A ) ) /\ P =/= R ) -> P e. A )
34 simpl3r 
 |-  ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( R e. A /\ S e. A ) ) /\ P =/= R ) -> S e. A )
35 simpl3l 
 |-  ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( R e. A /\ S e. A ) ) /\ P =/= R ) -> R e. A )
36 simpr 
 |-  ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( R e. A /\ S e. A ) ) /\ P =/= R ) -> P =/= R )
37 1 2 3 hlatexchb1 
 |-  ( ( K e. HL /\ ( P e. A /\ S e. A /\ R e. A ) /\ P =/= R ) -> ( P .<_ ( R .\/ S ) <-> ( R .\/ P ) = ( R .\/ S ) ) )
38 32 33 34 35 36 37 syl131anc 
 |-  ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( R e. A /\ S e. A ) ) /\ P =/= R ) -> ( P .<_ ( R .\/ S ) <-> ( R .\/ P ) = ( R .\/ S ) ) )
39 31 38 sylibd 
 |-  ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( R e. A /\ S e. A ) ) /\ P =/= R ) -> ( ( P .\/ Q ) .<_ ( R .\/ S ) -> ( R .\/ P ) = ( R .\/ S ) ) )
40 39 3impia 
 |-  ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( R e. A /\ S e. A ) ) /\ P =/= R /\ ( P .\/ Q ) .<_ ( R .\/ S ) ) -> ( R .\/ P ) = ( R .\/ S ) )
41 15 40 eqtrd 
 |-  ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( R e. A /\ S e. A ) ) /\ P =/= R /\ ( P .\/ Q ) .<_ ( R .\/ S ) ) -> ( P .\/ R ) = ( R .\/ S ) )
42 9 41 breqtrrd 
 |-  ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( R e. A /\ S e. A ) ) /\ P =/= R /\ ( P .\/ Q ) .<_ ( R .\/ S ) ) -> ( P .\/ Q ) .<_ ( P .\/ R ) )
43 42 3expia 
 |-  ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( R e. A /\ S e. A ) ) /\ P =/= R ) -> ( ( P .\/ Q ) .<_ ( R .\/ S ) -> ( P .\/ Q ) .<_ ( P .\/ R ) ) )
44 18 2 3 hlatjcl 
 |-  ( ( K e. HL /\ P e. A /\ R e. A ) -> ( P .\/ R ) e. ( Base ` K ) )
45 10 11 12 44 syl3anc 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( R e. A /\ S e. A ) ) -> ( P .\/ R ) e. ( Base ` K ) )
46 18 1 2 latjle12 
 |-  ( ( K e. Lat /\ ( P e. ( Base ` K ) /\ Q e. ( Base ` K ) /\ ( P .\/ R ) e. ( Base ` K ) ) ) -> ( ( P .<_ ( P .\/ R ) /\ Q .<_ ( P .\/ R ) ) <-> ( P .\/ Q ) .<_ ( P .\/ R ) ) )
47 17 20 23 45 46 syl13anc 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( R e. A /\ S e. A ) ) -> ( ( P .<_ ( P .\/ R ) /\ Q .<_ ( P .\/ R ) ) <-> ( P .\/ Q ) .<_ ( P .\/ R ) ) )
48 simpr 
 |-  ( ( P .<_ ( P .\/ R ) /\ Q .<_ ( P .\/ R ) ) -> Q .<_ ( P .\/ R ) )
49 simp23 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( R e. A /\ S e. A ) ) -> P =/= Q )
50 49 necomd 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( R e. A /\ S e. A ) ) -> Q =/= P )
51 1 2 3 hlatexchb1 
 |-  ( ( K e. HL /\ ( Q e. A /\ R e. A /\ P e. A ) /\ Q =/= P ) -> ( Q .<_ ( P .\/ R ) <-> ( P .\/ Q ) = ( P .\/ R ) ) )
52 10 21 12 11 50 51 syl131anc 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( R e. A /\ S e. A ) ) -> ( Q .<_ ( P .\/ R ) <-> ( P .\/ Q ) = ( P .\/ R ) ) )
53 48 52 imbitrid 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( R e. A /\ S e. A ) ) -> ( ( P .<_ ( P .\/ R ) /\ Q .<_ ( P .\/ R ) ) -> ( P .\/ Q ) = ( P .\/ R ) ) )
54 47 53 sylbird 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( R e. A /\ S e. A ) ) -> ( ( P .\/ Q ) .<_ ( P .\/ R ) -> ( P .\/ Q ) = ( P .\/ R ) ) )
55 54 adantr 
 |-  ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( R e. A /\ S e. A ) ) /\ P =/= R ) -> ( ( P .\/ Q ) .<_ ( P .\/ R ) -> ( P .\/ Q ) = ( P .\/ R ) ) )
56 43 55 syld 
 |-  ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( R e. A /\ S e. A ) ) /\ P =/= R ) -> ( ( P .\/ Q ) .<_ ( R .\/ S ) -> ( P .\/ Q ) = ( P .\/ R ) ) )
57 56 3impia 
 |-  ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( R e. A /\ S e. A ) ) /\ P =/= R /\ ( P .\/ Q ) .<_ ( R .\/ S ) ) -> ( P .\/ Q ) = ( P .\/ R ) )
58 57 41 eqtrd 
 |-  ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( R e. A /\ S e. A ) ) /\ P =/= R /\ ( P .\/ Q ) .<_ ( R .\/ S ) ) -> ( P .\/ Q ) = ( R .\/ S ) )
59 58 3expia 
 |-  ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( R e. A /\ S e. A ) ) /\ P =/= R ) -> ( ( P .\/ Q ) .<_ ( R .\/ S ) -> ( P .\/ Q ) = ( R .\/ S ) ) )
60 18 2 3 hlatjcl 
 |-  ( ( K e. HL /\ P e. A /\ S e. A ) -> ( P .\/ S ) e. ( Base ` K ) )
61 10 11 24 60 syl3anc 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( R e. A /\ S e. A ) ) -> ( P .\/ S ) e. ( Base ` K ) )
62 18 1 2 latjle12 
 |-  ( ( K e. Lat /\ ( P e. ( Base ` K ) /\ Q e. ( Base ` K ) /\ ( P .\/ S ) e. ( Base ` K ) ) ) -> ( ( P .<_ ( P .\/ S ) /\ Q .<_ ( P .\/ S ) ) <-> ( P .\/ Q ) .<_ ( P .\/ S ) ) )
63 17 20 23 61 62 syl13anc 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( R e. A /\ S e. A ) ) -> ( ( P .<_ ( P .\/ S ) /\ Q .<_ ( P .\/ S ) ) <-> ( P .\/ Q ) .<_ ( P .\/ S ) ) )
64 simpr 
 |-  ( ( P .<_ ( P .\/ S ) /\ Q .<_ ( P .\/ S ) ) -> Q .<_ ( P .\/ S ) )
65 63 64 biimtrrdi 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( R e. A /\ S e. A ) ) -> ( ( P .\/ Q ) .<_ ( P .\/ S ) -> Q .<_ ( P .\/ S ) ) )
66 1 2 3 hlatexchb1 
 |-  ( ( K e. HL /\ ( Q e. A /\ S e. A /\ P e. A ) /\ Q =/= P ) -> ( Q .<_ ( P .\/ S ) <-> ( P .\/ Q ) = ( P .\/ S ) ) )
67 10 21 24 11 50 66 syl131anc 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( R e. A /\ S e. A ) ) -> ( Q .<_ ( P .\/ S ) <-> ( P .\/ Q ) = ( P .\/ S ) ) )
68 65 67 sylibd 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( R e. A /\ S e. A ) ) -> ( ( P .\/ Q ) .<_ ( P .\/ S ) -> ( P .\/ Q ) = ( P .\/ S ) ) )
69 8 59 68 pm2.61ne 
 |-  ( ( 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 ) ) )
70 18 2 3 hlatjcl 
 |-  ( ( K e. HL /\ P e. A /\ Q e. A ) -> ( P .\/ Q ) e. ( Base ` K ) )
71 10 11 21 70 syl3anc 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( R e. A /\ S e. A ) ) -> ( P .\/ Q ) e. ( Base ` K ) )
72 18 1 latref 
 |-  ( ( K e. Lat /\ ( P .\/ Q ) e. ( Base ` K ) ) -> ( P .\/ Q ) .<_ ( P .\/ Q ) )
73 17 71 72 syl2anc 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( R e. A /\ S e. A ) ) -> ( P .\/ Q ) .<_ ( P .\/ Q ) )
74 breq2 
 |-  ( ( P .\/ Q ) = ( R .\/ S ) -> ( ( P .\/ Q ) .<_ ( P .\/ Q ) <-> ( P .\/ Q ) .<_ ( R .\/ S ) ) )
75 73 74 syl5ibcom 
 |-  ( ( 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 ) ) )
76 69 75 impbid 
 |-  ( ( 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 ) ) )