lplnexatN

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

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

Proof

Step	Hyp	Ref	Expression
1		lplnexat.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		lplnexat.j	$⊢ \underset{˙}{\lor} = join (K)$
3		lplnexat.a	$⊢ A = Atoms (K)$
4		lplnexat.n	$⊢ N = LLines (K)$
5		lplnexat.p	$⊢ P = LPlanes (K)$
6		simp1	$⊢ (K \in HL \land X \in P \land Y \in N) \to K \in HL$
7		simp3	$⊢ (K \in HL \land X \in P \land Y \in N) \to Y \in N$
8		simp2	$⊢ (K \in HL \land X \in P \land Y \in N) \to X \in P$
9	6 7 8	3jca	$⊢ (K \in HL \land X \in P \land Y \in N) \to (K \in HL \land Y \in N \land X \in P)$
10		eqid	$⊢ ⋖_{K} = ⋖_{K}$
11	1 10 4 5	llncvrlpln2	$⊢ ((K \in HL \land Y \in N \land X \in P) \land Y \underset{˙}{\leq} X) \to Y ⋖_{K} X$
12	9 11	sylan	$⊢ ((K \in HL \land X \in P \land Y \in N) \land Y \underset{˙}{\leq} X) \to Y ⋖_{K} X$
13		simpl1	$⊢ ((K \in HL \land X \in P \land Y \in N) \land Y \underset{˙}{\leq} X) \to K \in HL$
14		simpl3	$⊢ ((K \in HL \land X \in P \land Y \in N) \land Y \underset{˙}{\leq} X) \to Y \in N$
15		eqid	$⊢ {Base}_{K} = {Base}_{K}$
16	15 4	llnbase	$⊢ Y \in N \to Y \in {Base}_{K}$
17	14 16	syl	$⊢ ((K \in HL \land X \in P \land Y \in N) \land Y \underset{˙}{\leq} X) \to Y \in {Base}_{K}$
18		simpl2	$⊢ ((K \in HL \land X \in P \land Y \in N) \land Y \underset{˙}{\leq} X) \to X \in P$
19	15 5	lplnbase	$⊢ X \in P \to X \in {Base}_{K}$
20	18 19	syl	$⊢ ((K \in HL \land X \in P \land Y \in N) \land Y \underset{˙}{\leq} X) \to X \in {Base}_{K}$
21	15 1 2 10 3	cvrval3	$⊢ (K \in HL \land Y \in {Base}_{K} \land X \in {Base}_{K}) \to (Y ⋖_{K} X \leftrightarrow \exists q \in A (\neg q \underset{˙}{\leq} Y \land Y \underset{˙}{\lor} q = X))$
22	13 17 20 21	syl3anc	$⊢ ((K \in HL \land X \in P \land Y \in N) \land Y \underset{˙}{\leq} X) \to (Y ⋖_{K} X \leftrightarrow \exists q \in A (\neg q \underset{˙}{\leq} Y \land Y \underset{˙}{\lor} q = X))$
23		eqcom	$⊢ Y \underset{˙}{\lor} q = X \leftrightarrow X = Y \underset{˙}{\lor} q$
24	23	anbi2i	$⊢ (\neg q \underset{˙}{\leq} Y \land Y \underset{˙}{\lor} q = X) \leftrightarrow (\neg q \underset{˙}{\leq} Y \land X = Y \underset{˙}{\lor} q)$
25	24	rexbii	$⊢ \exists q \in A (\neg q \underset{˙}{\leq} Y \land Y \underset{˙}{\lor} q = X) \leftrightarrow \exists q \in A (\neg q \underset{˙}{\leq} Y \land X = Y \underset{˙}{\lor} q)$
26	22 25	bitrdi	$⊢ ((K \in HL \land X \in P \land Y \in N) \land Y \underset{˙}{\leq} X) \to (Y ⋖_{K} X \leftrightarrow \exists q \in A (\neg q \underset{˙}{\leq} Y \land X = Y \underset{˙}{\lor} q))$
27	12 26	mpbid	$⊢ ((K \in HL \land X \in P \land Y \in N) \land Y \underset{˙}{\leq} X) \to \exists q \in A (\neg q \underset{˙}{\leq} Y \land X = Y \underset{˙}{\lor} q)$

Metamath Proof Explorer

Theorem lplnexatN

Proof