Metamath Proof Explorer

Theorem isline2

Description: Definition of line in terms of projective map. (Contributed by NM, 25-Jan-2012)

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

Proof

Step Hyp Ref Expression
1 isline2.j ⊢ ∨ ˙ = join ⁡ K
2 isline2.a ⊢ A = Atoms ⁡ K
3 isline2.n ⊢ N = Lines ⁡ K
4 isline2.m ⊢ M = pmap ⁡ K
5 eqid ⊢ ≤ K = ≤ K
6 5 1 2 3 isline ⊢ K ∈ Lat → X ∈ N ↔ ∃ p ∈ A ∃ q ∈ A p ≠ q ∧ X = r ∈ A | r ≤ K p ∨ ˙ q
7 simpl ⊢ K ∈ Lat ∧ p ∈ A ∧ q ∈ A → K ∈ Lat
8 eqid ⊢ Base K = Base K
9 8 2 atbase ⊢ p ∈ A → p ∈ Base K
10 9 ad2antrl ⊢ K ∈ Lat ∧ p ∈ A ∧ q ∈ A → p ∈ Base K
11 8 2 atbase ⊢ q ∈ A → q ∈ Base K
12 11 ad2antll ⊢ K ∈ Lat ∧ p ∈ A ∧ q ∈ A → q ∈ Base K
13 8 1 latjcl ⊢ K ∈ Lat ∧ p ∈ Base K ∧ q ∈ Base K → p ∨ ˙ q ∈ Base K
14 7 10 12 13 syl3anc ⊢ K ∈ Lat ∧ p ∈ A ∧ q ∈ A → p ∨ ˙ q ∈ Base K
15 8 5 2 4 pmapval ⊢ K ∈ Lat ∧ p ∨ ˙ q ∈ Base K → M ⁡ p ∨ ˙ q = r ∈ A | r ≤ K p ∨ ˙ q
16 14 15 syldan ⊢ K ∈ Lat ∧ p ∈ A ∧ q ∈ A → M ⁡ p ∨ ˙ q = r ∈ A | r ≤ K p ∨ ˙ q
17 16 eqeq2d ⊢ K ∈ Lat ∧ p ∈ A ∧ q ∈ A → X = M ⁡ p ∨ ˙ q ↔ X = r ∈ A | r ≤ K p ∨ ˙ q
18 17 anbi2d ⊢ K ∈ Lat ∧ p ∈ A ∧ q ∈ A → p ≠ q ∧ X = M ⁡ p ∨ ˙ q ↔ p ≠ q ∧ X = r ∈ A | r ≤ K p ∨ ˙ q
19 18 2rexbidva ⊢ K ∈ Lat → ∃ p ∈ A ∃ q ∈ A p ≠ q ∧ X = M ⁡ p ∨ ˙ q ↔ ∃ p ∈ A ∃ q ∈ A p ≠ q ∧ X = r ∈ A | r ≤ K p ∨ ˙ q
20 6 19 bitr4d ⊢ K ∈ Lat → X ∈ N ↔ ∃ p ∈ A ∃ q ∈ A p ≠ q ∧ X = M ⁡ p ∨ ˙ q