Metamath Proof Explorer

Theorem linepsubN

Description: A line is a projective subspace. (Contributed by NM, 16-Oct-2011) (New usage is discouraged.)

Ref Expression
Hypotheses linepsub.n 
|- N = ( Lines ` K )
linepsub.s 
|- S = ( PSubSp ` K )
Assertion linepsubN 
|- ( ( K e. Lat /\ X e. N ) -> X e. S )

Proof

Step Hyp Ref Expression
1 linepsub.n 
 |-  N = ( Lines ` K )
2 linepsub.s 
 |-  S = ( PSubSp ` K )
3 ssrab2 
 |-  { c e. ( Atoms ` K ) | c ( le ` K ) ( a ( join ` K ) b ) } C_ ( Atoms ` K )
4 sseq1 
 |-  ( X = { c e. ( Atoms ` K ) | c ( le ` K ) ( a ( join ` K ) b ) } -> ( X C_ ( Atoms ` K ) <-> { c e. ( Atoms ` K ) | c ( le ` K ) ( a ( join ` K ) b ) } C_ ( Atoms ` K ) ) )
5 3 4 mpbiri 
 |-  ( X = { c e. ( Atoms ` K ) | c ( le ` K ) ( a ( join ` K ) b ) } -> X C_ ( Atoms ` K ) )
6 5 a1i 
 |-  ( ( K e. Lat /\ ( a e. ( Atoms ` K ) /\ b e. ( Atoms ` K ) ) ) -> ( X = { c e. ( Atoms ` K ) | c ( le ` K ) ( a ( join ` K ) b ) } -> X C_ ( Atoms ` K ) ) )
7 eqid 
 |-  ( Base ` K ) = ( Base ` K )
8 eqid 
 |-  ( Atoms ` K ) = ( Atoms ` K )
9 7 8 atbase 
 |-  ( a e. ( Atoms ` K ) -> a e. ( Base ` K ) )
10 7 8 atbase 
 |-  ( b e. ( Atoms ` K ) -> b e. ( Base ` K ) )
11 9 10 anim12i 
 |-  ( ( a e. ( Atoms ` K ) /\ b e. ( Atoms ` K ) ) -> ( a e. ( Base ` K ) /\ b e. ( Base ` K ) ) )
12 eqid 
 |-  ( join ` K ) = ( join ` K )
13 7 12 latjcl 
 |-  ( ( K e. Lat /\ a e. ( Base ` K ) /\ b e. ( Base ` K ) ) -> ( a ( join ` K ) b ) e. ( Base ` K ) )
14 13 3expb 
 |-  ( ( K e. Lat /\ ( a e. ( Base ` K ) /\ b e. ( Base ` K ) ) ) -> ( a ( join ` K ) b ) e. ( Base ` K ) )
15 11 14 sylan2 
 |-  ( ( K e. Lat /\ ( a e. ( Atoms ` K ) /\ b e. ( Atoms ` K ) ) ) -> ( a ( join ` K ) b ) e. ( Base ` K ) )
16 eleq2 
 |-  ( X = { c e. ( Atoms ` K ) | c ( le ` K ) ( a ( join ` K ) b ) } -> ( p e. X <-> p e. { c e. ( Atoms ` K ) | c ( le ` K ) ( a ( join ` K ) b ) } ) )
17 breq1 
 |-  ( c = p -> ( c ( le ` K ) ( a ( join ` K ) b ) <-> p ( le ` K ) ( a ( join ` K ) b ) ) )
18 17 elrab 
 |-  ( p e. { c e. ( Atoms ` K ) | c ( le ` K ) ( a ( join ` K ) b ) } <-> ( p e. ( Atoms ` K ) /\ p ( le ` K ) ( a ( join ` K ) b ) ) )
19 7 8 atbase 
 |-  ( p e. ( Atoms ` K ) -> p e. ( Base ` K ) )
20 19 anim1i 
 |-  ( ( p e. ( Atoms ` K ) /\ p ( le ` K ) ( a ( join ` K ) b ) ) -> ( p e. ( Base ` K ) /\ p ( le ` K ) ( a ( join ` K ) b ) ) )
21 18 20 sylbi 
 |-  ( p e. { c e. ( Atoms ` K ) | c ( le ` K ) ( a ( join ` K ) b ) } -> ( p e. ( Base ` K ) /\ p ( le ` K ) ( a ( join ` K ) b ) ) )
22 16 21 syl6bi 
 |-  ( X = { c e. ( Atoms ` K ) | c ( le ` K ) ( a ( join ` K ) b ) } -> ( p e. X -> ( p e. ( Base ` K ) /\ p ( le ` K ) ( a ( join ` K ) b ) ) ) )
23 eleq2 
 |-  ( X = { c e. ( Atoms ` K ) | c ( le ` K ) ( a ( join ` K ) b ) } -> ( q e. X <-> q e. { c e. ( Atoms ` K ) | c ( le ` K ) ( a ( join ` K ) b ) } ) )
24 breq1 
 |-  ( c = q -> ( c ( le ` K ) ( a ( join ` K ) b ) <-> q ( le ` K ) ( a ( join ` K ) b ) ) )
25 24 elrab 
 |-  ( q e. { c e. ( Atoms ` K ) | c ( le ` K ) ( a ( join ` K ) b ) } <-> ( q e. ( Atoms ` K ) /\ q ( le ` K ) ( a ( join ` K ) b ) ) )
26 7 8 atbase 
 |-  ( q e. ( Atoms ` K ) -> q e. ( Base ` K ) )
27 26 anim1i 
 |-  ( ( q e. ( Atoms ` K ) /\ q ( le ` K ) ( a ( join ` K ) b ) ) -> ( q e. ( Base ` K ) /\ q ( le ` K ) ( a ( join ` K ) b ) ) )
28 25 27 sylbi 
 |-  ( q e. { c e. ( Atoms ` K ) | c ( le ` K ) ( a ( join ` K ) b ) } -> ( q e. ( Base ` K ) /\ q ( le ` K ) ( a ( join ` K ) b ) ) )
29 23 28 syl6bi 
 |-  ( X = { c e. ( Atoms ` K ) | c ( le ` K ) ( a ( join ` K ) b ) } -> ( q e. X -> ( q e. ( Base ` K ) /\ q ( le ` K ) ( a ( join ` K ) b ) ) ) )
30 22 29 anim12d 
 |-  ( X = { c e. ( Atoms ` K ) | c ( le ` K ) ( a ( join ` K ) b ) } -> ( ( p e. X /\ q e. X ) -> ( ( p e. ( Base ` K ) /\ p ( le ` K ) ( a ( join ` K ) b ) ) /\ ( q e. ( Base ` K ) /\ q ( le ` K ) ( a ( join ` K ) b ) ) ) ) )
31 an4 
 |-  ( ( ( p e. ( Base ` K ) /\ p ( le ` K ) ( a ( join ` K ) b ) ) /\ ( q e. ( Base ` K ) /\ q ( le ` K ) ( a ( join ` K ) b ) ) ) <-> ( ( p e. ( Base ` K ) /\ q e. ( Base ` K ) ) /\ ( p ( le ` K ) ( a ( join ` K ) b ) /\ q ( le ` K ) ( a ( join ` K ) b ) ) ) )
32 30 31 syl6ib 
 |-  ( X = { c e. ( Atoms ` K ) | c ( le ` K ) ( a ( join ` K ) b ) } -> ( ( p e. X /\ q e. X ) -> ( ( p e. ( Base ` K ) /\ q e. ( Base ` K ) ) /\ ( p ( le ` K ) ( a ( join ` K ) b ) /\ q ( le ` K ) ( a ( join ` K ) b ) ) ) ) )
33 32 imp 
 |-  ( ( X = { c e. ( Atoms ` K ) | c ( le ` K ) ( a ( join ` K ) b ) } /\ ( p e. X /\ q e. X ) ) -> ( ( p e. ( Base ` K ) /\ q e. ( Base ` K ) ) /\ ( p ( le ` K ) ( a ( join ` K ) b ) /\ q ( le ` K ) ( a ( join ` K ) b ) ) ) )
34 33 anim2i 
 |-  ( ( ( K e. Lat /\ ( a ( join ` K ) b ) e. ( Base ` K ) ) /\ ( X = { c e. ( Atoms ` K ) | c ( le ` K ) ( a ( join ` K ) b ) } /\ ( p e. X /\ q e. X ) ) ) -> ( ( K e. Lat /\ ( a ( join ` K ) b ) e. ( Base ` K ) ) /\ ( ( p e. ( Base ` K ) /\ q e. ( Base ` K ) ) /\ ( p ( le ` K ) ( a ( join ` K ) b ) /\ q ( le ` K ) ( a ( join ` K ) b ) ) ) ) )
35 34 anassrs 
 |-  ( ( ( ( K e. Lat /\ ( a ( join ` K ) b ) e. ( Base ` K ) ) /\ X = { c e. ( Atoms ` K ) | c ( le ` K ) ( a ( join ` K ) b ) } ) /\ ( p e. X /\ q e. X ) ) -> ( ( K e. Lat /\ ( a ( join ` K ) b ) e. ( Base ` K ) ) /\ ( ( p e. ( Base ` K ) /\ q e. ( Base ` K ) ) /\ ( p ( le ` K ) ( a ( join ` K ) b ) /\ q ( le ` K ) ( a ( join ` K ) b ) ) ) ) )
36 7 8 atbase 
 |-  ( r e. ( Atoms ` K ) -> r e. ( Base ` K ) )
37 eqid 
 |-  ( le ` K ) = ( le ` K )
38 7 37 12 latjle12 
 |-  ( ( K e. Lat /\ ( p e. ( Base ` K ) /\ q e. ( Base ` K ) /\ ( a ( join ` K ) b ) e. ( Base ` K ) ) ) -> ( ( p ( le ` K ) ( a ( join ` K ) b ) /\ q ( le ` K ) ( a ( join ` K ) b ) ) <-> ( p ( join ` K ) q ) ( le ` K ) ( a ( join ` K ) b ) ) )
39 38 biimpd 
 |-  ( ( K e. Lat /\ ( p e. ( Base ` K ) /\ q e. ( Base ` K ) /\ ( a ( join ` K ) b ) e. ( Base ` K ) ) ) -> ( ( p ( le ` K ) ( a ( join ` K ) b ) /\ q ( le ` K ) ( a ( join ` K ) b ) ) -> ( p ( join ` K ) q ) ( le ` K ) ( a ( join ` K ) b ) ) )
40 39 3exp2 
 |-  ( K e. Lat -> ( p e. ( Base ` K ) -> ( q e. ( Base ` K ) -> ( ( a ( join ` K ) b ) e. ( Base ` K ) -> ( ( p ( le ` K ) ( a ( join ` K ) b ) /\ q ( le ` K ) ( a ( join ` K ) b ) ) -> ( p ( join ` K ) q ) ( le ` K ) ( a ( join ` K ) b ) ) ) ) ) )
41 40 impd 
 |-  ( K e. Lat -> ( ( p e. ( Base ` K ) /\ q e. ( Base ` K ) ) -> ( ( a ( join ` K ) b ) e. ( Base ` K ) -> ( ( p ( le ` K ) ( a ( join ` K ) b ) /\ q ( le ` K ) ( a ( join ` K ) b ) ) -> ( p ( join ` K ) q ) ( le ` K ) ( a ( join ` K ) b ) ) ) ) )
42 41 com23 
 |-  ( K e. Lat -> ( ( a ( join ` K ) b ) e. ( Base ` K ) -> ( ( p e. ( Base ` K ) /\ q e. ( Base ` K ) ) -> ( ( p ( le ` K ) ( a ( join ` K ) b ) /\ q ( le ` K ) ( a ( join ` K ) b ) ) -> ( p ( join ` K ) q ) ( le ` K ) ( a ( join ` K ) b ) ) ) ) )
43 42 imp43 
 |-  ( ( ( K e. Lat /\ ( a ( join ` K ) b ) e. ( Base ` K ) ) /\ ( ( p e. ( Base ` K ) /\ q e. ( Base ` K ) ) /\ ( p ( le ` K ) ( a ( join ` K ) b ) /\ q ( le ` K ) ( a ( join ` K ) b ) ) ) ) -> ( p ( join ` K ) q ) ( le ` K ) ( a ( join ` K ) b ) )
44 43 adantr 
 |-  ( ( ( ( K e. Lat /\ ( a ( join ` K ) b ) e. ( Base ` K ) ) /\ ( ( p e. ( Base ` K ) /\ q e. ( Base ` K ) ) /\ ( p ( le ` K ) ( a ( join ` K ) b ) /\ q ( le ` K ) ( a ( join ` K ) b ) ) ) ) /\ r e. ( Base ` K ) ) -> ( p ( join ` K ) q ) ( le ` K ) ( a ( join ` K ) b ) )
45 7 12 latjcl 
 |-  ( ( K e. Lat /\ p e. ( Base ` K ) /\ q e. ( Base ` K ) ) -> ( p ( join ` K ) q ) e. ( Base ` K ) )
46 45 3expib 
 |-  ( K e. Lat -> ( ( p e. ( Base ` K ) /\ q e. ( Base ` K ) ) -> ( p ( join ` K ) q ) e. ( Base ` K ) ) )
47 7 37 lattr 
 |-  ( ( K e. Lat /\ ( r e. ( Base ` K ) /\ ( p ( join ` K ) q ) e. ( Base ` K ) /\ ( a ( join ` K ) b ) e. ( Base ` K ) ) ) -> ( ( r ( le ` K ) ( p ( join ` K ) q ) /\ ( p ( join ` K ) q ) ( le ` K ) ( a ( join ` K ) b ) ) -> r ( le ` K ) ( a ( join ` K ) b ) ) )
48 47 3exp2 
 |-  ( K e. Lat -> ( r e. ( Base ` K ) -> ( ( p ( join ` K ) q ) e. ( Base ` K ) -> ( ( a ( join ` K ) b ) e. ( Base ` K ) -> ( ( r ( le ` K ) ( p ( join ` K ) q ) /\ ( p ( join ` K ) q ) ( le ` K ) ( a ( join ` K ) b ) ) -> r ( le ` K ) ( a ( join ` K ) b ) ) ) ) ) )
49 48 com24 
 |-  ( K e. Lat -> ( ( a ( join ` K ) b ) e. ( Base ` K ) -> ( ( p ( join ` K ) q ) e. ( Base ` K ) -> ( r e. ( Base ` K ) -> ( ( r ( le ` K ) ( p ( join ` K ) q ) /\ ( p ( join ` K ) q ) ( le ` K ) ( a ( join ` K ) b ) ) -> r ( le ` K ) ( a ( join ` K ) b ) ) ) ) ) )
50 46 49 syl5d 
 |-  ( K e. Lat -> ( ( a ( join ` K ) b ) e. ( Base ` K ) -> ( ( p e. ( Base ` K ) /\ q e. ( Base ` K ) ) -> ( r e. ( Base ` K ) -> ( ( r ( le ` K ) ( p ( join ` K ) q ) /\ ( p ( join ` K ) q ) ( le ` K ) ( a ( join ` K ) b ) ) -> r ( le ` K ) ( a ( join ` K ) b ) ) ) ) ) )
51 50 imp41 
 |-  ( ( ( ( K e. Lat /\ ( a ( join ` K ) b ) e. ( Base ` K ) ) /\ ( p e. ( Base ` K ) /\ q e. ( Base ` K ) ) ) /\ r e. ( Base ` K ) ) -> ( ( r ( le ` K ) ( p ( join ` K ) q ) /\ ( p ( join ` K ) q ) ( le ` K ) ( a ( join ` K ) b ) ) -> r ( le ` K ) ( a ( join ` K ) b ) ) )
52 51 adantlrr 
 |-  ( ( ( ( K e. Lat /\ ( a ( join ` K ) b ) e. ( Base ` K ) ) /\ ( ( p e. ( Base ` K ) /\ q e. ( Base ` K ) ) /\ ( p ( le ` K ) ( a ( join ` K ) b ) /\ q ( le ` K ) ( a ( join ` K ) b ) ) ) ) /\ r e. ( Base ` K ) ) -> ( ( r ( le ` K ) ( p ( join ` K ) q ) /\ ( p ( join ` K ) q ) ( le ` K ) ( a ( join ` K ) b ) ) -> r ( le ` K ) ( a ( join ` K ) b ) ) )
53 44 52 mpan2d 
 |-  ( ( ( ( K e. Lat /\ ( a ( join ` K ) b ) e. ( Base ` K ) ) /\ ( ( p e. ( Base ` K ) /\ q e. ( Base ` K ) ) /\ ( p ( le ` K ) ( a ( join ` K ) b ) /\ q ( le ` K ) ( a ( join ` K ) b ) ) ) ) /\ r e. ( Base ` K ) ) -> ( r ( le ` K ) ( p ( join ` K ) q ) -> r ( le ` K ) ( a ( join ` K ) b ) ) )
54 35 36 53 syl2an 
 |-  ( ( ( ( ( K e. Lat /\ ( a ( join ` K ) b ) e. ( Base ` K ) ) /\ X = { c e. ( Atoms ` K ) | c ( le ` K ) ( a ( join ` K ) b ) } ) /\ ( p e. X /\ q e. X ) ) /\ r e. ( Atoms ` K ) ) -> ( r ( le ` K ) ( p ( join ` K ) q ) -> r ( le ` K ) ( a ( join ` K ) b ) ) )
55 simpr 
 |-  ( ( ( ( ( K e. Lat /\ ( a ( join ` K ) b ) e. ( Base ` K ) ) /\ X = { c e. ( Atoms ` K ) | c ( le ` K ) ( a ( join ` K ) b ) } ) /\ ( p e. X /\ q e. X ) ) /\ r e. ( Atoms ` K ) ) -> r e. ( Atoms ` K ) )
56 54 55 jctild 
 |-  ( ( ( ( ( K e. Lat /\ ( a ( join ` K ) b ) e. ( Base ` K ) ) /\ X = { c e. ( Atoms ` K ) | c ( le ` K ) ( a ( join ` K ) b ) } ) /\ ( p e. X /\ q e. X ) ) /\ r e. ( Atoms ` K ) ) -> ( r ( le ` K ) ( p ( join ` K ) q ) -> ( r e. ( Atoms ` K ) /\ r ( le ` K ) ( a ( join ` K ) b ) ) ) )
57 eleq2 
 |-  ( X = { c e. ( Atoms ` K ) | c ( le ` K ) ( a ( join ` K ) b ) } -> ( r e. X <-> r e. { c e. ( Atoms ` K ) | c ( le ` K ) ( a ( join ` K ) b ) } ) )
58 breq1 
 |-  ( c = r -> ( c ( le ` K ) ( a ( join ` K ) b ) <-> r ( le ` K ) ( a ( join ` K ) b ) ) )
59 58 elrab 
 |-  ( r e. { c e. ( Atoms ` K ) | c ( le ` K ) ( a ( join ` K ) b ) } <-> ( r e. ( Atoms ` K ) /\ r ( le ` K ) ( a ( join ` K ) b ) ) )
60 57 59 bitrdi 
 |-  ( X = { c e. ( Atoms ` K ) | c ( le ` K ) ( a ( join ` K ) b ) } -> ( r e. X <-> ( r e. ( Atoms ` K ) /\ r ( le ` K ) ( a ( join ` K ) b ) ) ) )
61 60 ad3antlr 
 |-  ( ( ( ( ( K e. Lat /\ ( a ( join ` K ) b ) e. ( Base ` K ) ) /\ X = { c e. ( Atoms ` K ) | c ( le ` K ) ( a ( join ` K ) b ) } ) /\ ( p e. X /\ q e. X ) ) /\ r e. ( Atoms ` K ) ) -> ( r e. X <-> ( r e. ( Atoms ` K ) /\ r ( le ` K ) ( a ( join ` K ) b ) ) ) )
62 56 61 sylibrd 
 |-  ( ( ( ( ( K e. Lat /\ ( a ( join ` K ) b ) e. ( Base ` K ) ) /\ X = { c e. ( Atoms ` K ) | c ( le ` K ) ( a ( join ` K ) b ) } ) /\ ( p e. X /\ q e. X ) ) /\ r e. ( Atoms ` K ) ) -> ( r ( le ` K ) ( p ( join ` K ) q ) -> r e. X ) )
63 62 ralrimiva 
 |-  ( ( ( ( K e. Lat /\ ( a ( join ` K ) b ) e. ( Base ` K ) ) /\ X = { c e. ( Atoms ` K ) | c ( le ` K ) ( a ( join ` K ) b ) } ) /\ ( p e. X /\ q e. X ) ) -> A. r e. ( Atoms ` K ) ( r ( le ` K ) ( p ( join ` K ) q ) -> r e. X ) )
64 63 ralrimivva 
 |-  ( ( ( K e. Lat /\ ( a ( join ` K ) b ) e. ( Base ` K ) ) /\ X = { c e. ( Atoms ` K ) | c ( le ` K ) ( a ( join ` K ) b ) } ) -> A. p e. X A. q e. X A. r e. ( Atoms ` K ) ( r ( le ` K ) ( p ( join ` K ) q ) -> r e. X ) )
65 64 ex 
 |-  ( ( K e. Lat /\ ( a ( join ` K ) b ) e. ( Base ` K ) ) -> ( X = { c e. ( Atoms ` K ) | c ( le ` K ) ( a ( join ` K ) b ) } -> A. p e. X A. q e. X A. r e. ( Atoms ` K ) ( r ( le ` K ) ( p ( join ` K ) q ) -> r e. X ) ) )
66 15 65 syldan 
 |-  ( ( K e. Lat /\ ( a e. ( Atoms ` K ) /\ b e. ( Atoms ` K ) ) ) -> ( X = { c e. ( Atoms ` K ) | c ( le ` K ) ( a ( join ` K ) b ) } -> A. p e. X A. q e. X A. r e. ( Atoms ` K ) ( r ( le ` K ) ( p ( join ` K ) q ) -> r e. X ) ) )
67 6 66 jcad 
 |-  ( ( K e. Lat /\ ( a e. ( Atoms ` K ) /\ b e. ( Atoms ` K ) ) ) -> ( X = { c e. ( Atoms ` K ) | c ( le ` K ) ( a ( join ` K ) b ) } -> ( X C_ ( Atoms ` K ) /\ A. p e. X A. q e. X A. r e. ( Atoms ` K ) ( r ( le ` K ) ( p ( join ` K ) q ) -> r e. X ) ) ) )
68 67 adantld 
 |-  ( ( K e. Lat /\ ( a e. ( Atoms ` K ) /\ b e. ( Atoms ` K ) ) ) -> ( ( a =/= b /\ X = { c e. ( Atoms ` K ) | c ( le ` K ) ( a ( join ` K ) b ) } ) -> ( X C_ ( Atoms ` K ) /\ A. p e. X A. q e. X A. r e. ( Atoms ` K ) ( r ( le ` K ) ( p ( join ` K ) q ) -> r e. X ) ) ) )
69 68 rexlimdvva 
 |-  ( K e. Lat -> ( E. a e. ( Atoms ` K ) E. b e. ( Atoms ` K ) ( a =/= b /\ X = { c e. ( Atoms ` K ) | c ( le ` K ) ( a ( join ` K ) b ) } ) -> ( X C_ ( Atoms ` K ) /\ A. p e. X A. q e. X A. r e. ( Atoms ` K ) ( r ( le ` K ) ( p ( join ` K ) q ) -> r e. X ) ) ) )
70 37 12 8 1 isline 
 |-  ( K e. Lat -> ( X e. N <-> E. a e. ( Atoms ` K ) E. b e. ( Atoms ` K ) ( a =/= b /\ X = { c e. ( Atoms ` K ) | c ( le ` K ) ( a ( join ` K ) b ) } ) ) )
71 37 12 8 2 ispsubsp 
 |-  ( K e. Lat -> ( X e. S <-> ( X C_ ( Atoms ` K ) /\ A. p e. X A. q e. X A. r e. ( Atoms ` K ) ( r ( le ` K ) ( p ( join ` K ) q ) -> r e. X ) ) ) )
72 69 70 71 3imtr4d 
 |-  ( K e. Lat -> ( X e. N -> X e. S ) )
73 72 imp 
 |-  ( ( K e. Lat /\ X e. N ) -> X e. S )