lncvrat

Description: A line covers the atoms it contains. (Contributed by NM, 30-Apr-2012)

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

Proof

Step	Hyp	Ref	Expression
1		lncvrat.b	$⊢ B = {Base}_{K}$
2		lncvrat.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		lncvrat.c	$⊢ C = ⋖_{K}$
4		lncvrat.a	$⊢ A = Atoms (K)$
5		lncvrat.n	$⊢ N = Lines (K)$
6		lncvrat.m	$⊢ M = pmap (K)$
7		simprl	$⊢ ((K \in HL \land X \in B \land P \in A) \land (M (X) \in N \land P \underset{˙}{\leq} X)) \to M (X) \in N$
8		simpl1	$⊢ ((K \in HL \land X \in B \land P \in A) \land (M (X) \in N \land P \underset{˙}{\leq} X)) \to K \in HL$
9		simpl2	$⊢ ((K \in HL \land X \in B \land P \in A) \land (M (X) \in N \land P \underset{˙}{\leq} X)) \to X \in B$
10		eqid	$⊢ join (K) = join (K)$
11	1 10 4 5 6	isline3	$⊢ (K \in HL \land X \in B) \to (M (X) \in N \leftrightarrow \exists q \in A \exists r \in A (q \neq r \land X = q join (K) r))$
12	8 9 11	syl2anc	$⊢ ((K \in HL \land X \in B \land P \in A) \land (M (X) \in N \land P \underset{˙}{\leq} X)) \to (M (X) \in N \leftrightarrow \exists q \in A \exists r \in A (q \neq r \land X = q join (K) r))$
13	7 12	mpbid	$⊢ ((K \in HL \land X \in B \land P \in A) \land (M (X) \in N \land P \underset{˙}{\leq} X)) \to \exists q \in A \exists r \in A (q \neq r \land X = q join (K) r)$
14		simp1l1	$⊢ (((K \in HL \land X \in B \land P \in A) \land (M (X) \in N \land P \underset{˙}{\leq} X)) \land (q \in A \land r \in A) \land (q \neq r \land X = q join (K) r)) \to K \in HL$
15		simp1l3	$⊢ (((K \in HL \land X \in B \land P \in A) \land (M (X) \in N \land P \underset{˙}{\leq} X)) \land (q \in A \land r \in A) \land (q \neq r \land X = q join (K) r)) \to P \in A$
16		simp2l	$⊢ (((K \in HL \land X \in B \land P \in A) \land (M (X) \in N \land P \underset{˙}{\leq} X)) \land (q \in A \land r \in A) \land (q \neq r \land X = q join (K) r)) \to q \in A$
17		simp2r	$⊢ (((K \in HL \land X \in B \land P \in A) \land (M (X) \in N \land P \underset{˙}{\leq} X)) \land (q \in A \land r \in A) \land (q \neq r \land X = q join (K) r)) \to r \in A$
18		simp3l	$⊢ (((K \in HL \land X \in B \land P \in A) \land (M (X) \in N \land P \underset{˙}{\leq} X)) \land (q \in A \land r \in A) \land (q \neq r \land X = q join (K) r)) \to q \neq r$
19		simp1rr	$⊢ (((K \in HL \land X \in B \land P \in A) \land (M (X) \in N \land P \underset{˙}{\leq} X)) \land (q \in A \land r \in A) \land (q \neq r \land X = q join (K) r)) \to P \underset{˙}{\leq} X$
20		simp3r	$⊢ (((K \in HL \land X \in B \land P \in A) \land (M (X) \in N \land P \underset{˙}{\leq} X)) \land (q \in A \land r \in A) \land (q \neq r \land X = q join (K) r)) \to X = q join (K) r$
21	19 20	breqtrd	$⊢ (((K \in HL \land X \in B \land P \in A) \land (M (X) \in N \land P \underset{˙}{\leq} X)) \land (q \in A \land r \in A) \land (q \neq r \land X = q join (K) r)) \to P \underset{˙}{\leq} (q join (K) r)$
22	2 10 3 4	atcvrj2	$⊢ (K \in HL \land (P \in A \land q \in A \land r \in A) \land (q \neq r \land P \underset{˙}{\leq} (q join (K) r))) \to P C (q join (K) r)$
23	14 15 16 17 18 21 22	syl132anc	$⊢ (((K \in HL \land X \in B \land P \in A) \land (M (X) \in N \land P \underset{˙}{\leq} X)) \land (q \in A \land r \in A) \land (q \neq r \land X = q join (K) r)) \to P C (q join (K) r)$
24	23 20	breqtrrd	$⊢ (((K \in HL \land X \in B \land P \in A) \land (M (X) \in N \land P \underset{˙}{\leq} X)) \land (q \in A \land r \in A) \land (q \neq r \land X = q join (K) r)) \to P C X$
25	24	3exp	$⊢ ((K \in HL \land X \in B \land P \in A) \land (M (X) \in N \land P \underset{˙}{\leq} X)) \to ((q \in A \land r \in A) \to ((q \neq r \land X = q join (K) r) \to P C X))$
26	25	rexlimdvv	$⊢ ((K \in HL \land X \in B \land P \in A) \land (M (X) \in N \land P \underset{˙}{\leq} X)) \to (\exists q \in A \exists r \in A (q \neq r \land X = q join (K) r) \to P C X)$
27	13 26	mpd	$⊢ ((K \in HL \land X \in B \land P \in A) \land (M (X) \in N \land P \underset{˙}{\leq} X)) \to P C X$

Metamath Proof Explorer

Theorem lncvrat

Proof