lplnnle2at

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

	Ref	Expression
Hypotheses	lplnnle2at.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	lplnnle2at.j	$⊢ \underset{˙}{\lor} = join (K)$
	lplnnle2at.a	$⊢ A = Atoms (K)$
	lplnnle2at.p	$⊢ P = LPlanes (K)$
Assertion	lplnnle2at	$⊢ (K \in HL \land (X \in P \land Q \in A \land R \in A)) \to \neg X \underset{˙}{\leq} (Q \underset{˙}{\lor} R)$

Proof

Step	Hyp	Ref	Expression
1		lplnnle2at.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		lplnnle2at.j	$⊢ \underset{˙}{\lor} = join (K)$
3		lplnnle2at.a	$⊢ A = Atoms (K)$
4		lplnnle2at.p	$⊢ P = LPlanes (K)$
5		simpr1	$⊢ (K \in HL \land (X \in P \land Q \in A \land R \in A)) \to X \in P$
6		eqid	$⊢ {Base}_{K} = {Base}_{K}$
7		eqid	$⊢ ⋖_{K} = ⋖_{K}$
8		eqid	$⊢ LLines (K) = LLines (K)$
9	6 7 8 4	islpln	$⊢ K \in HL \to (X \in P \leftrightarrow (X \in {Base}_{K} \land \exists y \in LLines (K) y ⋖_{K} X))$
10	9	adantr	$⊢ (K \in HL \land (X \in P \land Q \in A \land R \in A)) \to (X \in P \leftrightarrow (X \in {Base}_{K} \land \exists y \in LLines (K) y ⋖_{K} X))$
11	5 10	mpbid	$⊢ (K \in HL \land (X \in P \land Q \in A \land R \in A)) \to (X \in {Base}_{K} \land \exists y \in LLines (K) y ⋖_{K} X)$
12	11	simprd	$⊢ (K \in HL \land (X \in P \land Q \in A \land R \in A)) \to \exists y \in LLines (K) y ⋖_{K} X$
13		oveq1	$⊢ Q = R \to Q \underset{˙}{\lor} R = R \underset{˙}{\lor} R$
14	13	breq2d	$⊢ Q = R \to (X \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \leftrightarrow X \underset{˙}{\leq} (R \underset{˙}{\lor} R))$
15	14	notbid	$⊢ Q = R \to (\neg X \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \leftrightarrow \neg X \underset{˙}{\leq} (R \underset{˙}{\lor} R))$
16		simpl1	$⊢ ((K \in HL \land (X \in P \land Q \in A \land R \in A) \land (y \in LLines (K) \land y ⋖_{K} X)) \land Q \neq R) \to K \in HL$
17		simpl3l	$⊢ ((K \in HL \land (X \in P \land Q \in A \land R \in A) \land (y \in LLines (K) \land y ⋖_{K} X)) \land Q \neq R) \to y \in LLines (K)$
18		simpl22	$⊢ ((K \in HL \land (X \in P \land Q \in A \land R \in A) \land (y \in LLines (K) \land y ⋖_{K} X)) \land Q \neq R) \to Q \in A$
19		simpl23	$⊢ ((K \in HL \land (X \in P \land Q \in A \land R \in A) \land (y \in LLines (K) \land y ⋖_{K} X)) \land Q \neq R) \to R \in A$
20		simpr	$⊢ ((K \in HL \land (X \in P \land Q \in A \land R \in A) \land (y \in LLines (K) \land y ⋖_{K} X)) \land Q \neq R) \to Q \neq R$
21	2 3 8	llni2	$⊢ ((K \in HL \land Q \in A \land R \in A) \land Q \neq R) \to Q \underset{˙}{\lor} R \in LLines (K)$
22	16 18 19 20 21	syl31anc	$⊢ ((K \in HL \land (X \in P \land Q \in A \land R \in A) \land (y \in LLines (K) \land y ⋖_{K} X)) \land Q \neq R) \to Q \underset{˙}{\lor} R \in LLines (K)$
23		eqid	$⊢ <_{K} = <_{K}$
24	23 8	llnnlt	$⊢ (K \in HL \land y \in LLines (K) \land Q \underset{˙}{\lor} R \in LLines (K)) \to \neg y <_{K} (Q \underset{˙}{\lor} R)$
25	16 17 22 24	syl3anc	$⊢ ((K \in HL \land (X \in P \land Q \in A \land R \in A) \land (y \in LLines (K) \land y ⋖_{K} X)) \land Q \neq R) \to \neg y <_{K} (Q \underset{˙}{\lor} R)$
26	6 8	llnbase	$⊢ y \in LLines (K) \to y \in {Base}_{K}$
27	17 26	syl	$⊢ ((K \in HL \land (X \in P \land Q \in A \land R \in A) \land (y \in LLines (K) \land y ⋖_{K} X)) \land Q \neq R) \to y \in {Base}_{K}$
28		simpl21	$⊢ ((K \in HL \land (X \in P \land Q \in A \land R \in A) \land (y \in LLines (K) \land y ⋖_{K} X)) \land Q \neq R) \to X \in P$
29	6 4	lplnbase	$⊢ X \in P \to X \in {Base}_{K}$
30	28 29	syl	$⊢ ((K \in HL \land (X \in P \land Q \in A \land R \in A) \land (y \in LLines (K) \land y ⋖_{K} X)) \land Q \neq R) \to X \in {Base}_{K}$
31		simpl3r	$⊢ ((K \in HL \land (X \in P \land Q \in A \land R \in A) \land (y \in LLines (K) \land y ⋖_{K} X)) \land Q \neq R) \to y ⋖_{K} X$
32	6 23 7	cvrlt	$⊢ ((K \in HL \land y \in {Base}_{K} \land X \in {Base}_{K}) \land y ⋖_{K} X) \to y <_{K} X$
33	16 27 30 31 32	syl31anc	$⊢ ((K \in HL \land (X \in P \land Q \in A \land R \in A) \land (y \in LLines (K) \land y ⋖_{K} X)) \land Q \neq R) \to y <_{K} X$
34		hlpos	$⊢ K \in HL \to K \in Poset$
35	16 34	syl	$⊢ ((K \in HL \land (X \in P \land Q \in A \land R \in A) \land (y \in LLines (K) \land y ⋖_{K} X)) \land Q \neq R) \to K \in Poset$
36	6 2 3	hlatjcl	$⊢ (K \in HL \land Q \in A \land R \in A) \to Q \underset{˙}{\lor} R \in {Base}_{K}$
37	16 18 19 36	syl3anc	$⊢ ((K \in HL \land (X \in P \land Q \in A \land R \in A) \land (y \in LLines (K) \land y ⋖_{K} X)) \land Q \neq R) \to Q \underset{˙}{\lor} R \in {Base}_{K}$
38	6 1 23	pltletr	$⊢ (K \in Poset \land (y \in {Base}_{K} \land X \in {Base}_{K} \land Q \underset{˙}{\lor} R \in {Base}_{K})) \to ((y <_{K} X \land X \underset{˙}{\leq} (Q \underset{˙}{\lor} R)) \to y <_{K} (Q \underset{˙}{\lor} R))$
39	35 27 30 37 38	syl13anc	$⊢ ((K \in HL \land (X \in P \land Q \in A \land R \in A) \land (y \in LLines (K) \land y ⋖_{K} X)) \land Q \neq R) \to ((y <_{K} X \land X \underset{˙}{\leq} (Q \underset{˙}{\lor} R)) \to y <_{K} (Q \underset{˙}{\lor} R))$
40	33 39	mpand	$⊢ ((K \in HL \land (X \in P \land Q \in A \land R \in A) \land (y \in LLines (K) \land y ⋖_{K} X)) \land Q \neq R) \to (X \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \to y <_{K} (Q \underset{˙}{\lor} R))$
41	25 40	mtod	$⊢ ((K \in HL \land (X \in P \land Q \in A \land R \in A) \land (y \in LLines (K) \land y ⋖_{K} X)) \land Q \neq R) \to \neg X \underset{˙}{\leq} (Q \underset{˙}{\lor} R)$
42		simp1	$⊢ (K \in HL \land (X \in P \land Q \in A \land R \in A) \land (y \in LLines (K) \land y ⋖_{K} X)) \to K \in HL$
43		simp3l	$⊢ (K \in HL \land (X \in P \land Q \in A \land R \in A) \land (y \in LLines (K) \land y ⋖_{K} X)) \to y \in LLines (K)$
44		simp23	$⊢ (K \in HL \land (X \in P \land Q \in A \land R \in A) \land (y \in LLines (K) \land y ⋖_{K} X)) \to R \in A$
45	1 3 8	llnnleat	$⊢ (K \in HL \land y \in LLines (K) \land R \in A) \to \neg y \underset{˙}{\leq} R$
46	42 43 44 45	syl3anc	$⊢ (K \in HL \land (X \in P \land Q \in A \land R \in A) \land (y \in LLines (K) \land y ⋖_{K} X)) \to \neg y \underset{˙}{\leq} R$
47	43 26	syl	$⊢ (K \in HL \land (X \in P \land Q \in A \land R \in A) \land (y \in LLines (K) \land y ⋖_{K} X)) \to y \in {Base}_{K}$
48		simp21	$⊢ (K \in HL \land (X \in P \land Q \in A \land R \in A) \land (y \in LLines (K) \land y ⋖_{K} X)) \to X \in P$
49	48 29	syl	$⊢ (K \in HL \land (X \in P \land Q \in A \land R \in A) \land (y \in LLines (K) \land y ⋖_{K} X)) \to X \in {Base}_{K}$
50		simp3r	$⊢ (K \in HL \land (X \in P \land Q \in A \land R \in A) \land (y \in LLines (K) \land y ⋖_{K} X)) \to y ⋖_{K} X$
51	42 47 49 50 32	syl31anc	$⊢ (K \in HL \land (X \in P \land Q \in A \land R \in A) \land (y \in LLines (K) \land y ⋖_{K} X)) \to y <_{K} X$
52	34	3ad2ant1	$⊢ (K \in HL \land (X \in P \land Q \in A \land R \in A) \land (y \in LLines (K) \land y ⋖_{K} X)) \to K \in Poset$
53	6 3	atbase	$⊢ R \in A \to R \in {Base}_{K}$
54	44 53	syl	$⊢ (K \in HL \land (X \in P \land Q \in A \land R \in A) \land (y \in LLines (K) \land y ⋖_{K} X)) \to R \in {Base}_{K}$
55	6 1 23	pltletr	$⊢ (K \in Poset \land (y \in {Base}_{K} \land X \in {Base}_{K} \land R \in {Base}_{K})) \to ((y <_{K} X \land X \underset{˙}{\leq} R) \to y <_{K} R)$
56	52 47 49 54 55	syl13anc	$⊢ (K \in HL \land (X \in P \land Q \in A \land R \in A) \land (y \in LLines (K) \land y ⋖_{K} X)) \to ((y <_{K} X \land X \underset{˙}{\leq} R) \to y <_{K} R)$
57	51 56	mpand	$⊢ (K \in HL \land (X \in P \land Q \in A \land R \in A) \land (y \in LLines (K) \land y ⋖_{K} X)) \to (X \underset{˙}{\leq} R \to y <_{K} R)$
58	1 23	pltle	$⊢ (K \in HL \land y \in LLines (K) \land R \in A) \to (y <_{K} R \to y \underset{˙}{\leq} R)$
59	42 43 44 58	syl3anc	$⊢ (K \in HL \land (X \in P \land Q \in A \land R \in A) \land (y \in LLines (K) \land y ⋖_{K} X)) \to (y <_{K} R \to y \underset{˙}{\leq} R)$
60	57 59	syld	$⊢ (K \in HL \land (X \in P \land Q \in A \land R \in A) \land (y \in LLines (K) \land y ⋖_{K} X)) \to (X \underset{˙}{\leq} R \to y \underset{˙}{\leq} R)$
61	46 60	mtod	$⊢ (K \in HL \land (X \in P \land Q \in A \land R \in A) \land (y \in LLines (K) \land y ⋖_{K} X)) \to \neg X \underset{˙}{\leq} R$
62	2 3	hlatjidm	$⊢ (K \in HL \land R \in A) \to R \underset{˙}{\lor} R = R$
63	42 44 62	syl2anc	$⊢ (K \in HL \land (X \in P \land Q \in A \land R \in A) \land (y \in LLines (K) \land y ⋖_{K} X)) \to R \underset{˙}{\lor} R = R$
64	63	breq2d	$⊢ (K \in HL \land (X \in P \land Q \in A \land R \in A) \land (y \in LLines (K) \land y ⋖_{K} X)) \to (X \underset{˙}{\leq} (R \underset{˙}{\lor} R) \leftrightarrow X \underset{˙}{\leq} R)$
65	61 64	mtbird	$⊢ (K \in HL \land (X \in P \land Q \in A \land R \in A) \land (y \in LLines (K) \land y ⋖_{K} X)) \to \neg X \underset{˙}{\leq} (R \underset{˙}{\lor} R)$
66	15 41 65	pm2.61ne	$⊢ (K \in HL \land (X \in P \land Q \in A \land R \in A) \land (y \in LLines (K) \land y ⋖_{K} X)) \to \neg X \underset{˙}{\leq} (Q \underset{˙}{\lor} R)$
67	66	3exp	$⊢ K \in HL \to ((X \in P \land Q \in A \land R \in A) \to ((y \in LLines (K) \land y ⋖_{K} X) \to \neg X \underset{˙}{\leq} (Q \underset{˙}{\lor} R)))$
68	67	exp4a	$⊢ K \in HL \to ((X \in P \land Q \in A \land R \in A) \to (y \in LLines (K) \to (y ⋖_{K} X \to \neg X \underset{˙}{\leq} (Q \underset{˙}{\lor} R))))$
69	68	imp	$⊢ (K \in HL \land (X \in P \land Q \in A \land R \in A)) \to (y \in LLines (K) \to (y ⋖_{K} X \to \neg X \underset{˙}{\leq} (Q \underset{˙}{\lor} R)))$
70	69	rexlimdv	$⊢ (K \in HL \land (X \in P \land Q \in A \land R \in A)) \to (\exists y \in LLines (K) y ⋖_{K} X \to \neg X \underset{˙}{\leq} (Q \underset{˙}{\lor} R))$
71	12 70	mpd	$⊢ (K \in HL \land (X \in P \land Q \in A \land R \in A)) \to \neg X \underset{˙}{\leq} (Q \underset{˙}{\lor} R)$

Metamath Proof Explorer

Theorem lplnnle2at

Proof