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 \in Lat \land X \in N) \to X \in S$

Proof

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

Metamath Proof Explorer

Theorem linepsubN

Proof