atcvrlln2

Description: An atom under a line is covered by it. (Contributed by NM, 2-Jul-2012)

	Ref	Expression
Hypotheses	atcvrlln2.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	atcvrlln2.c	$⊢ C = ⋖_{K}$
	atcvrlln2.a	$⊢ A = Atoms (K)$
	atcvrlln2.n	$⊢ N = LLines (K)$
Assertion	atcvrlln2	$⊢ ((K \in HL \land P \in A \land X \in N) \land P \underset{˙}{\leq} X) \to P C X$

Proof

Step	Hyp	Ref	Expression
1		atcvrlln2.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		atcvrlln2.c	$⊢ C = ⋖_{K}$
3		atcvrlln2.a	$⊢ A = Atoms (K)$
4		atcvrlln2.n	$⊢ N = LLines (K)$
5		simpl3	$⊢ ((K \in HL \land P \in A \land X \in N) \land P \underset{˙}{\leq} X) \to X \in N$
6		simpl1	$⊢ ((K \in HL \land P \in A \land X \in N) \land P \underset{˙}{\leq} X) \to K \in HL$
7		eqid	$⊢ {Base}_{K} = {Base}_{K}$
8	7 4	llnbase	$⊢ X \in N \to X \in {Base}_{K}$
9	5 8	syl	$⊢ ((K \in HL \land P \in A \land X \in N) \land P \underset{˙}{\leq} X) \to X \in {Base}_{K}$
10		eqid	$⊢ join (K) = join (K)$
11	7 10 3 4	islln3	$⊢ (K \in HL \land X \in {Base}_{K}) \to (X \in N \leftrightarrow \exists q \in A \exists r \in A (q \neq r \land X = q join (K) r))$
12	6 9 11	syl2anc	$⊢ ((K \in HL \land P \in A \land X \in N) \land P \underset{˙}{\leq} X) \to (X \in N \leftrightarrow \exists q \in A \exists r \in A (q \neq r \land X = q join (K) r))$
13	5 12	mpbid	$⊢ ((K \in HL \land P \in A \land 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 P \in A \land 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		simp1l2	$⊢ (((K \in HL \land P \in A \land 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 P \in A \land 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 P \in A \land 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 P \in A \land 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		simp1r	$⊢ (((K \in HL \land P \in A \land 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 P \in A \land 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 P \in A \land 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	1 10 2 3	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 P \in A \land 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 P \in A \land 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 P \in A \land 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 P \in A \land 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 P \in A \land X \in N) \land P \underset{˙}{\leq} X) \to P C X$

Metamath Proof Explorer

Theorem atcvrlln2

Proof