hhshsslem2

Description: Lemma for hhsssh . (Contributed by NM, 6-Apr-2008) (New usage is discouraged.)

	Ref	Expression
Hypotheses	hhsst.1	$⊢ U = ⟨⟨+_{ℎ}, \cdot_{ℎ}⟩, {norm}_{ℎ}⟩$
	hhsst.2	$⊢ W = ⟨⟨{+_{ℎ} ↾}_{(H \times H)}, {\cdot_{ℎ} ↾}_{(ℂ \times H)}⟩, {{norm}_{ℎ} ↾}_{H}⟩$
	hhssp3.3	$⊢ W \in SubSp (U)$
	hhssp3.4	$⊢ H \subseteq ℋ$
Assertion	hhshsslem2	$⊢ H \in S_{ℋ}$

Proof

Step	Hyp	Ref	Expression
1		hhsst.1	$⊢ U = ⟨⟨+_{ℎ}, \cdot_{ℎ}⟩, {norm}_{ℎ}⟩$
2		hhsst.2	$⊢ W = ⟨⟨{+_{ℎ} ↾}_{(H \times H)}, {\cdot_{ℎ} ↾}_{(ℂ \times H)}⟩, {{norm}_{ℎ} ↾}_{H}⟩$
3		hhssp3.3	$⊢ W \in SubSp (U)$
4		hhssp3.4	$⊢ H \subseteq ℋ$
5	1	hhnv	$⊢ U \in NrmCVec$
6	1	hh0v	$⊢ 0_{ℎ} = 0_{vec} (U)$
7		eqid	$⊢ 0_{vec} (W) = 0_{vec} (W)$
8		eqid	$⊢ SubSp (U) = SubSp (U)$
9	6 7 8	sspz	$⊢ (U \in NrmCVec \land W \in SubSp (U)) \to 0_{vec} (W) = 0_{ℎ}$
10	5 3 9	mp2an	$⊢ 0_{vec} (W) = 0_{ℎ}$
11	8	sspnv	$⊢ (U \in NrmCVec \land W \in SubSp (U)) \to W \in NrmCVec$
12	5 3 11	mp2an	$⊢ W \in NrmCVec$
13		eqid	$⊢ BaseSet (W) = BaseSet (W)$
14	13 7	nvzcl	$⊢ W \in NrmCVec \to 0_{vec} (W) \in BaseSet (W)$
15	12 14	ax-mp	$⊢ 0_{vec} (W) \in BaseSet (W)$
16	1 2 3 4	hhshsslem1	$⊢ H = BaseSet (W)$
17	15 16	eleqtrri	$⊢ 0_{vec} (W) \in H$
18	10 17	eqeltrri	$⊢ 0_{ℎ} \in H$
19	4 18	pm3.2i	$⊢ (H \subseteq ℋ \land 0_{ℎ} \in H)$
20	1	hhva	$⊢ +_{ℎ} = +_{v} (U)$
21		eqid	$⊢ +_{v} (W) = +_{v} (W)$
22	16 20 21 8	sspgval	$⊢ ((U \in NrmCVec \land W \in SubSp (U)) \land (x \in H \land y \in H)) \to x +_{v} (W) y = x +_{ℎ} y$
23	5 3 22	mpanl12	$⊢ (x \in H \land y \in H) \to x +_{v} (W) y = x +_{ℎ} y$
24	16 21	nvgcl	$⊢ (W \in NrmCVec \land x \in H \land y \in H) \to x +_{v} (W) y \in H$
25	12 24	mp3an1	$⊢ (x \in H \land y \in H) \to x +_{v} (W) y \in H$
26	23 25	eqeltrrd	$⊢ (x \in H \land y \in H) \to x +_{ℎ} y \in H$
27	26	rgen2	$⊢ \forall x \in H \forall y \in H x +_{ℎ} y \in H$
28	1	hhsm	$⊢ \cdot_{ℎ} = \cdot_{𝑠OLD} (U)$
29		eqid	$⊢ \cdot_{𝑠OLD} (W) = \cdot_{𝑠OLD} (W)$
30	16 28 29 8	sspsval	$⊢ ((U \in NrmCVec \land W \in SubSp (U)) \land (x \in ℂ \land y \in H)) \to x \cdot_{𝑠OLD} (W) y = x \cdot_{ℎ} y$
31	5 3 30	mpanl12	$⊢ (x \in ℂ \land y \in H) \to x \cdot_{𝑠OLD} (W) y = x \cdot_{ℎ} y$
32	16 29	nvscl	$⊢ (W \in NrmCVec \land x \in ℂ \land y \in H) \to x \cdot_{𝑠OLD} (W) y \in H$
33	12 32	mp3an1	$⊢ (x \in ℂ \land y \in H) \to x \cdot_{𝑠OLD} (W) y \in H$
34	31 33	eqeltrrd	$⊢ (x \in ℂ \land y \in H) \to x \cdot_{ℎ} y \in H$
35	34	rgen2	$⊢ \forall x \in ℂ \forall y \in H x \cdot_{ℎ} y \in H$
36	27 35	pm3.2i	$⊢ (\forall x \in H \forall y \in H x +_{ℎ} y \in H \land \forall x \in ℂ \forall y \in H x \cdot_{ℎ} y \in H)$
37		issh2	$⊢ H \in S_{ℋ} \leftrightarrow ((H \subseteq ℋ \land 0_{ℎ} \in H) \land (\forall x \in H \forall y \in H x +_{ℎ} y \in H \land \forall x \in ℂ \forall y \in H x \cdot_{ℎ} y \in H))$
38	19 36 37	mpbir2an	$⊢ H \in S_{ℋ}$

Metamath Proof Explorer

Theorem hhshsslem2

Proof