islpln3

Description: The predicate "is a lattice plane". (Contributed by NM, 17-Jun-2012)

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

Proof

Step	Hyp	Ref	Expression
1		islpln3.b	$⊢ B = {Base}_{K}$
2		islpln3.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		islpln3.j	$⊢ \underset{˙}{\lor} = join (K)$
4		islpln3.a	$⊢ A = Atoms (K)$
5		islpln3.n	$⊢ N = LLines (K)$
6		islpln3.p	$⊢ P = LPlanes (K)$
7		eqid	$⊢ ⋖_{K} = ⋖_{K}$
8	1 7 5 6	islpln4	$⊢ (K \in HL \land X \in B) \to (X \in P \leftrightarrow \exists y \in N y ⋖_{K} X)$
9		simpll	$⊢ ((K \in HL \land X \in B) \land y \in N) \to K \in HL$
10	1 5	llnbase	$⊢ y \in N \to y \in B$
11	10	adantl	$⊢ ((K \in HL \land X \in B) \land y \in N) \to y \in B$
12		simplr	$⊢ ((K \in HL \land X \in B) \land y \in N) \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 N) \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 N) \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 N) \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 N) \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 N) \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 N y ⋖_{K} X \leftrightarrow \exists y \in N \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 P \leftrightarrow \exists y \in N \exists p \in A (\neg p \underset{˙}{\leq} y \land X = y \underset{˙}{\lor} p))$

Metamath Proof Explorer

Theorem islpln3

Proof