sspval

Description: The set of all subspaces of a normed complex vector space. (Contributed by NM, 26-Jan-2008) (Revised by Mario Carneiro, 16-Nov-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	sspval.g	$⊢ G = +_{v} (U)$
	sspval.s	$⊢ S = \cdot_{𝑠OLD} (U)$
	sspval.n	$⊢ N = {norm}_{CV} (U)$
	sspval.h	$⊢ H = SubSp (U)$
Assertion	sspval	$⊢ U \in NrmCVec \to H = \{w \in NrmCVec \| (+_{v} (w) \subseteq G \land \cdot_{𝑠OLD} (w) \subseteq S \land {norm}_{CV} (w) \subseteq N)\}$

Proof

Step	Hyp	Ref	Expression
1		sspval.g	$⊢ G = +_{v} (U)$
2		sspval.s	$⊢ S = \cdot_{𝑠OLD} (U)$
3		sspval.n	$⊢ N = {norm}_{CV} (U)$
4		sspval.h	$⊢ H = SubSp (U)$
5		fveq2	$⊢ u = U \to +_{v} (u) = +_{v} (U)$
6	5 1	eqtr4di	$⊢ u = U \to +_{v} (u) = G$
7	6	sseq2d	$⊢ u = U \to (+_{v} (w) \subseteq +_{v} (u) \leftrightarrow +_{v} (w) \subseteq G)$
8		fveq2	$⊢ u = U \to \cdot_{𝑠OLD} (u) = \cdot_{𝑠OLD} (U)$
9	8 2	eqtr4di	$⊢ u = U \to \cdot_{𝑠OLD} (u) = S$
10	9	sseq2d	$⊢ u = U \to (\cdot_{𝑠OLD} (w) \subseteq \cdot_{𝑠OLD} (u) \leftrightarrow \cdot_{𝑠OLD} (w) \subseteq S)$
11		fveq2	$⊢ u = U \to {norm}_{CV} (u) = {norm}_{CV} (U)$
12	11 3	eqtr4di	$⊢ u = U \to {norm}_{CV} (u) = N$
13	12	sseq2d	$⊢ u = U \to ({norm}_{CV} (w) \subseteq {norm}_{CV} (u) \leftrightarrow {norm}_{CV} (w) \subseteq N)$
14	7 10 13	3anbi123d	$⊢ u = U \to ((+_{v} (w) \subseteq +_{v} (u) \land \cdot_{𝑠OLD} (w) \subseteq \cdot_{𝑠OLD} (u) \land {norm}_{CV} (w) \subseteq {norm}_{CV} (u)) \leftrightarrow (+_{v} (w) \subseteq G \land \cdot_{𝑠OLD} (w) \subseteq S \land {norm}_{CV} (w) \subseteq N))$
15	14	rabbidv	$⊢ u = U \to \{w \in NrmCVec \| (+_{v} (w) \subseteq +_{v} (u) \land \cdot_{𝑠OLD} (w) \subseteq \cdot_{𝑠OLD} (u) \land {norm}_{CV} (w) \subseteq {norm}_{CV} (u))\} = \{w \in NrmCVec \| (+_{v} (w) \subseteq G \land \cdot_{𝑠OLD} (w) \subseteq S \land {norm}_{CV} (w) \subseteq N)\}$
16		df-ssp	$⊢ SubSp = (u \in NrmCVec ⟼ \{w \in NrmCVec \| (+_{v} (w) \subseteq +_{v} (u) \land \cdot_{𝑠OLD} (w) \subseteq \cdot_{𝑠OLD} (u) \land {norm}_{CV} (w) \subseteq {norm}_{CV} (u))\})$
17	1	fvexi	$⊢ G \in V$
18	17	pwex	$⊢ 𝒫 G \in V$
19	2	fvexi	$⊢ S \in V$
20	19	pwex	$⊢ 𝒫 S \in V$
21	18 20	xpex	$⊢ 𝒫 G \times 𝒫 S \in V$
22	3	fvexi	$⊢ N \in V$
23	22	pwex	$⊢ 𝒫 N \in V$
24	21 23	xpex	$⊢ (𝒫 G \times 𝒫 S) \times 𝒫 N \in V$
25		rabss	$⊢ \{w \in NrmCVec \| (+_{v} (w) \subseteq G \land \cdot_{𝑠OLD} (w) \subseteq S \land {norm}_{CV} (w) \subseteq N)\} \subseteq (𝒫 G \times 𝒫 S) \times 𝒫 N \leftrightarrow \forall w \in NrmCVec ((+_{v} (w) \subseteq G \land \cdot_{𝑠OLD} (w) \subseteq S \land {norm}_{CV} (w) \subseteq N) \to w \in ((𝒫 G \times 𝒫 S) \times 𝒫 N))$
26		fvex	$⊢ +_{v} (w) \in V$
27	26	elpw	$⊢ +_{v} (w) \in 𝒫 G \leftrightarrow +_{v} (w) \subseteq G$
28		fvex	$⊢ \cdot_{𝑠OLD} (w) \in V$
29	28	elpw	$⊢ \cdot_{𝑠OLD} (w) \in 𝒫 S \leftrightarrow \cdot_{𝑠OLD} (w) \subseteq S$
30		opelxpi	$⊢ (+_{v} (w) \in 𝒫 G \land \cdot_{𝑠OLD} (w) \in 𝒫 S) \to ⟨+_{v} (w), \cdot_{𝑠OLD} (w)⟩ \in (𝒫 G \times 𝒫 S)$
31	27 29 30	syl2anbr	$⊢ (+_{v} (w) \subseteq G \land \cdot_{𝑠OLD} (w) \subseteq S) \to ⟨+_{v} (w), \cdot_{𝑠OLD} (w)⟩ \in (𝒫 G \times 𝒫 S)$
32		fvex	$⊢ {norm}_{CV} (w) \in V$
33	32	elpw	$⊢ {norm}_{CV} (w) \in 𝒫 N \leftrightarrow {norm}_{CV} (w) \subseteq N$
34	33	biimpri	$⊢ {norm}_{CV} (w) \subseteq N \to {norm}_{CV} (w) \in 𝒫 N$
35		opelxpi	$⊢ (⟨+_{v} (w), \cdot_{𝑠OLD} (w)⟩ \in (𝒫 G \times 𝒫 S) \land {norm}_{CV} (w) \in 𝒫 N) \to ⟨⟨+_{v} (w), \cdot_{𝑠OLD} (w)⟩, {norm}_{CV} (w)⟩ \in ((𝒫 G \times 𝒫 S) \times 𝒫 N)$
36	31 34 35	syl2an	$⊢ ((+_{v} (w) \subseteq G \land \cdot_{𝑠OLD} (w) \subseteq S) \land {norm}_{CV} (w) \subseteq N) \to ⟨⟨+_{v} (w), \cdot_{𝑠OLD} (w)⟩, {norm}_{CV} (w)⟩ \in ((𝒫 G \times 𝒫 S) \times 𝒫 N)$
37	36	3impa	$⊢ (+_{v} (w) \subseteq G \land \cdot_{𝑠OLD} (w) \subseteq S \land {norm}_{CV} (w) \subseteq N) \to ⟨⟨+_{v} (w), \cdot_{𝑠OLD} (w)⟩, {norm}_{CV} (w)⟩ \in ((𝒫 G \times 𝒫 S) \times 𝒫 N)$
38		eqid	$⊢ +_{v} (w) = +_{v} (w)$
39		eqid	$⊢ \cdot_{𝑠OLD} (w) = \cdot_{𝑠OLD} (w)$
40		eqid	$⊢ {norm}_{CV} (w) = {norm}_{CV} (w)$
41	38 39 40	nvop	$⊢ w \in NrmCVec \to w = ⟨⟨+_{v} (w), \cdot_{𝑠OLD} (w)⟩, {norm}_{CV} (w)⟩$
42	41	eleq1d	$⊢ w \in NrmCVec \to (w \in ((𝒫 G \times 𝒫 S) \times 𝒫 N) \leftrightarrow ⟨⟨+_{v} (w), \cdot_{𝑠OLD} (w)⟩, {norm}_{CV} (w)⟩ \in ((𝒫 G \times 𝒫 S) \times 𝒫 N))$
43	37 42	syl5ibr	$⊢ w \in NrmCVec \to ((+_{v} (w) \subseteq G \land \cdot_{𝑠OLD} (w) \subseteq S \land {norm}_{CV} (w) \subseteq N) \to w \in ((𝒫 G \times 𝒫 S) \times 𝒫 N))$
44	25 43	mprgbir	$⊢ \{w \in NrmCVec \| (+_{v} (w) \subseteq G \land \cdot_{𝑠OLD} (w) \subseteq S \land {norm}_{CV} (w) \subseteq N)\} \subseteq (𝒫 G \times 𝒫 S) \times 𝒫 N$
45	24 44	ssexi	$⊢ \{w \in NrmCVec \| (+_{v} (w) \subseteq G \land \cdot_{𝑠OLD} (w) \subseteq S \land {norm}_{CV} (w) \subseteq N)\} \in V$
46	15 16 45	fvmpt	$⊢ U \in NrmCVec \to SubSp (U) = \{w \in NrmCVec \| (+_{v} (w) \subseteq G \land \cdot_{𝑠OLD} (w) \subseteq S \land {norm}_{CV} (w) \subseteq N)\}$
47	4 46	syl5eq	$⊢ U \in NrmCVec \to H = \{w \in NrmCVec \| (+_{v} (w) \subseteq G \land \cdot_{𝑠OLD} (w) \subseteq S \land {norm}_{CV} (w) \subseteq N)\}$

Metamath Proof Explorer

Theorem sspval

Proof