islvol3

Description: The predicate "is a 3-dim lattice volume". (Contributed by NM, 1-Jul-2012)

	Ref	Expression
Hypotheses	islvol3.b	$⊢ B = {Base}_{K}$
	islvol3.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	islvol3.j	$⊢ \underset{˙}{\lor} = join (K)$
	islvol3.a	$⊢ A = Atoms (K)$
	islvol3.p	$⊢ P = LPlanes (K)$
	islvol3.v	$⊢ V = LVols (K)$
Assertion	islvol3	$⊢ (K \in HL \land X \in B) \to (X \in V \leftrightarrow \exists y \in P \exists p \in A (\neg p \underset{˙}{\leq} y \land X = y \underset{˙}{\lor} p))$

Proof

Step	Hyp	Ref	Expression
1		islvol3.b	$⊢ B = {Base}_{K}$
2		islvol3.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		islvol3.j	$⊢ \underset{˙}{\lor} = join (K)$
4		islvol3.a	$⊢ A = Atoms (K)$
5		islvol3.p	$⊢ P = LPlanes (K)$
6		islvol3.v	$⊢ V = LVols (K)$
7		eqid	$⊢ ⋖_{K} = ⋖_{K}$
8	1 7 5 6	islvol4	$⊢ (K \in HL \land X \in B) \to (X \in V \leftrightarrow \exists y \in P y ⋖_{K} X)$
9		simpll	$⊢ ((K \in HL \land X \in B) \land y \in P) \to K \in HL$
10	1 5	lplnbase	$⊢ y \in P \to y \in B$
11	10	adantl	$⊢ ((K \in HL \land X \in B) \land y \in P) \to y \in B$
12		simplr	$⊢ ((K \in HL \land X \in B) \land y \in P) \to X \in B$
13	1 2 3 7 4	cvrval3	$⊢ (K \in HL \land y \in B \land X \in B) \to (y ⋖_{K} X \leftrightarrow \exists p \in A (\neg p \underset{˙}{\leq} y \land y \underset{˙}{\lor} p = X))$
14	9 11 12 13	syl3anc	$⊢ ((K \in HL \land X \in B) \land y \in P) \to (y ⋖_{K} X \leftrightarrow \exists p \in A (\neg p \underset{˙}{\leq} y \land y \underset{˙}{\lor} p = X))$
15		eqcom	$⊢ y \underset{˙}{\lor} p = X \leftrightarrow X = y \underset{˙}{\lor} p$
16	15	a1i	$⊢ (((K \in HL \land X \in B) \land y \in P) \land p \in A) \to (y \underset{˙}{\lor} p = X \leftrightarrow X = y \underset{˙}{\lor} p)$
17	16	anbi2d	$⊢ (((K \in HL \land X \in B) \land y \in P) \land p \in A) \to ((\neg p \underset{˙}{\leq} y \land y \underset{˙}{\lor} p = X) \leftrightarrow (\neg p \underset{˙}{\leq} y \land X = y \underset{˙}{\lor} p))$
18	17	rexbidva	$⊢ ((K \in HL \land X \in B) \land y \in P) \to (\exists p \in A (\neg p \underset{˙}{\leq} y \land y \underset{˙}{\lor} p = X) \leftrightarrow \exists p \in A (\neg p \underset{˙}{\leq} y \land X = y \underset{˙}{\lor} p))$
19	14 18	bitrd	$⊢ ((K \in HL \land X \in B) \land y \in P) \to (y ⋖_{K} X \leftrightarrow \exists p \in A (\neg p \underset{˙}{\leq} y \land X = y \underset{˙}{\lor} p))$
20	19	rexbidva	$⊢ (K \in HL \land X \in B) \to (\exists y \in P y ⋖_{K} X \leftrightarrow \exists y \in P \exists p \in A (\neg p \underset{˙}{\leq} y \land X = y \underset{˙}{\lor} p))$
21	8 20	bitrd	$⊢ (K \in HL \land X \in B) \to (X \in V \leftrightarrow \exists y \in P \exists p \in A (\neg p \underset{˙}{\leq} y \land X = y \underset{˙}{\lor} p))$

Metamath Proof Explorer

Theorem islvol3

Proof