Metamath Proof Explorer

Theorem linepmap

Description: A line described with a projective map. (Contributed by NM, 3-Feb-2012)

Ref Expression
Hypotheses isline2.j ⊢ ∨ ˙ = join ⁡ K
isline2.a ⊢ A = Atoms ⁡ K
isline2.n ⊢ N = Lines ⁡ K
isline2.m ⊢ M = pmap ⁡ K
Assertion linepmap ⊢ K ∈ Lat ∧ P ∈ A ∧ Q ∈ A ∧ P ≠ Q → M ⁡ P ∨ ˙ Q ∈ N

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 simpl1 ⊢ K ∈ Lat ∧ P ∈ A ∧ Q ∈ A ∧ P ≠ Q → K ∈ Lat
6 simpl2 ⊢ K ∈ Lat ∧ P ∈ A ∧ Q ∈ A ∧ P ≠ Q → P ∈ A
7 eqid ⊢ Base K = Base K
8 7 2 atbase ⊢ P ∈ A → P ∈ Base K
9 6 8 syl ⊢ K ∈ Lat ∧ P ∈ A ∧ Q ∈ A ∧ P ≠ Q → P ∈ Base K
10 simpl3 ⊢ K ∈ Lat ∧ P ∈ A ∧ Q ∈ A ∧ P ≠ Q → Q ∈ A
11 7 2 atbase ⊢ Q ∈ A → Q ∈ Base K
12 10 11 syl ⊢ K ∈ Lat ∧ P ∈ A ∧ Q ∈ A ∧ P ≠ Q → Q ∈ Base K
13 7 1 latjcl ⊢ K ∈ Lat ∧ P ∈ Base K ∧ Q ∈ Base K → P ∨ ˙ Q ∈ Base K
14 5 9 12 13 syl3anc ⊢ K ∈ Lat ∧ P ∈ A ∧ Q ∈ A ∧ P ≠ Q → P ∨ ˙ Q ∈ Base K
15 eqid ⊢ ≤ K = ≤ K
16 7 15 2 4 pmapval ⊢ K ∈ Lat ∧ P ∨ ˙ Q ∈ Base K → M ⁡ P ∨ ˙ Q = r ∈ A | r ≤ K P ∨ ˙ Q
17 5 14 16 syl2anc ⊢ K ∈ Lat ∧ P ∈ A ∧ Q ∈ A ∧ P ≠ Q → M ⁡ P ∨ ˙ Q = r ∈ A | r ≤ K P ∨ ˙ Q
18 eqid ⊢ r ∈ A | r ≤ K P ∨ ˙ Q = r ∈ A | r ≤ K P ∨ ˙ Q
19 15 1 2 3 islinei ⊢ K ∈ Lat ∧ P ∈ A ∧ Q ∈ A ∧ P ≠ Q ∧ r ∈ A | r ≤ K P ∨ ˙ Q = r ∈ A | r ≤ K P ∨ ˙ Q → r ∈ A | r ≤ K P ∨ ˙ Q ∈ N
20 18 19 mpanr2 ⊢ K ∈ Lat ∧ P ∈ A ∧ Q ∈ A ∧ P ≠ Q → r ∈ A | r ≤ K P ∨ ˙ Q ∈ N
21 17 20 eqeltrd ⊢ K ∈ Lat ∧ P ∈ A ∧ Q ∈ A ∧ P ≠ Q → M ⁡ P ∨ ˙ Q ∈ N