llnexatN

Description: Given an atom on a line, there is another atom whose join equals the line. (Contributed by NM, 26-Jun-2012) (New usage is discouraged.)

	Ref	Expression
Hypotheses	llnexat.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	llnexat.j	$⊢ \underset{˙}{\lor} = join (K)$
	llnexat.a	$⊢ A = Atoms (K)$
	llnexat.n	$⊢ N = LLines (K)$
Assertion	llnexatN	$⊢ ((K \in HL \land X \in N \land P \in A) \land P \underset{˙}{\leq} X) \to \exists q \in A (P \neq q \land X = P \underset{˙}{\lor} q)$

Proof

Step	Hyp	Ref	Expression
1		llnexat.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		llnexat.j	$⊢ \underset{˙}{\lor} = join (K)$
3		llnexat.a	$⊢ A = Atoms (K)$
4		llnexat.n	$⊢ N = LLines (K)$
5		simp1	$⊢ (K \in HL \land X \in N \land P \in A) \to K \in HL$
6		simp3	$⊢ (K \in HL \land X \in N \land P \in A) \to P \in A$
7		simp2	$⊢ (K \in HL \land X \in N \land P \in A) \to X \in N$
8	5 6 7	3jca	$⊢ (K \in HL \land X \in N \land P \in A) \to (K \in HL \land P \in A \land X \in N)$
9		eqid	$⊢ ⋖_{K} = ⋖_{K}$
10	1 9 3 4	atcvrlln2	$⊢ ((K \in HL \land P \in A \land X \in N) \land P \underset{˙}{\leq} X) \to P ⋖_{K} X$
11	8 10	sylan	$⊢ ((K \in HL \land X \in N \land P \in A) \land P \underset{˙}{\leq} X) \to P ⋖_{K} X$
12		simpl1	$⊢ ((K \in HL \land X \in N \land P \in A) \land P \underset{˙}{\leq} X) \to K \in HL$
13		simpl3	$⊢ ((K \in HL \land X \in N \land P \in A) \land P \underset{˙}{\leq} X) \to P \in A$
14		eqid	$⊢ {Base}_{K} = {Base}_{K}$
15	14 3	atbase	$⊢ P \in A \to P \in {Base}_{K}$
16	13 15	syl	$⊢ ((K \in HL \land X \in N \land P \in A) \land P \underset{˙}{\leq} X) \to P \in {Base}_{K}$
17		simpl2	$⊢ ((K \in HL \land X \in N \land P \in A) \land P \underset{˙}{\leq} X) \to X \in N$
18	14 4	llnbase	$⊢ X \in N \to X \in {Base}_{K}$
19	17 18	syl	$⊢ ((K \in HL \land X \in N \land P \in A) \land P \underset{˙}{\leq} X) \to X \in {Base}_{K}$
20	14 1 2 9 3	cvrval3	$⊢ (K \in HL \land P \in {Base}_{K} \land X \in {Base}_{K}) \to (P ⋖_{K} X \leftrightarrow \exists q \in A (\neg q \underset{˙}{\leq} P \land P \underset{˙}{\lor} q = X))$
21	12 16 19 20	syl3anc	$⊢ ((K \in HL \land X \in N \land P \in A) \land P \underset{˙}{\leq} X) \to (P ⋖_{K} X \leftrightarrow \exists q \in A (\neg q \underset{˙}{\leq} P \land P \underset{˙}{\lor} q = X))$
22		simpll1	$⊢ (((K \in HL \land X \in N \land P \in A) \land P \underset{˙}{\leq} X) \land q \in A) \to K \in HL$
23		hlatl	$⊢ K \in HL \to K \in AtLat$
24	22 23	syl	$⊢ (((K \in HL \land X \in N \land P \in A) \land P \underset{˙}{\leq} X) \land q \in A) \to K \in AtLat$
25		simpr	$⊢ (((K \in HL \land X \in N \land P \in A) \land P \underset{˙}{\leq} X) \land q \in A) \to q \in A$
26		simpll3	$⊢ (((K \in HL \land X \in N \land P \in A) \land P \underset{˙}{\leq} X) \land q \in A) \to P \in A$
27	1 3	atncmp	$⊢ (K \in AtLat \land q \in A \land P \in A) \to (\neg q \underset{˙}{\leq} P \leftrightarrow q \neq P)$
28	24 25 26 27	syl3anc	$⊢ (((K \in HL \land X \in N \land P \in A) \land P \underset{˙}{\leq} X) \land q \in A) \to (\neg q \underset{˙}{\leq} P \leftrightarrow q \neq P)$
29	28	anbi1d	$⊢ (((K \in HL \land X \in N \land P \in A) \land P \underset{˙}{\leq} X) \land q \in A) \to ((\neg q \underset{˙}{\leq} P \land P \underset{˙}{\lor} q = X) \leftrightarrow (q \neq P \land P \underset{˙}{\lor} q = X))$
30		necom	$⊢ q \neq P \leftrightarrow P \neq q$
31		eqcom	$⊢ P \underset{˙}{\lor} q = X \leftrightarrow X = P \underset{˙}{\lor} q$
32	30 31	anbi12i	$⊢ (q \neq P \land P \underset{˙}{\lor} q = X) \leftrightarrow (P \neq q \land X = P \underset{˙}{\lor} q)$
33	29 32	bitrdi	$⊢ (((K \in HL \land X \in N \land P \in A) \land P \underset{˙}{\leq} X) \land q \in A) \to ((\neg q \underset{˙}{\leq} P \land P \underset{˙}{\lor} q = X) \leftrightarrow (P \neq q \land X = P \underset{˙}{\lor} q))$
34	33	rexbidva	$⊢ ((K \in HL \land X \in N \land P \in A) \land P \underset{˙}{\leq} X) \to (\exists q \in A (\neg q \underset{˙}{\leq} P \land P \underset{˙}{\lor} q = X) \leftrightarrow \exists q \in A (P \neq q \land X = P \underset{˙}{\lor} q))$
35	21 34	bitrd	$⊢ ((K \in HL \land X \in N \land P \in A) \land P \underset{˙}{\leq} X) \to (P ⋖_{K} X \leftrightarrow \exists q \in A (P \neq q \land X = P \underset{˙}{\lor} q))$
36	11 35	mpbid	$⊢ ((K \in HL \land X \in N \land P \in A) \land P \underset{˙}{\leq} X) \to \exists q \in A (P \neq q \land X = P \underset{˙}{\lor} q)$

Metamath Proof Explorer

Theorem llnexatN

Proof