2dim

Description: Generate a height-3 element (2-dimensional plane) from an atom. (Contributed by NM, 3-May-2012)

	Ref	Expression
Hypotheses	2dim.j	$⊢ \underset{˙}{\lor} = join (K)$
	2dim.c	$⊢ C = ⋖_{K}$
	2dim.a	$⊢ A = Atoms (K)$
Assertion	2dim	$⊢ (K \in HL \land P \in A) \to \exists q \in A \exists r \in A (P C (P \underset{˙}{\lor} q) \land (P \underset{˙}{\lor} q) C ((P \underset{˙}{\lor} q) \underset{˙}{\lor} r))$

Proof

Step	Hyp	Ref	Expression
1		2dim.j	$⊢ \underset{˙}{\lor} = join (K)$
2		2dim.c	$⊢ C = ⋖_{K}$
3		2dim.a	$⊢ A = Atoms (K)$
4		eqid	$⊢ \leq_{K} = \leq_{K}$
5	1 4 3	3dim1	$⊢ (K \in HL \land P \in A) \to \exists q \in A \exists r \in A \exists s \in A (P \neq q \land \neg r \leq_{K} (P \underset{˙}{\lor} q) \land \neg s \leq_{K} ((P \underset{˙}{\lor} q) \underset{˙}{\lor} r))$
6		df-3an	$⊢ (P \neq q \land \neg r \leq_{K} (P \underset{˙}{\lor} q) \land \neg s \leq_{K} ((P \underset{˙}{\lor} q) \underset{˙}{\lor} r)) \leftrightarrow ((P \neq q \land \neg r \leq_{K} (P \underset{˙}{\lor} q)) \land \neg s \leq_{K} ((P \underset{˙}{\lor} q) \underset{˙}{\lor} r))$
7	6	rexbii	$⊢ \exists s \in A (P \neq q \land \neg r \leq_{K} (P \underset{˙}{\lor} q) \land \neg s \leq_{K} ((P \underset{˙}{\lor} q) \underset{˙}{\lor} r)) \leftrightarrow \exists s \in A ((P \neq q \land \neg r \leq_{K} (P \underset{˙}{\lor} q)) \land \neg s \leq_{K} ((P \underset{˙}{\lor} q) \underset{˙}{\lor} r))$
8		r19.42v	$⊢ \exists s \in A ((P \neq q \land \neg r \leq_{K} (P \underset{˙}{\lor} q)) \land \neg s \leq_{K} ((P \underset{˙}{\lor} q) \underset{˙}{\lor} r)) \leftrightarrow ((P \neq q \land \neg r \leq_{K} (P \underset{˙}{\lor} q)) \land \exists s \in A \neg s \leq_{K} ((P \underset{˙}{\lor} q) \underset{˙}{\lor} r))$
9	7 8	bitri	$⊢ \exists s \in A (P \neq q \land \neg r \leq_{K} (P \underset{˙}{\lor} q) \land \neg s \leq_{K} ((P \underset{˙}{\lor} q) \underset{˙}{\lor} r)) \leftrightarrow ((P \neq q \land \neg r \leq_{K} (P \underset{˙}{\lor} q)) \land \exists s \in A \neg s \leq_{K} ((P \underset{˙}{\lor} q) \underset{˙}{\lor} r))$
10	9	simplbi	$⊢ \exists s \in A (P \neq q \land \neg r \leq_{K} (P \underset{˙}{\lor} q) \land \neg s \leq_{K} ((P \underset{˙}{\lor} q) \underset{˙}{\lor} r)) \to (P \neq q \land \neg r \leq_{K} (P \underset{˙}{\lor} q))$
11		simplll	$⊢ (((K \in HL \land P \in A) \land q \in A) \land r \in A) \to K \in HL$
12		hlatl	$⊢ K \in HL \to K \in AtLat$
13	11 12	syl	$⊢ (((K \in HL \land P \in A) \land q \in A) \land r \in A) \to K \in AtLat$
14		simplr	$⊢ (((K \in HL \land P \in A) \land q \in A) \land r \in A) \to q \in A$
15		simpllr	$⊢ (((K \in HL \land P \in A) \land q \in A) \land r \in A) \to P \in A$
16	4 3	atncmp	$⊢ (K \in AtLat \land q \in A \land P \in A) \to (\neg q \leq_{K} P \leftrightarrow q \neq P)$
17	13 14 15 16	syl3anc	$⊢ (((K \in HL \land P \in A) \land q \in A) \land r \in A) \to (\neg q \leq_{K} P \leftrightarrow q \neq P)$
18		necom	$⊢ q \neq P \leftrightarrow P \neq q$
19	17 18	bitr2di	$⊢ (((K \in HL \land P \in A) \land q \in A) \land r \in A) \to (P \neq q \leftrightarrow \neg q \leq_{K} P)$
20		eqid	$⊢ {Base}_{K} = {Base}_{K}$
21	20 3	atbase	$⊢ P \in A \to P \in {Base}_{K}$
22	15 21	syl	$⊢ (((K \in HL \land P \in A) \land q \in A) \land r \in A) \to P \in {Base}_{K}$
23	20 4 1 2 3	cvr1	$⊢ (K \in HL \land P \in {Base}_{K} \land q \in A) \to (\neg q \leq_{K} P \leftrightarrow P C (P \underset{˙}{\lor} q))$
24	11 22 14 23	syl3anc	$⊢ (((K \in HL \land P \in A) \land q \in A) \land r \in A) \to (\neg q \leq_{K} P \leftrightarrow P C (P \underset{˙}{\lor} q))$
25	19 24	bitrd	$⊢ (((K \in HL \land P \in A) \land q \in A) \land r \in A) \to (P \neq q \leftrightarrow P C (P \underset{˙}{\lor} q))$
26	20 1 3	hlatjcl	$⊢ (K \in HL \land P \in A \land q \in A) \to P \underset{˙}{\lor} q \in {Base}_{K}$
27	11 15 14 26	syl3anc	$⊢ (((K \in HL \land P \in A) \land q \in A) \land r \in A) \to P \underset{˙}{\lor} q \in {Base}_{K}$
28		simpr	$⊢ (((K \in HL \land P \in A) \land q \in A) \land r \in A) \to r \in A$
29	20 4 1 2 3	cvr1	$⊢ (K \in HL \land P \underset{˙}{\lor} q \in {Base}_{K} \land r \in A) \to (\neg r \leq_{K} (P \underset{˙}{\lor} q) \leftrightarrow (P \underset{˙}{\lor} q) C ((P \underset{˙}{\lor} q) \underset{˙}{\lor} r))$
30	11 27 28 29	syl3anc	$⊢ (((K \in HL \land P \in A) \land q \in A) \land r \in A) \to (\neg r \leq_{K} (P \underset{˙}{\lor} q) \leftrightarrow (P \underset{˙}{\lor} q) C ((P \underset{˙}{\lor} q) \underset{˙}{\lor} r))$
31	25 30	anbi12d	$⊢ (((K \in HL \land P \in A) \land q \in A) \land r \in A) \to ((P \neq q \land \neg r \leq_{K} (P \underset{˙}{\lor} q)) \leftrightarrow (P C (P \underset{˙}{\lor} q) \land (P \underset{˙}{\lor} q) C ((P \underset{˙}{\lor} q) \underset{˙}{\lor} r)))$
32	10 31	imbitrid	$⊢ (((K \in HL \land P \in A) \land q \in A) \land r \in A) \to (\exists s \in A (P \neq q \land \neg r \leq_{K} (P \underset{˙}{\lor} q) \land \neg s \leq_{K} ((P \underset{˙}{\lor} q) \underset{˙}{\lor} r)) \to (P C (P \underset{˙}{\lor} q) \land (P \underset{˙}{\lor} q) C ((P \underset{˙}{\lor} q) \underset{˙}{\lor} r)))$
33	32	reximdva	$⊢ ((K \in HL \land P \in A) \land q \in A) \to (\exists r \in A \exists s \in A (P \neq q \land \neg r \leq_{K} (P \underset{˙}{\lor} q) \land \neg s \leq_{K} ((P \underset{˙}{\lor} q) \underset{˙}{\lor} r)) \to \exists r \in A (P C (P \underset{˙}{\lor} q) \land (P \underset{˙}{\lor} q) C ((P \underset{˙}{\lor} q) \underset{˙}{\lor} r)))$
34	33	reximdva	$⊢ (K \in HL \land P \in A) \to (\exists q \in A \exists r \in A \exists s \in A (P \neq q \land \neg r \leq_{K} (P \underset{˙}{\lor} q) \land \neg s \leq_{K} ((P \underset{˙}{\lor} q) \underset{˙}{\lor} r)) \to \exists q \in A \exists r \in A (P C (P \underset{˙}{\lor} q) \land (P \underset{˙}{\lor} q) C ((P \underset{˙}{\lor} q) \underset{˙}{\lor} r)))$
35	5 34	mpd	$⊢ (K \in HL \land P \in A) \to \exists q \in A \exists r \in A (P C (P \underset{˙}{\lor} q) \land (P \underset{˙}{\lor} q) C ((P \underset{˙}{\lor} q) \underset{˙}{\lor} r))$

Metamath Proof Explorer

Theorem 2dim

Proof