ispsubcl2N

Description: Alternate predicate for "is a closed projective subspace". Remark in Holland95 p. 223. (Contributed by NM, 24-Jan-2012) (New usage is discouraged.)

	Ref	Expression
Hypotheses	pmapsubcl.b	$⊢ B = {Base}_{K}$
	pmapsubcl.m	$⊢ M = pmap (K)$
	pmapsubcl.c	$⊢ C = PSubCl (K)$
Assertion	ispsubcl2N	$⊢ K \in HL \to (X \in C \leftrightarrow \exists y \in B X = M (y))$

Proof

Step	Hyp	Ref	Expression
1		pmapsubcl.b	$⊢ B = {Base}_{K}$
2		pmapsubcl.m	$⊢ M = pmap (K)$
3		pmapsubcl.c	$⊢ C = PSubCl (K)$
4		eqid	$⊢ Atoms (K) = Atoms (K)$
5		eqid	$⊢ ⊥_{𝑃} (K) = ⊥_{𝑃} (K)$
6	4 5 3	ispsubclN	$⊢ K \in HL \to (X \in C \leftrightarrow (X \subseteq Atoms (K) \land ⊥_{𝑃} (K) (⊥_{𝑃} (K) (X)) = X))$
7		hlop	$⊢ K \in HL \to K \in OP$
8	7	adantr	$⊢ (K \in HL \land X \subseteq Atoms (K)) \to K \in OP$
9		hlclat	$⊢ K \in HL \to K \in CLat$
10	9	adantr	$⊢ (K \in HL \land X \subseteq Atoms (K)) \to K \in CLat$
11	4 5	polssatN	$⊢ (K \in HL \land X \subseteq Atoms (K)) \to ⊥_{𝑃} (K) (X) \subseteq Atoms (K)$
12	1 4	atssbase	$⊢ Atoms (K) \subseteq B$
13	11 12	sstrdi	$⊢ (K \in HL \land X \subseteq Atoms (K)) \to ⊥_{𝑃} (K) (X) \subseteq B$
14		eqid	$⊢ lub (K) = lub (K)$
15	1 14	clatlubcl	$⊢ (K \in CLat \land ⊥_{𝑃} (K) (X) \subseteq B) \to lub (K) (⊥_{𝑃} (K) (X)) \in B$
16	10 13 15	syl2anc	$⊢ (K \in HL \land X \subseteq Atoms (K)) \to lub (K) (⊥_{𝑃} (K) (X)) \in B$
17		eqid	$⊢ oc (K) = oc (K)$
18	1 17	opoccl	$⊢ (K \in OP \land lub (K) (⊥_{𝑃} (K) (X)) \in B) \to oc (K) (lub (K) (⊥_{𝑃} (K) (X))) \in B$
19	8 16 18	syl2anc	$⊢ (K \in HL \land X \subseteq Atoms (K)) \to oc (K) (lub (K) (⊥_{𝑃} (K) (X))) \in B$
20	19	ex	$⊢ K \in HL \to (X \subseteq Atoms (K) \to oc (K) (lub (K) (⊥_{𝑃} (K) (X))) \in B)$
21	20	adantrd	$⊢ K \in HL \to ((X \subseteq Atoms (K) \land ⊥_{𝑃} (K) (⊥_{𝑃} (K) (X)) = X) \to oc (K) (lub (K) (⊥_{𝑃} (K) (X))) \in B)$
22	14 17 4 2 5	polval2N	$⊢ (K \in HL \land ⊥_{𝑃} (K) (X) \subseteq Atoms (K)) \to ⊥_{𝑃} (K) (⊥_{𝑃} (K) (X)) = M (oc (K) (lub (K) (⊥_{𝑃} (K) (X))))$
23	11 22	syldan	$⊢ (K \in HL \land X \subseteq Atoms (K)) \to ⊥_{𝑃} (K) (⊥_{𝑃} (K) (X)) = M (oc (K) (lub (K) (⊥_{𝑃} (K) (X))))$
24	23	ex	$⊢ K \in HL \to (X \subseteq Atoms (K) \to ⊥_{𝑃} (K) (⊥_{𝑃} (K) (X)) = M (oc (K) (lub (K) (⊥_{𝑃} (K) (X)))))$
25		eqeq1	$⊢ ⊥_{𝑃} (K) (⊥_{𝑃} (K) (X)) = X \to (⊥_{𝑃} (K) (⊥_{𝑃} (K) (X)) = M (oc (K) (lub (K) (⊥_{𝑃} (K) (X)))) \leftrightarrow X = M (oc (K) (lub (K) (⊥_{𝑃} (K) (X)))))$
26	25	biimpcd	$⊢ ⊥_{𝑃} (K) (⊥_{𝑃} (K) (X)) = M (oc (K) (lub (K) (⊥_{𝑃} (K) (X)))) \to (⊥_{𝑃} (K) (⊥_{𝑃} (K) (X)) = X \to X = M (oc (K) (lub (K) (⊥_{𝑃} (K) (X)))))$
27	24 26	syl6	$⊢ K \in HL \to (X \subseteq Atoms (K) \to (⊥_{𝑃} (K) (⊥_{𝑃} (K) (X)) = X \to X = M (oc (K) (lub (K) (⊥_{𝑃} (K) (X))))))$
28	27	impd	$⊢ K \in HL \to ((X \subseteq Atoms (K) \land ⊥_{𝑃} (K) (⊥_{𝑃} (K) (X)) = X) \to X = M (oc (K) (lub (K) (⊥_{𝑃} (K) (X)))))$
29	21 28	jcad	$⊢ K \in HL \to ((X \subseteq Atoms (K) \land ⊥_{𝑃} (K) (⊥_{𝑃} (K) (X)) = X) \to (oc (K) (lub (K) (⊥_{𝑃} (K) (X))) \in B \land X = M (oc (K) (lub (K) (⊥_{𝑃} (K) (X))))))$
30		fveq2	$⊢ y = oc (K) (lub (K) (⊥_{𝑃} (K) (X))) \to M (y) = M (oc (K) (lub (K) (⊥_{𝑃} (K) (X))))$
31	30	rspceeqv	$⊢ (oc (K) (lub (K) (⊥_{𝑃} (K) (X))) \in B \land X = M (oc (K) (lub (K) (⊥_{𝑃} (K) (X))))) \to \exists y \in B X = M (y)$
32	29 31	syl6	$⊢ K \in HL \to ((X \subseteq Atoms (K) \land ⊥_{𝑃} (K) (⊥_{𝑃} (K) (X)) = X) \to \exists y \in B X = M (y))$
33	1 4 2	pmapssat	$⊢ (K \in HL \land y \in B) \to M (y) \subseteq Atoms (K)$
34	1 2 5	2polpmapN	$⊢ (K \in HL \land y \in B) \to ⊥_{𝑃} (K) (⊥_{𝑃} (K) (M (y))) = M (y)$
35		sseq1	$⊢ X = M (y) \to (X \subseteq Atoms (K) \leftrightarrow M (y) \subseteq Atoms (K))$
36		2fveq3	$⊢ X = M (y) \to ⊥_{𝑃} (K) (⊥_{𝑃} (K) (X)) = ⊥_{𝑃} (K) (⊥_{𝑃} (K) (M (y)))$
37		id	$⊢ X = M (y) \to X = M (y)$
38	36 37	eqeq12d	$⊢ X = M (y) \to (⊥_{𝑃} (K) (⊥_{𝑃} (K) (X)) = X \leftrightarrow ⊥_{𝑃} (K) (⊥_{𝑃} (K) (M (y))) = M (y))$
39	35 38	anbi12d	$⊢ X = M (y) \to ((X \subseteq Atoms (K) \land ⊥_{𝑃} (K) (⊥_{𝑃} (K) (X)) = X) \leftrightarrow (M (y) \subseteq Atoms (K) \land ⊥_{𝑃} (K) (⊥_{𝑃} (K) (M (y))) = M (y)))$
40	39	biimprcd	$⊢ (M (y) \subseteq Atoms (K) \land ⊥_{𝑃} (K) (⊥_{𝑃} (K) (M (y))) = M (y)) \to (X = M (y) \to (X \subseteq Atoms (K) \land ⊥_{𝑃} (K) (⊥_{𝑃} (K) (X)) = X))$
41	33 34 40	syl2anc	$⊢ (K \in HL \land y \in B) \to (X = M (y) \to (X \subseteq Atoms (K) \land ⊥_{𝑃} (K) (⊥_{𝑃} (K) (X)) = X))$
42	41	rexlimdva	$⊢ K \in HL \to (\exists y \in B X = M (y) \to (X \subseteq Atoms (K) \land ⊥_{𝑃} (K) (⊥_{𝑃} (K) (X)) = X))$
43	32 42	impbid	$⊢ K \in HL \to ((X \subseteq Atoms (K) \land ⊥_{𝑃} (K) (⊥_{𝑃} (K) (X)) = X) \leftrightarrow \exists y \in B X = M (y))$
44	6 43	bitrd	$⊢ K \in HL \to (X \in C \leftrightarrow \exists y \in B X = M (y))$

Metamath Proof Explorer

Theorem ispsubcl2N

Proof