Metamath Proof Explorer

Theorem isline4N

Description: Definition of line in terms of original lattice elements. (Contributed by NM, 16-Jun-2012) (New usage is discouraged.)

Ref Expression
Hypotheses isline4.b ⊢ B = Base K
isline4.c ⊢ C = ⋖ K
isline4.a ⊢ A = Atoms ⁡ K
isline4.n ⊢ N = Lines ⁡ K
isline4.m ⊢ M = pmap ⁡ K
Assertion isline4N ⊢ K ∈ HL ∧ X ∈ B → M ⁡ X ∈ N ↔ ∃ p ∈ A p C X

Proof

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