llnnleat

Description: An atom cannot majorize a lattice line. (Contributed by NM, 8-Jul-2012)

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

Proof

Step	Hyp	Ref	Expression
1		llnnleat.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		llnnleat.a	$⊢ A = Atoms (K)$
3		llnnleat.n	$⊢ N = LLines (K)$
4		simp2	$⊢ (K \in HL \land X \in N \land P \in A) \to X \in N$
5		eqid	$⊢ {Base}_{K} = {Base}_{K}$
6		eqid	$⊢ ⋖_{K} = ⋖_{K}$
7	5 6 2 3	islln	$⊢ K \in HL \to (X \in N \leftrightarrow (X \in {Base}_{K} \land \exists q \in A q ⋖_{K} X))$
8	7	3ad2ant1	$⊢ (K \in HL \land X \in N \land P \in A) \to (X \in N \leftrightarrow (X \in {Base}_{K} \land \exists q \in A q ⋖_{K} X))$
9	4 8	mpbid	$⊢ (K \in HL \land X \in N \land P \in A) \to (X \in {Base}_{K} \land \exists q \in A q ⋖_{K} X)$
10	9	simprd	$⊢ (K \in HL \land X \in N \land P \in A) \to \exists q \in A q ⋖_{K} X$
11		simp11	$⊢ ((K \in HL \land X \in N \land P \in A) \land q \in A \land q ⋖_{K} X) \to K \in HL$
12		hlatl	$⊢ K \in HL \to K \in AtLat$
13	11 12	syl	$⊢ ((K \in HL \land X \in N \land P \in A) \land q \in A \land q ⋖_{K} X) \to K \in AtLat$
14		simp2	$⊢ ((K \in HL \land X \in N \land P \in A) \land q \in A \land q ⋖_{K} X) \to q \in A$
15		simp13	$⊢ ((K \in HL \land X \in N \land P \in A) \land q \in A \land q ⋖_{K} X) \to P \in A$
16		eqid	$⊢ <_{K} = <_{K}$
17	16 2	atnlt	$⊢ (K \in AtLat \land q \in A \land P \in A) \to \neg q <_{K} P$
18	13 14 15 17	syl3anc	$⊢ ((K \in HL \land X \in N \land P \in A) \land q \in A \land q ⋖_{K} X) \to \neg q <_{K} P$
19	5 2	atbase	$⊢ q \in A \to q \in {Base}_{K}$
20	19	3ad2ant2	$⊢ ((K \in HL \land X \in N \land P \in A) \land q \in A \land q ⋖_{K} X) \to q \in {Base}_{K}$
21		simp12	$⊢ ((K \in HL \land X \in N \land P \in A) \land q \in A \land q ⋖_{K} X) \to X \in N$
22	5 3	llnbase	$⊢ X \in N \to X \in {Base}_{K}$
23	21 22	syl	$⊢ ((K \in HL \land X \in N \land P \in A) \land q \in A \land q ⋖_{K} X) \to X \in {Base}_{K}$
24		simp3	$⊢ ((K \in HL \land X \in N \land P \in A) \land q \in A \land q ⋖_{K} X) \to q ⋖_{K} X$
25	5 16 6	cvrlt	$⊢ ((K \in HL \land q \in {Base}_{K} \land X \in {Base}_{K}) \land q ⋖_{K} X) \to q <_{K} X$
26	11 20 23 24 25	syl31anc	$⊢ ((K \in HL \land X \in N \land P \in A) \land q \in A \land q ⋖_{K} X) \to q <_{K} X$
27		hlpos	$⊢ K \in HL \to K \in Poset$
28	11 27	syl	$⊢ ((K \in HL \land X \in N \land P \in A) \land q \in A \land q ⋖_{K} X) \to K \in Poset$
29	5 2	atbase	$⊢ P \in A \to P \in {Base}_{K}$
30	15 29	syl	$⊢ ((K \in HL \land X \in N \land P \in A) \land q \in A \land q ⋖_{K} X) \to P \in {Base}_{K}$
31	5 1 16	pltletr	$⊢ (K \in Poset \land (q \in {Base}_{K} \land X \in {Base}_{K} \land P \in {Base}_{K})) \to ((q <_{K} X \land X \underset{˙}{\leq} P) \to q <_{K} P)$
32	28 20 23 30 31	syl13anc	$⊢ ((K \in HL \land X \in N \land P \in A) \land q \in A \land q ⋖_{K} X) \to ((q <_{K} X \land X \underset{˙}{\leq} P) \to q <_{K} P)$
33	26 32	mpand	$⊢ ((K \in HL \land X \in N \land P \in A) \land q \in A \land q ⋖_{K} X) \to (X \underset{˙}{\leq} P \to q <_{K} P)$
34	18 33	mtod	$⊢ ((K \in HL \land X \in N \land P \in A) \land q \in A \land q ⋖_{K} X) \to \neg X \underset{˙}{\leq} P$
35	34	rexlimdv3a	$⊢ (K \in HL \land X \in N \land P \in A) \to (\exists q \in A q ⋖_{K} X \to \neg X \underset{˙}{\leq} P)$
36	10 35	mpd	$⊢ (K \in HL \land X \in N \land P \in A) \to \neg X \underset{˙}{\leq} P$

Metamath Proof Explorer

Theorem llnnleat

Proof