Metamath Proof Explorer

Theorem islpln3

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

Ref Expression
Hypotheses islpln3.b ⊢ B = Base K
islpln3.l ⊢ ≤ ˙ = ≤ K
islpln3.j ⊢ ∨ ˙ = join ⁡ K
islpln3.a ⊢ A = Atoms ⁡ K
islpln3.n ⊢ N = LLines ⁡ K
islpln3.p ⊢ P = LPlanes ⁡ K
Assertion islpln3 ⊢ K ∈ HL ∧ X ∈ B → X ∈ P ↔ ∃ y ∈ N ∃ p ∈ A ¬ p ≤ ˙ y ∧ X = y ∨ ˙ p

Proof

Step Hyp Ref Expression
1 islpln3.b ⊢ B = Base K
2 islpln3.l ⊢ ≤ ˙ = ≤ K
3 islpln3.j ⊢ ∨ ˙ = 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 ∈ HL ∧ X ∈ B → X ∈ P ↔ ∃ y ∈ N y ⋖ K X
9 simpll ⊢ K ∈ HL ∧ X ∈ B ∧ y ∈ N → K ∈ HL
10 1 5 llnbase ⊢ y ∈ N → y ∈ B
11 10 adantl ⊢ K ∈ HL ∧ X ∈ B ∧ y ∈ N → y ∈ B
12 simplr ⊢ K ∈ HL ∧ X ∈ B ∧ y ∈ N → X ∈ B
13 1 2 3 7 4 cvrval3 ⊢ K ∈ HL ∧ y ∈ B ∧ X ∈ B → y ⋖ K X ↔ ∃ p ∈ A ¬ p ≤ ˙ y ∧ y ∨ ˙ p = X
14 9 11 12 13 syl3anc ⊢ K ∈ HL ∧ X ∈ B ∧ y ∈ N → y ⋖ K X ↔ ∃ p ∈ A ¬ p ≤ ˙ y ∧ y ∨ ˙ p = X
15 eqcom ⊢ y ∨ ˙ p = X ↔ X = y ∨ ˙ p
16 15 a1i ⊢ K ∈ HL ∧ X ∈ B ∧ y ∈ N ∧ p ∈ A → y ∨ ˙ p = X ↔ X = y ∨ ˙ p
17 16 anbi2d ⊢ K ∈ HL ∧ X ∈ B ∧ y ∈ N ∧ p ∈ A → ¬ p ≤ ˙ y ∧ y ∨ ˙ p = X ↔ ¬ p ≤ ˙ y ∧ X = y ∨ ˙ p
18 17 rexbidva ⊢ K ∈ HL ∧ X ∈ B ∧ y ∈ N → ∃ p ∈ A ¬ p ≤ ˙ y ∧ y ∨ ˙ p = X ↔ ∃ p ∈ A ¬ p ≤ ˙ y ∧ X = y ∨ ˙ p
19 14 18 bitrd ⊢ K ∈ HL ∧ X ∈ B ∧ y ∈ N → y ⋖ K X ↔ ∃ p ∈ A ¬ p ≤ ˙ y ∧ X = y ∨ ˙ p
20 19 rexbidva ⊢ K ∈ HL ∧ X ∈ B → ∃ y ∈ N y ⋖ K X ↔ ∃ y ∈ N ∃ p ∈ A ¬ p ≤ ˙ y ∧ X = y ∨ ˙ p
21 8 20 bitrd ⊢ K ∈ HL ∧ X ∈ B → X ∈ P ↔ ∃ y ∈ N ∃ p ∈ A ¬ p ≤ ˙ y ∧ X = y ∨ ˙ p