lplnle

Description: Any element greater than 0 and not an atom and not a lattice line majorizes a lattice plane. (Contributed by NM, 28-Jun-2012)

	Ref	Expression
Hypotheses	lplnle.b	$⊢ B = {Base}_{K}$
	lplnle.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	lplnle.z	$⊢ \underset{˙}{0} = 0. (K)$
	lplnle.a	$⊢ A = Atoms (K)$
	lplnle.n	$⊢ N = LLines (K)$
	lplnle.p	$⊢ P = LPlanes (K)$
Assertion	lplnle	$⊢ ((K \in HL \land X \in B) \land (X \neq \underset{˙}{0} \land \neg X \in A \land \neg X \in N)) \to \exists y \in P y \underset{˙}{\leq} X$

Proof

Step	Hyp	Ref	Expression
1		lplnle.b	$⊢ B = {Base}_{K}$
2		lplnle.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		lplnle.z	$⊢ \underset{˙}{0} = 0. (K)$
4		lplnle.a	$⊢ A = Atoms (K)$
5		lplnle.n	$⊢ N = LLines (K)$
6		lplnle.p	$⊢ P = LPlanes (K)$
7	1 2 3 4 5	llnle	$⊢ ((K \in HL \land X \in B) \land (X \neq \underset{˙}{0} \land \neg X \in A)) \to \exists z \in N z \underset{˙}{\leq} X$
8	7	3adantr3	$⊢ ((K \in HL \land X \in B) \land (X \neq \underset{˙}{0} \land \neg X \in A \land \neg X \in N)) \to \exists z \in N z \underset{˙}{\leq} X$
9		simp1ll	$⊢ (((K \in HL \land X \in B) \land (X \neq \underset{˙}{0} \land \neg X \in A \land \neg X \in N)) \land z \in N \land z \underset{˙}{\leq} X) \to K \in HL$
10	1 5	llnbase	$⊢ z \in N \to z \in B$
11	10	3ad2ant2	$⊢ (((K \in HL \land X \in B) \land (X \neq \underset{˙}{0} \land \neg X \in A \land \neg X \in N)) \land z \in N \land z \underset{˙}{\leq} X) \to z \in B$
12		simp1lr	$⊢ (((K \in HL \land X \in B) \land (X \neq \underset{˙}{0} \land \neg X \in A \land \neg X \in N)) \land z \in N \land z \underset{˙}{\leq} X) \to X \in B$
13		simp3	$⊢ (((K \in HL \land X \in B) \land (X \neq \underset{˙}{0} \land \neg X \in A \land \neg X \in N)) \land z \in N \land z \underset{˙}{\leq} X) \to z \underset{˙}{\leq} X$
14		simp2	$⊢ (((K \in HL \land X \in B) \land (X \neq \underset{˙}{0} \land \neg X \in A \land \neg X \in N)) \land z \in N \land z \underset{˙}{\leq} X) \to z \in N$
15		simp1r3	$⊢ (((K \in HL \land X \in B) \land (X \neq \underset{˙}{0} \land \neg X \in A \land \neg X \in N)) \land z \in N \land z \underset{˙}{\leq} X) \to \neg X \in N$
16		nelne2	$⊢ (z \in N \land \neg X \in N) \to z \neq X$
17	14 15 16	syl2anc	$⊢ (((K \in HL \land X \in B) \land (X \neq \underset{˙}{0} \land \neg X \in A \land \neg X \in N)) \land z \in N \land z \underset{˙}{\leq} X) \to z \neq X$
18		eqid	$⊢ <_{K} = <_{K}$
19	2 18	pltval	$⊢ (K \in HL \land z \in N \land X \in B) \to (z <_{K} X \leftrightarrow (z \underset{˙}{\leq} X \land z \neq X))$
20	9 14 12 19	syl3anc	$⊢ (((K \in HL \land X \in B) \land (X \neq \underset{˙}{0} \land \neg X \in A \land \neg X \in N)) \land z \in N \land z \underset{˙}{\leq} X) \to (z <_{K} X \leftrightarrow (z \underset{˙}{\leq} X \land z \neq X))$
21	13 17 20	mpbir2and	$⊢ (((K \in HL \land X \in B) \land (X \neq \underset{˙}{0} \land \neg X \in A \land \neg X \in N)) \land z \in N \land z \underset{˙}{\leq} X) \to z <_{K} X$
22		eqid	$⊢ join (K) = join (K)$
23		eqid	$⊢ ⋖_{K} = ⋖_{K}$
24	1 2 18 22 23 4	hlrelat3	$⊢ ((K \in HL \land z \in B \land X \in B) \land z <_{K} X) \to \exists p \in A (z ⋖_{K} (z join (K) p) \land (z join (K) p) \underset{˙}{\leq} X)$
25	9 11 12 21 24	syl31anc	$⊢ (((K \in HL \land X \in B) \land (X \neq \underset{˙}{0} \land \neg X \in A \land \neg X \in N)) \land z \in N \land z \underset{˙}{\leq} X) \to \exists p \in A (z ⋖_{K} (z join (K) p) \land (z join (K) p) \underset{˙}{\leq} X)$
26		simp1ll	$⊢ (((K \in HL \land X \in B) \land (X \neq \underset{˙}{0} \land \neg X \in A \land \neg X \in N)) \land (z \in N \land z \underset{˙}{\leq} X \land p \in A) \land (z ⋖_{K} (z join (K) p) \land (z join (K) p) \underset{˙}{\leq} X)) \to K \in HL$
27	26	hllatd	$⊢ (((K \in HL \land X \in B) \land (X \neq \underset{˙}{0} \land \neg X \in A \land \neg X \in N)) \land (z \in N \land z \underset{˙}{\leq} X \land p \in A) \land (z ⋖_{K} (z join (K) p) \land (z join (K) p) \underset{˙}{\leq} X)) \to K \in Lat$
28		simp21	$⊢ (((K \in HL \land X \in B) \land (X \neq \underset{˙}{0} \land \neg X \in A \land \neg X \in N)) \land (z \in N \land z \underset{˙}{\leq} X \land p \in A) \land (z ⋖_{K} (z join (K) p) \land (z join (K) p) \underset{˙}{\leq} X)) \to z \in N$
29	28 10	syl	$⊢ (((K \in HL \land X \in B) \land (X \neq \underset{˙}{0} \land \neg X \in A \land \neg X \in N)) \land (z \in N \land z \underset{˙}{\leq} X \land p \in A) \land (z ⋖_{K} (z join (K) p) \land (z join (K) p) \underset{˙}{\leq} X)) \to z \in B$
30		simp23	$⊢ (((K \in HL \land X \in B) \land (X \neq \underset{˙}{0} \land \neg X \in A \land \neg X \in N)) \land (z \in N \land z \underset{˙}{\leq} X \land p \in A) \land (z ⋖_{K} (z join (K) p) \land (z join (K) p) \underset{˙}{\leq} X)) \to p \in A$
31	1 4	atbase	$⊢ p \in A \to p \in B$
32	30 31	syl	$⊢ (((K \in HL \land X \in B) \land (X \neq \underset{˙}{0} \land \neg X \in A \land \neg X \in N)) \land (z \in N \land z \underset{˙}{\leq} X \land p \in A) \land (z ⋖_{K} (z join (K) p) \land (z join (K) p) \underset{˙}{\leq} X)) \to p \in B$
33	1 22	latjcl	$⊢ (K \in Lat \land z \in B \land p \in B) \to z join (K) p \in B$
34	27 29 32 33	syl3anc	$⊢ (((K \in HL \land X \in B) \land (X \neq \underset{˙}{0} \land \neg X \in A \land \neg X \in N)) \land (z \in N \land z \underset{˙}{\leq} X \land p \in A) \land (z ⋖_{K} (z join (K) p) \land (z join (K) p) \underset{˙}{\leq} X)) \to z join (K) p \in B$
35		simp3l	$⊢ (((K \in HL \land X \in B) \land (X \neq \underset{˙}{0} \land \neg X \in A \land \neg X \in N)) \land (z \in N \land z \underset{˙}{\leq} X \land p \in A) \land (z ⋖_{K} (z join (K) p) \land (z join (K) p) \underset{˙}{\leq} X)) \to z ⋖_{K} (z join (K) p)$
36	1 23 5 6	lplni	$⊢ ((K \in HL \land z join (K) p \in B \land z \in N) \land z ⋖_{K} (z join (K) p)) \to z join (K) p \in P$
37	26 34 28 35 36	syl31anc	$⊢ (((K \in HL \land X \in B) \land (X \neq \underset{˙}{0} \land \neg X \in A \land \neg X \in N)) \land (z \in N \land z \underset{˙}{\leq} X \land p \in A) \land (z ⋖_{K} (z join (K) p) \land (z join (K) p) \underset{˙}{\leq} X)) \to z join (K) p \in P$
38		simp3r	$⊢ (((K \in HL \land X \in B) \land (X \neq \underset{˙}{0} \land \neg X \in A \land \neg X \in N)) \land (z \in N \land z \underset{˙}{\leq} X \land p \in A) \land (z ⋖_{K} (z join (K) p) \land (z join (K) p) \underset{˙}{\leq} X)) \to (z join (K) p) \underset{˙}{\leq} X$
39		breq1	$⊢ y = z join (K) p \to (y \underset{˙}{\leq} X \leftrightarrow (z join (K) p) \underset{˙}{\leq} X)$
40	39	rspcev	$⊢ (z join (K) p \in P \land (z join (K) p) \underset{˙}{\leq} X) \to \exists y \in P y \underset{˙}{\leq} X$
41	37 38 40	syl2anc	$⊢ (((K \in HL \land X \in B) \land (X \neq \underset{˙}{0} \land \neg X \in A \land \neg X \in N)) \land (z \in N \land z \underset{˙}{\leq} X \land p \in A) \land (z ⋖_{K} (z join (K) p) \land (z join (K) p) \underset{˙}{\leq} X)) \to \exists y \in P y \underset{˙}{\leq} X$
42	41	3exp	$⊢ ((K \in HL \land X \in B) \land (X \neq \underset{˙}{0} \land \neg X \in A \land \neg X \in N)) \to ((z \in N \land z \underset{˙}{\leq} X \land p \in A) \to ((z ⋖_{K} (z join (K) p) \land (z join (K) p) \underset{˙}{\leq} X) \to \exists y \in P y \underset{˙}{\leq} X))$
43	42	3expd	$⊢ ((K \in HL \land X \in B) \land (X \neq \underset{˙}{0} \land \neg X \in A \land \neg X \in N)) \to (z \in N \to (z \underset{˙}{\leq} X \to (p \in A \to ((z ⋖_{K} (z join (K) p) \land (z join (K) p) \underset{˙}{\leq} X) \to \exists y \in P y \underset{˙}{\leq} X))))$
44	43	3imp	$⊢ (((K \in HL \land X \in B) \land (X \neq \underset{˙}{0} \land \neg X \in A \land \neg X \in N)) \land z \in N \land z \underset{˙}{\leq} X) \to (p \in A \to ((z ⋖_{K} (z join (K) p) \land (z join (K) p) \underset{˙}{\leq} X) \to \exists y \in P y \underset{˙}{\leq} X))$
45	44	rexlimdv	$⊢ (((K \in HL \land X \in B) \land (X \neq \underset{˙}{0} \land \neg X \in A \land \neg X \in N)) \land z \in N \land z \underset{˙}{\leq} X) \to (\exists p \in A (z ⋖_{K} (z join (K) p) \land (z join (K) p) \underset{˙}{\leq} X) \to \exists y \in P y \underset{˙}{\leq} X)$
46	25 45	mpd	$⊢ (((K \in HL \land X \in B) \land (X \neq \underset{˙}{0} \land \neg X \in A \land \neg X \in N)) \land z \in N \land z \underset{˙}{\leq} X) \to \exists y \in P y \underset{˙}{\leq} X$
47	46	3exp	$⊢ ((K \in HL \land X \in B) \land (X \neq \underset{˙}{0} \land \neg X \in A \land \neg X \in N)) \to (z \in N \to (z \underset{˙}{\leq} X \to \exists y \in P y \underset{˙}{\leq} X))$
48	47	rexlimdv	$⊢ ((K \in HL \land X \in B) \land (X \neq \underset{˙}{0} \land \neg X \in A \land \neg X \in N)) \to (\exists z \in N z \underset{˙}{\leq} X \to \exists y \in P y \underset{˙}{\leq} X)$
49	8 48	mpd	$⊢ ((K \in HL \land X \in B) \land (X \neq \underset{˙}{0} \land \neg X \in A \land \neg X \in N)) \to \exists y \in P y \underset{˙}{\leq} X$

Metamath Proof Explorer

Theorem lplnle

Proof