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	$⊢ \underset{˙}{\leq} = \leq_{K}$
	lneq2at.j	$⊢ \underset{˙}{\lor} = join (K)$
	lneq2at.a	$⊢ A = Atoms (K)$
	lneq2at.n	$⊢ N = Lines (K)$
	lneq2at.m	$⊢ M = pmap (K)$
Assertion	lneq2at	$⊢ ((K \in HL \land X \in B \land M (X) \in N) \land (P \in A \land Q \in A \land P \neq Q) \land (P \underset{˙}{\leq} X \land Q \underset{˙}{\leq} X)) \to X = P \underset{˙}{\lor} Q$

Proof

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

Metamath Proof Explorer

Theorem lneq2at

Proof