Metamath Proof Explorer

Theorem snatpsubN

Description: The singleton of an atom is a projective subspace. (Contributed by NM, 9-Sep-2013) (New usage is discouraged.)

Ref Expression
Hypotheses snpsub.a ⊢ A = Atoms ⁡ K
snpsub.s ⊢ S = PSubSp ⁡ K
Assertion snatpsubN ⊢ K ∈ AtLat ∧ P ∈ A → P ∈ S

Proof

Step Hyp Ref Expression
1 snpsub.a ⊢ A = Atoms ⁡ K
2 snpsub.s ⊢ S = PSubSp ⁡ K
3 snssi ⊢ P ∈ A → P ⊆ A
4 3 adantl ⊢ K ∈ AtLat ∧ P ∈ A → P ⊆ A
5 atllat ⊢ K ∈ AtLat → K ∈ Lat
6 eqid ⊢ Base K = Base K
7 6 1 atbase ⊢ P ∈ A → P ∈ Base K
8 eqid ⊢ join ⁡ K = join ⁡ K
9 6 8 latjidm ⊢ K ∈ Lat ∧ P ∈ Base K → P join ⁡ K P = P
10 5 7 9 syl2an ⊢ K ∈ AtLat ∧ P ∈ A → P join ⁡ K P = P
11 10 adantr ⊢ K ∈ AtLat ∧ P ∈ A ∧ r ∈ A → P join ⁡ K P = P
12 11 breq2d ⊢ K ∈ AtLat ∧ P ∈ A ∧ r ∈ A → r ≤ K P join ⁡ K P ↔ r ≤ K P
13 eqid ⊢ ≤ K = ≤ K
14 13 1 atcmp ⊢ K ∈ AtLat ∧ r ∈ A ∧ P ∈ A → r ≤ K P ↔ r = P
15 14 3com23 ⊢ K ∈ AtLat ∧ P ∈ A ∧ r ∈ A → r ≤ K P ↔ r = P
16 15 3expa ⊢ K ∈ AtLat ∧ P ∈ A ∧ r ∈ A → r ≤ K P ↔ r = P
17 16 biimpd ⊢ K ∈ AtLat ∧ P ∈ A ∧ r ∈ A → r ≤ K P → r = P
18 12 17 sylbid ⊢ K ∈ AtLat ∧ P ∈ A ∧ r ∈ A → r ≤ K P join ⁡ K P → r = P
19 18 adantld ⊢ K ∈ AtLat ∧ P ∈ A ∧ r ∈ A → p = P ∧ q = P ∧ r ≤ K P join ⁡ K P → r = P
20 velsn ⊢ p ∈ P ↔ p = P
21 velsn ⊢ q ∈ P ↔ q = P
22 20 21 anbi12i ⊢ p ∈ P ∧ q ∈ P ↔ p = P ∧ q = P
23 22 anbi1i ⊢ p ∈ P ∧ q ∈ P ∧ r ≤ K p join ⁡ K q ↔ p = P ∧ q = P ∧ r ≤ K p join ⁡ K q
24 oveq12 ⊢ p = P ∧ q = P → p join ⁡ K q = P join ⁡ K P
25 24 breq2d ⊢ p = P ∧ q = P → r ≤ K p join ⁡ K q ↔ r ≤ K P join ⁡ K P
26 25 pm5.32i ⊢ p = P ∧ q = P ∧ r ≤ K p join ⁡ K q ↔ p = P ∧ q = P ∧ r ≤ K P join ⁡ K P
27 23 26 bitri ⊢ p ∈ P ∧ q ∈ P ∧ r ≤ K p join ⁡ K q ↔ p = P ∧ q = P ∧ r ≤ K P join ⁡ K P
28 velsn ⊢ r ∈ P ↔ r = P
29 19 27 28 3imtr4g ⊢ K ∈ AtLat ∧ P ∈ A ∧ r ∈ A → p ∈ P ∧ q ∈ P ∧ r ≤ K p join ⁡ K q → r ∈ P
30 29 exp4b ⊢ K ∈ AtLat ∧ P ∈ A → r ∈ A → p ∈ P ∧ q ∈ P → r ≤ K p join ⁡ K q → r ∈ P
31 30 com23 ⊢ K ∈ AtLat ∧ P ∈ A → p ∈ P ∧ q ∈ P → r ∈ A → r ≤ K p join ⁡ K q → r ∈ P
32 31 ralrimdv ⊢ K ∈ AtLat ∧ P ∈ A → p ∈ P ∧ q ∈ P → ∀ r ∈ A r ≤ K p join ⁡ K q → r ∈ P
33 32 ralrimivv ⊢ K ∈ AtLat ∧ P ∈ A → ∀ p ∈ P ∀ q ∈ P ∀ r ∈ A r ≤ K p join ⁡ K q → r ∈ P
34 4 33 jca ⊢ K ∈ AtLat ∧ P ∈ A → P ⊆ A ∧ ∀ p ∈ P ∀ q ∈ P ∀ r ∈ A r ≤ K p join ⁡ K q → r ∈ P
35 34 ex ⊢ K ∈ AtLat → P ∈ A → P ⊆ A ∧ ∀ p ∈ P ∀ q ∈ P ∀ r ∈ A r ≤ K p join ⁡ K q → r ∈ P
36 13 8 1 2 ispsubsp ⊢ K ∈ AtLat → P ∈ S ↔ P ⊆ A ∧ ∀ p ∈ P ∀ q ∈ P ∀ r ∈ A r ≤ K p join ⁡ K q → r ∈ P
37 35 36 sylibrd ⊢ K ∈ AtLat → P ∈ A → P ∈ S
38 37 imp ⊢ K ∈ AtLat ∧ P ∈ A → P ∈ S