Metamath Proof Explorer

Theorem lplni

Description: Condition implying a lattice plane. (Contributed by NM, 20-Jun-2012)

Ref Expression
Hypotheses lplnset.b ⊢ B = Base K
lplnset.c ⊢ C = ⋖ K
lplnset.n ⊢ N = LLines ⁡ K
lplnset.p ⊢ P = LPlanes ⁡ K
Assertion lplni ⊢ K ∈ D ∧ Y ∈ B ∧ X ∈ N ∧ X C Y → Y ∈ P

Proof

Step Hyp Ref Expression
1 lplnset.b ⊢ B = Base K
2 lplnset.c ⊢ C = ⋖ K
3 lplnset.n ⊢ N = LLines ⁡ K
4 lplnset.p ⊢ P = LPlanes ⁡ K
5 simpl2 ⊢ K ∈ D ∧ Y ∈ B ∧ X ∈ N ∧ X C Y → Y ∈ B
6 breq1 ⊢ x = X → x C Y ↔ X C Y
7 6 rspcev ⊢ X ∈ N ∧ X C Y → ∃ x ∈ N x C Y
8 7 3ad2antl3 ⊢ K ∈ D ∧ Y ∈ B ∧ X ∈ N ∧ X C Y → ∃ x ∈ N x C Y
9 simpl1 ⊢ K ∈ D ∧ Y ∈ B ∧ X ∈ N ∧ X C Y → K ∈ D
10 1 2 3 4 islpln ⊢ K ∈ D → Y ∈ P ↔ Y ∈ B ∧ ∃ x ∈ N x C Y
11 9 10 syl ⊢ K ∈ D ∧ Y ∈ B ∧ X ∈ N ∧ X C Y → Y ∈ P ↔ Y ∈ B ∧ ∃ x ∈ N x C Y
12 5 8 11 mpbir2and ⊢ K ∈ D ∧ Y ∈ B ∧ X ∈ N ∧ X C Y → Y ∈ P