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 e. AtLat /\ P e. A ) -> { P } e. S )

Proof

Step Hyp Ref Expression
1 snpsub.a 
 |-  A = ( Atoms ` K )
2 snpsub.s 
 |-  S = ( PSubSp ` K )
3 snssi 
 |-  ( P e. A -> { P } C_ A )
4 3 adantl 
 |-  ( ( K e. AtLat /\ P e. A ) -> { P } C_ A )
5 atllat 
 |-  ( K e. AtLat -> K e. Lat )
6 eqid 
 |-  ( Base ` K ) = ( Base ` K )
7 6 1 atbase 
 |-  ( P e. A -> P e. ( Base ` K ) )
8 eqid 
 |-  ( join ` K ) = ( join ` K )
9 6 8 latjidm 
 |-  ( ( K e. Lat /\ P e. ( Base ` K ) ) -> ( P ( join ` K ) P ) = P )
10 5 7 9 syl2an 
 |-  ( ( K e. AtLat /\ P e. A ) -> ( P ( join ` K ) P ) = P )
11 10 adantr 
 |-  ( ( ( K e. AtLat /\ P e. A ) /\ r e. A ) -> ( P ( join ` K ) P ) = P )
12 11 breq2d 
 |-  ( ( ( K e. AtLat /\ P e. A ) /\ r e. A ) -> ( r ( le ` K ) ( P ( join ` K ) P ) <-> r ( le ` K ) P ) )
13 eqid 
 |-  ( le ` K ) = ( le ` K )
14 13 1 atcmp 
 |-  ( ( K e. AtLat /\ r e. A /\ P e. A ) -> ( r ( le ` K ) P <-> r = P ) )
15 14 3com23 
 |-  ( ( K e. AtLat /\ P e. A /\ r e. A ) -> ( r ( le ` K ) P <-> r = P ) )
16 15 3expa 
 |-  ( ( ( K e. AtLat /\ P e. A ) /\ r e. A ) -> ( r ( le ` K ) P <-> r = P ) )
17 16 biimpd 
 |-  ( ( ( K e. AtLat /\ P e. A ) /\ r e. A ) -> ( r ( le ` K ) P -> r = P ) )
18 12 17 sylbid 
 |-  ( ( ( K e. AtLat /\ P e. A ) /\ r e. A ) -> ( r ( le ` K ) ( P ( join ` K ) P ) -> r = P ) )
19 18 adantld 
 |-  ( ( ( K e. AtLat /\ P e. A ) /\ r e. A ) -> ( ( ( p = P /\ q = P ) /\ r ( le ` K ) ( P ( join ` K ) P ) ) -> r = P ) )
20 velsn 
 |-  ( p e. { P } <-> p = P )
21 velsn 
 |-  ( q e. { P } <-> q = P )
22 20 21 anbi12i 
 |-  ( ( p e. { P } /\ q e. { P } ) <-> ( p = P /\ q = P ) )
23 22 anbi1i 
 |-  ( ( ( p e. { P } /\ q e. { P } ) /\ r ( le ` K ) ( p ( join ` K ) q ) ) <-> ( ( p = P /\ q = P ) /\ r ( le ` 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 ( le ` K ) ( p ( join ` K ) q ) <-> r ( le ` K ) ( P ( join ` K ) P ) ) )
26 25 pm5.32i 
 |-  ( ( ( p = P /\ q = P ) /\ r ( le ` K ) ( p ( join ` K ) q ) ) <-> ( ( p = P /\ q = P ) /\ r ( le ` K ) ( P ( join ` K ) P ) ) )
27 23 26 bitri 
 |-  ( ( ( p e. { P } /\ q e. { P } ) /\ r ( le ` K ) ( p ( join ` K ) q ) ) <-> ( ( p = P /\ q = P ) /\ r ( le ` K ) ( P ( join ` K ) P ) ) )
28 velsn 
 |-  ( r e. { P } <-> r = P )
29 19 27 28 3imtr4g 
 |-  ( ( ( K e. AtLat /\ P e. A ) /\ r e. A ) -> ( ( ( p e. { P } /\ q e. { P } ) /\ r ( le ` K ) ( p ( join ` K ) q ) ) -> r e. { P } ) )
30 29 exp4b 
 |-  ( ( K e. AtLat /\ P e. A ) -> ( r e. A -> ( ( p e. { P } /\ q e. { P } ) -> ( r ( le ` K ) ( p ( join ` K ) q ) -> r e. { P } ) ) ) )
31 30 com23 
 |-  ( ( K e. AtLat /\ P e. A ) -> ( ( p e. { P } /\ q e. { P } ) -> ( r e. A -> ( r ( le ` K ) ( p ( join ` K ) q ) -> r e. { P } ) ) ) )
32 31 ralrimdv 
 |-  ( ( K e. AtLat /\ P e. A ) -> ( ( p e. { P } /\ q e. { P } ) -> A. r e. A ( r ( le ` K ) ( p ( join ` K ) q ) -> r e. { P } ) ) )
33 32 ralrimivv 
 |-  ( ( K e. AtLat /\ P e. A ) -> A. p e. { P } A. q e. { P } A. r e. A ( r ( le ` K ) ( p ( join ` K ) q ) -> r e. { P } ) )
34 4 33 jca 
 |-  ( ( K e. AtLat /\ P e. A ) -> ( { P } C_ A /\ A. p e. { P } A. q e. { P } A. r e. A ( r ( le ` K ) ( p ( join ` K ) q ) -> r e. { P } ) ) )
35 34 ex 
 |-  ( K e. AtLat -> ( P e. A -> ( { P } C_ A /\ A. p e. { P } A. q e. { P } A. r e. A ( r ( le ` K ) ( p ( join ` K ) q ) -> r e. { P } ) ) ) )
36 13 8 1 2 ispsubsp 
 |-  ( K e. AtLat -> ( { P } e. S <-> ( { P } C_ A /\ A. p e. { P } A. q e. { P } A. r e. A ( r ( le ` K ) ( p ( join ` K ) q ) -> r e. { P } ) ) ) )
37 35 36 sylibrd 
 |-  ( K e. AtLat -> ( P e. A -> { P } e. S ) )
38 37 imp 
 |-  ( ( K e. AtLat /\ P e. A ) -> { P } e. S )