snatpsubN

Description: The singleton of an atom is a projective subspace. (Contributed by NM, 9-Sep-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	snpsub.a	$⊢ A = Atoms (K)$
	snpsub.s	$⊢ S = PSubSp (K)$
Assertion	snatpsubN	$⊢ (K \in AtLat \land P \in A) \to \{P\} \in S$

Proof

Step	Hyp	Ref	Expression
1		snpsub.a	$⊢ A = Atoms (K)$
2		snpsub.s	$⊢ S = PSubSp (K)$
3		snssi	$⊢ P \in A \to \{P\} \subseteq A$
4	3	adantl	$⊢ (K \in AtLat \land P \in A) \to \{P\} \subseteq A$
5		atllat	$⊢ K \in AtLat \to K \in Lat$
6		eqid	$⊢ {Base}_{K} = {Base}_{K}$
7	6 1	atbase	$⊢ P \in A \to P \in {Base}_{K}$
8		eqid	$⊢ join (K) = join (K)$
9	6 8	latjidm	$⊢ (K \in Lat \land P \in {Base}_{K}) \to P join (K) P = P$
10	5 7 9	syl2an	$⊢ (K \in AtLat \land P \in A) \to P join (K) P = P$
11	10	adantr	$⊢ ((K \in AtLat \land P \in A) \land r \in A) \to P join (K) P = P$
12	11	breq2d	$⊢ ((K \in AtLat \land P \in A) \land r \in A) \to (r \leq_{K} (P join (K) P) \leftrightarrow r \leq_{K} P)$
13		eqid	$⊢ \leq_{K} = \leq_{K}$
14	13 1	atcmp	$⊢ (K \in AtLat \land r \in A \land P \in A) \to (r \leq_{K} P \leftrightarrow r = P)$
15	14	3com23	$⊢ (K \in AtLat \land P \in A \land r \in A) \to (r \leq_{K} P \leftrightarrow r = P)$
16	15	3expa	$⊢ ((K \in AtLat \land P \in A) \land r \in A) \to (r \leq_{K} P \leftrightarrow r = P)$
17	16	biimpd	$⊢ ((K \in AtLat \land P \in A) \land r \in A) \to (r \leq_{K} P \to r = P)$
18	12 17	sylbid	$⊢ ((K \in AtLat \land P \in A) \land r \in A) \to (r \leq_{K} (P join (K) P) \to r = P)$
19	18	adantld	$⊢ ((K \in AtLat \land P \in A) \land r \in A) \to (((p = P \land q = P) \land r \leq_{K} (P join (K) P)) \to r = P)$
20		velsn	$⊢ p \in \{P\} \leftrightarrow p = P$
21		velsn	$⊢ q \in \{P\} \leftrightarrow q = P$
22	20 21	anbi12i	$⊢ (p \in \{P\} \land q \in \{P\}) \leftrightarrow (p = P \land q = P)$
23	22	anbi1i	$⊢ ((p \in \{P\} \land q \in \{P\}) \land r \leq_{K} (p join (K) q)) \leftrightarrow ((p = P \land q = P) \land r \leq_{K} (p join (K) q))$
24		oveq12	$⊢ (p = P \land q = P) \to p join (K) q = P join (K) P$
25	24	breq2d	$⊢ (p = P \land q = P) \to (r \leq_{K} (p join (K) q) \leftrightarrow r \leq_{K} (P join (K) P))$
26	25	pm5.32i	$⊢ ((p = P \land q = P) \land r \leq_{K} (p join (K) q)) \leftrightarrow ((p = P \land q = P) \land r \leq_{K} (P join (K) P))$
27	23 26	bitri	$⊢ ((p \in \{P\} \land q \in \{P\}) \land r \leq_{K} (p join (K) q)) \leftrightarrow ((p = P \land q = P) \land r \leq_{K} (P join (K) P))$
28		velsn	$⊢ r \in \{P\} \leftrightarrow r = P$
29	19 27 28	3imtr4g	$⊢ ((K \in AtLat \land P \in A) \land r \in A) \to (((p \in \{P\} \land q \in \{P\}) \land r \leq_{K} (p join (K) q)) \to r \in \{P\})$
30	29	exp4b	$⊢ (K \in AtLat \land P \in A) \to (r \in A \to ((p \in \{P\} \land q \in \{P\}) \to (r \leq_{K} (p join (K) q) \to r \in \{P\})))$
31	30	com23	$⊢ (K \in AtLat \land P \in A) \to ((p \in \{P\} \land q \in \{P\}) \to (r \in A \to (r \leq_{K} (p join (K) q) \to r \in \{P\})))$
32	31	ralrimdv	$⊢ (K \in AtLat \land P \in A) \to ((p \in \{P\} \land q \in \{P\}) \to \forall r \in A (r \leq_{K} (p join (K) q) \to r \in \{P\}))$
33	32	ralrimivv	$⊢ (K \in AtLat \land P \in A) \to \forall p \in \{P\} \forall q \in \{P\} \forall r \in A (r \leq_{K} (p join (K) q) \to r \in \{P\})$
34	4 33	jca	$⊢ (K \in AtLat \land P \in A) \to (\{P\} \subseteq A \land \forall p \in \{P\} \forall q \in \{P\} \forall r \in A (r \leq_{K} (p join (K) q) \to r \in \{P\}))$
35	34	ex	$⊢ K \in AtLat \to (P \in A \to (\{P\} \subseteq A \land \forall p \in \{P\} \forall q \in \{P\} \forall r \in A (r \leq_{K} (p join (K) q) \to r \in \{P\})))$
36	13 8 1 2	ispsubsp	$⊢ K \in AtLat \to (\{P\} \in S \leftrightarrow (\{P\} \subseteq A \land \forall p \in \{P\} \forall q \in \{P\} \forall r \in A (r \leq_{K} (p join (K) q) \to r \in \{P\})))$
37	35 36	sylibrd	$⊢ K \in AtLat \to (P \in A \to \{P\} \in S)$
38	37	imp	$⊢ (K \in AtLat \land P \in A) \to \{P\} \in S$

Metamath Proof Explorer

Theorem snatpsubN

Proof