3dim0

Description: There exists a 3-dimensional (height-4) element i.e. a volume. (Contributed by NM, 25-Jul-2012)

	Ref	Expression
Hypotheses	3dim0.j	$⊢ \underset{˙}{\lor} = join (K)$
	3dim0.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	3dim0.a	$⊢ A = Atoms (K)$
Assertion	3dim0	$⊢ K \in HL \to \exists p \in A \exists q \in A \exists r \in A \exists s \in A (p \neq q \land \neg r \underset{˙}{\leq} (p \underset{˙}{\lor} q) \land \neg s \underset{˙}{\leq} ((p \underset{˙}{\lor} q) \underset{˙}{\lor} r))$

Proof

Step	Hyp	Ref	Expression
1		3dim0.j	$⊢ \underset{˙}{\lor} = join (K)$
2		3dim0.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		3dim0.a	$⊢ A = Atoms (K)$
4		eqid	$⊢ ⋖_{K} = ⋖_{K}$
5	1 4 3	athgt	$⊢ K \in HL \to \exists p \in A \exists q \in A (p ⋖_{K} (p \underset{˙}{\lor} q) \land \exists r \in A ((p \underset{˙}{\lor} q) ⋖_{K} ((p \underset{˙}{\lor} q) \underset{˙}{\lor} r) \land \exists s \in A ((p \underset{˙}{\lor} q) \underset{˙}{\lor} r) ⋖_{K} (((p \underset{˙}{\lor} q) \underset{˙}{\lor} r) \underset{˙}{\lor} s)))$
6		df-3an	$⊢ (p \neq q \land \neg r \underset{˙}{\leq} (p \underset{˙}{\lor} q) \land \neg s \underset{˙}{\leq} ((p \underset{˙}{\lor} q) \underset{˙}{\lor} r)) \leftrightarrow ((p \neq q \land \neg r \underset{˙}{\leq} (p \underset{˙}{\lor} q)) \land \neg s \underset{˙}{\leq} ((p \underset{˙}{\lor} q) \underset{˙}{\lor} r))$
7		simpll1	$⊢ (((K \in HL \land p \in A \land q \in A) \land r \in A) \land s \in A) \to K \in HL$
8		eqid	$⊢ {Base}_{K} = {Base}_{K}$
9	8 1 3	hlatjcl	$⊢ (K \in HL \land p \in A \land q \in A) \to p \underset{˙}{\lor} q \in {Base}_{K}$
10	9	ad2antrr	$⊢ (((K \in HL \land p \in A \land q \in A) \land r \in A) \land s \in A) \to p \underset{˙}{\lor} q \in {Base}_{K}$
11		simplr	$⊢ (((K \in HL \land p \in A \land q \in A) \land r \in A) \land s \in A) \to r \in A$
12	8 2 1 4 3	cvr1	$⊢ (K \in HL \land p \underset{˙}{\lor} q \in {Base}_{K} \land r \in A) \to (\neg r \underset{˙}{\leq} (p \underset{˙}{\lor} q) \leftrightarrow (p \underset{˙}{\lor} q) ⋖_{K} ((p \underset{˙}{\lor} q) \underset{˙}{\lor} r))$
13	7 10 11 12	syl3anc	$⊢ (((K \in HL \land p \in A \land q \in A) \land r \in A) \land s \in A) \to (\neg r \underset{˙}{\leq} (p \underset{˙}{\lor} q) \leftrightarrow (p \underset{˙}{\lor} q) ⋖_{K} ((p \underset{˙}{\lor} q) \underset{˙}{\lor} r))$
14	13	anbi2d	$⊢ (((K \in HL \land p \in A \land q \in A) \land r \in A) \land s \in A) \to ((p \neq q \land \neg r \underset{˙}{\leq} (p \underset{˙}{\lor} q)) \leftrightarrow (p \neq q \land (p \underset{˙}{\lor} q) ⋖_{K} ((p \underset{˙}{\lor} q) \underset{˙}{\lor} r)))$
15	7	hllatd	$⊢ (((K \in HL \land p \in A \land q \in A) \land r \in A) \land s \in A) \to K \in Lat$
16	8 3	atbase	$⊢ r \in A \to r \in {Base}_{K}$
17	16	ad2antlr	$⊢ (((K \in HL \land p \in A \land q \in A) \land r \in A) \land s \in A) \to r \in {Base}_{K}$
18	8 1	latjcl	$⊢ (K \in Lat \land p \underset{˙}{\lor} q \in {Base}_{K} \land r \in {Base}_{K}) \to (p \underset{˙}{\lor} q) \underset{˙}{\lor} r \in {Base}_{K}$
19	15 10 17 18	syl3anc	$⊢ (((K \in HL \land p \in A \land q \in A) \land r \in A) \land s \in A) \to (p \underset{˙}{\lor} q) \underset{˙}{\lor} r \in {Base}_{K}$
20		simpr	$⊢ (((K \in HL \land p \in A \land q \in A) \land r \in A) \land s \in A) \to s \in A$
21	8 2 1 4 3	cvr1	$⊢ (K \in HL \land (p \underset{˙}{\lor} q) \underset{˙}{\lor} r \in {Base}_{K} \land s \in A) \to (\neg s \underset{˙}{\leq} ((p \underset{˙}{\lor} q) \underset{˙}{\lor} r) \leftrightarrow ((p \underset{˙}{\lor} q) \underset{˙}{\lor} r) ⋖_{K} (((p \underset{˙}{\lor} q) \underset{˙}{\lor} r) \underset{˙}{\lor} s))$
22	7 19 20 21	syl3anc	$⊢ (((K \in HL \land p \in A \land q \in A) \land r \in A) \land s \in A) \to (\neg s \underset{˙}{\leq} ((p \underset{˙}{\lor} q) \underset{˙}{\lor} r) \leftrightarrow ((p \underset{˙}{\lor} q) \underset{˙}{\lor} r) ⋖_{K} (((p \underset{˙}{\lor} q) \underset{˙}{\lor} r) \underset{˙}{\lor} s))$
23	14 22	anbi12d	$⊢ (((K \in HL \land p \in A \land q \in A) \land r \in A) \land s \in A) \to (((p \neq q \land \neg r \underset{˙}{\leq} (p \underset{˙}{\lor} q)) \land \neg s \underset{˙}{\leq} ((p \underset{˙}{\lor} q) \underset{˙}{\lor} r)) \leftrightarrow ((p \neq q \land (p \underset{˙}{\lor} q) ⋖_{K} ((p \underset{˙}{\lor} q) \underset{˙}{\lor} r)) \land ((p \underset{˙}{\lor} q) \underset{˙}{\lor} r) ⋖_{K} (((p \underset{˙}{\lor} q) \underset{˙}{\lor} r) \underset{˙}{\lor} s)))$
24	6 23	bitrid	$⊢ (((K \in HL \land p \in A \land q \in A) \land r \in A) \land s \in A) \to ((p \neq q \land \neg r \underset{˙}{\leq} (p \underset{˙}{\lor} q) \land \neg s \underset{˙}{\leq} ((p \underset{˙}{\lor} q) \underset{˙}{\lor} r)) \leftrightarrow ((p \neq q \land (p \underset{˙}{\lor} q) ⋖_{K} ((p \underset{˙}{\lor} q) \underset{˙}{\lor} r)) \land ((p \underset{˙}{\lor} q) \underset{˙}{\lor} r) ⋖_{K} (((p \underset{˙}{\lor} q) \underset{˙}{\lor} r) \underset{˙}{\lor} s)))$
25	24	rexbidva	$⊢ ((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 \underset{˙}{\leq} (p \underset{˙}{\lor} q) \land \neg s \underset{˙}{\leq} ((p \underset{˙}{\lor} q) \underset{˙}{\lor} r)) \leftrightarrow \exists s \in A ((p \neq q \land (p \underset{˙}{\lor} q) ⋖_{K} ((p \underset{˙}{\lor} q) \underset{˙}{\lor} r)) \land ((p \underset{˙}{\lor} q) \underset{˙}{\lor} r) ⋖_{K} (((p \underset{˙}{\lor} q) \underset{˙}{\lor} r) \underset{˙}{\lor} s)))$
26		r19.42v	$⊢ \exists s \in A ((p \neq q \land (p \underset{˙}{\lor} q) ⋖_{K} ((p \underset{˙}{\lor} q) \underset{˙}{\lor} r)) \land ((p \underset{˙}{\lor} q) \underset{˙}{\lor} r) ⋖_{K} (((p \underset{˙}{\lor} q) \underset{˙}{\lor} r) \underset{˙}{\lor} s)) \leftrightarrow ((p \neq q \land (p \underset{˙}{\lor} q) ⋖_{K} ((p \underset{˙}{\lor} q) \underset{˙}{\lor} r)) \land \exists s \in A ((p \underset{˙}{\lor} q) \underset{˙}{\lor} r) ⋖_{K} (((p \underset{˙}{\lor} q) \underset{˙}{\lor} r) \underset{˙}{\lor} s))$
27		anass	$⊢ ((p \neq q \land (p \underset{˙}{\lor} q) ⋖_{K} ((p \underset{˙}{\lor} q) \underset{˙}{\lor} r)) \land \exists s \in A ((p \underset{˙}{\lor} q) \underset{˙}{\lor} r) ⋖_{K} (((p \underset{˙}{\lor} q) \underset{˙}{\lor} r) \underset{˙}{\lor} s)) \leftrightarrow (p \neq q \land ((p \underset{˙}{\lor} q) ⋖_{K} ((p \underset{˙}{\lor} q) \underset{˙}{\lor} r) \land \exists s \in A ((p \underset{˙}{\lor} q) \underset{˙}{\lor} r) ⋖_{K} (((p \underset{˙}{\lor} q) \underset{˙}{\lor} r) \underset{˙}{\lor} s)))$
28	26 27	bitri	$⊢ \exists s \in A ((p \neq q \land (p \underset{˙}{\lor} q) ⋖_{K} ((p \underset{˙}{\lor} q) \underset{˙}{\lor} r)) \land ((p \underset{˙}{\lor} q) \underset{˙}{\lor} r) ⋖_{K} (((p \underset{˙}{\lor} q) \underset{˙}{\lor} r) \underset{˙}{\lor} s)) \leftrightarrow (p \neq q \land ((p \underset{˙}{\lor} q) ⋖_{K} ((p \underset{˙}{\lor} q) \underset{˙}{\lor} r) \land \exists s \in A ((p \underset{˙}{\lor} q) \underset{˙}{\lor} r) ⋖_{K} (((p \underset{˙}{\lor} q) \underset{˙}{\lor} r) \underset{˙}{\lor} s)))$
29	25 28	bitrdi	$⊢ ((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 \underset{˙}{\leq} (p \underset{˙}{\lor} q) \land \neg s \underset{˙}{\leq} ((p \underset{˙}{\lor} q) \underset{˙}{\lor} r)) \leftrightarrow (p \neq q \land ((p \underset{˙}{\lor} q) ⋖_{K} ((p \underset{˙}{\lor} q) \underset{˙}{\lor} r) \land \exists s \in A ((p \underset{˙}{\lor} q) \underset{˙}{\lor} r) ⋖_{K} (((p \underset{˙}{\lor} q) \underset{˙}{\lor} r) \underset{˙}{\lor} s))))$
30	29	rexbidva	$⊢ (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 \underset{˙}{\leq} (p \underset{˙}{\lor} q) \land \neg s \underset{˙}{\leq} ((p \underset{˙}{\lor} q) \underset{˙}{\lor} r)) \leftrightarrow \exists r \in A (p \neq q \land ((p \underset{˙}{\lor} q) ⋖_{K} ((p \underset{˙}{\lor} q) \underset{˙}{\lor} r) \land \exists s \in A ((p \underset{˙}{\lor} q) \underset{˙}{\lor} r) ⋖_{K} (((p \underset{˙}{\lor} q) \underset{˙}{\lor} r) \underset{˙}{\lor} s))))$
31		r19.42v	$⊢ \exists r \in A (p \neq q \land ((p \underset{˙}{\lor} q) ⋖_{K} ((p \underset{˙}{\lor} q) \underset{˙}{\lor} r) \land \exists s \in A ((p \underset{˙}{\lor} q) \underset{˙}{\lor} r) ⋖_{K} (((p \underset{˙}{\lor} q) \underset{˙}{\lor} r) \underset{˙}{\lor} s))) \leftrightarrow (p \neq q \land \exists r \in A ((p \underset{˙}{\lor} q) ⋖_{K} ((p \underset{˙}{\lor} q) \underset{˙}{\lor} r) \land \exists s \in A ((p \underset{˙}{\lor} q) \underset{˙}{\lor} r) ⋖_{K} (((p \underset{˙}{\lor} q) \underset{˙}{\lor} r) \underset{˙}{\lor} s)))$
32	30 31	bitrdi	$⊢ (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 \underset{˙}{\leq} (p \underset{˙}{\lor} q) \land \neg s \underset{˙}{\leq} ((p \underset{˙}{\lor} q) \underset{˙}{\lor} r)) \leftrightarrow (p \neq q \land \exists r \in A ((p \underset{˙}{\lor} q) ⋖_{K} ((p \underset{˙}{\lor} q) \underset{˙}{\lor} r) \land \exists s \in A ((p \underset{˙}{\lor} q) \underset{˙}{\lor} r) ⋖_{K} (((p \underset{˙}{\lor} q) \underset{˙}{\lor} r) \underset{˙}{\lor} s))))$
33	1 4 3	atcvr1	$⊢ (K \in HL \land p \in A \land q \in A) \to (p \neq q \leftrightarrow p ⋖_{K} (p \underset{˙}{\lor} q))$
34	33	anbi1d	$⊢ (K \in HL \land p \in A \land q \in A) \to ((p \neq q \land \exists r \in A ((p \underset{˙}{\lor} q) ⋖_{K} ((p \underset{˙}{\lor} q) \underset{˙}{\lor} r) \land \exists s \in A ((p \underset{˙}{\lor} q) \underset{˙}{\lor} r) ⋖_{K} (((p \underset{˙}{\lor} q) \underset{˙}{\lor} r) \underset{˙}{\lor} s))) \leftrightarrow (p ⋖_{K} (p \underset{˙}{\lor} q) \land \exists r \in A ((p \underset{˙}{\lor} q) ⋖_{K} ((p \underset{˙}{\lor} q) \underset{˙}{\lor} r) \land \exists s \in A ((p \underset{˙}{\lor} q) \underset{˙}{\lor} r) ⋖_{K} (((p \underset{˙}{\lor} q) \underset{˙}{\lor} r) \underset{˙}{\lor} s))))$
35	32 34	bitrd	$⊢ (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 \underset{˙}{\leq} (p \underset{˙}{\lor} q) \land \neg s \underset{˙}{\leq} ((p \underset{˙}{\lor} q) \underset{˙}{\lor} r)) \leftrightarrow (p ⋖_{K} (p \underset{˙}{\lor} q) \land \exists r \in A ((p \underset{˙}{\lor} q) ⋖_{K} ((p \underset{˙}{\lor} q) \underset{˙}{\lor} r) \land \exists s \in A ((p \underset{˙}{\lor} q) \underset{˙}{\lor} r) ⋖_{K} (((p \underset{˙}{\lor} q) \underset{˙}{\lor} r) \underset{˙}{\lor} s))))$
36	35	3expb	$⊢ (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 \underset{˙}{\leq} (p \underset{˙}{\lor} q) \land \neg s \underset{˙}{\leq} ((p \underset{˙}{\lor} q) \underset{˙}{\lor} r)) \leftrightarrow (p ⋖_{K} (p \underset{˙}{\lor} q) \land \exists r \in A ((p \underset{˙}{\lor} q) ⋖_{K} ((p \underset{˙}{\lor} q) \underset{˙}{\lor} r) \land \exists s \in A ((p \underset{˙}{\lor} q) \underset{˙}{\lor} r) ⋖_{K} (((p \underset{˙}{\lor} q) \underset{˙}{\lor} r) \underset{˙}{\lor} s))))$
37	36	2rexbidva	$⊢ K \in HL \to (\exists p \in A \exists q \in A \exists r \in A \exists s \in A (p \neq q \land \neg r \underset{˙}{\leq} (p \underset{˙}{\lor} q) \land \neg s \underset{˙}{\leq} ((p \underset{˙}{\lor} q) \underset{˙}{\lor} r)) \leftrightarrow \exists p \in A \exists q \in A (p ⋖_{K} (p \underset{˙}{\lor} q) \land \exists r \in A ((p \underset{˙}{\lor} q) ⋖_{K} ((p \underset{˙}{\lor} q) \underset{˙}{\lor} r) \land \exists s \in A ((p \underset{˙}{\lor} q) \underset{˙}{\lor} r) ⋖_{K} (((p \underset{˙}{\lor} q) \underset{˙}{\lor} r) \underset{˙}{\lor} s))))$
38	5 37	mpbird	$⊢ K \in HL \to \exists p \in A \exists q \in A \exists r \in A \exists s \in A (p \neq q \land \neg r \underset{˙}{\leq} (p \underset{˙}{\lor} q) \land \neg s \underset{˙}{\leq} ((p \underset{˙}{\lor} q) \underset{˙}{\lor} r))$

Metamath Proof Explorer

Theorem 3dim0

Proof