isssp

Description: The predicate "is a subspace." (Contributed by NM, 26-Jan-2008) (New usage is discouraged.)

	Ref	Expression
Hypotheses	isssp.g	$⊢ G = +_{v} (U)$
	isssp.f	$⊢ F = +_{v} (W)$
	isssp.s	$⊢ S = \cdot_{𝑠OLD} (U)$
	isssp.r	$⊢ R = \cdot_{𝑠OLD} (W)$
	isssp.n	$⊢ N = {norm}_{CV} (U)$
	isssp.m	$⊢ M = {norm}_{CV} (W)$
	isssp.h	$⊢ H = SubSp (U)$
Assertion	isssp	$⊢ U \in NrmCVec \to (W \in H \leftrightarrow (W \in NrmCVec \land (F \subseteq G \land R \subseteq S \land M \subseteq N)))$

Proof

Step	Hyp	Ref	Expression
1		isssp.g	$⊢ G = +_{v} (U)$
2		isssp.f	$⊢ F = +_{v} (W)$
3		isssp.s	$⊢ S = \cdot_{𝑠OLD} (U)$
4		isssp.r	$⊢ R = \cdot_{𝑠OLD} (W)$
5		isssp.n	$⊢ N = {norm}_{CV} (U)$
6		isssp.m	$⊢ M = {norm}_{CV} (W)$
7		isssp.h	$⊢ H = SubSp (U)$
8	1 3 5 7	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)\}$
9	8	eleq2d	$⊢ U \in NrmCVec \to (W \in H \leftrightarrow W \in \{w \in NrmCVec \| (+_{v} (w) \subseteq G \land \cdot_{𝑠OLD} (w) \subseteq S \land {norm}_{CV} (w) \subseteq N)\})$
10		fveq2	$⊢ w = W \to +_{v} (w) = +_{v} (W)$
11	10 2	eqtr4di	$⊢ w = W \to +_{v} (w) = F$
12	11	sseq1d	$⊢ w = W \to (+_{v} (w) \subseteq G \leftrightarrow F \subseteq G)$
13		fveq2	$⊢ w = W \to \cdot_{𝑠OLD} (w) = \cdot_{𝑠OLD} (W)$
14	13 4	eqtr4di	$⊢ w = W \to \cdot_{𝑠OLD} (w) = R$
15	14	sseq1d	$⊢ w = W \to (\cdot_{𝑠OLD} (w) \subseteq S \leftrightarrow R \subseteq S)$
16		fveq2	$⊢ w = W \to {norm}_{CV} (w) = {norm}_{CV} (W)$
17	16 6	eqtr4di	$⊢ w = W \to {norm}_{CV} (w) = M$
18	17	sseq1d	$⊢ w = W \to ({norm}_{CV} (w) \subseteq N \leftrightarrow M \subseteq N)$
19	12 15 18	3anbi123d	$⊢ w = W \to ((+_{v} (w) \subseteq G \land \cdot_{𝑠OLD} (w) \subseteq S \land {norm}_{CV} (w) \subseteq N) \leftrightarrow (F \subseteq G \land R \subseteq S \land M \subseteq N))$
20	19	elrab	$⊢ W \in \{w \in NrmCVec \| (+_{v} (w) \subseteq G \land \cdot_{𝑠OLD} (w) \subseteq S \land {norm}_{CV} (w) \subseteq N)\} \leftrightarrow (W \in NrmCVec \land (F \subseteq G \land R \subseteq S \land M \subseteq N))$
21	9 20	bitrdi	$⊢ U \in NrmCVec \to (W \in H \leftrightarrow (W \in NrmCVec \land (F \subseteq G \land R \subseteq S \land M \subseteq N)))$

Metamath Proof Explorer

Theorem isssp

Proof