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 syl6bi 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 syl6bi 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 syl6ib 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