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	$⊢ \underset{˙}{\leq} = \leq_{K}$
	ps1.j	$⊢ \underset{˙}{\lor} = join (K)$
	ps1.a	$⊢ A = Atoms (K)$
Assertion	ps-1	$⊢ (K \in HL \land (P \in A \land Q \in A \land P \neq Q) \land (R \in A \land S \in A)) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\leq} (R \underset{˙}{\lor} S) \leftrightarrow P \underset{˙}{\lor} Q = R \underset{˙}{\lor} S)$

Proof

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

Metamath Proof Explorer

Theorem ps-1

Proof