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 ˙ = K
ps1.j ˙ = join K
ps1.a A = Atoms K
Assertion ps-1 K HL P A Q A P Q R A S A P ˙ Q ˙ R ˙ S P ˙ Q = R ˙ S

Proof

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