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 )