Metamath Proof Explorer

Theorem isline3

Description: Definition of line in terms of original lattice elements. (Contributed by NM, 29-Apr-2012)

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

Proof

Step Hyp Ref Expression
1 isline3.b ⊢ B = Base K
2 isline3.j ⊢ ∨ ˙ = join ⁡ K
3 isline3.a ⊢ A = Atoms ⁡ K
4 isline3.n ⊢ N = Lines ⁡ K
5 isline3.m ⊢ M = pmap ⁡ K
6 hllat ⊢ K ∈ HL → K ∈ Lat
7 6 adantr ⊢ K ∈ HL ∧ X ∈ B → K ∈ Lat
8 2 3 4 5 isline2 ⊢ K ∈ Lat → M ⁡ X ∈ N ↔ ∃ p ∈ A ∃ q ∈ A p ≠ q ∧ M ⁡ X = M ⁡ p ∨ ˙ q
9 7 8 syl ⊢ K ∈ HL ∧ X ∈ B → M ⁡ X ∈ N ↔ ∃ p ∈ A ∃ q ∈ A p ≠ q ∧ M ⁡ X = M ⁡ p ∨ ˙ q
10 simpll ⊢ K ∈ HL ∧ X ∈ B ∧ p ∈ A ∧ q ∈ A → K ∈ HL
11 simplr ⊢ K ∈ HL ∧ X ∈ B ∧ p ∈ A ∧ q ∈ A → X ∈ B
12 6 ad2antrr ⊢ K ∈ HL ∧ X ∈ B ∧ p ∈ A ∧ q ∈ A → K ∈ Lat
13 1 3 atbase ⊢ p ∈ A → p ∈ B
14 13 ad2antrl ⊢ K ∈ HL ∧ X ∈ B ∧ p ∈ A ∧ q ∈ A → p ∈ B
15 1 3 atbase ⊢ q ∈ A → q ∈ B
16 15 ad2antll ⊢ K ∈ HL ∧ X ∈ B ∧ p ∈ A ∧ q ∈ A → q ∈ B
17 1 2 latjcl ⊢ K ∈ Lat ∧ p ∈ B ∧ q ∈ B → p ∨ ˙ q ∈ B
18 12 14 16 17 syl3anc ⊢ K ∈ HL ∧ X ∈ B ∧ p ∈ A ∧ q ∈ A → p ∨ ˙ q ∈ B
19 1 5 pmap11 ⊢ K ∈ HL ∧ X ∈ B ∧ p ∨ ˙ q ∈ B → M ⁡ X = M ⁡ p ∨ ˙ q ↔ X = p ∨ ˙ q
20 10 11 18 19 syl3anc ⊢ K ∈ HL ∧ X ∈ B ∧ p ∈ A ∧ q ∈ A → M ⁡ X = M ⁡ p ∨ ˙ q ↔ X = p ∨ ˙ q
21 20 anbi2d ⊢ K ∈ HL ∧ X ∈ B ∧ p ∈ A ∧ q ∈ A → p ≠ q ∧ M ⁡ X = M ⁡ p ∨ ˙ q ↔ p ≠ q ∧ X = p ∨ ˙ q
22 21 2rexbidva ⊢ K ∈ HL ∧ X ∈ B → ∃ p ∈ A ∃ q ∈ A p ≠ q ∧ M ⁡ X = M ⁡ p ∨ ˙ q ↔ ∃ p ∈ A ∃ q ∈ A p ≠ q ∧ X = p ∨ ˙ q
23 9 22 bitrd ⊢ K ∈ HL ∧ X ∈ B → M ⁡ X ∈ N ↔ ∃ p ∈ A ∃ q ∈ A p ≠ q ∧ X = p ∨ ˙ q