Metamath Proof Explorer

Theorem islln3

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

Ref Expression
Hypotheses islln3.b ⊢ B = Base K
islln3.j ⊢ ∨ ˙ = join ⁡ K
islln3.a ⊢ A = Atoms ⁡ K
islln3.n ⊢ N = LLines ⁡ K
Assertion islln3 ⊢ K ∈ HL ∧ X ∈ B → X ∈ N ↔ ∃ p ∈ A ∃ q ∈ A p ≠ q ∧ X = p ∨ ˙ q

Proof

Step Hyp Ref Expression
1 islln3.b ⊢ B = Base K
2 islln3.j ⊢ ∨ ˙ = join ⁡ K
3 islln3.a ⊢ A = Atoms ⁡ K
4 islln3.n ⊢ N = LLines ⁡ K
5 eqid ⊢ ⋖ K = ⋖ K
6 1 5 3 4 islln4 ⊢ K ∈ HL ∧ X ∈ B → X ∈ N ↔ ∃ p ∈ A p ⋖ K X
7 simpll ⊢ K ∈ HL ∧ X ∈ B ∧ p ∈ A → K ∈ HL
8 1 3 atbase ⊢ p ∈ A → p ∈ B
9 8 adantl ⊢ K ∈ HL ∧ X ∈ B ∧ p ∈ A → p ∈ B
10 simplr ⊢ K ∈ HL ∧ X ∈ B ∧ p ∈ A → X ∈ B
11 eqid ⊢ ≤ K = ≤ K
12 1 11 2 5 3 cvrval3 ⊢ K ∈ HL ∧ p ∈ B ∧ X ∈ B → p ⋖ K X ↔ ∃ q ∈ A ¬ q ≤ K p ∧ p ∨ ˙ q = X
13 7 9 10 12 syl3anc ⊢ K ∈ HL ∧ X ∈ B ∧ p ∈ A → p ⋖ K X ↔ ∃ q ∈ A ¬ q ≤ K p ∧ p ∨ ˙ q = X
14 hlatl ⊢ K ∈ HL → K ∈ AtLat
15 14 ad3antrrr ⊢ K ∈ HL ∧ X ∈ B ∧ p ∈ A ∧ q ∈ A → K ∈ AtLat
16 simpr ⊢ K ∈ HL ∧ X ∈ B ∧ p ∈ A ∧ q ∈ A → q ∈ A
17 simplr ⊢ K ∈ HL ∧ X ∈ B ∧ p ∈ A ∧ q ∈ A → p ∈ A
18 11 3 atncmp ⊢ K ∈ AtLat ∧ q ∈ A ∧ p ∈ A → ¬ q ≤ K p ↔ q ≠ p
19 15 16 17 18 syl3anc ⊢ K ∈ HL ∧ X ∈ B ∧ p ∈ A ∧ q ∈ A → ¬ q ≤ K p ↔ q ≠ p
20 necom ⊢ q ≠ p ↔ p ≠ q
21 19 20 bitrdi ⊢ K ∈ HL ∧ X ∈ B ∧ p ∈ A ∧ q ∈ A → ¬ q ≤ K p ↔ p ≠ q
22 eqcom ⊢ p ∨ ˙ q = X ↔ X = p ∨ ˙ q
23 22 a1i ⊢ K ∈ HL ∧ X ∈ B ∧ p ∈ A ∧ q ∈ A → p ∨ ˙ q = X ↔ X = p ∨ ˙ q
24 21 23 anbi12d ⊢ K ∈ HL ∧ X ∈ B ∧ p ∈ A ∧ q ∈ A → ¬ q ≤ K p ∧ p ∨ ˙ q = X ↔ p ≠ q ∧ X = p ∨ ˙ q
25 24 rexbidva ⊢ K ∈ HL ∧ X ∈ B ∧ p ∈ A → ∃ q ∈ A ¬ q ≤ K p ∧ p ∨ ˙ q = X ↔ ∃ q ∈ A p ≠ q ∧ X = p ∨ ˙ q
26 13 25 bitrd ⊢ K ∈ HL ∧ X ∈ B ∧ p ∈ A → p ⋖ K X ↔ ∃ q ∈ A p ≠ q ∧ X = p ∨ ˙ q
27 26 rexbidva ⊢ K ∈ HL ∧ X ∈ B → ∃ p ∈ A p ⋖ K X ↔ ∃ p ∈ A ∃ q ∈ A p ≠ q ∧ X = p ∨ ˙ q
28 6 27 bitrd ⊢ K ∈ HL ∧ X ∈ B → X ∈ N ↔ ∃ p ∈ A ∃ q ∈ A p ≠ q ∧ X = p ∨ ˙ q