psubclsetN

Description: The set of closed projective subspaces in a Hilbert lattice. (Contributed by NM, 23-Jan-2012) (New usage is discouraged.)

	Ref	Expression
Hypotheses	psubclset.a	$⊢ A = Atoms (K)$
	psubclset.p	$⊢ \underset{˙}{⊥} = ⊥_{𝑃} (K)$
	psubclset.c	$⊢ C = PSubCl (K)$
Assertion	psubclsetN	$⊢ K \in B \to C = \{s \| (s \subseteq A \land \underset{˙}{⊥} (\underset{˙}{⊥} (s)) = s)\}$

Proof

Step	Hyp	Ref	Expression
1		psubclset.a	$⊢ A = Atoms (K)$
2		psubclset.p	$⊢ \underset{˙}{⊥} = ⊥_{𝑃} (K)$
3		psubclset.c	$⊢ C = PSubCl (K)$
4		elex	$⊢ K \in B \to K \in V$
5		fveq2	$⊢ k = K \to Atoms (k) = Atoms (K)$
6	5 1	eqtr4di	$⊢ k = K \to Atoms (k) = A$
7	6	sseq2d	$⊢ k = K \to (s \subseteq Atoms (k) \leftrightarrow s \subseteq A)$
8		fveq2	$⊢ k = K \to ⊥_{𝑃} (k) = ⊥_{𝑃} (K)$
9	8 2	eqtr4di	$⊢ k = K \to ⊥_{𝑃} (k) = \underset{˙}{⊥}$
10	9	fveq1d	$⊢ k = K \to ⊥_{𝑃} (k) (s) = \underset{˙}{⊥} (s)$
11	9 10	fveq12d	$⊢ k = K \to ⊥_{𝑃} (k) (⊥_{𝑃} (k) (s)) = \underset{˙}{⊥} (\underset{˙}{⊥} (s))$
12	11	eqeq1d	$⊢ k = K \to (⊥_{𝑃} (k) (⊥_{𝑃} (k) (s)) = s \leftrightarrow \underset{˙}{⊥} (\underset{˙}{⊥} (s)) = s)$
13	7 12	anbi12d	$⊢ k = K \to ((s \subseteq Atoms (k) \land ⊥_{𝑃} (k) (⊥_{𝑃} (k) (s)) = s) \leftrightarrow (s \subseteq A \land \underset{˙}{⊥} (\underset{˙}{⊥} (s)) = s))$
14	13	abbidv	$⊢ k = K \to \{s \| (s \subseteq Atoms (k) \land ⊥_{𝑃} (k) (⊥_{𝑃} (k) (s)) = s)\} = \{s \| (s \subseteq A \land \underset{˙}{⊥} (\underset{˙}{⊥} (s)) = s)\}$
15		df-psubclN	$⊢ PSubCl = (k \in V ⟼ \{s \| (s \subseteq Atoms (k) \land ⊥_{𝑃} (k) (⊥_{𝑃} (k) (s)) = s)\})$
16	1	fvexi	$⊢ A \in V$
17	16	pwex	$⊢ 𝒫 A \in V$
18		velpw	$⊢ s \in 𝒫 A \leftrightarrow s \subseteq A$
19	18	anbi1i	$⊢ (s \in 𝒫 A \land \underset{˙}{⊥} (\underset{˙}{⊥} (s)) = s) \leftrightarrow (s \subseteq A \land \underset{˙}{⊥} (\underset{˙}{⊥} (s)) = s)$
20	19	abbii	$⊢ \{s \| (s \in 𝒫 A \land \underset{˙}{⊥} (\underset{˙}{⊥} (s)) = s)\} = \{s \| (s \subseteq A \land \underset{˙}{⊥} (\underset{˙}{⊥} (s)) = s)\}$
21		ssab2	$⊢ \{s \| (s \in 𝒫 A \land \underset{˙}{⊥} (\underset{˙}{⊥} (s)) = s)\} \subseteq 𝒫 A$
22	20 21	eqsstrri	$⊢ \{s \| (s \subseteq A \land \underset{˙}{⊥} (\underset{˙}{⊥} (s)) = s)\} \subseteq 𝒫 A$
23	17 22	ssexi	$⊢ \{s \| (s \subseteq A \land \underset{˙}{⊥} (\underset{˙}{⊥} (s)) = s)\} \in V$
24	14 15 23	fvmpt	$⊢ K \in V \to PSubCl (K) = \{s \| (s \subseteq A \land \underset{˙}{⊥} (\underset{˙}{⊥} (s)) = s)\}$
25	3 24	syl5eq	$⊢ K \in V \to C = \{s \| (s \subseteq A \land \underset{˙}{⊥} (\underset{˙}{⊥} (s)) = s)\}$
26	4 25	syl	$⊢ K \in B \to C = \{s \| (s \subseteq A \land \underset{˙}{⊥} (\underset{˙}{⊥} (s)) = s)\}$

Metamath Proof Explorer

Theorem psubclsetN

Proof