Theorem pointpsub 17231

Description: A point (singleton of an atom) is a projective subspace. Remark below Definition 15.1 of [MaedaMaeda] p. 61.

Hypotheses

Ref	Expression
pointpsub.p	|- P = (Points` K)
pointpsub.s	|- S = (PSubSp` K)

Assertion

Ref	Expression
pointpsub	|- ((K e. OL /\ X e. P) -> X e. S)

Proof of Theorem pointpsub

Step	Hyp	Ref	Expression
1		simpr 350	. . . . . . . 8 |- ((a e. (AtomsNEW` K) /\ X = {a}) -> X = {a})
2		snssi 3129	. . . . . . . . 9 |- (a e. (AtomsNEW` K) -> {a} C_ (AtomsNEW` K))
3	2	adantr 425	. . . . . . . 8 |- ((a e. (AtomsNEW` K) /\ X = {a}) -> {a} C_ (AtomsNEW` K))
4	1, 3	eqsstrd 2651	. . . . . . 7 |- ((a e. (AtomsNEW` K) /\ X = {a}) -> X C_ (AtomsNEW` K))
5	4	3adant1 894	. . . . . 6 |- ((K e. OL /\ a e. (AtomsNEW` K) /\ X = {a}) -> X C_ (AtomsNEW` K))
6		eqid 1884	. . . . . . . . . . . . . . . . . 18 |- (base` K) = (base` K)
7		eqid 1884	. . . . . . . . . . . . . . . . . 18 |- (join` K) = (join` K)
8	6, 7	latjidm 16869	. . . . . . . . . . . . . . . . 17 |- ((K e. LatNEW /\ a e. (base` K)) -> (a(join` K)a) = a)
9		ollat 16940	. . . . . . . . . . . . . . . . 17 |- (K e. OL -> K e. LatNEW)
10		eqid 1884	. . . . . . . . . . . . . . . . . 18 |- (AtomsNEW` K) = (AtomsNEW` K)
11	6, 10	atombase 17003	. . . . . . . . . . . . . . . . 17 |- (a e. (AtomsNEW` K) -> a e. (base` K))
12	8, 9, 11	syl2an 503	. . . . . . . . . . . . . . . 16 |- ((K e. OL /\ a e. (AtomsNEW` K)) -> (a(join` K)a) = a)
13	12	adantr 425	. . . . . . . . . . . . . . 15 |- (((K e. OL /\ a e. (AtomsNEW` K)) /\ r e. (AtomsNEW` K)) -> (a(join` K)a) = a)
14	13	breq2d 3350	. . . . . . . . . . . . . 14 |- (((K e. OL /\ a e. (AtomsNEW` K)) /\ r e. (AtomsNEW` K)) -> (r(le` K)(a(join` K)a) <-> r(le` K)a))
15		eqid 1884	. . . . . . . . . . . . . . . . . . 19 |- (le` K) = (le` K)
16	15, 10	atomcmp 17008	. . . . . . . . . . . . . . . . . 18 |- ((K e. OP /\ r e. (AtomsNEW` K) /\ a e. (AtomsNEW` K)) -> (r(le` K)a <-> r = a))
17	16	3com23 1074	. . . . . . . . . . . . . . . . 17 |- ((K e. OP /\ a e. (AtomsNEW` K) /\ r e. (AtomsNEW` K)) -> (r(le` K)a <-> r = a))
18	17	3expa 1067	. . . . . . . . . . . . . . . 16 |- (((K e. OP /\ a e. (AtomsNEW` K)) /\ r e. (AtomsNEW` K)) -> (r(le` K)a <-> r = a))
19		olop 16941	. . . . . . . . . . . . . . . 16 |- (K e. OL -> K e. OP)
20	18, 19	sylanl1 509	. . . . . . . . . . . . . . 15 |- (((K e. OL /\ a e. (AtomsNEW` K)) /\ r e. (AtomsNEW` K)) -> (r(le` K)a <-> r = a))
21	20	biimpd 170	. . . . . . . . . . . . . 14 |- (((K e. OL /\ a e. (AtomsNEW` K)) /\ r e. (AtomsNEW` K)) -> (r(le` K)a -> r = a))
22	14, 21	sylbid 220	. . . . . . . . . . . . 13 |- (((K e. OL /\ a e. (AtomsNEW` K)) /\ r e. (AtomsNEW` K)) -> (r(le` K)(a(join` K)a) -> r = a))
23	22	3adantl3 1034	. . . . . . . . . . . 12 |- (((K e. OL /\ a e. (AtomsNEW` K) /\ X = {a}) /\ r e. (AtomsNEW` K)) -> (r(le` K)(a(join` K)a) -> r = a))
24	23	adantld 426	. . . . . . . . . . 11 |- (((K e. OL /\ a e. (AtomsNEW` K) /\ X = {a}) /\ r e. (AtomsNEW` K)) -> (((p = a /\ q = a) /\ r(le` K)(a(join` K)a)) -> r = a))
25		eleq2 1958	. . . . . . . . . . . . . . . . 17 |- (X = {a} -> (p e. X <-> p e. {a}))
26		elsn 3058	. . . . . . . . . . . . . . . . 17 |- (p e. {a} <-> p = a)
27	25, 26	syl6bb 595	. . . . . . . . . . . . . . . 16 |- (X = {a} -> (p e. X <-> p = a))
28		eleq2 1958	. . . . . . . . . . . . . . . . 17 |- (X = {a} -> (q e. X <-> q e. {a}))
29		elsn 3058	. . . . . . . . . . . . . . . . 17 |- (q e. {a} <-> q = a)
30	28, 29	syl6bb 595	. . . . . . . . . . . . . . . 16 |- (X = {a} -> (q e. X <-> q = a))
31	27, 30	anbi12d 690	. . . . . . . . . . . . . . 15 |- (X = {a} -> ((p e. X /\ q e. X) <-> (p = a /\ q = a)))
32	31	anbi1d 679	. . . . . . . . . . . . . 14 |- (X = {a} -> (((p e. X /\ q e. X) /\ r(le` K)(p(join` K)q)) <-> ((p = a /\ q = a) /\ r(le` K)(p(join` K)q))))
33		opreq12 4891	. . . . . . . . . . . . . . . 16 |- ((p = a /\ q = a) -> (p(join` K)q) = (a(join` K)a))
34	33	breq2d 3350	. . . . . . . . . . . . . . 15 |- ((p = a /\ q = a) -> (r(le` K)(p(join` K)q) <-> r(le` K)(a(join` K)a)))
35	34	pm5.32i 707	. . . . . . . . . . . . . 14 |- (((p = a /\ q = a) /\ r(le` K)(p(join` K)q)) <-> ((p = a /\ q = a) /\ r(le` K)(a(join` K)a)))
36	32, 35	syl6bb 595	. . . . . . . . . . . . 13 |- (X = {a} -> (((p e. X /\ q e. X) /\ r(le` K)(p(join` K)q)) <-> ((p = a /\ q = a) /\ r(le` K)(a(join` K)a))))
37	36	3ad2ant3 899	. . . . . . . . . . . 12 |- ((K e. OL /\ a e. (AtomsNEW` K) /\ X = {a}) -> (((p e. X /\ q e. X) /\ r(le` K)(p(join` K)q)) <-> ((p = a /\ q = a) /\ r(le` K)(a(join` K)a))))
38	37	adantr 425	. . . . . . . . . . 11 |- (((K e. OL /\ a e. (AtomsNEW` K) /\ X = {a}) /\ r e. (AtomsNEW` K)) -> (((p e. X /\ q e. X) /\ r(le` K)(p(join` K)q)) <-> ((p = a /\ q = a) /\ r(le` K)(a(join` K)a))))
39		eleq2 1958	. . . . . . . . . . . . . 14 |- (X = {a} -> (r e. X <-> r e. {a}))
40		elsn 3058	. . . . . . . . . . . . . 14 |- (r e. {a} <-> r = a)
41	39, 40	syl6bb 595	. . . . . . . . . . . . 13 |- (X = {a} -> (r e. X <-> r = a))
42	41	3ad2ant3 899	. . . . . . . . . . . 12 |- ((K e. OL /\ a e. (AtomsNEW` K) /\ X = {a}) -> (r e. X <-> r = a))
43	42	adantr 425	. . . . . . . . . . 11 |- (((K e. OL /\ a e. (AtomsNEW` K) /\ X = {a}) /\ r e. (AtomsNEW` K)) -> (r e. X <-> r = a))
44	24, 38, 43	3imtr4d 602	. . . . . . . . . 10 |- (((K e. OL /\ a e. (AtomsNEW` K) /\ X = {a}) /\ r e. (AtomsNEW` K)) -> (((p e. X /\ q e. X) /\ r(le` K)(p(join` K)q)) -> r e. X))
45	44	exp4b 410	. . . . . . . . 9 |- ((K e. OL /\ a e. (AtomsNEW` K) /\ X = {a}) -> (r e. (AtomsNEW` K) -> ((p e. X /\ q e. X) -> (r(le` K)(p(join` K)q) -> r e. X))))
46	45	com23 36	. . . . . . . 8 |- ((K e. OL /\ a e. (AtomsNEW` K) /\ X = {a}) -> ((p e. X /\ q e. X) -> (r e. (AtomsNEW` K) -> (r(le` K)(p(join` K)q) -> r e. X))))
47	46	r19.21adv 2181	. . . . . . 7 |- ((K e. OL /\ a e. (AtomsNEW` K) /\ X = {a}) -> ((p e. X /\ q e. X) -> A.r e. (AtomsNEW` K)(r(le` K)(p(join` K)q) -> r e. X)))
48	47	r19.21aivv 2183	. . . . . 6 |- ((K e. OL /\ a e. (AtomsNEW` K) /\ X = {a}) -> A.p e. X A.q e. X A.r e. (AtomsNEW` K)(r(le` K)(p(join` K)q) -> r e. X))
49	5, 48	jca 310	. . . . 5 |- ((K e. OL /\ a e. (AtomsNEW` K) /\ X = {a}) -> (X C_ (AtomsNEW` K) /\ A.p e. X A.q e. X A.r e. (AtomsNEW` K)(r(le` K)(p(join` K)q) -> r e. X)))
50	49	3exp 1066	. . . 4 |- (K e. OL -> (a e. (AtomsNEW` K) -> (X = {a} -> (X C_ (AtomsNEW` K) /\ A.p e. X A.q e. X A.r e. (AtomsNEW` K)(r(le` K)(p(join` K)q) -> r e. X)))))
51	50	r19.23adv 2215	. . 3 |- (K e. OL -> (E.a e. (AtomsNEW` K)X = {a} -> (X C_ (AtomsNEW` K) /\ A.p e. X A.q e. X A.r e. (AtomsNEW` K)(r(le` K)(p(join` K)q) -> r e. X))))
52		pointpsub.p	. . . 4 |- P = (Points` K)
53	10, 52	ispoint 17223	. . 3 |- (K e. OL -> (X e. P <-> E.a e. (AtomsNEW` K)X = {a}))
54		pointpsub.s	. . . 4 |- S = (PSubSp` K)
55	15, 7, 10, 54	ispsubsp 17226	. . 3 |- (K e. OL -> (X e. S <-> (X C_ (AtomsNEW` K) /\ A.p e. X A.q e. X A.r e. (AtomsNEW` K)(r(le` K)(p(join` K)q) -> r e. X))))
56	51, 53, 55	3imtr4d 602	. 2 |- (K e. OL -> (X e. P -> X e. S))
57	56	imp 377	1 |- ((K e. OL /\ X e. P) -> X e. S)

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240   /\ w3a 858   = wceq 1298   e. wcel 1300  A.wral 2105  E.wrex 2106   C_ wss 2593  {csn 3044   class class class wbr 3338  ` cfv 3998  (class class class)co 4884  basecbs 16758  lecple 16759  joincjn 16766  LatNEWclat 16834  OPcops 16837  OLcol 16839  AtomsNEWcatm 16981  Pointscpoints 17212  PSubSpcpsubsp 17213

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-13 1311  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-rep 3428  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524  ax-un 3790

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3an 860  df-tru 1262  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-ral 2109  df-rex 2110  df-reu 2111  df-rab 2112  df-v 2294  df-sbc 2454  df-csb 2541  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-nul 2876  df-if 2983  df-pw 3035  df-sn 3049  df-pr 3050  df-op 3053  df-uni 3178  df-br 3339  df-opab 3396  df-id 3586  df-xp 4000  df-rel 4001  df-cnv 4002  df-co 4003  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fun 4008  df-fn 4009  df-f 4010  df-f1 4011  df-fo 4012  df-f1o 4013  df-fv 4014  df-opr 4886  df-oprab 4887  df-mpt 5006  df-mpt2 5007  df-iota 5089  df-er 5318  df-en 5427  df-dom 5428  df-sdom 5429  df-undef 5556  df-riota 5560  df-struct 16708  df-poset 16772  df-plt 16780  df-lub 16799  df-join 16801  df-lat 16847  df-oposet 16905  df-ol 16907  df-covers 16984  df-atoms 16985  df-points 17216  df-psubsp 17217

Copyright terms: Public domain