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 ∈ Lat ∧ X ∈ N → X ∈ S

Proof

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