lncvrelatN

Description: A lattice element covered by a line is an atom. (Contributed by NM, 28-Apr-2012) (New usage is discouraged.)

	Ref	Expression
Hypotheses	lncvrelat.b	$⊢ B = {Base}_{K}$
	lncvrelat.c	$⊢ C = ⋖_{K}$
	lncvrelat.a	$⊢ A = Atoms (K)$
	lncvrelat.n	$⊢ N = Lines (K)$
	lncvrelat.m	$⊢ M = pmap (K)$
Assertion	lncvrelatN	$⊢ ((K \in HL \land X \in B \land P \in B) \land (M (X) \in N \land P C X)) \to P \in A$

Proof

Step	Hyp	Ref	Expression
1		lncvrelat.b	$⊢ B = {Base}_{K}$
2		lncvrelat.c	$⊢ C = ⋖_{K}$
3		lncvrelat.a	$⊢ A = Atoms (K)$
4		lncvrelat.n	$⊢ N = Lines (K)$
5		lncvrelat.m	$⊢ M = pmap (K)$
6		hllat	$⊢ K \in HL \to K \in Lat$
7	6	3ad2ant1	$⊢ (K \in HL \land X \in B \land P \in B) \to K \in Lat$
8		eqid	$⊢ join (K) = join (K)$
9	8 3 4 5	isline2	$⊢ K \in Lat \to (M (X) \in N \leftrightarrow \exists q \in A \exists r \in A (q \neq r \land M (X) = M (q join (K) r)))$
10	7 9	syl	$⊢ (K \in HL \land X \in B \land P \in B) \to (M (X) \in N \leftrightarrow \exists q \in A \exists r \in A (q \neq r \land M (X) = M (q join (K) r)))$
11		simpll1	$⊢ (((K \in HL \land X \in B \land P \in B) \land (q \in A \land r \in A)) \land q \neq r) \to K \in HL$
12		simpll2	$⊢ (((K \in HL \land X \in B \land P \in B) \land (q \in A \land r \in A)) \land q \neq r) \to X \in B$
13	11 6	syl	$⊢ (((K \in HL \land X \in B \land P \in B) \land (q \in A \land r \in A)) \land q \neq r) \to K \in Lat$
14		simplrl	$⊢ (((K \in HL \land X \in B \land P \in B) \land (q \in A \land r \in A)) \land q \neq r) \to q \in A$
15	1 3	atbase	$⊢ q \in A \to q \in B$
16	14 15	syl	$⊢ (((K \in HL \land X \in B \land P \in B) \land (q \in A \land r \in A)) \land q \neq r) \to q \in B$
17		simplrr	$⊢ (((K \in HL \land X \in B \land P \in B) \land (q \in A \land r \in A)) \land q \neq r) \to r \in A$
18	1 3	atbase	$⊢ r \in A \to r \in B$
19	17 18	syl	$⊢ (((K \in HL \land X \in B \land P \in B) \land (q \in A \land r \in A)) \land q \neq r) \to r \in B$
20	1 8	latjcl	$⊢ (K \in Lat \land q \in B \land r \in B) \to q join (K) r \in B$
21	13 16 19 20	syl3anc	$⊢ (((K \in HL \land X \in B \land P \in B) \land (q \in A \land r \in A)) \land q \neq r) \to q join (K) r \in B$
22	1 5	pmap11	$⊢ (K \in HL \land X \in B \land q join (K) r \in B) \to (M (X) = M (q join (K) r) \leftrightarrow X = q join (K) r)$
23	11 12 21 22	syl3anc	$⊢ (((K \in HL \land X \in B \land P \in B) \land (q \in A \land r \in A)) \land q \neq r) \to (M (X) = M (q join (K) r) \leftrightarrow X = q join (K) r)$
24		breq2	$⊢ X = q join (K) r \to (P C X \leftrightarrow P C (q join (K) r))$
25	24	biimpd	$⊢ X = q join (K) r \to (P C X \to P C (q join (K) r))$
26	11	adantr	$⊢ ((((K \in HL \land X \in B \land P \in B) \land (q \in A \land r \in A)) \land q \neq r) \land P C (q join (K) r)) \to K \in HL$
27		simpll3	$⊢ (((K \in HL \land X \in B \land P \in B) \land (q \in A \land r \in A)) \land q \neq r) \to P \in B$
28	27 14 17	3jca	$⊢ (((K \in HL \land X \in B \land P \in B) \land (q \in A \land r \in A)) \land q \neq r) \to (P \in B \land q \in A \land r \in A)$
29	28	adantr	$⊢ ((((K \in HL \land X \in B \land P \in B) \land (q \in A \land r \in A)) \land q \neq r) \land P C (q join (K) r)) \to (P \in B \land q \in A \land r \in A)$
30		simplr	$⊢ ((((K \in HL \land X \in B \land P \in B) \land (q \in A \land r \in A)) \land q \neq r) \land P C (q join (K) r)) \to q \neq r$
31		simpr	$⊢ ((((K \in HL \land X \in B \land P \in B) \land (q \in A \land r \in A)) \land q \neq r) \land P C (q join (K) r)) \to P C (q join (K) r)$
32	1 8 2 3	cvrat2	$⊢ (K \in HL \land (P \in B \land q \in A \land r \in A) \land (q \neq r \land P C (q join (K) r))) \to P \in A$
33	26 29 30 31 32	syl112anc	$⊢ ((((K \in HL \land X \in B \land P \in B) \land (q \in A \land r \in A)) \land q \neq r) \land P C (q join (K) r)) \to P \in A$
34	33	ex	$⊢ (((K \in HL \land X \in B \land P \in B) \land (q \in A \land r \in A)) \land q \neq r) \to (P C (q join (K) r) \to P \in A)$
35	25 34	syl9r	$⊢ (((K \in HL \land X \in B \land P \in B) \land (q \in A \land r \in A)) \land q \neq r) \to (X = q join (K) r \to (P C X \to P \in A))$
36	23 35	sylbid	$⊢ (((K \in HL \land X \in B \land P \in B) \land (q \in A \land r \in A)) \land q \neq r) \to (M (X) = M (q join (K) r) \to (P C X \to P \in A))$
37	36	expimpd	$⊢ ((K \in HL \land X \in B \land P \in B) \land (q \in A \land r \in A)) \to ((q \neq r \land M (X) = M (q join (K) r)) \to (P C X \to P \in A))$
38	37	rexlimdvva	$⊢ (K \in HL \land X \in B \land P \in B) \to (\exists q \in A \exists r \in A (q \neq r \land M (X) = M (q join (K) r)) \to (P C X \to P \in A))$
39	10 38	sylbid	$⊢ (K \in HL \land X \in B \land P \in B) \to (M (X) \in N \to (P C X \to P \in A))$
40	39	imp32	$⊢ ((K \in HL \land X \in B \land P \in B) \land (M (X) \in N \land P C X)) \to P \in A$

Metamath Proof Explorer

Theorem lncvrelatN

Proof