lnatexN

Description: There is an atom in a line different from any other. (Contributed by NM, 30-Apr-2012) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		lnatex.b	$⊢ B = {Base}_{K}$
2		lnatex.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		lnatex.a	$⊢ A = Atoms (K)$
4		lnatex.n	$⊢ N = Lines (K)$
5		lnatex.m	$⊢ M = pmap (K)$
6		eqid	$⊢ join (K) = join (K)$
7	1 6 3 4 5	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 join (K) s))$
8	7	biimp3a	$⊢ (K \in HL \land X \in B \land M (X) \in N) \to \exists r \in A \exists s \in A (r \neq s \land X = r join (K) s)$
9		simpl2r	$⊢ (((K \in HL \land X \in B \land M (X) \in N) \land (r \in A \land s \in A) \land (r \neq s \land X = r join (K) s)) \land r = P) \to s \in A$
10		simpl3l	$⊢ (((K \in HL \land X \in B \land M (X) \in N) \land (r \in A \land s \in A) \land (r \neq s \land X = r join (K) s)) \land r = P) \to r \neq s$
11	10	necomd	$⊢ (((K \in HL \land X \in B \land M (X) \in N) \land (r \in A \land s \in A) \land (r \neq s \land X = r join (K) s)) \land r = P) \to s \neq r$
12		simpr	$⊢ (((K \in HL \land X \in B \land M (X) \in N) \land (r \in A \land s \in A) \land (r \neq s \land X = r join (K) s)) \land r = P) \to r = P$
13	11 12	neeqtrd	$⊢ (((K \in HL \land X \in B \land M (X) \in N) \land (r \in A \land s \in A) \land (r \neq s \land X = r join (K) s)) \land r = P) \to s \neq P$
14		simpl11	$⊢ (((K \in HL \land X \in B \land M (X) \in N) \land (r \in A \land s \in A) \land (r \neq s \land X = r join (K) s)) \land r = P) \to K \in HL$
15		simpl2l	$⊢ (((K \in HL \land X \in B \land M (X) \in N) \land (r \in A \land s \in A) \land (r \neq s \land X = r join (K) s)) \land r = P) \to r \in A$
16	2 6 3	hlatlej2	$⊢ (K \in HL \land r \in A \land s \in A) \to s \underset{˙}{\leq} (r join (K) s)$
17	14 15 9 16	syl3anc	$⊢ (((K \in HL \land X \in B \land M (X) \in N) \land (r \in A \land s \in A) \land (r \neq s \land X = r join (K) s)) \land r = P) \to s \underset{˙}{\leq} (r join (K) s)$
18		simpl3r	$⊢ (((K \in HL \land X \in B \land M (X) \in N) \land (r \in A \land s \in A) \land (r \neq s \land X = r join (K) s)) \land r = P) \to X = r join (K) s$
19	17 18	breqtrrd	$⊢ (((K \in HL \land X \in B \land M (X) \in N) \land (r \in A \land s \in A) \land (r \neq s \land X = r join (K) s)) \land r = P) \to s \underset{˙}{\leq} X$
20		neeq1	$⊢ q = s \to (q \neq P \leftrightarrow s \neq P)$
21		breq1	$⊢ q = s \to (q \underset{˙}{\leq} X \leftrightarrow s \underset{˙}{\leq} X)$
22	20 21	anbi12d	$⊢ q = s \to ((q \neq P \land q \underset{˙}{\leq} X) \leftrightarrow (s \neq P \land s \underset{˙}{\leq} X))$
23	22	rspcev	$⊢ (s \in A \land (s \neq P \land s \underset{˙}{\leq} X)) \to \exists q \in A (q \neq P \land q \underset{˙}{\leq} X)$
24	9 13 19 23	syl12anc	$⊢ (((K \in HL \land X \in B \land M (X) \in N) \land (r \in A \land s \in A) \land (r \neq s \land X = r join (K) s)) \land r = P) \to \exists q \in A (q \neq P \land q \underset{˙}{\leq} X)$
25		simpl2l	$⊢ (((K \in HL \land X \in B \land M (X) \in N) \land (r \in A \land s \in A) \land (r \neq s \land X = r join (K) s)) \land r \neq P) \to r \in A$
26		simpr	$⊢ (((K \in HL \land X \in B \land M (X) \in N) \land (r \in A \land s \in A) \land (r \neq s \land X = r join (K) s)) \land r \neq P) \to r \neq P$
27		simpl11	$⊢ (((K \in HL \land X \in B \land M (X) \in N) \land (r \in A \land s \in A) \land (r \neq s \land X = r join (K) s)) \land r \neq P) \to K \in HL$
28		simpl2r	$⊢ (((K \in HL \land X \in B \land M (X) \in N) \land (r \in A \land s \in A) \land (r \neq s \land X = r join (K) s)) \land r \neq P) \to s \in A$
29	2 6 3	hlatlej1	$⊢ (K \in HL \land r \in A \land s \in A) \to r \underset{˙}{\leq} (r join (K) s)$
30	27 25 28 29	syl3anc	$⊢ (((K \in HL \land X \in B \land M (X) \in N) \land (r \in A \land s \in A) \land (r \neq s \land X = r join (K) s)) \land r \neq P) \to r \underset{˙}{\leq} (r join (K) s)$
31		simpl3r	$⊢ (((K \in HL \land X \in B \land M (X) \in N) \land (r \in A \land s \in A) \land (r \neq s \land X = r join (K) s)) \land r \neq P) \to X = r join (K) s$
32	30 31	breqtrrd	$⊢ (((K \in HL \land X \in B \land M (X) \in N) \land (r \in A \land s \in A) \land (r \neq s \land X = r join (K) s)) \land r \neq P) \to r \underset{˙}{\leq} X$
33		neeq1	$⊢ q = r \to (q \neq P \leftrightarrow r \neq P)$
34		breq1	$⊢ q = r \to (q \underset{˙}{\leq} X \leftrightarrow r \underset{˙}{\leq} X)$
35	33 34	anbi12d	$⊢ q = r \to ((q \neq P \land q \underset{˙}{\leq} X) \leftrightarrow (r \neq P \land r \underset{˙}{\leq} X))$
36	35	rspcev	$⊢ (r \in A \land (r \neq P \land r \underset{˙}{\leq} X)) \to \exists q \in A (q \neq P \land q \underset{˙}{\leq} X)$
37	25 26 32 36	syl12anc	$⊢ (((K \in HL \land X \in B \land M (X) \in N) \land (r \in A \land s \in A) \land (r \neq s \land X = r join (K) s)) \land r \neq P) \to \exists q \in A (q \neq P \land q \underset{˙}{\leq} X)$
38	24 37	pm2.61dane	$⊢ ((K \in HL \land X \in B \land M (X) \in N) \land (r \in A \land s \in A) \land (r \neq s \land X = r join (K) s)) \to \exists q \in A (q \neq P \land q \underset{˙}{\leq} X)$
39	38	3exp	$⊢ (K \in HL \land X \in B \land M (X) \in N) \to ((r \in A \land s \in A) \to ((r \neq s \land X = r join (K) s) \to \exists q \in A (q \neq P \land q \underset{˙}{\leq} X)))$
40	39	rexlimdvv	$⊢ (K \in HL \land X \in B \land M (X) \in N) \to (\exists r \in A \exists s \in A (r \neq s \land X = r join (K) s) \to \exists q \in A (q \neq P \land q \underset{˙}{\leq} X))$
41	8 40	mpd	$⊢ (K \in HL \land X \in B \land M (X) \in N) \to \exists q \in A (q \neq P \land q \underset{˙}{\leq} X)$

Metamath Proof Explorer

Theorem lnatexN

Proof