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 syl6bir
 |-  ( ( 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 syl5ib
 |-  ( ( 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 syl6bir
 |-  ( ( 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 ) ) )