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 ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
snpsub.s ⊢ 𝑆 = ( PSubSp ‘ 𝐾 )
Assertion snatpsubN ( ( 𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ) → { 𝑃 } ∈ 𝑆 )

Proof

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